
diff -r 0069bca6dd51 -r 45e1d324c493 Journal/Paper.thy
--- a/Journal/Paper.thy	Tue Jun 10 10:44:48 2014 +0100
+++ b/Journal/Paper.thy	Thu Jun 12 10:14:50 2014 +0100
@@ -56,7 +56,7 @@
   The classic example where this happened is the software that
   controlled the Mars Pathfinder mission in 1997 \cite{Reeves98}.
   On Earth the software run mostly without any problem, but
-  once the spacecraft landed on Mars, it shut down at irregular
+  once the spacecraft landed on Mars, it shut down at irregular, but frequent,
   intervals leading to loss of project time as normal operation of the
   craft could only resume the next day (the mission and data already
   collected were fortunately not lost, because of a clever system
@@ -112,9 +112,9 @@
   In our opinion, there is clearly a need for investigating correct
   algorithms for PIP. A few specifications for PIP exist (in English)
   and also a few high-level descriptions of implementations (e.g.~in
-  the textbook \cite[Section 5.6.5]{Vahalia96}), but they help little
-  with actual implementations. That this is a problem in practice is
-  proved by an email by Baker, who wrote on 13 July 2009 on the Linux
+  the textbooks \cite[Section 12.3.1]{Liu00} and \cite[Section 5.6.5]{Vahalia96}), 
+  but they help little with actual implementations. That this is a problem in 
+  practice is proved by an email by Baker, who wrote on 13 July 2009 on the Linux
   Kernel mailing list:
 
   \begin{quote}
@@ -130,43 +130,66 @@
   at PIP from a more abstract level (but still concrete enough
   to inform an implementation), and makes PIP a good candidate for a
   formal verification. An additional reason is that the original
-  presentation of PIP~\cite{Sha90}, despite being informally
+  specification of PIP~\cite{Sha90}, despite being informally
   ``proved'' correct, is actually \emph{flawed}. 
+  
 
-  Yodaiken \cite{Yodaiken02} and also Moylan et al.~\cite{deinheritance} 
-  point to a subtlety that had been
+  Yodaiken \cite{Yodaiken02} and also Moylan et
+  al.~\cite{deinheritance} point to a subtlety that had been
   overlooked in the informal proof by Sha et al. They specify in
   \cite{Sha90} that after the thread (whose priority has been raised)
-  completes its critical section and releases the lock, it ``{\it returns
-  to its original priority level}''. This leads them to believe that an
-  implementation of PIP is ``{\it rather straightforward}''~\cite{Sha90}.
-  Unfortunately, as Yodaiken and Moylan et al.~point out, this behaviour is too
-  simplistic. Moylan et al.~write that there are ``{\it some hidden traps}''. 
-  Consider the case where the low priority thread $L$
-  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. A similar error is made in the textbook
-  \cite[Section 2.3.1]{book} which specifies for a process that 
-  inherited a higher priority and exits a critical section ``{\it it resumes 
-  the priority it had at the point of entry into the critical section}''.
-  The same error can also be found in the more recent textbook 
-  \cite[Page 119]{Laplante11} which states ``{\it when [the task] exits the critical 
-  section that caused the block, it reverts to the priority it had when 
-  it entered that section}''.
-   
-  While \cite{Laplante11,book,Sha90} are the only formal publications we have 
-  found that describe the incorrect behaviour, not all, but many
-  informal\footnote{informal as in ``found on the Web''} 
-  descriptions of PIP overlook the possibility that another
+  completes its critical section and releases the lock, it ``{\it
+  returns to its original priority level}''. This leads them to
+  believe that an implementation of PIP is ``{\it rather
+  straightforward}''~\cite{Sha90}.  Unfortunately, as Yodaiken and
+  Moylan et al.~point out, this behaviour is too simplistic. Moylan et
+  al.~write that there are ``{\it some hidden traps}''~\cite{deinheritance}.  Consider the
+  case where the low priority thread $L$ 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. 
+  A similar
+  error is made in the textbook \cite[Section 2.3.1]{book} which
+  specifies for a process that inherited a higher priority and exits a
+  critical section ``{\it it resumes the priority it had at the point
+  of entry into the critical section}''.  The same error can also be
+  found in the more recent textbook \cite[Page 119]{Laplante11} where the
+  authors state: ``{\it when [the task] exits the critical section that caused
+  the block, it reverts to the priority it had when it entered that
+  section}''. The textbook \cite[Page 286]{Liu00} contains a simlar
+  flawed specification and even goes on to develop pseudo-code based on this
+  flawed specification. Accordingly, the operating system primitives
+  for inheritance and restoration of priorities in \cite{Liu00} depend on
+  maintaining a  data structure called \emph{inheritance log}. This log
+  is maintained for every thread and broadly specified as containing ``{\it
+  [h]istorical information on how the thread inherited its current
+  priority}'' \cite[Page 527]{Liu00}. Unfortunately, the important
+  information about actually
+  computing the priority to be restored solely from this log is  not explained in
+  \cite{Liu00} but left as an ``{\it excercise}'' to the reader.
+  Of course, a correct version of PIP does not need to maintain
+  this (potentially expensive) data structure at all. 
+
+  
+  While \cite{Laplante11,Liu00,book,Sha90} are the only formal publications we have 
+  found that specify the incorrect behaviour, it seems also many
+  informal 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).\medskip\smallskip
+  A notable exception is the texbook \cite{buttazzo}, which gives the correct 
+  behaviour of resetting the priority of a thread to the highest remaining priority of the 
+  threads it blocks. This textbook also gives an informal proof for 
+  the correctness of PIP in the style of Sha et al. Unfortunately, this informal 
+  proof is too vague to be useful for formalising the correctness of PIP
+  and the specification leaves out nearly all details in order 
+  to implement PIP efficiently.\medskip\smallskip
+  %
+  %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).
 
   \noindent
   {\bf Contributions:} There have been earlier formal investigations
@@ -186,9 +209,9 @@
   to the thread with the highest priority so that it terminates more
   quickly.  We were also being able to generalise the scheduler of Sha
   et al.~\cite{Sha90} to the practically relevant case where critical 
-  sections can overlap; see Figure~\ref{overlap} below for an example of 
-  this restriction. In the existing literature there is no 
-  proof and also no proving method that cover this generalised case.
+  sections can overlap; see Figure~\ref{overlap} \emph{a)} below for an example of 
+  this restriction. %In the existing literature there is no 
+  %proof and also no proving method that cover this generalised case.
 
   \begin{figure}
   \begin{center}




