pip: comparison Journal/Paper.thy

equal deleted inserted replaced

-:55d1591b17f0
+:9f0b78fcc894
 thread with priority $M$, and so $H$ sits there potentially waiting
 indefinitely. Since $H$ is blocked by threads with lower
 priorities, the problem is called Priority Inversion. It was first
 described in \cite{Lampson80} in the context of the
 Mesa programming language designed for concurrent programming.
 If the problem of Priority Inversion is ignored, real-time systems
 can become unpredictable and resulting bugs can be hard to diagnose.
 The classic example where this happened is the software that
 controlled the Mars Pathfinder mission in 1997 \cite{Reeves98}.
 Once the spacecraft landed, the software shut down at irregular
 wait indefinitely, because $L$ cannot be blocked by threads having
 priority $M$. While a few other solutions exist for the Priority
 Inversion problem, PIP is one that is widely deployed and
 implemented. This includes VxWorks (a proprietary real-time OS used
 in the Mars Pathfinder mission, in Boeing's 787 Dreamliner, Honda's
-ASIMO robot, etc.), but also the POSIX 1003.1c Standard realised for
+ASIMO robot, etc.) and ThreadX (another proprietary real-time OS
+used in HP inkjet printers \cite{ThreadX}), but also
+the POSIX 1003.1c Standard realised for
 example in libraries for FreeBSD, Solaris and Linux.
-Two advantages of PIP are that increasing the priority of a thread
+Two advantages of PIP are that it is deterministic and that increasing the priority of a thread
-can be performed dynamically by the scheduler and is deterministic.
+can be performed dynamically by the scheduler.
 This is in contrast to \emph{Priority Ceiling}
 \cite{Sha90}, another solution to the Priority Inversion problem,
 which requires static analysis of the program in order to prevent
-Priority Inversion, and also to the Windows NT scheduler, which avoids
+Priority Inversion, and also in contrast to the Windows NT scheduler, which avoids
-this problem by randomly boosting the priority of ready (low priority) threads
+this problem by randomly boosting the priority of ready low-priority threads
-(e.g.~\cite{WINDOWSNT}).
+(see for instance~\cite{WINDOWSNT}).
 However, there has also been strong criticism against
 PIP. For instance, PIP cannot prevent deadlocks when lock
 dependencies are circular, and also blocking times can be
 substantial (more than just the duration of a critical section).
 Though, most criticism against PIP centres around unreliable
 locks \emph{two} resources, and two high-priority threads $H$ and
 $H'$ each wait for one of them.  If $L$ releases one resource
 so that $H$, say, can proceed, then we still have Priority Inversion
 with $H'$ (which waits for the other resource). The correct
 behaviour for $L$ is to switch to the highest remaining priority of
-the threads that it blocks. The advantage of formalising the
+the threads that it blocks. While
+\cite{Sha90} is the only formal publication we have
+found that describes the incorrect behaviour, not all, but many
+informal\footnote{informal as in ``found on the Web''}
+descriptions of PIP overlook the possibility that another
+high-priority might wait for a low-priority process to finish.
+The advantage of formalising the
 correctness of a high-level specification of PIP in a theorem prover
 is that such issues clearly show up and cannot be overlooked as in
 informal reasoning (since we have to analyse all possible behaviours
-of threads, i.e.~\emph{traces}, that could possibly happen).\footnote{While
+of threads, i.e.~\emph{traces}, that could possibly happen).\medskip\smallskip
-\cite{Sha90} is the only formal publication we have
-found that describes the incorrect behaviour, not all, but many
-informal descriptions of PIP overlook the case...}\medskip
 \noindent
 {\bf Contributions:} There have been earlier formal investigations
 into PIP \cite{Faria08,Jahier09,Wellings07}, but they employ model
 checking techniques. This paper presents a formalised and
 \begin{isabelle}\ \ \ \ \ %%%
 @{thm cs_depend_def}
 \end{isabelle}
-\noindent
-If there is no cycle, then every RAG can be pictured as a forrest of trees, for example as follows:
+\begin{figure}[t]
-\begin{figure}[ph]
 \begin{center}
 \newcommand{\fnt}{\fontsize{7}{8}\selectfont}
 \begin{tikzpicture}[scale=1]
 %%\draw[step=2mm] (-3,2) grid (1,-1);
 \end{center}
 \caption{An instance of a Resource Allocation Graph (RAG).\label{RAGgraph}}
 \end{figure}
 \noindent
