1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
|
\documentclass[a4paper,10pt,twocolumn]{article}
\usepackage[english]{babel}
\usepackage[latin1]{inputenc}
\usepackage[margin=18mm,top=15mm]{geometry}
\usepackage{url}
\usepackage[hidelinks]{hyperref}
\usepackage{graphicx}
\usepackage{minted}
% Not so much list item spacing; see http://tex.stackexchange.com/a/10689/23992
\usepackage{enumitem}
\setlist{itemsep=0pt,parsep=1pt}
\title{Modelling dining savages}
\author{Camil Staps}
\begin{document}
\maketitle
\begin{abstract}
Unfortunately, missionaries aren't always popular. Although it is difficult to get an exact picture due to the few people returning to their home country, experts estimate that nearly all missionaries end up as a savage's stew. To plan future missions, it is important to be able to tell more precisely how many missionaries get eaten and when. We need to take into account the amount of savages in the destination country, the size of their pots and the speed with which their cook can make stewed missionary.
Allen B. Downey has, inspired by Gregory Andrews, designed a model that can help us with this important task \cite[p.~121~ff.]{downey}. In this paper, we will attempt to prove correctness properties claimed by Downey using the model checker UPPAAL \cite{uppaal}.
\end{abstract}
\section{Report organisation}
\label{sec:introduction}
In Section \ref{sec:models} I will discuss and argue the realisation of UPPAAL models based on Downey's solution. Section \ref{sec:analysis} provides an analysis of the properties of the models and a verification of the properties Downey claims his solution has. In Section \ref{sec:discussion} I will give a small tip to Downey to improve his book, and briefly summarise some things I learned from this assignment.
\section{The models}
\label{sec:models}
The models used are directly based on Downey's code. I used Roelof Hamberg and Frits Vaandrager's UPPAAL model of a semaphore \cite[p.~10]{uppaal-semaphores}, which has not been included here for the sake of brevity.
First, let's see some common declarations:
\begin{minted}[tabsize=0,xleftmargin=16pt,breaklines]{c}
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.
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.
In the system declarations, we create the needed semaphores. Here, \texttt{N} is the total number of processes. \texttt{5} is the number of savages plus 1.
\begin{minted}[tabsize=0,xleftmargin=16pt,breaklines]{c}
EmptyPot = Semaphore(emptyPot, N-1, 0);
FullPot = Semaphore(fullPot, N-1, 0);
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}).
\begin{figure*}[h]
\centering
\includegraphics[width=.75\linewidth]{model-cook}
\caption{UPPAAL model for the cook}
\label{fig:model-cook}
\end{figure*}
The model of the savages in Figure \ref{fig:model-savage} is only slightly more complicated. As in Downey's code, the savage gains control of a \texttt{mutex}. Then, if there is a serving in the pot (\texttt{servings > 0}) he directly continues eating (\texttt{servings = servings - 1}). If there is no serving in the pot (\texttt{servings == 0}), he wakes up the cook using the \texttt{emptyPot} semaphore. He then waits for the \texttt{fullPot} semaphore (which is signalled by the cook) to start eating. After eating, the savage leaves the \texttt{mutex}.
\begin{figure*}[h]
\centering
\includegraphics[width=.75\linewidth]{model-savage}
\caption{UPPAAL model for the savages}
\label{fig:model-savage}
\end{figure*}
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}
The only place where we put two statements on a single edge is when the savage finds an empty pot. Here, no relevant extra concurrency safety is assumed (and obviously the edges with only one statement don't assume extra concurrency safety). Therefore, this is a valid model of Downey's solution. We did not make any assumptions about his code. Both models are very straightforward, and no difficulties were experienced when designing them.
These are \emph{good models} \cite{good-models}:
\begin{itemize}
\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 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.
\end{itemize}
\section{Analysis}
\label{sec:analysis}
Using UPPAAL, we can analyse the properties of these models. The synchronisation constraints Downey wanted to satisfy \cite[p.~122]{downey} were:
\begin{itemize}
\item Savages cannot invoke \texttt{getServingsFromPot} if the pot is empty
\item The cook can invoke \texttt{putServingsInPot} only if the pot is empty
\end{itemize}
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.
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.
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<> 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.
\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.
UPPAAL manages to search the whole state space in far under a second with reasonable numbers of savages. We do not need to make any abstractions or simplifications from Downey's code.
\section{Discussion}
\label{sec:discussion}
Downey's solution is clear, and follows logically from the problem. A naive implementation of his solution in UPPAAL leads to \emph{good models} \cite{good-models}, which tells us something about the quality of his solution. The only thing I see he could do to improve his solution is to let the cook fill the pot (i.e., put \texttt{servings = M} in the code of the cook). This is more logical. Downey argues that in this way it is clearer that all accesses to \texttt{servings} are inside the mutex, however, this dissociates the model from reality and doesn't even add that much clarity.
This report was written in the context of the undergraduate course Operating Systems at the Radboud University Nijmegen. By making this report, experience was gained in working with a model checker. Also, I learned to look critically at other people's work.
However, I would have preferred a more creative assignment, such as the one in the Processors course. It would have been more interesting to have to invent the solution yourself, and then prove its correctness in UPPAAL. Of course, this also would have taken more time.
\begin{thebibliography}{9}
\bibitem{downey} Downey, A. B (2008). \emph{The little book of semaphores}. \url{http://greenteapress.com/semaphores/}
\bibitem{uppaal} \textsc{Uppaal} 4.0.14, an integrated tool environment for modeling, validation and verification of real-time systems [\,\dots]. \url{http://uppaal.org/}
\bibitem{uppaal-semaphores} Hamberg, R. \& Vaandrager, F. (2007). \emph{Using model checkers in an introductory course on operating systems}.
\bibitem{good-models} Vaandrager, F. (2010). \emph{What is a good model?} Retrieved October 25, 2015. \url{http://www.cs.ru.nl/~fvaan/PV/what_is_a_good_model.html}
\end{thebibliography}
\end{document}
|
