UniTO/anno3/vpc/consegne/3/analisi.org at 0347f90e15f4bcdaae8aa03a00a0a1d4bb0c4b77

Francesco Mecca 0347f90e15 3.9

2020-05-08 19:23:51 +02:00

19 KiB

Raw Blame History

[1/7]
Proprieta` del modello
Algoritmo 3.2
- NuSMV
- GreatSPN
- CCS
- Risultati
Algoritmo 3.5
- NuSMV
- GreatSPN
- CCS
- Risultati
Algoritmo 3.6
- NuSMV
- GreatSPN
- CCS
- Risultati
Algoritmo 3.8
- NuSMV
- GreatSPN
- CCS
- Risultati
Algoritmo 3.9
- NuSMV
- GreatSPN
- CCS
- Risultati

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
Controlla in 3.6 Starvation: nusmv no, greatspn si`
3.6, dealock: correttezza spiegazione della differenza greatspn nusmv?
3.6, starvation: perche` nusmv con processi non ha starvation?
3.6, Amparore ha detto che deadlock: AG(EF(#critical_P == 1)) ??
3.6, inserisci controesempi dove necessario

NOTA: nel caso di Ampararore, la formula:

da qualsiasi stato e` sempre possibile arrivare a critical_P == 1

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ₚ∨¬c_q)
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ₚ∨c_q)
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ₚ∨¬c_q)

AG(wₚ → AF(cₚ∨c_q)

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)+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};

#+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 || \#Wait_Q == 1) -> AF (#Critical_P == 1 || \#Critical_Q == 1)) = false
AG (#Wait_P==1 -> AF (#Critical_P == 1)) = false

/bparodi/UniTO/media/commit/0347f90e15f4bcdaae8aa03a00a0a1d4bb0c4b77/anno3/vpc/consegne/3/3.2.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 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)+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};

#+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

/bparodi/UniTO/media/commit/0347f90e15f4bcdaae8aa03a00a0a1d4bb0c4b77/anno3/vpc/consegne/3/3.5.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

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 per ogni processo

state: {local, await, critical, setTrue, setFalse};

#+include 3.6.smv

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))

/bparodi/UniTO/media/commit/0347f90e15f4bcdaae8aa03a00a0a1d4bb0c4b77/anno3/vpc/consegne/3/3.6.jpg

TODO CCS

TODO Risultati

Nella tabella mostriamo i risultati ottenuti

	NuSMV	GreatSPN
Mutua Esclusione	false	false
Assenza di deadlock	true	false
No Starvation	true	false

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

G(wₚ → F(cₚ∨c_q)

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ₚ	c_q))
AG(#await_P == 1 -> EF(#critical_Q==1	\#critical_P == 1))

che risulta rispettata.

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. #+include 3.8.b.smv

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. /bparodi/UniTO/media/commit/0347f90e15f4bcdaae8aa03a00a0a1d4bb0c4b77/anno3/vpc/consegne/3/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
  -> State: 1.2 <-
    p.state = setTrue
    q.state = setTrue
  -- Loop starts here
  -> State: 1.3 <-
    wantP = TRUE
    wantQ = TRUE
    p.state = await
    q.state = await
  -> State: 1.4 <-

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. #+include 3.9.smv

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. /bparodi/UniTO/media/commit/0347f90e15f4bcdaae8aa03a00a0a1d4bb0c4b77/anno3/vpc/consegne/3/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

19 KiB Raw Blame History Unescape Escape

TODO [1/7]

TODO Proprieta` del modello

Algoritmo 3.2

NuSMV

GreatSPN

TODO CCS

Risultati

Algoritmo 3.5

NuSMV

GreatSPN

TODO CCS

Risultati

Algoritmo 3.6

NuSMV

GreatSPN

TODO CCS

TODO Risultati

Algoritmo 3.8

NuSMV

GreatSPN

TODO CCS

Risultati

Algoritmo 3.9

NuSMV

GreatSPN

TODO CCS

Risultati

19 KiB

Raw Blame History

TODO `[1/7]`