+If there is no cycle, then every RAG can be pictured as a forrest of trees, as
+for example in Figure~\ref{RAGgraph}.
 We will design our scheduler
 so that every thread can be in the possession of several resources, that is
 it has potentially several incoming holding edges in the RAG, but has at most one outgoing
 waiting edge. The reason is that when a thread asks for resource that is locked
 already, then the process is blocked and cannot ask for another resource.
 section {* Properties for an Implementation\label{implement} *}
 text {*
 While our formalised proof gives us confidence about the correctness of our model of PIP,
 we found that the formalisation can even help us with efficiently implementing it.
 For example Baker complained that calculating the current precedence
 in PIP is quite ``heavy weight'' in Linux (see the Introduction).
 In our model of PIP the current precedence of a thread in a state @{text s}
 depends on all its dependants---a ``global'' transitive notion,
 which is indeed heavy weight (see Def.~shown in \eqref{cpreced}).
 \noindent
 This lemma states that if an intermediate @{term cp}-value does not change, then
 the procedure can also stop, because none of its dependent threads will
 have their current precedence changed.
-*}
+*}(*<*)end(*>*)text {*
-(*<*)
-end
-(*>*)
-text {*
-\noindent
 As can be seen, a pleasing byproduct of our formalisation is that the properties in
 this section closely inform an implementation of PIP, namely whether the
 RAG needs to be reconfigured or current precedences need to
 be recalculated for an event. This information is provided by the lemmas we proved.
 We confirmed that our observations translate into practice by implementing
 an unlocked resource is given next to the waiting thread with the
 highest precedence is realised in our implementation by priority queues. We implemented
 them as \emph{Braun trees} \cite{Paulson96}, which provide efficient @{text "O(log n)"}-operations
 for accessing and updating. In the code we shall describe below, we use the function
 @{ML_text "queue_insert"}, for inserting a new element into a priority queue, and
-@{ML_text "queue_update"}, for updating the position of an element that is already
+the function @{ML_text "queue_update"}, for updating the position of an element that is already
 in a queue. Both functions take an extra argument that specifies the
 comparison function used for organising the priority queue.
 Apart from having to implement relatively complex data\-structures in C
 using pointers, our experience with the implementation has been very positive: our specification
 If not, then the assertions indicate a bug in PINTOS and the result will be
 a ``kernel panic''.
-\begin{figure}[t]
+\begin{figure}[tph]
 \begin{lstlisting}
 void lock_acquire (struct lock *lock)
 { ASSERT (lock != NULL);
 ASSERT (!intr_context());
 ASSERT (!lock_held_by_current_thread (lock));
 verification of this algorithm, involving more fine-grained events,
 is a magnitude harder than the one we presented here, but still
 within reach of current theorem proving technology. We leave this
 for future work.
+To us, it seems sound reasoning about scheduling algorithms is fiendishly difficult
+if done informally by ``pencil-and-paper''. This is proved by the flawed proof
+in the paper by Sha et al.~\cite{Sha90} and also by Regehr \cite{Regehr} who
+pointed out an error in a paper about Preemption
+Threshold Scheduling \cite{ThreadX}. The use of a theorem prover was
+invaluable to us in order to feel confident about the correctness of our results.
 The most closely related work to ours is the formal verification in
 PVS of the Priority Ceiling Protocol done by Dutertre
 \cite{dutertre99b}---another solution to the Priority Inversion
 problem, which however needs static analysis of programs in order to
 avoid it. There have been earlier formal investigations
 consists of around 210 lemmas and overall 6950 lines of readable Isabelle/Isar
 code with a few apply-scripts interspersed. The formal model of PIP
 is 385 lines long; the formal correctness proof 3800 lines. Some auxiliary
 definitions and proofs span over 770 lines of code. The properties relevant
 for an implementation require 2000 lines.
-%The code of our formalisation
+The code of our formalisation
-%can be downloaded from
+can be downloaded from the Mercurial repository at
-%\url{http://www.inf.kcl.ac.uk/staff/urbanc/pip.html}.
+\url{http://www.inf.kcl.ac.uk/staff/urbanc/pip.html}.
 %\medskip
 %\noindent
 %{\bf Acknowledgements:}

changeset 22	9f0b78fcc894
parent 20	b56616fd88dd
child 23	24e6884d9258