UniTO/anno3/vpc/consegne/3/analisi.org

• [1/4]
• Proprieta` del modello
• Algoritmo 3.2
  • NuSMV

TODO [1/4]

• Cosa significa FAIRNESS running alla fine dei .smv
• Completa tabelle e immagine con greatspn
• Riformula liveness
• chiedi a lei di safety, liveness, fairness

TODO Proprieta` del modello

Ogni modello successivamente mostrato rispetta le seguenti proprieta`: Siano p e q due generici processi,

1. Mutua esclusione (safety): garantisce che al piu` un solo processo e` nella sezione critica ad ogni istante

   G (¬cₚ∨¬cq)

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

3. 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)+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 Nella tabella mostriamo i risultati ottenuti

	NuSMV	GreatSPN
Mutua Esclusione	True
Assenza di deadlock	True
No Starvation	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.