diff options
Diffstat (limited to 'uppaalassignment')
| -rw-r--r-- | uppaalassignment/report.tex | 17 |
1 files changed, 7 insertions, 10 deletions
diff --git a/uppaalassignment/report.tex b/uppaalassignment/report.tex index 1ae5bca..fa3585f 100644 --- a/uppaalassignment/report.tex +++ b/uppaalassignment/report.tex @@ -41,12 +41,11 @@ First, let's see some common declarations: const int emptyPot = 0; const int fullPot = 1; const int mutex = 2; - int servings = 5; const int max_servings = 5; \end{minted} -Some declarations that are common to any semaphore model in have been left out. +Some declarations that are common to any semaphore model have been left out. The first three constants define semaphore identifiers. The \texttt{servings} variable holds at any time the number of servings in the pot. The \texttt{max\_servings} constant is the maximum number of servings the pot can hold, and also the number the cook will set \texttt{servings} to when invoked. @@ -58,7 +57,7 @@ In the system declarations, we create the needed semaphores. Here, \texttt{N} is Mutex = Semaphore(mutex, 5, 1); \end{minted} -The model for the cook is very straightforward and can be found in Figure \ref{fig:model-cook}. We see the two semaphores, \texttt{emptyPot} and \texttt{fullPot}. In contrast with Downey's code, I let the cook rather than a savage fill the pot (\texttt{servings := max\_servings}). +The model for the cook is very straightforward and can be found in Figure \ref{fig:model-cook}. We see the two semaphores, \texttt{emptyPot} and \texttt{fullPot}. In contrast with Downey's code, I let the cook rather than the savages fill the pot (\texttt{servings := max\_servings}). \begin{figure*}[h] \centering @@ -80,12 +79,10 @@ This gives us the following additional system declarations: \begin{minted}[tabsize=0,xleftmargin=16pt,breaklines]{c} cook = Cook(0); - s1 = Savage(0); s2 = Savage(1); s3 = Savage(2); s4 = Savage(3); - system EmptyPot, FullPot, Mutex, cook, s1, s2, s3, s4; \end{minted} @@ -97,7 +94,7 @@ These are \emph{good models} \cite{good-models}: \item Both have a clear \emph{object of modeling}: the cook, or the savage. \item They have a clear \emph{purpose}: as explained above, we are going to use these models to verify properties Downey claims about his code. \item The models are \emph{traceable}: every line (not counting the implicit `\texttt{while True}') relates to one or at most two (in the case of a \texttt{wait()} call) edges in the models. Only the line \texttt{eat()} is left out, because it's redundant. - \item Both models are \emph{truthful}. The implementation of a sleeping cook that can be woken up using a semaphore makes sense, as does the semaphore that is used to signal a savage when the cook refilled the pot. It makes sense that the cook resets \texttt{servings} (refills the pot) and that the savages decrease it (eat). + \item Both models are \emph{truthful}. The implementation of a sleeping cook that can be woken up using a semaphore makes sense, as does the semaphore that is used to signal a savage when the cook refilled the pot. It makes sense that the cook resets \texttt{servings} (refills the pot) and that the savages decrease it (eat from it). \item The models are minimal and \emph{simple}. As said above, we translated (nearly) every line of code into a single edge in the model, so that we don't assume any concurrency safety in the model. Furthermore, no other edges were added, which makes these models minimal. \item By using parameters (\texttt{pid}), the models have been made \emph{extensible and reusable}. It is possible to analyse multiple savages, or multiple cooks, at once. The models interact using the well known and broadly used interface of semaphores, which furthermore makes it possible to use this cook model in interaction with a different savage model, or vice versa. \item Both models have a clear interface (that of the semaphore). This allows for \emph{interoperability and sharing} of semantics. @@ -114,19 +111,19 @@ Using UPPAAL, we can analyse the properties of these models. The synchronisation Furthermore, Downey claims \cite[p.~125]{downey} that ``this solution is deadlock-free''. -If savages can invoke \texttt{getServingsFromPot} when the pot is empty, there must be a situation possible where \texttt{s1.eat and servings == 0}. Here, \texttt{s1} is one of the savages. This of course doesn't check if the same holds for \texttt{s2}, however, these two are equivalent, so we only have to consider one savage. We thus check in UPPAAL: \texttt{A[] not (s1.eat and servings == 0)}. Also this property is satisfied. +If savages can invoke \texttt{getServingsFromPot} when the pot is empty, there must be a situation possible where \texttt{s1.eat and servings == 0}. Here, \texttt{s1} is one of the savages. This of course doesn't check if the same holds for \texttt{s2}, however, these two are equivalent, so we only have to consider one savage. We thus check in UPPAAL: \texttt{A[] not (s1.eat and servings == 0)}. This property is satisfied. The second constraint Downey wanted to satisfy translates to the UPPAAL query \texttt{A[] not (cook.put and servings != 0)}, which also turns out to be satisfied, after checking. -We can check the claim about deadlock-freeness with UPPAAL's verifier. The query \texttt{A[] not deadlock} can be verified (well within a tenth of a second), so Downey is correct in this. +We can check the claim about deadlock-freedom with UPPAAL's verifier. The query \texttt{A[] not deadlock} can be verified (well within a tenth of a second), so Downey is correct in this. To verify some other constraints, common to semaphore environments or otherwise relevant to this problem, I also added and checked the following properties: \begin{itemize} - \item \texttt{E<> servings == 0}, to verify there is a situation where the pot is empty. Essentially, this makes sure that the savages are eating. + \item \texttt{E<> servings == 0}, to verify there is a situation where the pot is empty. Essentially, this makes sure that the savages are eating, and do not notify the cook too early. \item \texttt{E<> cook.put}, to check there is a situation where the cook has to work. \item \texttt{A[] not (Mutex.overflow or FullPot.overflow or EmptyPot.overflow)}, to verify that the semaphores are used properly. - \item \texttt{A[] servings >= 0}, because a pot cannot hold a negative number of missionaries. + \item \texttt{A[] servings >= 0}, because a pot cannot hold a negative number of servings. \end{itemize} Lastly, Downey poses the question, ``Does this solution assume that the pot is thread-safe, or does it guarantee that \texttt{putServingsInPot} and \texttt{getServingFromPot} are executed exclusively?'' We did not assume a thread-safe pot. Our pot is a simple a variable (\texttt{servings}, and from the models it is clear that nothing has been assumed about this variable. Thread-safety is totally ensured by three semaphores. |