bparodi/UniTO
1
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
UniTO/anno2/YearI/SecondSem/VPC/labs/analisi/3.2/32.tex

1992 lines
53 KiB
TeX
Raw Normal View History

MCAD 2019
2018-11-22 13:09:11 +01:00
\documentclass{article}
%\usepackage{times}
\usepackage[utf8]{inputenc}
%\usepackage{amsthm}
\usepackage{algorithm} % for pseudo-codes
%\usepackage{enumerate}
\usepackage{algpseudocode}
%\usepackage{DotArrow}
%\usepackage{subfig}
%\usepackage{amsmath, environ}
%\usepackage{amssymb}
%\usepackage{amsthm}
%%\usepackage{bm}
%%\usepackage{mathtools}
\usepackage{graphicx}
%\usepackage{wrapfig}
%\usepackage{minibox}
%\usepackage{multirow}
%\usepackage{pifont} % \ding{}
%\usepackage[percent]{overpic}
%\usepackage{scrextend} % labeling environment
%
%\newtheorem{theorem}{Theorem}
%\newtheorem{definition}{Definition}
%\newtheorem{example}{Example}
%
%\renewcommand{\textfraction}{0.05}
%\renewcommand{\floatpagefraction}{0.75}
\usepackage{listings}
\usepackage{color}
\definecolor{dkgreen}{rgb}{0,0.6,0}
\definecolor{gray}{rgb}{0.5,0.5,0.5}
\definecolor{mauve}{rgb}{0.58,0,0.82}
\lstset{frame=tb,
%language=NuSmv,
aboveskip=3mm,
belowskip=3mm,
showstringspaces=false,
columns=flexible,
basicstyle={\small\ttfamily},
numbers=none,
numberstyle=\tiny\color{gray},
keywordstyle=\color{blue},
commentstyle=\color{dkgreen},
stringstyle=\color{mauve},
breaklines=true,
breakatwhitespace=true,
tabsize=3
}
\newcommand{\centerimage}[5][-7pt]{ % [vskip] | graphics-opt | imgname | label | caption
\begin{figure}[!htb]%
\centering%
\vspace{#1}%
\includegraphics[#2]{#3}%
\caption{#5}\label{#4}\vspace{2mm}%
%\vspace{-3pt}\caption{#5}\label{#4}\vspace{-2pt}%
\end{figure}}
\date{}
%\includegraphics[trim=1cm 2cm 3cm 4cm, clip=true]{example.pdf}
\begin{document}
\title{Relazione Esercizio Model Checking}
\author{Francesco Gallà, francesco.galla@edu.unito.it}
\maketitle
%=========================================================================
%%%%%%% INTRODUCTION %%%%%%%
%=========================================================================
\section{Descrizione} \label{sec:Descrizione}
Di seguito viene effettuata la valutazione di correttezza per alcuni algoritmi di mutua
esclusione, mostrati in ordine di complessit\`a. Per ognuno si mostrano il modello in NuSMV,
GreatSPN e algebra dei processi. In ogni modello sono state controllate le tre propriet\`a
essenziali, qui riportate:
\begin{description}
\item{1.} Mutua esclusione
\item{2.} Assenza di Deadlock
\item{3.} Assenza di Starvation Individuale
\end{description}
%=========================================================================================================
\section{Esercizio 3.2} \label{ssec:Es32}
\centerimage{width=\columnwidth}
{32-testo.jpg}{img:32-testo}
{Descrizione dell'algoritmo}
\break
I modelli di seguito riportati utilizzano le seguenti specifiche per controllare le $3$
propriet\`a di cui sopra (espresse in CTL):
\begin{description}
\item{1.} AG !(p.state = critical \& q.state = critical) \textbf{True}
\item{2.} AG (p.state = enter $->$ AF (p.state = critical $|$ q.state = critical))
\textbf{False}
\item{3.} AG (p.state = enter $->$ AF p.state = critical) \textbf{False}
\end{description}
\textit{Nota: le propriet\`a $2$ e $3$ sono equivalenti sostituendo $q$ a $p$. Le propriet\`a
in linguaggio LTL sono riportate di seguito.}
\subsection{NuSMV}
Il modello NuSMV implementa l'algoritmo pi\`u triviale per la mutua esclusione, ossia
l'alternanza di due processi sull'accesso a una sezione critica in base a una variabile
booleana $turn$.
Sono stati utilizzati 4 stati, di cui:
\begin{description}
\item{$local$: } Rappresenta l'esecuzione non critica e non forza il progresso
\item{$enter$: } Obbliga l'attesa per l'accesso, controllando la variabile $turn$
\item{$critical$: } Rappresenta la sezione critica
\item{$exit$: } Cambia il valore di $turn$ per garantire l'accesso all'altro processo ed
esce dalla SC.
\end{description}
\newpage
\begin{lstlisting}
MODULE main
VAR
turn : 1..2;
p : process user(turn, 1, 2);
q : process user(turn, 2, 1);
ASSIGN
init(turn) := 1;
SPEC -- PROGRESS
AG (p.state = local -> EF p.state = enter )
SPEC -- MUTUAL EXCLUSION
AG !(p.state = critical & q.state = critical)
SPEC -- DEADLOCK
AG (p.state = enter -> AF (p.state = critical | q.state = critical))
SPEC -- INDIVIDUAL STARVATION
AG (p.state = enter -> AF p.state = critical)
MODULE user(turnloc, myproc, otherproc)
VAR
state : {local,enter,critical,exit};
ASSIGN
init(state) := local;
next(state) :=
case
state = local : {local, enter};
state = enter & turnloc = myproc : critical;
state = critical : exit;
state = exit : local;
TRUE : state;
esac;
next(turnloc) :=
case
state = exit : otherproc;
TRUE : turnloc;
esac;
FAIRNESS
running
\end{lstlisting}
Il modello NuSmv model per l'algoritmo $3.2$.
\newpage
\subsection{Rete di Petri}
%\centerimage{trim=1cm 10cm 3cm 4cm, clip=true}
\centerimage{width=\columnwidth}
{rete32.jpg}{img:rete32}
{Modello P/T della rete 3.2}
% ---- PROPRIETA`
\subsection{Mutua Esclusione}
\subsubsection{NuSmv}
CTL: \textbf{True}
\begin{lstlisting}
AG !(p.state = critical & q.state = critical)
\end{lstlisting}
LTL: \textbf{True}
\begin{lstlisting}
G !(p.state = critical & q.state = critical)
\end{lstlisting}
\subsubsection{GreatSPN}
CTL: \textbf{True}
\begin{lstlisting}
AG !(#P3 == 1 && #Q3 == 1)
\end{lstlisting}
\break
La mutua esclusione \`e rispettata sia in NuSMV che in GreatSPN, in quanto non esiste un
caso in cui entrambi i processi siano contemporaneamente nella sezione critica.
\`E anche vero per\`o che i processi si aspettano a vicenda nella fase di $enter$,
pertanto il loro accesso sar\`a per forza alternato.
\subsection{Assenza di Deadlock}
\subsubsection{NuSmv}
CTL: \textbf{False}
\begin{lstlisting}
AG (p.state = enter -> AF (p.state = critical | q.state = critical))
\end{lstlisting}
LTL: \textbf{False}
\begin{lstlisting}
G (p.state = enter -> F (p.state = critical | q.state = critical))
\end{lstlisting}
\subsubsection{GreatSPN}
CTL: \textbf{False}
\begin{lstlisting}
AG (#P2 == 1 -> AF ( #P3 == 1 || #Q3 == 1))
\end{lstlisting}
La propriet\`a di assenza di deadlock non pu\`o essere rispettata in quanto i processi si
aspettano a vicenda nella fase di $enter$. Essendo inoltre che i processi nella fase $local$
non sono obbligati al progresso, se un processo resta in local indefinitamente non permette
il proseguimento dell'altro.
\break
Infatti, solo nel caso in cui entrambi i processi richiedono la sezione critica, e quindi
sono entrambi nella fase $enter$, si evita il deadlock.
\break
\break
Di seguito si riporta il controesempio alla propriet\`a.
\begin{lstlisting}
-- specification AG (p.state = enter -> 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 = local
q.state = local
-> Input: 1.2 <-
_process_selector_ = p
running = FALSE
q.running = FALSE
p.running = TRUE
-> State: 1.2 <-
p.state = enter
-> Input: 1.3 <-
-> State: 1.3 <-
p.state = critical
-> Input: 1.4 <-
-> State: 1.4 <-
p.state = exit
-> Input: 1.5 <-
-> State: 1.5 <-
turn = 2
p.state = local
-> Input: 1.6 <-
-- Loop starts here
-> State: 1.6 <-
p.state = enter
-> Input: 1.7 <-
_process_selector_ = q
q.running = TRUE
p.running = FALSE
-- Loop starts here
-> State: 1.7 <-
-> Input: 1.8 <-
_process_selector_ = p
q.running = FALSE
p.running = TRUE
-- Loop starts here
-> State: 1.8 <-
-> Input: 1.9 <-
_process_selector_ = main
running = TRUE
p.running = FALSE
-> State: 1.9 <-
\end{lstlisting}
Il controesempio fornito da NuSmv per la propriet\`a $2$.
\break
\break
%\centerimage{trim=1cm 10cm 3cm 4cm, clip=true}
\centerimage{width=\columnwidth}
{rete32-2.jpg}{img:rete32-2}
{Controesempio fornito da GreatSPN per la propriet\`a $2$.}
\newpage
\subsection{Assenza di Starvation Individuale}
CTL: \textbf{False}
\begin{lstlisting}
AG (p.state = enter -> AF (p.state = critical))
\end{lstlisting}
LTL: \textbf{False}
\begin{lstlisting}
G (p.state = enter -> F (p.state = critical))
\end{lstlisting}
\subsubsection{GreatSPN}
CTL: \textbf{False}
\begin{lstlisting}
AG (#P2 == 1 -> AF ( #P3 == 1 ))
\end{lstlisting}
\break
L'assenza di starvation individuale non \`e rispettata in quanto la propriet\`a di assenza di deadlock non lo \`e.
Di seguito si riporta il controesempio alla propriet\`a.
\break
\begin{lstlisting}
-- specification AG (p.state = enter -> AF p.state = critical) is false
-- as demonstrated by the following execution sequence
Trace Description: CTL Counterexample
Trace Type: Counterexample
-> State: 2.1 <-
turn = 1
p.state = local
q.state = local
-> Input: 2.2 <-
_process_selector_ = p
running = FALSE
q.running = FALSE
p.running = TRUE
-> State: 2.2 <-
p.state = enter
-> Input: 2.3 <-
-> State: 2.3 <-
p.state = critical
-> Input: 2.4 <-
-> State: 2.4 <-
p.state = exit
-> Input: 2.5 <-
-> State: 2.5 <-
turn = 2
p.state = local
-> Input: 2.6 <-
-- Loop starts here
-> State: 2.6 <-
p.state = enter
-> Input: 2.7 <-
_process_selector_ = q
q.running = TRUE
p.running = FALSE
-- Loop starts here
-> State: 2.7 <-
-> Input: 2.8 <-
_process_selector_ = p
q.running = FALSE
p.running = TRUE
-- Loop starts here
-> State: 2.8 <-
-> Input: 2.9 <-
_process_selector_ = main
running = TRUE
p.running = FALSE
-> State: 2.9 <-
\end{lstlisting}
Il controesempio fornito da NuSmv per la propriet\`a $3$.
\break
\break
%\centerimage{trim=1cm 10cm 3cm 4cm, clip=true}
\centerimage{width=\columnwidth}
{rete32-3.jpg}{img:rete32-3}
{Controesempio fornito da GreatSPN per la propriet\`a $3$.}
\newpage
\subsection{Algebra dei Processi}
Si presenta un modello in algebra dei processi per l'algoritmo $3.2$. La nomenclatura vuole
richiamare i posti e le transizioni definiti nella rete P/T, per agevolare il confronto tra
il Derivation Graph in CCS e il Reachability Graph in GreatSPN.
\break
\break
Come si nota, il DG e il RG hanno lo stesso numero di nodi e archi corrispondenti.
Per questo possiamo affermare l'equivalenza del modello CCS con il modello P/T.
\begin{lstlisting}
Actions = {isTurnP, isTurnQ, setP, setQ, locP, locQ, criticalP, criticalQ}
TurnP = setP.TurnP + setQ.TurnQ + isTurnP.TurnP
TurnQ = setQ.TurnQ + setP.TurnP + isTurnQ.TurnQ
P1 = locP.P1 + locP.P2
P2 = [isTurnP].P3
P3 = criticalP.P4
P4 = [setQ].P1
Q1 = locQ.Q1 + locQ.Q2
Q2 = [isTurnQ].Q3
Q3 = criticalP.Q4
Q4 = [setP].Q1
Sync = {isTurnP, isTurnQ, setP, setQ}
Sys = {(P1 || Q1) || TurnP} / Sync
\end{lstlisting}
Modello CCS per l'algoritmo 3.2.
\textit{Nota: un'azione contornata da '[]' \`e considerata un'azione in output, tutte le altre
sono considerate in input.}
\break
%\centerimage{trim=1cm 10cm 3cm 4cm, clip=true}
\centerimage{width=\columnwidth}
{dg.pdf}{img:32dg}
{Derivation Graph per la rete 3.2}
\break
%\centerimage{trim=1cm 10cm 3cm 4cm, clip=true}
\centerimage{width=\columnwidth}
{32rg.pdf}{img:32rg}
{Reachability Graph di GreatSPN per la rete 3.2}
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
\newpage
\section{Esercizio 3.5} \label{ssec:Es32}
\centerimage{width=\columnwidth}
{35-testo.jpg}{img:35-testo}
{Descrizione dell'algoritmo}
I modelli di seguito riportati utilizzano le seguenti specifiche per controllare le $3$
propriet\`a di cui sopra (espresse in CTL):
\begin{description}
\item{1.} AG !(p.state = exit \& q.state = exit) \textbf{True}
\item{2.} AG (p.state = enter $->$ AF (p.state = exit $|$ q.state = exit))
\textbf{False}
\item{3.} AG (p.state = enter $->$ AF p.state = exit) \textbf{False}
\end{description}
\textit{Nota: le propriet\`a $2$ e $3$ sono equivalenti sostituendo $q$ a $p$. Le propriet\`a
LTL si ottengono rimuovendo gli operatori di universalit\`a e esistenzialit\`a.}
\subsection{NuSMV}
Il modello NuSMV implementa l'algoritmo semplificato per la mutua esclusione, ossia
l'alternanza di due processi sull'accesso a una sezione critica in base a una variabile
booleana $turn$.
Sono stati utilizzati 2 stati, di cui:
\begin{description}
\item{$enter$: } Obbliga l'attesa per l'accesso, controllando la variabile $turn$. In
questo caso il progresso non \`e forzato: il processo pu\`o rimanere in attesa per un
tempo indefinito.
\item{$exit$: } Cambia il valore di $turn$ per garantire l'accesso all'altro processo e
ritorna a $enter$.
\end{description}
Questo modello si presenta come una versione semplificata dell'algoritmo $3.2$ (sono infatti
stati rimossi gli stati di sezione non critica e critica, mantenendo solo la richiesta in
$enter$ e il passaggio del turno in $exit$). Pertanto, i risultati sono gli stessi: la
mutua esclusione \`e rispettata, mentre l'assenza di deadlock e di starvation individuale
non lo sono.
Anche in questo caso i processi hanno un'alternanza all'accesso forzata dall'assegnazione in
$exit$ del turno al processo opposto dopo ogni accesso alla SC.
\break
\break
Si riportano di seguito i modelli NuSmv e GreatSPN. Le tracce di esecuzione sono simili
all'esercizio $3.2$.
\newpage
\begin{lstlisting}
MODULE main
VAR
turn : 1..2;
p : process user(turn, 1, 2);
q : process user(turn, 2, 1);
ASSIGN
init(turn) := 1;
SPEC -- MUTUAL EXCLUSION
AG !(p.state = exit & q.state = exit)
SPEC -- DEADLOCK
AG (p.state = enter -> AF (p.state = exit | q.state = exit))
SPEC -- INDIVIDUAL STARVATION
AG (p.state = enter -> AF p.state = exit)
MODULE user(turnloc, myproc, otherproc)
VAR
state : {enter,exit};
ASSIGN
init(state) := enter;
next(state) :=
case
state = enter & turnloc = myproc : {enter,exit};
state = exit : enter;
TRUE : state;
esac;
next(turnloc) :=
case
state = exit : otherproc;
TRUE : turnloc;
esac;
FAIRNESS
running
\end{lstlisting}
Il modello NuSmv model per l'algoritmo $3.5$.
\newpage
\subsection{Rete di Petri}
%\centerimage{trim=1cm 10cm 3cm 4cm, clip=true}
\centerimage{width=\columnwidth}
{rete35.jpg}{img:rete35}
{Modello P/T della rete 3.5}
% ---- PROPRIETA`
\newpage
\subsection{Algebra dei Processi}
Si presenta un modello in algebra dei processi per l'algoritmo $3.5$. La nomenclatura vuole
richiamare i posti e le transizioni definiti nella rete P/T, per agevolare il confronto tra
il Derivation Graph in CCS e il Reachability Graph in GreatSPN.
\break
\break
Come si nota, il DG e il RG hanno lo stesso numero di nodi e archi corrispondenti.
Per questo possiamo affermare l'equivalenza del modello CCS con il modello P/T.
\begin{lstlisting}
Actions = {isTurnP, isTurnQ, setP, setQ, waitP, waitQ}
TurnP = setP.TurnP + setQ.TurnQ + isTurnP.TurnP
TurnQ = setQ.TurnQ + setP.TurnP + isTurnQ.TurnQ
P1 = [isTurnP].P2 + waitP.P1
P2 = [setQ].P1
Q1 = [isTurnQ].Q2 + waitQ.Q1
Q2 = [setP].Q1
Sync = {isTurnP, isTurnQ, setP, setQ}
Sys = {(P1 || Q1) || TurnP} / Sync
\end{lstlisting}
Modello CCS per l'algoritmo 3.5.
\textit{Nota: un'azione contornata da '[]' \`e considerata un'azione in output, tutte le altre
sono considerate in input.}
\break
%\centerimage{trim=1cm 10cm 3cm 4cm, clip=true}
\centerimage{width=\columnwidth}
{35dg.pdf}{img:35dg}
{Derivation Graph per la rete 3.5}
\break
%\centerimage{trim=1cm 10cm 3cm 4cm, clip=true}
\centerimage{width=\columnwidth}
{35rg.pdf}{img:35rg}
{Reachability Graph di GreatSPN per la rete 3.5}
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
\newpage
\section{Esercizio 3.6} \label{ssec:Es32}
\centerimage{width=\columnwidth}
{36-testo.jpg}{img:36-testo}
{Descrizione dell'algoritmo}
I modelli di seguito riportati utilizzano le seguenti specifiche per controllare le $3$
propriet\`a di cui sopra (espresse in CTL):
\begin{description}
\item{1.} AG !(p.state = critical \& q.state = critical) \textbf{False}
\item{2.} AG (p.state = enter $->$ AF (p.state = critical $|$ q.state = critical))
\textbf{True}
\item{3.} AG (p.state = enter $->$ AF p.state = critical) \textbf{False}
\end{description}
\textit{Nota: le propriet\`a $2$ e $3$ sono equivalenti sostituendo $q$ a $p$. Le propriet\`a
LTL si ottengono rimuovendo gli operatori di universalit\`a e esistenzialit\`a.}
\subsection{NuSMV}
Il modello NuSMV implementa il primo algoritmo per la mutua esclusione basato su due
variabili anzich\`e una condivisa.
Sono stati utilizzati 5 stati, di cui:
\begin{description}
\item{$local$: } Sezione non critica.
\item{$enter$: } Obbliga l'attesa per l'accesso, controllando la variabile $want$ opposta. In
questo caso il progresso non \`e forzato: il processo pu\`o rimanere in attesa per un
tempo indefinito.
\item{$set$: } Ottenuto l'accesso, assegna alla variabile il valore $TRUE$.
\item{$critical$: } Sezione critica.
\item{$exit$: } Cambia il valore di $want$ a $FALSE$ e ritorna a $local$.
\end{description}
Il modello utilizza due variabili, $wantp$ e $wantq$, una per ogni processo. Non si
utilizza pi\`u la variabile $turn$, ma i processi conoscono solo lo stato delle due
variabili.
\break
\break
Si riportano di seguito i modelli NuSmv e GreatSPN.
\newpage
\begin{lstlisting}
MODULE main
VAR
wp : boolean;
wq : boolean;
p : process user(wp,wq);
q : process user(wq,wp);
ASSIGN
init(wp) := FALSE;
init(wq) := FALSE;
SPEC -- PROGRESS
AG (p.state = local -> EF p.state = enter )
SPEC -- MUTUAL EXCLUSION
AG !(p.state = critical & q.state = critical)
SPEC -- DEADLOCK
AG (p.state = enter -> AF (p.state = critical | q.state = critical))
SPEC -- INDIVIDUAL STARVATION
AG (p.state = enter -> AF p.state = critical)
MODULE user(wp, wq)
VAR
state : {local,enter,set,critical,exit};
ASSIGN
init(state) := local;
next(state) :=
case
state = local : {local, enter};
state = enter & wq = FALSE : set;
state = set : critical;
state = critical : exit;
state = exit : local;
TRUE : state;
esac;
next(wp) :=
case
state = set : TRUE;
state = exit : FALSE;
TRUE : wp;
esac;
FAIRNESS
running
\end{lstlisting}
Il modello NuSmv per l'algoritmo $3.6$.
\newpage
%\centerimage{trim=1cm 10cm 3cm 4cm, clip=true}
\centerimage{width=\columnwidth}
{rete36.jpg}{img:rete36}
{Modello GreatSPN per l'algoritmo $3.6$}
% ---- PROPRIETA`
\subsection{Mutua Esclusione}
\subsubsection{NuSmv}
CTL: \textbf{False}
\begin{lstlisting}
AG !(p.state = critical & q.state = critical)
\end{lstlisting}
LTL: \textbf{False}
\begin{lstlisting}
G !(p.state = critical & q.state = critical)
\end{lstlisting}
\subsubsection{GreatSPN}
CTL: \textbf{False}
\begin{lstlisting}
AG !(#P4 == 1 && #Q4 == 1)
\end{lstlisting}
\break
La mutua esclusione non \`e rispettata dall'algoritmo $3.6$, come si vede dall'esecuzione di
controesempio di NuSmv e GreatSPN. Se i due processi si trovano entrambi in stato di $enter$:
$wantp == wantq == FALSE$, pertanto \`e possibile che riescano entrambi a passare in stato di $set$.
Si riportano di seguito i controesempi.
\begin{lstlisting}
specification AG !(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 <-
wp = FALSE
wq = 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 = enter
-> Input: 1.3 <-
_process_selector_ = q
q.running = TRUE
p.running = FALSE
-> State: 1.3 <-
q.state = enter
-> Input: 1.4 <-
-> State: 1.4 <-
q.state = set
-> Input: 1.5 <-
_process_selector_ = p
q.running = FALSE
p.running = TRUE
-> State: 1.5 <-
p.state = set
-> Input: 1.6 <-
-> State: 1.6 <-
wp = TRUE
p.state = critical
-> Input: 1.7 <-
_process_selector_ = q
q.running = TRUE
p.running = FALSE
-> State: 1.7 <-
wq = TRUE
q.state = critical
\end{lstlisting}
\newpage
%\centerimage{trim=1cm 10cm 3cm 4cm, clip=true}
\centerimage{width=\columnwidth}
{rete36-1.jpg}{img:rete36-1}
{Controesempio per la mutua esclusione di GreatSPN.}
\newpage
\subsection{Assenza di Deadlock}
\subsubsection{NuSmv}
CTL: \textbf{True}
\begin{lstlisting}
AG (p.state = enter -> AF (p.state = critical | q.state = critical))
\end{lstlisting}
LTL: \textbf{True}
\begin{lstlisting}
G (p.state = enter -> F (p.state = critical | q.state = critical))
\end{lstlisting}
\subsubsection{GreatSPN}
CTL: \textbf{False}
\begin{lstlisting}
AG (#P1 == 1 -> AF (#P4 == 1 || #Q4 == 1))
\end{lstlisting}
La propriet\a` di assenza di deadlock \`e vera nel caso di NuSmv, in quanto non \`e possibile
che un processo rimanga in attesa in $enter$ per un tempo indefinito: se l'altro processo
entra, dovr\`a per forza uscire e cambiare il valore di $want$, altrimenti la variabile $want$
gli permette l'accesso a $set$.
\break
\break
In GreatSPN, la propriet\`a risulta invece falsa, in quanto \`e possibile che un processo
entri in $P1$ (attesa) ma l'altro esegua continuamente la transizione di non progresso.
Possiamo forzare questa propriet\`a estendendo la definizione di assenza di deadlock,
utilizzando quindi la seguente formula CTL:
\begin{lstlisting}
AG (#P1 == 1 -> EF (#P4 == 1 || #Q4 == 1))
\end{lstlisting}
Che viene valutata \textbf{True}.
\subsection{Assenza di Starvation Individuale}
CTL: \textbf{False}
\begin{lstlisting}
AG (p.state = enter -> AF (p.state = critical))
\end{lstlisting}
LTL: \textbf{False}
\begin{lstlisting}
G (p.state = enter -> F (p.state = critical))
\end{lstlisting}
\subsubsection{GreatSPN}
CTL: \textbf{False}
\begin{lstlisting}
AG (#P1 == 1 -> AF (#P4 == 1 ))
\end{lstlisting}
\break
L'assenza starvation individuale non \`e rispettata n\`e in NuSmv n\`e in GreatSPN. Questo
perch\`e \`e possibile che uno dei due processi continui ad accedere alla sezione critica
senza permettere all'altro di fare lo stesso.
\begin{lstlisting}
-- specification AG (p.state = enter -> AF p.state = critical) is false
-- as demonstrated by the following execution sequence
Trace Description: CTL Counterexample
Trace Type: Counterexample
-> State: 2.1 <-
wp = FALSE
wq = FALSE
p.state = local
q.state = local
-> Input: 2.2 <-
_process_selector_ = p
running = FALSE
q.running = FALSE
p.running = TRUE
-- Loop starts here
-> State: 2.2 <-
p.state = enter
-> Input: 2.3 <-
_process_selector_ = q
q.running = TRUE
p.running = FALSE
-> State: 2.3 <-
q.state = enter
-> Input: 2.4 <-
-> State: 2.4 <-
q.state = set
-> Input: 2.5 <-
-> State: 2.5 <-
wq = TRUE
q.state = critical
-> Input: 2.6 <-
_process_selector_ = p
q.running = FALSE
p.running = TRUE
-> State: 2.6 <-
-> Input: 2.7 <-
_process_selector_ = q
q.running = TRUE
p.running = FALSE
-> State: 2.7 <-
q.state = exit
-> Input: 2.8 <-
-> State: 2.8 <-
wq = FALSE
q.state = local
\end{lstlisting}
\centerimage{width=\columnwidth}
{rete36-3.jpg}{img:rete36-3}
{Controesempio per la starvation individuale di GreatSPN.}
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
\newpage
\section{Esercizio 3.8} \label{ssec:Es32}
\centerimage{width=\columnwidth}
{38-testo.jpg}{img:38-testo}
{Descrizione dell'algoritmo}
I modelli di seguito riportati utilizzano le seguenti specifiche per controllare le $3$
propriet\`a di cui sopra (espresse in CTL):
\begin{description}
\item{1.} AG !(p.state = critical \& q.state = critical) \textbf{True}
\item{2.} AG (p.state = set $->$ AF (p.state = critical $|$ q.state = critical))
\textbf{False}
\item{3.} AG (p.state = set $->$ AF p.state = critical) \textbf{False}
\end{description}
\textit{Nota: le propriet\`a $2$ e $3$ sono equivalenti sostituendo $q$ a $p$. Le propriet\`a
LTL si ottengono rimuovendo gli operatori di universalit\`a e esistenzialit\`a.}
\subsection{NuSMV}
Il secondo algoritmo di mutua esclusione basato su due variabili \`e simile al $3.6$ ma
inverte gli stati $set$ e $enter$, di modo da segnalare la sua intenzione di entrare nella
sezione critica prima di mettersi in attesa.
Sono stati utilizzati 5 stati, di cui:
\begin{description}
\item{$local$: } Sezione non critica.
\item{$set$: } Richiede l'accesso assegnando alla variabile il valore $TRUE$.
\item{$enter$: } Obbliga l'attesa per l'accesso, controllando la variabile $want$ opposta. In
questo caso il progresso non \`e forzato: il processo pu\`o rimanere in attesa per un
tempo indefinito.
\item{$critical$: } Sezione critica.
\item{$exit$: } Cambia il valore di $want$ a $FALSE$ e ritorna a $local$.
\end{description}
Il modello utilizza due variabili, $wantp$ e $wantq$, una per ogni processo. Non si
utilizza pi\`u la variabile $turn$, ma i processi conoscono solo lo stato delle due
variabili.
\break
\break
Si riportano di seguito i modelli NuSmv e GreatSPN.
\begin{lstlisting}
MODULE main
VAR
wp : boolean;
wq : boolean;
p : process user(wp,wq);
q : process user(wq,wp);
ASSIGN
init(wp) := FALSE;
init(wq) := FALSE;
SPEC -- PROGRESS
AG (p.state = local -> EF p.state = enter )
SPEC -- MUTUAL EXCLUSION
AG !(p.state = critical & q.state = critical)
SPEC -- DEADLOCK
AG (p.state = set -> AF (p.state = critical | q.state = critical))
SPEC -- INDIVIDUAL STARVATION
AG (p.state = set -> AF p.state = critical)
MODULE user(wp, wq)
VAR
state : {local,set,enter,critical,exit};
ASSIGN
init(state) := local;
next(state) :=
case
state = local : {local, set};
state = set : enter;
state = enter & wq = FALSE : critical;
state = critical : exit;
state = exit : local;
TRUE : state;
esac;
next(wp) :=
case
state = set : TRUE;
state = exit : FALSE;
TRUE : wp;
esac;
FAIRNESS
running
\end{lstlisting}
Il modello NuSmv per l'algoritmo $3.8$.
\newpage
%\centerimage{trim=1cm 10cm 3cm 4cm, clip=true}
\centerimage{width=\columnwidth}
{rete38.jpg}{img:rete38}
{Modello GreatSPN per l'algoritmo $3.8$}
% ---- PROPRIETA`
\subsection{Mutua Esclusione}
\subsubsection{NuSmv}
CTL: \textbf{True}
\begin{lstlisting}
AG !(p.state = critical & q.state = critical)
\end{lstlisting}
LTL: \textbf{True}
\begin{lstlisting}
G !(p.state = critical & q.state = critical)
\end{lstlisting}
\subsubsection{GreatSPN}
CTL: \textbf{True}
\begin{lstlisting}
AG !(#P4 == 1 && #Q4 == 1)
\end{lstlisting}
\break
La mutua esclusione \`e rispettata in quanto la modifica della variabile $want$ viene
effettuata prima della fase di controllo. Questo permette di evitare il caso, presente
nell'esercizio $3.6$, in cui l'esecuzione interfogliata dei due processi portava all'accesso
di entrambi nella sezione critica.
\subsection{Assenza di Deadlock}
\subsubsection{NuSmv}
CTL: \textbf{False}
\begin{lstlisting}
AG (p.state = enter -> AF (p.state = critical | q.state = critical))
\end{lstlisting}
LTL: \textbf{False}
\begin{lstlisting}
G (p.state = enter -> F (p.state = critical | q.state = critical))
\end{lstlisting}
\subsubsection{GreatSPN}
CTL: \textbf{False}
\begin{lstlisting}
AG (#P1 == 1 -> AF (#P4 == 1 || #Q4 == 1))
\end{lstlisting}
L'assenza di deadlock non \`e rispettata n\`e in NuSmv ne in GreatSPN, in quanto se entrambi
i processi eseguono $set$, entrambe le variabili $want$ avranno valore $TRUE$ non permettendo
il progresso di nessuno dei due.
Si riportano i controesempi.
\begin{lstlisting}
-- specification AG (p.state = set -> 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 <-
wp = FALSE
wq = 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 = set
-> Input: 1.3 <-
_process_selector_ = q
q.running = TRUE
p.running = FALSE
-> State: 1.3 <-
q.state = set
-> Input: 1.4 <-
_process_selector_ = p
q.running = FALSE
p.running = TRUE
-> State: 1.4 <-
wp = TRUE
p.state = enter
-> Input: 1.5 <-
_process_selector_ = q
q.running = TRUE
p.running = FALSE
-- Loop starts here
-> State: 1.5 <-
wq = TRUE
q.state = enter
-> Input: 1.6 <-
-- Loop starts here
-> State: 1.6 <-
-> Input: 1.7 <-
_process_selector_ = p
q.running = FALSE
p.running = TRUE
-- Loop starts here
-> State: 1.7 <-
-> Input: 1.8 <-
_process_selector_ = main
running = TRUE
p.running = FALSE
-> State: 1.8 <-
\end{lstlisting}
Controesempio di NuSmv per l'assenza di deadlock dell'esercizio $3.8$.
\newpage
\centerimage{width=\columnwidth}
{rete38-2.jpg}{img:rete38-2}
{Controesempio per l'assenza di deadlock di GreatSPN.}
\newpage
\subsection{Assenza di Starvation Individuale}
CTL: \textbf{False}
\begin{lstlisting}
AG (p.state = enter -> AF (p.state = critical))
\end{lstlisting}
LTL: \textbf{False}
\begin{lstlisting}
G (p.state = enter -> F (p.state = critical))
\end{lstlisting}
\subsubsection{GreatSPN}
CTL: \textbf{False}
\begin{lstlisting}
AG (#P1 == 1 -> AF (#P4 == 1 ))
\end{lstlisting}
Essendo che la propriet\`a di assenza di deadlock \`e falsa, \`e lecito che anche quella di
starvation individuale lo sia. Si riportano i controesempi.
\begin{lstlisting}
-- specification AG (p.state = set -> AF p.state = critical) is false
-- as demonstrated by the following execution sequence
Trace Description: CTL Counterexample
Trace Type: Counterexample
-> State: 2.1 <-
wp = FALSE
wq = FALSE
p.state = local
q.state = local
-> Input: 2.2 <-
_process_selector_ = p
running = FALSE
q.running = FALSE
p.running = TRUE
-> State: 2.2 <-
p.state = set
-> Input: 2.3 <-
_process_selector_ = q
q.running = TRUE
p.running = FALSE
-> State: 2.3 <-
q.state = set
-> Input: 2.4 <-
_process_selector_ = p
q.running = FALSE
p.running = TRUE
-> State: 2.4 <-
wp = TRUE
p.state = enter
-> Input: 2.5 <-
_process_selector_ = q
q.running = TRUE
p.running = FALSE
-- Loop starts here
-> State: 2.5 <-
wq = TRUE
q.state = enter
-> Input: 2.6 <-
-- Loop starts here
-> State: 2.6 <-
-> Input: 2.7 <-
_process_selector_ = p
q.running = FALSE
p.running = TRUE
-- Loop starts here
-> State: 2.7 <-
-> Input: 2.8 <-
_process_selector_ = main
running = TRUE
p.running = FALSE
-> State: 2.8 <-
\end{lstlisting}
Controesempio per la starvation individuale di NuSmv.
\centerimage{width=\columnwidth}
{rete38-3.jpg}{img:rete38-3}
{Controesempio per l'assenza di starvation individuale di GreatSPN.}
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
\newpage
\section{Esercizio 3.9} \label{ssec:Es32}
\centerimage{width=\columnwidth}
{39-testo.jpg}{img:39-testo}
{Descrizione dell'algoritmo}
I modelli di seguito riportati utilizzano le seguenti specifiche per controllare le $3$
propriet\`a di cui sopra (espresse in CTL):
\begin{description}
\item{1.} AG !(p.state = critical \& q.state = critical) \textbf{True}
\item{2.} AG (p.state = set $->$ AF (p.state = critical $|$ q.state = critical))
\textbf{False}
\item{3.} AG (p.state = set $->$ AF p.state = critical) \textbf{False}
\end{description}
\textit{Nota: le propriet\`a $2$ e $3$ sono equivalenti sostituendo $q$ a $p$. Le propriet\`a
LTL si ottengono rimuovendo gli operatori di universalit\`a e esistenzialit\`a.}
\subsection{NuSMV}
Il modello implementa l'algoritmo $3.8$ migliorato per mitigare la situazione di deadlock
risultante dall'esecuzione interfogliata dei due processi. Entrambi eseguono un loop in
\textit{busy waiting} alternando il valore di $want$ da $FALSE$ a $TRUE$, di modo da
permettere l'accesso nel caso l'altro processo sia in attesa. Il deadlock non \`e per\`o
evitato del tutto: se i due processi entrano nel loop in maniera sincrona (un'istruzione alla
volta) non riusciranno mai a proseguire alla SC, come mostrano i controesempi seguenti.
\break
\break
Sono stati utilizzati 7 stati, di cui:
\begin{description}
\item{$local$: } Sezione non critica.
\item{$set$: } Richiede l'accesso assegnando alla variabile il valore $TRUE$.
\item{$enter$: } Lo stato inizia un loop che viene eseguito finch\`e la $want$ opposta
non diventa $FALSE$. Il loop itera sugli stati $loopUnset$ e $loopSet$.
\item{$loopUnset$: } Cambia il valore della variabile $want$ propria a $FALSE$, per
permettere l'accesso all'altro processo nel caso questo sia gi\`a in $enter$.
\item{$loopSet$: } Cambia il valore della variabile $want$ propria a $TRUE$, per
segnalare l'intezione di entrare nella sezione critica.
\item{$critical$: } Sezione critica.
\item{$exit$: } Cambia il valore di $want$ a $FALSE$ e ritorna a $local$.
\end{description}
Il modello utilizza due variabili, $wantp$ e $wantq$, una per ogni processo. Non si
utilizza pi\`u la variabile $turn$, ma i processi conoscono solo lo stato delle due
variabili.
\begin{lstlisting}
MODULE main
VAR
wp : boolean;
wq : boolean;
p : process user(wp,wq);
q : process user(wq,wp);
ASSIGN
init(wp) := FALSE;
init(wq) := FALSE;
SPEC -- PROGRESS
AG (p.state = local -> EF p.state = enter )
SPEC -- MUTUAL EXCLUSION
AG !(p.state = critical & q.state = critical)
SPEC -- DEADLOCK
AG (p.state = set -> AF (p.state = critical | q.state = critical))
SPEC -- INDIVIDUAL STARVATION
AG (p.state = set -> AF p.state = critical)
MODULE user(wp, wq)
VAR
state : {local,set,enter,loopUnset, loopSet, critical, exit};
ASSIGN
init(state) := local;
next(state) :=
case
state = local : {local, set};
state = set : enter;
state = enter & wq = FALSE : critical;
state = enter & wq = TRUE : loopUnset;
state = loopUnset : loopSet;
state = loopSet : enter;
state = critical : exit;
state = exit : local;
TRUE : state;
esac;
next(wp) :=
case
state = set : TRUE;
state = loopUnset : FALSE;
state = loopSet : TRUE;
state = exit : FALSE;
TRUE : wp;
esac;
FAIRNESS
running
\end{lstlisting}
Il modello NuSmv per l'algoritmo $3.9$.
\newpage
%\centerimage{trim=1cm 10cm 3cm 4cm, clip=true}
\centerimage{width=\columnwidth}
{rete39.jpg}{img:rete39}
{Modello GreatSPN per l'algoritmo $3.9$}
% ---- PROPRIETA`
\subsection{Mutua Esclusione}
\subsubsection{NuSmv}
CTL: \textbf{True}
\begin{lstlisting}
AG !(p.state = critical & q.state = critical)
\end{lstlisting}
LTL: \textbf{True}
\begin{lstlisting}
G !(p.state = critical & q.state = critical)
\end{lstlisting}
\subsubsection{GreatSPN}
CTL: \textbf{True}
\begin{lstlisting}
AG !(#P4 == 1 && #Q4 == 1)
\end{lstlisting}
\break
La mutua esclusione \`e rispettata in quanto la modifica della variabile $want$ viene
effettuata prima della fase di controllo. Il \textit{busy waiting} non cambia l'algoritmo da
rispetto al $3.8$ da questo punto di vista.
\subsection{Assenza di Deadlock}
\subsubsection{NuSmv}
CTL: \textbf{False}
\begin{lstlisting}
AG (p.state = enter -> AF (p.state = critical | q.state = critical))
\end{lstlisting}
LTL: \textbf{False}
\begin{lstlisting}
G (p.state = enter -> F (p.state = critical | q.state = critical))
\end{lstlisting}
\subsubsection{GreatSPN}
CTL: \textbf{False}
\begin{lstlisting}
AG (#P1 == 1 -> AF (#P4 == 1 || #Q4 == 1))
\end{lstlisting}
L'assenza di deadlock non \`e rispettata n\`e in NuSmv ne in GreatSPN. Anche con il \textit{busy
waiting} si ripresenta il problema dell'esercizio $3.8$: se i processi sono entrambi nello
stato di attesa ($enter$), entrambi entrano nel loop e ogni volta che viene eseguito il
controllo sulle variabili, entrambe saranno $TRUE$. Si riportano i controesempi.
\begin{lstlisting}
-- specification AG (p.state = set -> 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 <-
wp = FALSE
wq = 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 = set
-> Input: 1.3 <-
_process_selector_ = q
q.running = TRUE
p.running = FALSE
-> State: 1.3 <-
-> Input: 1.4 <-
_process_selector_ = p
q.running = FALSE
p.running = TRUE
-> State: 1.4 <-
wp = TRUE
p.state = enter
-> Input: 1.5 <-
_process_selector_ = q
q.running = TRUE
p.running = FALSE
-> State: 1.5 <-
-> Input: 1.6 <-
-> State: 1.6 <-
-> Input: 1.7 <-
-> State: 1.7 <-
q.state = set
-> Input: 1.8 <-
-> State: 1.8 <-
wq = TRUE
q.state = enter
-> Input: 1.9 <-
_process_selector_ = p
q.running = FALSE
p.running = TRUE
-> State: 1.9 <-
p.state = loopUnset
-> Input: 1.10 <-
_process_selector_ = q
q.running = TRUE
p.running = FALSE
-- Loop starts here
-> State: 1.10 <-
q.state = loopUnset
-> Input: 1.11 <-
-> State: 1.11 <-
wq = FALSE
q.state = loopSet
-> Input: 1.12 <-
_process_selector_ = p
q.running = FALSE
p.running = TRUE
-> State: 1.12 <-
wp = FALSE
p.state = loopSet
-> Input: 1.13 <-
-> State: 1.13 <-
wp = TRUE
p.state = enter
-> Input: 1.14 <-
_process_selector_ = q
q.running = TRUE
p.running = FALSE
-> State: 1.14 <-
wq = TRUE
q.state = enter
-> Input: 1.15 <-
_process_selector_ = p
q.running = FALSE
p.running = TRUE
-> State: 1.15 <-
p.state = loopUnset
-> Input: 1.16 <-
_process_selector_ = q
q.running = TRUE
p.running = FALSE
-> State: 1.16 <-
q.state = loopUnset
\end{lstlisting}
Controesempio di NuSmv per l'assenza di deadlock dell'esercizio $3.9$.
\newpage
\centerimage{width=\columnwidth}
{rete39-2.jpg}{img:rete39-2}
{Controesempio per l'assenza di deadlock di GreatSPN.}
\newpage
\subsection{Assenza di Starvation Individuale}
CTL: \textbf{False}
\begin{lstlisting}
AG (p.state = enter -> AF (p.state = critical))
\end{lstlisting}
LTL: \textbf{False}
\begin{lstlisting}
G (p.state = enter -> F (p.state = critical))
\end{lstlisting}
\subsubsection{GreatSPN}
CTL: \textbf{False}
\begin{lstlisting}
AG (#P1 == 1 -> AF (#P4 == 1 ))
\end{lstlisting}
Essendo che la propriet\`a di assenza di deadlock \`e falsa, \`e lecito che anche quella di
starvation individuale lo sia. Si riportano i controesempi.
\begin{lstlisting}
-- specification AG (p.state = set -> AF p.state = critical) is false
-- as demonstrated by the following execution sequence
Trace Description: CTL Counterexample
Trace Type: Counterexample
-> State: 2.1 <-
wp = FALSE
wq = FALSE
p.state = local
q.state = local
-> Input: 2.2 <-
_process_selector_ = p
running = FALSE
q.running = FALSE
p.running = TRUE
-> State: 2.2 <-
p.state = set
-> Input: 2.3 <-
_process_selector_ = q
q.running = TRUE
p.running = FALSE
-> State: 2.3 <-
-> Input: 2.4 <-
_process_selector_ = p
q.running = FALSE
p.running = TRUE
-- Loop starts here
-> State: 2.4 <-
wp = TRUE
p.state = enter
-> Input: 2.5 <-
_process_selector_ = q
q.running = TRUE
p.running = FALSE
-- Loop starts here
-> State: 2.5 <-
-> Input: 2.6 <-
-- Loop starts here
-> State: 2.6 <-
-> Input: 2.7 <-
-> State: 2.7 <-
q.state = set
-> Input: 2.8 <-
-> State: 2.8 <-
wq = TRUE
q.state = enter
-> Input: 2.9 <-
_process_selector_ = p
q.running = FALSE
p.running = TRUE
-> State: 2.9 <-
p.state = loopUnset
-> Input: 2.10 <-
-> State: 2.10 <-
wp = FALSE
p.state = loopSet
-> Input: 2.11 <-
_process_selector_ = q
q.running = TRUE
p.running = FALSE
-> State: 2.11 <-
q.state = critical
-> Input: 2.12 <-
_process_selector_ = p
q.running = FALSE
p.running = TRUE
-> State: 2.12 <-
wp = TRUE
p.state = enter
-> Input: 2.13 <-
_process_selector_ = q
q.running = TRUE
p.running = FALSE
-> State: 2.13 <-
q.state = exit
-> Input: 2.14 <-
-> State: 2.14 <-
wq = FALSE
q.state = local
\end{lstlisting}
Controesempio per la starvation individuale di NuSmv.
\centerimage{width=\columnwidth}
{rete39-3.jpg}{img:rete39-3}
{Controesempio per l'assenza di starvation individuale di GreatSPN.}
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
\newpage
\section{Esercizio 3.10} \label{ssec:Es32}
\centerimage{width=\columnwidth}
{310-testo.jpg}{img:310-testo}
{Descrizione dell'algoritmo}
I modelli di seguito riportati utilizzano le seguenti specifiche per controllare le $3$
propriet\`a di cui sopra (espresse in CTL):
\begin{description}
\item{1.} AG !(p.state = critical \& q.state = critical) \textbf{True}
\item{2.} AG (p.state = set $->$ AF (p.state = critical $|$ q.state = critical))
\textbf{True}
\item{3.} AG (p.state = set $->$ AF p.state = critical) \textbf{True}
\end{description}
\textit{Nota: le propriet\`a $2$ e $3$ sono equivalenti sostituendo $q$ a $p$. Le propriet\`a
LTL si ottengono rimuovendo gli operatori di universalit\`a e esistenzialit\`a.}
\subsection{NuSMV}
Il modello implementa l'algoritmo di Dekker, che fa uso sia delle due variabili booleane che
della variabile $turn$, riuscendo a rispettare tutte e $3$ le propriet\`a.
Sono stati utilizzati 10 stati, di cui:
\begin{description}
\item{$local$: } Sezione non critica.
\item{$set$: } Richiede l'accesso assegnando alla variabile il valore $TRUE$.
\item{$enter$: } Lo stato inizia un loop che viene eseguito finch\`e la $want$ opposta
non diventa $FALSE$. Il loop itera sugli stati $checkTurn$, $loopUnset$, $waitTurn$ e $loopSet$.
\item{$checkTurn$: } Controlla che il valore della variabile $turn$ sia corrispondente al
processo opposto. Se cos\`i \`e, allora permette la discesa nel loop. Altrimenti il
processo ritorna a $enter$.
\item{$loopUnset$: } Cambia il valore della variabile $want$ propria a $FALSE$, per
permettere l'accesso all'altro processo nel caso questo sia gi\`a in $enter$.
\item{$waitTurn$: } Obbliga l'attesa del proprio turno controllando la variabile $turn$.
\item{$loopSet$: } Cambia il valore della variabile $want$ propria a $TRUE$, per
segnalare l'intezione di entrare nella sezione critica.
\item{$critical$: } Sezione critica.
\item{$setTurn$: } Assegna il valore di $turn$ all'altro processo.
\item{$exit$: } Cambia il valore di $want$ a $FALSE$ e ritorna a $local$.
\end{description}
Ogni processo \`e a conoscenza di $wantp$, $wantq$, della variabile $turn$, del proprio
\textit{id} e di quello dell'altro processo.
\begin{lstlisting}
MODULE main
VAR
wp : boolean;
wq : boolean;
turn : 1..2;
p : process user(wp,wq, turn, 1, 2);
q : process user(wq,wp, turn, 2, 1);
ASSIGN
init(wp) := FALSE;
init(wq) := FALSE;
init(turn) := 1;
SPEC -- PROGRESS
AG (p.state = local -> EF p.state = enter )
SPEC -- MUTUAL EXCLUSION
AG !(p.state = critical & q.state = critical)
SPEC -- DEADLOCK
AG (p.state = set -> AF (p.state = critical | q.state = critical))
SPEC -- INDIVIDUAL STARVATION
AG (p.state = set -> AF p.state = critical)
MODULE user(wp, wq, turn, me, other)
VAR
state : {local, set, enter, checkTurn, loopUnset, waitTurn, loopSet, critical, setTurn, exit};
ASSIGN
init(state) := local;
next(state) :=
case
state = local : {local, set};
state = set : enter;
state = enter & wq = FALSE : critical; -- Go to CS
state = enter & wq = TRUE : checkTurn; -- Start waiting loop
state = checkTurn & turn = me : enter; -- Go back to loop check
state = checkTurn & turn = other : loopUnset; -- Descend in loop
state = loopUnset : waitTurn;
state = waitTurn & turn = me : loopSet; -- Wait until turn == 1
state = loopSet : enter; -- End of loop
state = critical : exit;
state = setTurn : exit;
state = exit : local;
TRUE : state;
esac;
next(wp) :=
case
state = set : TRUE;
state = loopUnset : FALSE;
state = loopSet : TRUE;
state = exit : FALSE;
TRUE : wp;
esac;
next(turn) :=
case
state = setTurn : other;
TRUE : turn;
esac;
FAIRNESS
running
\end{lstlisting}
Modello NuSmv per l'algoritmo di Dekker.
\newpage
\centerimage{width=\columnwidth}
{rete310.jpg}{img:rete310}
{Modello in GreatSPN dell'algoritmo di Dekker}
% ---- PROPRIETA`
\subsection{Mutua Esclusione}
\subsubsection{NuSmv}
CTL: \textbf{True}
\begin{lstlisting}
AG !(p.state = critical & q.state = critical)
\end{lstlisting}
LTL: \textbf{True}
\begin{lstlisting}
G !(p.state = critical & q.state = critical)
\end{lstlisting}
\subsubsection{GreatSPN}
CTL: \textbf{True}
\begin{lstlisting}
AG !(#P4 == 1 && #Q4 == 1)
\end{lstlisting}
\break
\subsection{Assenza di Deadlock}
\subsubsection{NuSmv}
CTL: \textbf{True}
\begin{lstlisting}
AG (p.state = enter -> AF (p.state = critical | q.state = critical))
\end{lstlisting}
LTL: \textbf{True}
\begin{lstlisting}
G (p.state = enter -> F (p.state = critical | q.state = critical))
\end{lstlisting}
\subsubsection{GreatSPN}
CTL: \textbf{False}
\begin{lstlisting}
AG (#P1 == 1 -> AF (#P4 == 1 || #Q4 == 1))
\end{lstlisting}
In NuSmv, dove \`e possibile imporre il requisito di fairness, l'assenza di deadlock \`e rispettat\`a.
In GreatSPN invece non \`e possibile imporre la fairness e per questo motivo pu\`o
accadere che si verifichi deadlock perch\`e uno dei processi rimane fermo (non esegue
transizioni di progresso).
\centerimage{width=\columnwidth}
{rete310-2.jpg}{img:rete310-2}
{Controesempio per l'assenza di deadlock di GreatSPN.}
\newpage
\subsection{Assenza di Starvation Individuale}
CTL: \textbf{True}
\begin{lstlisting}
AG (p.state = enter -> AF (p.state = critical))
\end{lstlisting}
LTL: \textbf{True}
\begin{lstlisting}
G (p.state = enter -> F (p.state = critical))
\end{lstlisting}
\subsubsection{GreatSPN}
CTL: \textbf{False}
\begin{lstlisting}
AG (#P1 == 1 -> AF (#P4 == 1 ))
\end{lstlisting}
Come per l'assenza di deadlock, anche per la starvation individuale NuSmv con $FAIRNESS
running$ ci garantisce che non si verifichi starvation, mentre per GreatSPN non si pu\`o dire
lo stesso.
\centerimage{width=\columnwidth}
{rete310-3.jpg}{img:rete310-3}
{Controesempio per l'assenza di starvation individuale di GreatSPN.}
\newpage
\subsection{Confronto tra NuSmv e GreatSPN}
\begin{table}[h!]
\centering
\begin{tabular}{ |p{3cm}||p{3cm}||p{3cm}||p{3cm}|}
\hline
\multicolumn{4}{|c|}{Propriet\`a degli algoritmi in NuSmv} \\
\hline
Esercizio & Mutua Esclusione & No Deadlock & No Starvation Ind. \\
\hline
3.2 & True & False & False \\
3.5 & True & False & False \\
3.6 & False & True & False \\
3.8 & True & False & False \\
3.9 & True & False & False \\
3.10 & True & True & True \\
\hline
\hline
\end{tabular} \\
\label{tab:nusmv-table}
\end{table}
\begin{table}[h!]
\centering
\begin{tabular}{ |p{3cm}||p{3cm}||p{3cm}||p{3cm}|}
\hline
\multicolumn{4}{|c|}{Propriet\`a degli algoritmi in GreatSPN} \\
\hline
Esercizio & Mutua Esclusione & No Deadlock & No Starvation Ind. \\
\hline
3.2 & True & False & False \\
3.5 & True & False & False \\
3.6 & False & \textbf{False} & False \\
3.8 & True & False & False \\
3.9 & True & False & False \\
3.10 & True & \textbf{False} & \textbf{False} \\
\hline
\hline
\end{tabular} \\
\label{tab:gspn-table}
\end{table}
\subsection{Bisimulazione: equivalenza tra esercizi $3.2$ e $3.5$}
Si vuole eguagliare i due modelli in algebra dei processi per determinare l'equivalenza dei
due algoritmi. Per fare ci\`o, si utilizza la tecnica di bisimulazione estesa, ovvero
l'algoritmo che considera le azioni $\tau$, nel modello segnate come $Sync$.
Si riportano di seguito i derivation graph per i due algoritmi, sostituendo le azioni in
$Sync$ a $\tau$.
\newpage
\centerimage{width=\columnwidth}
{dgsync.png}{img:dgsync}
{Derivation Graph per la rete 3.2}
\newpage
\centerimage{width=\columnwidth}
{35dgsync.pdf}{img:35dgsync}
{Derivation Graph per la rete 3.5}
Gli stati in comune tra i due modelli sono: \textbf{isTurnP, isTurnQ, setP, setQ}. Si applica lo
\textit{split} utilizzando questi stati come Azioni. Il set iniziale \`e rappresentato
dall'insieme degli stati dei due processi.
\subsubsection{Bisimulazione: Stato iniziale}
\begin{lstlisting}
{S1,T1}{T2,T3,T4,S2,S3,S4,S5,S6,S7,S8,S9,S10,S11,S12,S13,S14,S15,S16}
\end{lstlisting}
\subsubsection{Split su setP}
Si applica lo split sull'ultimo set:
\begin{lstlisting}
{T2,T3,T4,S2,S3,S4,S5,S6,S7,S8,S9,S10,S11,S12,S13,S14,S15,S16}
\end{lstlisting}
Si ottiene:
\begin{lstlisting}
{S1,T1}{T4,S15,S16}{T2,T3,S2,S3,S4,S5,S6,S7,S8,S9,S10,S11,S12,S13,S14}
\end{lstlisting}
\subsubsection{Split su isTurnQ}
Si applica lo split sull'ultimo set.
\begin{lstlisting}
{T2,T3,S2,S3,S4,S5,S6,S7,S8,S9,S10,S11,S12,S13,S14}
\end{lstlisting}
Si ottiene:
\begin{lstlisting}
{S1,T1}{T4,S15,S16}{T3,S12,S11}{T2,S2,S3,S4,S5,S6,S7,S8,S9,S10,S13,S14}
\end{lstlisting}
\subsubsection{Split su setQ}
Si applica lo split sull'ultimo set.
\begin{lstlisting}
{T2,S2,S3,S4,S5,S6,S7,S8,S9,S10,S13,S14}
\end{lstlisting}
Si ottiene:
\begin{lstlisting}
{S1,T1}{T4,S15,S16}{T3,S12,S11}{T2,S6,S9}{S2,S3,S4,S5,S7,S8,S10,S13,S14}
\end{lstlisting}
\subsubsection{Split su isTurnP}
Si applica lo split sul primo set.
\begin{lstlisting}
{S1,T1}
\end{lstlisting}
Si ottiene:
\begin{lstlisting}
{S1}{T1}{T4,S15,S16}{T3,S12,S11}{T2,S6,S9}{S2,S3,S4,S5,S7,S8,S10,S13,S14}
\end{lstlisting}
\subsubsection{Split su setQ}
Si applica lo split sul quarto set.
\begin{lstlisting}
{T2,S6,S9}
\end{lstlisting}
Si ottiene:
\begin{lstlisting}
{S1}{T1}{T4,S15,S16}{T3,S12,S11}{T2,S9}{S6}{S2,S3,S4,S5,S7,S8,S10,S13,S14}
\end{lstlisting}
\subsubsection{Split su isTurnQ}
Si applica lo split sul quarto set.
\begin{lstlisting}
{T3,S12,S11}
\end{lstlisting}
Si ottiene:
\begin{lstlisting}
{S1}{T1}{T4,S15,S16}{T3}{S11,S12}{T2,S6}{S9}{S2,S3,S4,S5,S7,S8,S10,S13,S14}
\end{lstlisting}
\subsubsection{Split su setP}
Si applica lo split sul terzo set.
\begin{lstlisting}
{T4,S15,S16}
\end{lstlisting}
Si ottiene:
\begin{lstlisting}
{S1}{T1}{T4}{S15,S16}{T3}{S11,S12}{T2,S6}{S9}{S2,S3,S4,S5,S7,S8,S10,S13,S14}
\end{lstlisting}
\subsubsection{Split su setQ}
Si applica lo spit sul settimo set.
\begin{lstlisting}
{T2,S6}
\end{lstlisting}
Si ottiene:
\begin{lstlisting}
{S1}{T1}{T4}{S15,S16}{T3}{S11,S12}{T2}{S6}{S9}{S2,S3,S4,S5,S7,S8,S10,S13,S14}
\end{lstlisting}
\subsubsection{Bisimulazione: conclusione}
L'algoritmo termina in quanto non \`e pi\`u possibile dividere alcun set sulla base delle
transizioni comuni.
Dopo aver applicato gli \textit{splitting} di cui sopra, i set sono partizionati nella
seguente maniera:
\begin{lstlisting}
{T1}{T4}{T3}{T2}{S1}{S15,S16}{S11,S12}{S6}{S9}{S2,S3,S4,S5,S7,S8,S10,S13,S14}
\end{lstlisting}
Come si pu\`o notare, gli stati dell'algoritmo $3.5$ sono gli unici elementi nel proprio set.
Se ci fosse bisimulazione, essi dovrebbero essere accoppiati a uno o pi\`u stati
dell'algoritmo $3.2$.
Possiamo quindi affermare che \textbf{non c'\`e bisimulazione} tra i due algoritmi.
\subsection{Riduzione Strutturale in modelli di reti P/T}
\subsubsection{3.2 - 3.5}
Si vogliono applicare le 4 tecniche viste di riduzione strutturale per confrontare le reti
$3.2$ e $3.5$. Si riportano i due modelli in reti P/T.
\centerimage{width=\columnwidth}
{rete32.jpg}{img:rete32}
{Modello P/T della rete 3.2}
\centerimage{width=\columnwidth}
{rete35.jpg}{img:rete35}
{Modello P/T della rete 3.5}
\break
La rete $3.5$ rappresenta un modello semplificato dell'algoritmo $3.2$, pertanto si riduce la
rete $3.2$.
Si applica:
\begin{description}
\item{\textbf{Fusion of places}: } La fusione dei posti $P0,P1$ - $Q0,Q1$ e $P2,P3$ -
$Q2,Q3$ (quindi su entrambe le transizioni $ncs$ e $cs$)
\end{description}
Ottenendo una rete equivalente alla $3.5$.
\subsubsection{3.6 - 3.8}
Si vogliono applicare le 4 tecniche viste di riduzione strutturale per confrontare le reti
$3.6$ e $3.8$. Si riportano i due modelli in reti P/T.
\centerimage{width=\columnwidth}
{rete36.jpg}{img:rete36}
{Modello P/T della rete 3.6}
\centerimage{width=\columnwidth}
{rete38.jpg}{img:rete38}
{Modello P/T della rete 3.8}
\break
La rete $3.6$ e la rete $3.8$ si differenziano per l'inversione delle istruzioni di $set$ e
$wait$.
Si applica:
\begin{description}
\item{\textbf{Fusion of places}: } La fusione dei posti $P0,P1$ - $Q0,Q1$ su entrambe le
reti.
\item{\textbf{Fusion of places}: } La fusione dei posti $P3,P4$ - $Q3,Q4$ su entrambe le
reti.
\item{\textbf{Self-loop elimination}: } L'eliminazione dei self-loop delle transizioni
$T1,T11$ su entrambe le reti.
\end{description}
A questo punto si puo` notare che le transizioni $set\{P,Q\}$ e $isWant\{P,Q\}$ non
sono riducibili in quanto non presentano nessuna delle strutture che permettono la
riduzione. Le due reti non sono quindi equivalenti.
\end{document}
Reference in a new issue Copy permalink