
diff -r 55d1591b17f0 -r 9f0b78fcc894 Journal/Paper.thy
--- a/Journal/Paper.thy	Fri Feb 28 12:49:58 2014 +0000
+++ b/Journal/Paper.thy	Mon Mar 03 16:22:48 2014 +0000
@@ -54,7 +54,7 @@
   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
@@ -81,17 +81,19 @@
   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
-  can be performed dynamically by the scheduler and is deterministic.
+  Two advantages of PIP are that it is deterministic and that increasing the priority of a thread
+  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
-  this problem by randomly boosting the priority of ready (low priority) threads
-  (e.g.~\cite{WINDOWSNT}).
+  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
+  (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
@@ -147,14 +149,17 @@
   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 
-  \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
+  of threads, i.e.~\emph{traces}, that could possibly happen).\medskip\smallskip
 
   \noindent
   {\bf Contributions:} There have been earlier formal investigations
@@ -326,10 +331,8 @@
   @{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}[ph]
+  \begin{figure}[t]
   \begin{center}
   \newcommand{\fnt}{\fontsize{7}{8}\selectfont}
   \begin{tikzpicture}[scale=1]
@@ -368,6 +371,9 @@
   \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  
@@ -1008,7 +1014,6 @@
 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}
@@ -1250,12 +1255,7 @@
   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 {*
-  \noindent
+  *}(*<*)end(*>*)text {*
   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
@@ -1288,7 +1288,7 @@
   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.
   
@@ -1314,7 +1314,7 @@
 
 
 
-  \begin{figure}[t]
+  \begin{figure}[tph]
   \begin{lstlisting}
 void lock_acquire (struct lock *lock)
 { ASSERT (lock != NULL);
@@ -1459,6 +1459,12 @@
   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
@@ -1478,9 +1484,9 @@
   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 
-  %can be downloaded from
-  %\url{http://www.inf.kcl.ac.uk/staff/urbanc/pip.html}.
+  The code of our formalisation 
+  can be downloaded from the Mercurial repository at
+  \url{http://www.inf.kcl.ac.uk/staff/urbanc/pip.html}.
 
   %\medskip
 




