From 7117cc6dce58eb1b269b2577c76951a62da523c0 Mon Sep 17 00:00:00 2001 From: Francesco Mecca Date: Wed, 6 May 2020 17:10:03 +0200 Subject: [PATCH] analisi --- anno3/vpc/consegne/3/3.2.b.smv | 38 +++++++++++++++++++ anno3/vpc/consegne/3/3.2.smv | 37 ++++++++++++++++++ anno3/vpc/consegne/3/analisi.org | 65 +++++++++++++++++++++++++++++--- anno3/vpc/consegne/3/prova.smv | 15 ++++++++ todo.org | 11 +++--- 5 files changed, 154 insertions(+), 12 deletions(-) create mode 100644 anno3/vpc/consegne/3/3.2.b.smv create mode 100644 anno3/vpc/consegne/3/3.2.smv create mode 100644 anno3/vpc/consegne/3/prova.smv diff --git a/anno3/vpc/consegne/3/3.2.b.smv b/anno3/vpc/consegne/3/3.2.b.smv new file mode 100644 index 0000000..94148ac --- /dev/null +++ b/anno3/vpc/consegne/3/3.2.b.smv @@ -0,0 +1,38 @@ +MODULE main +VAR + turn: 1 .. 2; + p: proc(turn, 1); + q: proc(turn, 2); +ASSIGN + init(turn) := 1; + next(turn) := + case + q.state = done: 1; + p.state = done: 2; + TRUE: turn; + esac; + +CTLSPEC -- no mutual exclusion + AG (p.state != critical | q.state != critical) + +CTLSPEC -- no deadlock + AG ((p.state = wait | q.state = wait) -> AF (p.state = critical | q.state = critical)) + +CTLSPEC -- no individual starvation + AG (p.state = wait -> AF p.state = critical) +CTLSPEC + AG (q.state = wait -> AF q.state = critical) + +MODULE proc(turn, id) -- Model a process taking turn +VAR + state: {begin, wait, critical, done}; +ASSIGN + init(state) := begin; + next(state) := + case + state = begin: {begin, wait}; + state = wait & turn = id: critical; + state = critical: critical; + state = done: begin; + TRUE: state; + esac; \ No newline at end of file diff --git a/anno3/vpc/consegne/3/3.2.smv b/anno3/vpc/consegne/3/3.2.smv new file mode 100644 index 0000000..b8fd8db --- /dev/null +++ b/anno3/vpc/consegne/3/3.2.smv @@ -0,0 +1,37 @@ +MODULE main +VAR + turn: 1..2; + p: process proc(turn, 1); + q: process proc(turn, 2); +ASSIGN + init(turn) := 1; + +CTLSPEC -- no mutual exclusion + AG (p.state != critical | q.state != critical) + +CTLSPEC -- no deadlock + AG (p.state = wait -> AF (p.state = critical | q.state = critical)) + +CTLSPEC -- no individual starvation + AG (p.state = wait -> AF p.state = critical) + +MODULE proc(turn, id) -- Model a process taking turn +VAR + state: {begin, wait, critical, done}; +ASSIGN + init(state) := begin; + next(state) := + case + state = begin: {begin, wait}; + state = wait & turn = id: critical; + state = critical: {critical, done}; + state = done: begin; + TRUE: state; + esac; + next(turn) := + case + state = done: (turn mod 2)+1; + TRUE: turn; + esac; +FAIRNESS + running \ No newline at end of file diff --git a/anno3/vpc/consegne/3/analisi.org b/anno3/vpc/consegne/3/analisi.org index 883c480..b27a700 100644 --- a/anno3/vpc/consegne/3/analisi.org +++ b/anno3/vpc/consegne/3/analisi.org @@ -1,6 +1,13 @@ -* Proprieta` del modello +* TODO [1/4] +- [X] 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ₚ∨¬c_{q}) @@ -10,15 +17,61 @@ Ogni modello successivamente mostrato rispetta le seguenti proprieta`: | 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 - | GFcₚ + | 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}) - | AGAFcₚ + | 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 +l'operatore di stato A, per queste tre proprieta` possiamo. -[ ] Correggi LTL E CTL dell'ultima. -[ ] Chiedi a galla` se e` giusto in termini di liveness safety e fairness +* 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 +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: +#+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. diff --git a/anno3/vpc/consegne/3/prova.smv b/anno3/vpc/consegne/3/prova.smv new file mode 100644 index 0000000..2c453a8 --- /dev/null +++ b/anno3/vpc/consegne/3/prova.smv @@ -0,0 +1,15 @@ +MODULE main +VAR + request: boolean; + status: {ready, busy}; +ASSIGN + init(status) := ready; + next(status) := case + request: busy; + TRUE: {ready, busy}; + esac; + +LTLSPEC + G(request -> F status=busy) +LTLSPEC + G(request -> F status=ready) \ No newline at end of file diff --git a/todo.org b/todo.org index 04d6874..3d50773 100644 --- a/todo.org +++ b/todo.org @@ -1,7 +1,7 @@ -* VPC [3/11] +* VPC [4/11] - [ ] sulle slide, quando si chiede come deve decidere il master - [X] chiedi della riduzione -- [ ] calcolo semiflussi come da mail +- [X] calcolo semiflussi come da mail - [ ] chiedi dell'esame - [X] Es1: definizioni - [ ] rete A, b, c, d @@ -23,11 +23,10 @@ - [X] Scrivile per date di esame -* TODO Tesi [2/4] +* TODO Tesi [4/6] - [X] segreteria: tesi inglese -- [ ] Gatti: inglese -- [ ] Gatti: Coppo mio relatore? -- [X] scrivi di nuovo a coppo +- [X] Gatti: inglese +- [X] Gatti: Coppo mio relatore - [ ] correzioni Coppo - [ ] Gabriel: finisci HALP