Start report UPPAAL assignment

4 files changed, 95 insertions, 0 deletions

diff --git a/uppaalassignment/model-cook.png b/uppaalassignment/model-cook.png
new file mode 100644
index 0000000..9c34df1
--- /dev/null
+++ b/uppaalassignment/model-cook.png
diff --git a/uppaalassignment/model-savage.png b/uppaalassignment/model-savage.png
new file mode 100644
index 0000000..3bb5ee5
--- /dev/null
+++ b/uppaalassignment/model-savage.png
diff --git a/uppaalassignment/model-semaphore.png b/uppaalassignment/model-semaphore.png
new file mode 100644
index 0000000..4d3a842
--- /dev/null
+++ b/uppaalassignment/model-semaphore.png
diff --git a/uppaalassignment/report.tex b/uppaalassignment/report.tex
new file mode 100644
index 0000000..850c0d3
--- /dev/null
+++ b/uppaalassignment/report.tex
@@ -0,0 +1,95 @@
+\documentclass[a4paper,10pt,twocolumn]{extarticle}
+
+\usepackage[english]{babel}
+\usepackage[latin1]{inputenc}
+\usepackage{url}
+\usepackage[hidelinks]{hyperref}
+\usepackage{graphicx}
+
+% 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. In this paper, we will attempt to prove correctness properties claimed by Downey using the model checker UPPAAL.
+    %todo cite Downey, Andrews, UPPAAL
+\end{abstract}
+
+\section{Introduction}
+\label{sec:introduction}
+%todo
+
+\section{The models}
+\label{sec:models}
+The models used are directly based on Downey's code.
+
+%todo semaphore model
+
+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=\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=\linewidth]{model-savage}
+    \caption{UPPAAL model for the savages}
+    \label{fig:model-savage}
+\end{figure*}
+
+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}: %todo cite
+
+\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.
+        %todo interoperability & sharing
+\end{itemize}
+
+\section{Analysis}
+\label{sec:analysis}
+Using UPPAAL, %todo cite
+we can analyse the properties of these models. The synchronisation constraints Downey wanted to satisfy were: %todo cite
+
+\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 %todo cite
+that ``this solution is deadlock-free''.
+
+%todo analysis
+
+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?''
+
+%todo analysis
+
+UPPAAL manages to search the whole state space in far under a second with reasonable numbers of savages. %todo test how many is a bottleneck
+We do not need to make any abstractions or simplifications from Downey's code.
+
+\begin{thebibliography}{9}
+%\bibitem{kp2009} Martin R. Albrecht, Kenneth G. Paterson and Gaven J. Watson. Plaintext Recovery Attacks against SSH, University of London, 2009. \url{http://isg.rhul.ac.uk/~kp/SandPfinal.pdf}
+\end{thebibliography}
+
+\end{document}