29 KiB
- Proprieta` del modello
- Algoritmo 3.2
- Algoritmo 3.5
- Algoritmo 3.6
- Algoritmo 3.8
- Algoritmo 3.9
- Algoritmo di Dekker per la mutua esclusione
- Confronto 3.2 e 3.6
Proprieta` del modello
Ogni modello successivamente mostrato rispetta le seguenti proprieta`: siano p e q due generici processi,
-
Mutua esclusione: garantisce che al piu` un solo processo e` nella sezione critica ad ogni istante. E` una proprieta` di safety.
G (¬cₚ∨¬cq) -
Assenza di deadlock: ogni qualvolta un processo e` in attesa di entrare nella sezione critica, eventualmente verra` concesso ad un processo di entrare nella sezione critica. E` una proprieta` di liveness.
G((wₚ∨wq) → F(cₚ∨cq)) -
Assenza di starvation individuale: ogni qualvolta un processo e` in attesa di entrare nella sezione critica, eventualmente gli verra` concesso.
G(wₚ → Fcₚ) Rispetto all'assenza di deadlock, e` una proprieta` di liveness ancora piu` forte della precedente.
∀p, G(wₚ → Fcₚ)
Possiamo convertire queste tre formule LTL in formule equivalenti CTL anteponendo l'operatore di stato A:
AG (¬cₚ∨¬cq) |
AG(wₚ → AF(cₚ∨cq) |
AG(wₚ → AFcₚ) |
Benche` non tutte le formule LTL possono essere convertite in una formula CTL equivalente anteponendo ad ogni operatore temporale l'operatore di stato A, per queste tre proprieta` possiamo.
Si specifica che i processi non sono forzati a progredire al di fuori della regione critica (possono rimanere per un tempo indeterminato nella sezione azione locale lₚ) e quindi:
G((wₚ∨wq) → F(cₚ∨cq) = false → G((lₚ∨lq) → F(cₚ∨cq) |
G((lₚ∨lq) → F(cₚ∨cq) = true → G((wₚ∨wq) → F(cₚ∨cq) |
Algoritmo 3.2
Due processi iterano all'infinito seguendo questo pseudocodice
while true:
non-critical section
await turn = ID
critical section
turn <- (ID%2)+1
NuSMV
Si e` deciso di modellare l'algoritmo usando per ognuno dei due processi un'enumerazione di 4 stati ed una variabile turno di tipo intero.
state: {begin, wait, critical, done}; |
\hrulefill \lstinputlisting[breaklines]{3.2.b.smv} \hrulefill
GreatSPN
Il codice utilizzato per le proprieta` CTL e` il seguente:
AG(!(#P3 == 1) || !(#P4 == 1))
AG ((#P1==1 || #Q1 == 1) -> AF (#P3 == 1 || #Q3 == 1))
AG (#P1==1 -> AF (#P3 == 1))
AG (#Q1==1 -> AF (#Q3 == 1))
AG (#Q1==1 -> EF (#Q3 == 1))
∈cludepdf{3.2.jpg}
Algebra dei processi
Riportiamo il modello dell'algoritmo 3.2 secondo l'algebra dei processi.
System = {(P₁ || Q₁) || Tₚ} \ttvar{/ }Sync |
S = {localₚ, localq, criticalₚ, criticalq} |
Sync = {isₚ, isq, setₚ, setq} |
Tₚ ::= isₚ.Tₚ + setₚ.Tₚ + setq.Tq |
Tq ::= isq.Tq + setₚ.Tₚ + setq.Tq |
P₁ ::= localₚ.P₂ + localₚ.P₁ |
P₂ ::= isₚ.P₃ |
P₃ ::= criticalₚ.P₄ |
P₄ ::= setq.P₁ |
Q₁ ::= localq.Q₂ + localq.Q₁ |
Q₂ ::= isq.Q₃ |
Q₃ ::= criticalq.Q₄ |
Q₄ ::= setp.Q₁ |
∈cludepdf{rg_3.2.jpg} ∈cludepdf{derivation_3.2.jpg}
Risultati
Nella tabella mostriamo i risultati ottenuti
NuSMV | GreatSPN | |
---|---|---|
Mutua Esclusione | True | True |
Assenza di deadlock | False | False |
No Starvation | False | False |
Il risultato della possibilita` di deadlock non deve stupire: la specifica non obbliga un processo a terminare la fase begin. Ne segue che anche l'assenza di starvation individuale non e` garantita. NuSMV conferma quanto detto mostrandoci un trace che fa da controesempio alla formula CTL:
-- specification AG (p.state = wait -> AF (p.state = critical | q.state = critical)) is false
-- as demonstrated by the following execution sequence
Trace Description: CTL Counterexample
Trace Type: Counterexample
-> State: 1.1 <-
turn = 1
p.state = begin
q.state = begin
-> Input: 1.2 <-
_process_selector_ = p
running = FALSE
q.running = FALSE
p.running = TRUE
-> State: 1.2 <-
p.state = wait
-> Input: 1.3 <-
-> State: 1.3 <-
p.state = critical
-> Input: 1.4 <-
-> State: 1.4 <-
p.state = done
-> Input: 1.5 <-
-> State: 1.5 <-
turn = 2
p.state = begin
-> Input: 1.6 <-
-- Loop starts here
-> State: 1.6 <-
p.state = wait
-> Input: 1.7 <-
_process_selector_ = q
q.running = TRUE
p.running = FALSE
-- Loop starts here
-> State: 1.7 <-
-> Input: 1.8 <-
_process_selector_ = p
q.running = FALSE
p.running = TRUE
-- Loop starts here
-> State: 1.8 <-
-> Input: 1.9 <-
_process_selector_ = main
running = TRUE
p.running = FALSE
-> State: 1.9 <-
Si vede che il processo q rimane nella fase begin e p, dopo essere entrato nella regione critica una volta, rimane bloccato in begin. Lo stesso trace mostra la possibilita` di starvation del processo. La rete modellata con GreatSPN ci conferma quanto visto con NuSMV. Inoltre il trace di GreatSPN ci mostra che non potendo forzare la fairness del modello, i processi possono iterare indefinitamente nella transizione iniziale, impedendo quindi il progresso dell'altro processo.
Initial state is: P1(1), Turn_P(1), Q1(1)
Initial state satisfies: E F (not ((not (Q1 = 1)) or (not E G (not (Q3 = 1))))).
1: P1(1), Turn_P(1), Q1(1)
State 1. does not satisfy: ((not (Q1 = 1)) or (not E G (not (Q3 = 1)))).
1.1: P1(1), Turn_P(1), Q1(1)
State 1.1.L. satisfies: (Q1 = 1).
State 1.1.R. satisfies: E G (not (Q3 = 1)). Start of loop.
1.1.R.1: P1(1), Turn_P(1), Q1(1)
State 1.1.R.1. does not satisfy: (Q3 = 1).
1.1.R.2: loop back to state 1.1.R.1.
Prendiamo in considerazione la seguente formula CTL
AG (wₚ -> EF cₚ) |
Sia GreatSPN che NuSMV ci mostrano che il sistema modellato rispetta questa proprieta`. Questo significa che un processo in attesa di entrare nella sezione critica ha la possibilita` di compiere progresso, ma solo nel caso in cui, come si intuisce dal controesempio precedente, l'altro processo decida di entrare in attesa a sua volta.
Algoritmo 3.5
Due processi iterano all'infinito seguendo questo pseudocodice
while true:
await turn = ID
turn <- (ID%2)+1
NuSMV
Si e` deciso di modellare l'algoritmo usando per ognuno dei due processi un'enumerazione di due stati e un contatore di turni intero
state: {await, done}; |
\hrulefill \lstinputlisting[breaklines]{3.5.smv} \hrulefill
GreatSPN
Il codice utilizzato per le proprieta` CTL e` il seguente:
AG(!(#Await_P == 1) || !(#Await_Q == 1)) = true
AG ((#Wait_P==1 || #Await_Q == 1) -> AF (#Done_P == 1 || #Done_Q == 1)) = false
AG (#Await_P==1 -> AF (#Done_P == 1)) = false
∈cludepdf{3.5.jpg}
Risultati
Nella tabella mostriamo i risultati ottenuti
NuSMV | GreatSPN | |
---|---|---|
Mutua Esclusione | true | true |
Assenza di deadlock | false | false |
No Starvation | false | false |
I risultati confermano il fatto che questo algoritmo e` solamente una versione semplificata del precedente (begin e wait sono stati fusi in await e done rimosso) e pertanto il trace di controesempio fornito da NuSMV e da GreatSPN presentano riflettono i risultati di questa semplificazione.
-
Possibilita` di deadlock:
– specification AG ((p.state = await | q.state = await) -> AF (p.state = done | q.state = done)) is false – as demonstrated by the following execution sequence Trace Description: CTL Counterexample Trace Type: Counterexample – Loop starts here -> State: 1.1 <- turn = 1 p.state = await q.state = await -> State: 1.2 <-
-
Possibilita` di starvation: i processi non compiono progresso iterando infinite volte su await.
– specification AG (p.state = await -> AF p.state = done) is false – as demonstrated by the following execution sequence Trace Description: CTL Counterexample Trace Type: Counterexample – Loop starts here -> State: 2.1 <- turn = 1 p.state = await q.state = await -> State: 2.2 <-
– specification AG (q.state = await -> AF q.state = done) is false – as demonstrated by the following execution sequence Trace Description: CTL Counterexample Trace Type: Counterexample – Loop starts here -> State: 3.1 <- turn = 1 p.state = await q.state = await -> State: 3.2 <- – specification AG (q.state = await -> EF q.state = done) is true
-
Possibilita` di compiere progresso:
specification AG (q.state = await -> EF q.state = done) is true
Algoritmo 3.6
Due processi iterano all'infinito seguendo questo pseudocodice
while true:
non-critical section
await wantQ = false
wantP <- true
critical section
wantP <- false
NuSMV
Si e` deciso di modellare l'algoritmo usando per ognuno dei due processi usando 5 stati
state: {local, await, critical, setTrue, setFalse}; |
\hrulefill \lstinputlisting[breaklines]{3.6.b.smv} \hrulefill
GreatSPN
Il codice utilizzato per le proprieta` CTL e` il seguente:
AG (!(#P4 == 1) || !(#Q4 == 1))
AG ((#P2==1 || #Q2 == 1) -> AF (#P4 == 1 || #Q4 == 1))
AG (#P1 == 1 -> EF(#Q4==1 || #Q4 == 1))
AG (#P2 == 1 -> AF (#P4 == 1))
AG (#Q2 == 1 -> AF (#Q4 == 1))
∈cludepdf{3.6.jpg}
Algebra dei processi
L'algoritmo 3.6 modellato secondo NuSMV e GreatSPN mostra che non c'e` la mutua esclusione. Questo viene evidenziato anche dal fatto che i nodi del Reachability Graph corrispondo al prodotto cartesiano P×Q. Anche il Derivation Graph del modello in algebra dei processi ha 25 nodi ed e` equivalente al Reachability Graph.
System = {(P₁ || Q₁) || (Wantₚ₀ || Wantq₀)} \ttvar{/ }Sync |
Sync = { isTrueₚ, isFalseₚ, setTrueₚ, setFalseₚ, |
ace{}\quad{}\quad{} isTrueq, isFalseq, setTrueq, setFalseq } |
S = {localₚ, criticalₚ, localq, criticalq} |
Wantₚ₁ ::= isTrueₚ.Wantₚ₁ + setTrueₚ.Wantₚ₁ + setFalseₚ.Wantₚ₀ |
Wantₚ₀ ::= isFalseₚ.Wantₚ₀ + setFalseₚ.Wantₚ₀ + setTrueₚ.Wantₚ₁ |
P₁ ::= localₚ.P₁ + localₚ.P₂ |
P₂ ::= isFalseq.P₃ |
P₃ ::= setTrueₚ.P₄ |
P₄ ::= criticalₚ.P₅ |
P₅ ::= setFalseₚ.P₁ |
Wantq₁ ::= isTrueq.Wantq₁ + setTrueq.Wantq₁ + setFalseq.Wantq₀ |
Wantq₀ ::= isFalseq.Wantq₀ + setFalseq.Wantq₀ + setTrueq.Wantq₁ |
Q₁ ::= localq.Q₁ + localq.Q₂ |
Q₂ ::= isFalsep.Q₃ |
Q₃ ::= setTrueq.Q₄ |
Q₄ ::= criticalq.Q₅ |
Q₅ ::= setFalseq.Q₁ |
∈cludepdf{rg_3.6.jpg} ∈cludepdf{derivation_3.6.jpg}
Risultati
Nella tabella mostriamo i risultati ottenuti
NuSMV | GreatSPN | |
---|---|---|
Mutua Esclusione | false | false |
Assenza di deadlock | true | false |
No Starvation | false | false |
Il trace di NuSMV mostra che la mutua esclusione puo` non essere rispettata dato che le due variabili wantP e wantQ possono essere contemporaneamente false.
-- specification AG (p.state != critical | q.state != critical) is false
-- as demonstrated by the following execution sequence
Trace Description: CTL Counterexample
Trace Type: Counterexample
-> State: 1.1 <-
wantP = FALSE
wantQ = FALSE
p.state = local
q.state = local
-> Input: 1.2 <-
_process_selector_ = p
running = FALSE
q.running = FALSE
p.running = TRUE
-> State: 1.2 <-
p.state = await
-> Input: 1.3 <-
-> State: 1.3 <-
p.state = setTrue
-> Input: 1.4 <-
_process_selector_ = q
q.running = TRUE
p.running = FALSE
-> State: 1.4 <-
q.state = await
-> Input: 1.5 <-
-> State: 1.5 <-
q.state = setTrue
-> Input: 1.6 <-
_process_selector_ = p
q.running = FALSE
p.running = TRUE
-> State: 1.6 <-
wantP = TRUE
p.state = critical
-> Input: 1.7 <-
_process_selector_ = q
q.running = TRUE
p.running = FALSE
-> State: 1.7 <-
wantQ = TRUE
q.state = critical
L'incoerenza del risultato dell'assenza di deadlock e` spiegabile dal fatto che nel caso di NuSMV non e` possibile che un processo rimanga nel primo stato (local) per un tempo indefinito mentre nel caso di GreatSPN e` possibile che il processo P vada nello spazio await e il processo Q decida di rimanere nel loop local_Q all'infinito. Notiamo che se forziamo i processi a fare del progresso dallo stato local, allora la formula CTL
AG(wₚ → AF(cₚ∨cq) |
risulta rispettata. Ancora meglio, piuttosto che rimuovere una transizione possibile, possiamo restringere la verifica dell'assenza di deadlock alla seguente formula CTL
AG (wₚ → EF (cₚ | cq)) |
AG(#await_P == 1 -> EF(#critical_Q==1 | #critical_P == 1)) |
che risulta rispettata. L'assenza di starvation individuale non e` rispettata ne` in NuSmv ne` in GreatSPN in quanto e` possibile che uno dei due processi continui ad accedere alla sezione critica senza permettere all’altro di fare lo stesso.
-- specification AG (q.state = await -> AF q.state = critical) is false
-- as demonstrated by the following execution sequence
Trace Description: CTL Counterexample
Trace Type: Counterexample
-> State: 3.1 <-
wantP = FALSE
wantQ = FALSE
p.state = local
q.state = local
-> Input: 3.2 <-
_process_selector_ = q
running = FALSE
q.running = TRUE
p.running = FALSE
-- Loop starts here
-> State: 3.2 <-
q.state = await
-> Input: 3.3 <-
_process_selector_ = p
q.running = FALSE
p.running = TRUE
-> State: 3.3 <-
p.state = await
-> Input: 3.4 <-
-> State: 3.4 <-
p.state = setTrue
-> Input: 3.5 <-
-> State: 3.5 <-
wantP = TRUE
p.state = critical
-> Input: 3.6 <-
_process_selector_ = q
q.running = TRUE
p.running = FALSE
-> State: 3.6 <-
-> Input: 3.7 <-
_process_selector_ = p
q.running = FALSE
p.running = TRUE
-> State: 3.7 <-
p.state = setFalse
-> Input: 3.8 <-
-> State: 3.8 <-
wantP = FALSE
p.state = local
Algoritmo 3.8
Due processi iterano all'infinito seguendo questo pseudocodice
while true:
non-critical section
wantP <- true
await wantQ = false
critical section
wantP <- false
NuSMV
Si e` deciso di modellare l'algoritmo allo stesso modo del precedente. \hrulefill \lstinputlisting[breaklines]{3.8.smv} \hrulefill
GreatSPN
Il codice utilizzato per le proprieta` CTL e` il seguente:
AG(!(#critical_P == 1) || !(#critical_Q == 1))
AG ((#await_P==1 || #await_Q == 1) -> AF (#critical_P == 1 || #critical_Q == 1))
AG (#await_P==1 -> AF (#critical_P == 1))
AG (#await_Q==1 -> AF (#critical_Q == 1))
Inoltre, per confermare alcune ipotesi, si e` testata anche la seguente formula CTL:
AG(#await_P == 1 -> EF(#critical_Q==1 || #critical_P == 1))
che conferma la presenza di deadlock causata dalle due variabili booleane. ∈cludepdf{3.8.jpg}
TODO CCS
Risultati
Nella tabella mostriamo i risultati ottenuti
NuSMV | GreatSPN | |
---|---|---|
Mutua Esclusione | True | True |
Assenza di deadlock | False | False |
No Starvation | False | False |
Questo algoritmo rispetto al precedente garantisce la mutua esclusione, ma non ci permette di evitare il deadlock (e di conseguenza neanche la starvation individuale).
Di seguito riportiamo la traccia di NuSMV che mostra che il deadlock avviene quando i progetti eseguono setTrue nello stesso momento.
-- specification AG ((p.state = await | q.state = await) -> AF (p.state = critical | q.state = critical)) is false
-- as demonstrated by the following execution sequence
Trace Description: CTL Counterexample
Trace Type: Counterexample
-> State: 1.1 <-
wantP = FALSE
wantQ = FALSE
p.state = local
q.state = local
-> Input: 1.2 <-
_process_selector_ = p
running = FALSE
q.running = FALSE
p.running = TRUE
-> State: 1.2 <-
p.state = setTrue
-> Input: 1.3 <-
-> State: 1.3 <-
wantP = TRUE
p.state = await
-> Input: 1.4 <-
_process_selector_ = q
q.running = TRUE
p.running = FALSE
-> State: 1.4 <-
q.state = setTrue
-> Input: 1.5 <-
-- Loop starts here
-> State: 1.5 <-
wantQ = TRUE
q.state = await
-> Input: 1.6 <-
_process_selector_ = p
q.running = FALSE
p.running = TRUE
-- Loop starts here
-> State: 1.6 <-
-> Input: 1.7 <-
_process_selector_ = main
running = TRUE
p.running = FALSE
-- Loop starts here
-> State: 1.7 <-
-> Input: 1.8 <-
_process_selector_ = q
running = FALSE
q.running = TRUE
-- Loop starts here
-> State: 1.8 <-
-> Input: 1.9 <-
_process_selector_ = p
q.running = FALSE
p.running = TRUE
-- Loop starts here
-> State: 1.9 <-
-> Input: 1.10 <-
_process_selector_ = main
running = TRUE
p.running = FALSE
-> State: 1.10 <-
Mostriamo invece il controesempio generato da GreatSPN che ci mostra una condizione di starvation individuale, dove, come in precedenza, il processo Q rimane in local_Q.
Generated counter-example:
==================================== Trace ====================================
Initial state is: local_P(1), wantP_FALSE(1), wantQ_FALSE(1), local_Q(1)
Initial state satisfies:
E F (not ((not (await_P = 1)) or (not E G (not (critical_P = 1))))).
1: local_P(1), wantP_FALSE(1), wantQ_FALSE(1), local_Q(1)
State 1. satisfies: ((not (await_P = 1)) or (not E G (not (critical_P = 1)))).
1.1: local_P(1), wantP_FALSE(1), wantQ_FALSE(1), local_Q(1)
State 1.1. does not satisfy: (await_P = 1).
2: SetTrue_P(1), wantP_FALSE(1), wantQ_FALSE(1), local_Q(1)
State 2. satisfies: ((not (await_P = 1)) or (not E G (not (critical_P = 1)))).
2.1: SetTrue_P(1), wantP_FALSE(1), wantQ_FALSE(1), local_Q(1)
State 2.1. does not satisfy: (await_P = 1).
3: wantP_TRUE(1), await_P(1), wantQ_FALSE(1), local_Q(1)
State 3. does not satisfy: ((not (await_P = 1)) or (not E G (not (critical_P = 1)))).
3.1: wantP_TRUE(1), await_P(1), wantQ_FALSE(1), local_Q(1)
State 3.1.L. satisfies: (await_P = 1).
State 3.1.R. satisfies: E G (not (critical_P = 1)). Start of loop.
3.1.R.1: wantP_TRUE(1), await_P(1), wantQ_FALSE(1), local_Q(1)
State 3.1.R.1. does not satisfy: (critical_P = 1).
3.1.R.2: loop back to state 3.1.R.1.
Algoritmo 3.9
Due processi iterano all'infinito seguendo questo pseudocodice
while true:
non-critical section
wantP <- true
while wantQ
wantP <- false
wantP <- true
critical section
wantP <- false
(l'altro processo segue uno pseudocodice simmetrico)
NuSMV
Si e` deciso di modellare l'algoritmo usando per ognuno dei due processi utilizzando l'espressione process per simulare di NuSMV e per ciascun process una variabile state di tipo enumerazione
state: {local, critical, setTrue, setFalse, resetTrue, resetFalse}; |
Benche` non fosse necessario distinguere il set della variabile booleana wantP, si e` preferito farlo in quanto l'enumerazione di tutti gli stati possibili, come evidenziato dal codice che segue, non risulta complesso. \hrulefill \lstinputlisting[breaklines]{3.9.smv} \hrulefill
GreatSPN
Il codice utilizzato per le proprieta` CTL e` il seguente:
AG(!(#critical_P == 1) || !(#critical_Q == 1))
AG ((#setTrue_P==1 || #setTrue_Q == 1) -> AF (#critical_P == 1 || #critical_Q == 1))
AG (#setTrue_P==1 -> AF (#critical_P == 1))
AG (#setTrue_Q==1 -> AF (#critical_Q == 1))
Inoltre, per confermare alcune ipotesi, si e` testata anche la seguente formula CTL:
AG(#setTrue_P == 1 -> EF(#critical_Q==1 | #critical_P == 1)) |
che conferma la presenza di deadlock causata dalle due variabili booleane. ∈cludepdf{3.9.jpg}
TODO CCS
Risultati
Nella tabella mostriamo i risultati ottenuti
NuSMV | GreatSPN | |
---|---|---|
Mutua Esclusione | true | true |
Assenza di deadlock | false | false |
No Starvation | false | false |
Il deadlock si verifica quando i entrambe le variabili booleane sono uguali a true. Ad esempio, se si esegue in locksetop il loop con la condizione booleana sulla variabile dell'altro processo, si verifica la condizione di deadlock. Viene riportato il trace di NuSMV che conferma questa ipotesi. GreatSPN fallisce per mancanza di RAM sulla macchina usata ma e` facile riprodurre il deadlock manualmente.
-- specification AG ((p.state = setTrue | q.state = setTrue) -> AF (p.state = critical | q.state = critical)) is false
-- as demonstrated by the following execution sequence
Trace Description: CTL Counterexample
Trace Type: Counterexample
-> State: 1.1 <-
wantP = FALSE
wantQ = FALSE
p.state = local
q.state = local
-> Input: 1.2 <-
_process_selector_ = p
running = FALSE
q.running = FALSE
p.running = TRUE
-> State: 1.2 <-
p.state = setTrue
-> Input: 1.3 <-
-> State: 1.3 <-
wantP = TRUE
p.state = critical
-> Input: 1.4 <-
-> State: 1.4 <-
p.state = setFalse
-> Input: 1.5 <-
_process_selector_ = q
q.running = TRUE
p.running = FALSE
-> State: 1.5 <-
q.state = setTrue
-> Input: 1.6 <-
-> State: 1.6 <-
wantQ = TRUE
q.state = resetFalse
-> Input: 1.7 <-
_process_selector_ = p
q.running = FALSE
p.running = TRUE
-> State: 1.7 <-
wantP = FALSE
p.state = local
-> Input: 1.8 <-
-> State: 1.8 <-
p.state = setTrue
-> Input: 1.9 <-
-- Loop starts here
-> State: 1.9 <-
wantP = TRUE
p.state = resetFalse
-> Input: 1.10 <-
_process_selector_ = q
q.running = TRUE
p.running = FALSE
-> State: 1.10 <-
wantQ = FALSE
q.state = resetTrue
-> Input: 1.11 <-
-- Loop starts here
-> State: 1.11 <-
wantQ = TRUE
q.state = resetFalse
-> Input: 1.12 <-
_process_selector_ = p
q.running = FALSE
p.running = TRUE
-> State: 1.12 <-
wantP = FALSE
p.state = resetTrue
-> Input: 1.13 <-
-- Loop starts here
-> State: 1.13 <-
wantP = TRUE
p.state = resetFalse
-> Input: 1.14 <-
_process_selector_ = q
q.running = TRUE
p.running = FALSE
-> State: 1.14 <-
wantQ = FALSE
q.state = resetTrue
-> Input: 1.15 <-
-- Loop starts here
-> State: 1.15 <-
wantQ = TRUE
q.state = resetFalse
-> Input: 1.16 <-
_process_selector_ = p
q.running = FALSE
p.running = TRUE
-> State: 1.16 <-
wantP = FALSE
p.state = resetTrue
-> Input: 1.17 <-
-> State: 1.17 <-
wantP = TRUE
p.state = resetFalse
Di seguito il trace che conferma la presenza di starvation individuale, sia in GreatSPN che NuSMV.
Generated counter-example:
==================================== Trace ====================================
Initial state is: local_Q(1), wantQ_FALSE(1), wantP_FALSE(1), local_P(1)
Initial state satisfies:
E F (not ((not (setTrue_Q = 1)) or (not E G (not (critical_Q = 1))))).
1: local_Q(1), wantQ_FALSE(1), wantP_FALSE(1), local_P(1)
State 1. satisfies: ((not (setTrue_Q = 1)) or (not E G (not (critical_Q = 1)))).
1.1: local_Q(1), wantQ_FALSE(1), wantP_FALSE(1), local_P(1)
State 1.1. does not satisfy: (setTrue_Q = 1).
2: setTrue_Q(1), wantQ_FALSE(1), wantP_FALSE(1), local_P(1)
State 2. does not satisfy: ((not (setTrue_Q = 1)) or (not E G (not (critical_Q = 1)))).
2.1: setTrue_Q(1), wantQ_FALSE(1), wantP_FALSE(1), local_P(1)
State 2.1.L. satisfies: (setTrue_Q = 1).
State 2.1.R. satisfies: E G (not (critical_Q = 1)). Start of loop.
2.1.R.1: setTrue_Q(1), wantQ_FALSE(1), wantP_FALSE(1), local_P(1)
State 2.1.R.1. does not satisfy: (critical_Q = 1).
2.1.R.2: loop back to state 2.1.R.1.
-- specification AG (q.state = setTrue -> AF q.state = critical) is false
-- as demonstrated by the following execution sequence
Trace Description: CTL Counterexample
Trace Type: Counterexample
-> State: 3.1 <-
wantP = FALSE
wantQ = FALSE
p.state = local
q.state = local
-> Input: 3.2 <-
_process_selector_ = q
running = FALSE
q.running = TRUE
p.running = FALSE
-> State: 3.2 <-
q.state = setTrue
-> Input: 3.3 <-
_process_selector_ = p
q.running = FALSE
p.running = TRUE
-> State: 3.3 <-
p.state = setTrue
-> Input: 3.4 <-
-> State: 3.4 <-
wantP = TRUE
p.state = critical
-> Input: 3.5 <-
_process_selector_ = q
q.running = TRUE
p.running = FALSE
-> State: 3.5 <-
wantQ = TRUE
q.state = resetFalse
-> Input: 3.6 <-
_process_selector_ = p
q.running = FALSE
p.running = TRUE
-- Loop starts here
-> State: 3.6 <-
p.state = setFalse
-> Input: 3.7 <-
_process_selector_ = main
running = TRUE
p.running = FALSE
-- Loop starts here
-> State: 3.7 <-
-> Input: 3.8 <-
_process_selector_ = q
running = FALSE
q.running = TRUE
-> State: 3.8 <-
wantQ = FALSE
q.state = resetTrue
-> Input: 3.9 <-
_process_selector_ = p
q.running = FALSE
p.running = TRUE
-> State: 3.9 <-
wantP = FALSE
p.state = local
-> Input: 3.10 <-
-> State: 3.10 <-
p.state = setTrue
-> Input: 3.11 <-
-> State: 3.11 <-
wantP = TRUE
p.state = critical
-> Input: 3.12 <-
_process_selector_ = q
q.running = TRUE
p.running = FALSE
-> State: 3.12 <-
wantQ = TRUE
q.state = resetFalse
-> Input: 3.13 <-
_process_selector_ = p
q.running = FALSE
p.running = TRUE
-> State: 3.13 <-
p.state = setFalse
Algoritmo di Dekker per la mutua esclusione
Due processi iterano all'infinito seguendo questo pseudocodice
while true:
non-critical section
wantP <- true
while wantQ:
if turn = 2:
wantp <- false
await turn = 1
wantp <- true
critical section
turn <- 2
wantp <- false
(l'altro processo segue uno pseudocodice simmetrico)
NuSMV
Si e` deciso di modellare l'algoritmo usando per ognuno dei due processi usando 9 stati
state: {local, set_true, while, loop_set_false, await, loop_set_true, critical, switch_turn, set_false}; |
\hrulefill \lstinputlisting[breaklines]{dekker_WN.smv} \hrulefill
GreatSPN
Il codice utilizzato per le proprieta` CTL e` il seguente:
AG(!(#critical_P == 1) || !(#critical_Q == 1))
AG ((#local_P==1 || #local_Q == 1) -> AF (#critical_P == 1 || \#critical_Q == 1))
AG (#local_P==1 -> AF (#critical_P == 1))
AG (#local_Q==1 -> AF (#critical_Q == 1))
∈cludepdf{dekker.jpg} Ci aspettiamo che come in precedenza ci sia deadlock perche` viene data ai processi la possibilita` di rimanere su local. Forzando i processi a fare del progresso dallo stato local, allora la formula CTL
AG((lₚ | lq) → AF(cₚ∨cq) |
risulta rispettata. Ancora meglio, piuttosto che rimuovere una transizione possibile, possiamo restringere la verifica dell'assenza di deadlock alla seguente formula CTL
AG (wₚ → EF (cₚ | cq)) |
AG(#await_P == 1 -> EF(#critical_Q==1 | #critical_P == 1)) |
che risulta rispettata.
C'e` possibilita` di starvation individuale perche` a differenza di NuSMV non possiamo rispettare il requisito di fairness.
Risultati
Nella tabella sono mostrati i risultati ottenuti
NuSMV | GreatSPN | |
---|---|---|
Mutua Esclusione | true | true |
Assenza di deadlock | true | false |
No Starvation | true | false |
Confronto 3.2 e 3.6
Precedentemente abbiamo modellato usando l'algebra dei processi l'algoritmo 3.2 e l'algoritmo 3.6. Entrambi hanno le seguenti azioni:
S = {localₚ, criticalₚ, localq, criticalq} ∪ {τ} |