--- a/prio/Paper/Paper.thy	Thu Feb 02 13:58:16 2012 +0000
+++ b/prio/Paper/Paper.thy	Fri Feb 03 11:26:11 2012 +0000
@@ -50,7 +50,7 @@
 
   The idea behind PIP is to let the process $L$ temporarily
   inherit the high priority from $H$ until $L$ leaves the critical
-  section unlocking the resource. This solves the problem of $H$
+  section by unlocking the resource. This solves the problem of $H$
   having to wait indefinitely, because $L$ cannot, for example, be
   blocked by processes having priority $M$. While a few other
   solutions exist for the Priority Inversion problem, PIP is one that is widely deployed
@@ -80,14 +80,17 @@
   He suggests to avoid PIP altogether by not allowing critical
   sections to be preempted. While this might have been a reasonable
   solution in 2002, in our modern multiprocessor world, this seems out
-  of date.  However, there is clearly a need for investigating correct
-  and efficient 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 practise is proved by an
-  email by Baker, who wrote on 13 July 2009 on the Linux Kernel
-  mailing list:
+  of date. The reason is that this precludes other high-priority 
+  processes from running that do not make any use of the locked
+  resource.
+
+  However, 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 practise is
+  proved by an email by Baker, who wrote on 13 July 2009 on the Linux
+  Kernel mailing list:
 
   \begin{quote}
   \it{}``I observed in the kernel code (to my disgust), the Linux PIP
@@ -102,13 +105,28 @@
   again at PIP from a more abstract level (but still concrete enough
   to inform an implementation) and makes PIP an ideal candidate for a
   formal verification. One reason, of course, is that the original
-  presentation of PIP \cite{Sha90}, despite being
-  informally ``proved'' correct, is actually \emph{flawed}. Yodaiken
+  presentation of PIP \cite{Sha90}, despite being informally
+  ``proved'' correct, is actually \emph{flawed}. Yodaiken
   \cite{Yodaiken02} points to a subtlety that had been overlooked by
-  Sha et al. They write in \cite{Sha90}
+  Sha et al. They specify in \cite{Sha90} that after the process whose
+  priority has been raised completes its critical section and releases
+  the lock, it ``returns to its original priority level.'' This leads
+  them to believe that an implementation of PIP is ``rather
+  straightforward'' \cite{Sha90}.  Unfortunately, as Yodaiken pointed
+  out, this behaviour is too simplistic.  Consider the case where the
+  low priority process $L$ locks \emph{two} resources, and two
+  high-priority processes $H$ and $H'$, respectively, wait for one of
+  them.  If $L$ releases only one of them so that $H$, say, can
+  proceed, then we still have Priority Inversion with $H'$: according
+  to Sha et al., $L$ already dropped back to its low priority, but has not yet
+  released the lock $H'$ is waiting for. Therefore the correct behaviour for $L$
+  is to revert to the highest remaining priority of processes which it
+  blocks. The advantage of a formalisation of PIP in a theorem prover 
+  is that such issues clearly show up and cannot be dodged. 
 
-  But this is too
-  simplistic. Consider
+  There have been earlier formal investigations into PIP, but ...
+
+  \bigskip
   Priority Inversion problem has been known since 1980
   \cite{Lampson80}, but Sha et al.~give the first
   thorough analysis and present an informal correctness proof for PIP

Binary file prio/paper.pdf has changed