7.1 KiB
Nella tabella mostriamo i risultati ottenuti
| NuSMV | GreatSPN | |
|---|---|---|
| Mutua Esclusione | ||
| Assenza di deadlock | ||
| No Starvation |
TODO
[1/7]
- Cosa significa FAIRNESS running alla fine dei .smv
- Riformula liveness
- chiedi a lei di safety, liveness, fairness
- Vedi necessita` di Sync e /
- Finisci tutto con algebra dei processi
- Reachability graph vs Derivation Graph
TODO Proprieta` del modello
Ogni modello successivamente mostrato rispetta le seguenti proprieta`: Siano p e q due generici processi,
-
Mutua esclusione (safety): garantisce che al piu` un solo processo e` nella sezione critica ad ogni istante
G (¬cₚ∨¬cq) -
Assenza di deadlock (liveness): ogni qualvolta un processo e` in attesa di entrare nella sezione critica, eventualmente verra` concesso ad un processo di entrare nella sezione critica
G(wₚ → F(cₚ∨cq) -
Assenza di starvation individuale (strong fairness): ogni qualvolta un processo e` in attesa di entrare nella sezione critica, eventualmente gli verra` concesso
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.
Algoritmo 3.2
Due processi iterano all'infinito seguendo questo pseudocodice
while true:
non-critical section
await turn = ID
critical section
turn <- (ID%2)+1NuSMV
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}; |
#+include 3.2.b.smv
GreatSPN
Il codice utilizzato per le proprieta` CTL e` il seguente:
AG(!(#Critical_P == 1) || !(#Critical_Q == 1)) = true
AG ((#Wait_P==1 || \#Critical_Q == 1) -> AF (#Critical_P == 1 || \#Critical_Q == 1)) = false
AG (#Wait_P==1 -> AF (#Critical_P == 1)) = false
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 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 | q.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
-- Loop starts here
-> State: 1.2 <-
q.state = wait
-> State: 1.3 <-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.
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)+1NuSMV
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}; |
#+include 3.5.b.smv
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
TODO CCS
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 <- falseNuSMV
Si e` deciso di modellare l'algoritmo usando per ognuno dei due processi …
| CODE |
#+include 3.6.smv