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

# SCHELETRO:

# * Algoritmo 3.5
# Due processi iterano all'infinito seguendo questo pseudocodice

# #+BEGIN_SRC 
# #+END_SRC

# ** NuSMV
# Si e` deciso di modellare l'algoritmo usando per ognuno dei due
# processi ...
# | CODE
# #+include 3.2.b.smv

# ** GreatSPN
# ** TODO CCS
# ** Risultati

Nella tabella mostriamo i risultati ottenuti
|                     | NuSMV | GreatSPN |
|---------------------+-------+----------|
| Mutua Esclusione    |  |     |
| Assenza di deadlock |  |     |
| No Starvation       |  |     |
* TODO [1/7]
- [X] 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, perche` Amparore ha detto che deadlock: AG(EF(#critical_P == 1)) ??

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,
1. Mutua esclusione (safety): garantisce che al piu` un solo processo e` nella
   sezione critica ad ogni istante
   | G (¬cₚ∨¬c_{q}) 
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ₚ∨c_{q})
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ₚ∨¬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

#+BEGIN_SRC 
while true:
      non-critical section
      await turn = ID
      critical section
      turn <- (ID%2)+1
#+END_SRC

** 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:
#+BEGIN_SRC
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
#+END_SRC
[[./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:
#+BEGIN_SRC
-- 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 <-
#+END_SRC
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

#+BEGIN_SRC 
while true:
   await turn = ID
   turn <- (ID%2)+1
#+END_SRC

** 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:
#+BEGIN_SRC
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
#+END_SRC
[[./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:
  #+BEGIN_SRC
    – 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 <-
  #+END_SRC
- Possibilita` di starvation: i processi non compiono progresso
  iterando infinite volte su /await/.
  #+BEGIN_SRC
    – 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 <-
  #+END_SRC
  #+BEGIN_SRC
    – 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
  #+END_SRC
- Possibilita` di compiere progresso:
  #+BEGIN_SRC
    specification AG (q.state = await -> EF q.state = done)  is true
  #+END_SRC

* Algoritmo 3.6
Due processi iterano all'infinito seguendo questo pseudocodice
#+BEGIN_SRC 
while true:
    non-critical section
    await wantQ = false
    wantP <- true
    critical section
    wantP <- false
#+END_SRC

** 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:
#+BEGIN_SRC
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))
#+END_SRC

** 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.