--- a/prio/Paper/Paper.thy	Wed Feb 01 17:46:36 2012 +0000
+++ b/prio/Paper/Paper.thy	Thu Feb 02 13:58:16 2012 +0000
@@ -30,14 +30,14 @@
   process with priority $M$, and so $H$ sits there potentially waiting
   indefinitely. Since $H$ is blocked by processes with lower
   priorities, the problem is called Priority Inversion. It was first
-  described in \cite{Lampson:Redell:cacm:1980} in the context of the
+  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{Reeves-Glenn-1998}.  Once the spacecraft landed, the software
+  \cite{Reeves98}.  Once the spacecraft landed, the software
   shut down at irregular 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
@@ -46,15 +46,14 @@
   priority task locking a resource prevented a high priority process
   from running in time leading to a system reset. Once the problem was found,
   it was rectified by enabling the \emph{Priority Inheritance Protocol} 
-  (PIP) \cite{journals/tc/ShaRL90} in the scheduling software.
+  (PIP) \cite{Sha90} in the scheduling software.
 
   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$
   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
-  \cite{Lampson:Redell:cacm:1980}, PIP is one that is widely deployed
+  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
@@ -62,14 +61,15 @@
 
   One advantage of PIP is that increasing the priority of a process
   can be dynamically calculated by the scheduler. This is in contrast
-  to, for example, \emph{Priority Ceiling}, another solution to the
-  Priority Inversion problem, which requires static analysis of the
-  program in order to be helpful. However, there has also been strong
-  criticism against PIP. For instance, PIP cannot prevent deadlocks,
-  and also blocking times can be substantial (more than just the
-  duration of a critical section).  Though, most criticism against PIP
-  centres around unreliable implementations and around PIP being
-  too complicated and too inefficient.  For example, Yodaiken writes in \cite{Yodaiken02}:
+  to, for example, \emph{Priority Ceiling} \cite{Sha90}, another
+  solution to the Priority Inversion problem, which requires static
+  analysis of the program in order to be helpful. 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 implementations and PIP being too complicated and
+  too inefficient.  For example, Yodaiken writes in \cite{Yodaiken02}:
 
   \begin{quote}
   \it{}``Priority inheritance is neither efficient nor reliable. Implementations
@@ -78,15 +78,16 @@
 
   \noindent
   He suggests to avoid PIP altogether by not allowing critical
-  sections to be preempted. While this was a sensible 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 from Baker, who wrote on 13 July 2009 on the Linux
-  Kernel mailing list:
+  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:
 
   \begin{quote}
   \it{}``I observed in the kernel code (to my disgust), the Linux PIP
@@ -97,18 +98,19 @@
   \end{quote}
 
   \noindent
-  This however means it is useful to look at PIP again 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, despite being informally ``proved'' correct, is
-  flawed. Yodaiken \cite{Yodaiken02} points to a subtlety that has
-  been overlooked by Sha et al.
+  The criticism by Yodaiken, Baker and others suggests to us to look
+  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
+  \cite{Yodaiken02} points to a subtlety that had been overlooked by
+  Sha et al. They write in \cite{Sha90}
 
   But this is too
   simplistic. Consider
   Priority Inversion problem has been known since 1980
-  \cite{Lampson:Redell:cacm:1980}, but Sha et al.~give the first
+  \cite{Lampson80}, but Sha et al.~give the first
   thorough analysis and present an informal correctness proof for PIP
   .\footnote{Sha et al.~call it the
   \emph{Basic Priority Inheritance Protocol}.}
@@ -125,20 +127,11 @@
   formal correctness proofs.
 
   
-  \noindent
-  Priority inversion referrers to the phenomena where tasks with higher 
-  priority are blocked by ones with lower priority. If priority inversion 
-  is not controlled, there will be no guarantee the urgent tasks will be 
-  processed in time. As reported in \cite{Reeves-Glenn-1998}, 
-  priority inversion used to cause software system resets and data lose in 
-  JPL's Mars pathfinder project. Therefore, the avoiding, detecting and controlling 
-  of priority inversion is a key issue to attain predictability in priority 
-  based real-time systems. 
 
-  The priority inversion phenomenon was first published in \cite{Lampson:Redell:cacm:1980}. 
+  The priority inversion phenomenon was first published in \cite{Lampson80}. 
   The two protocols widely used to eliminate priority inversion, namely 
   PI (Priority Inheritance) and PCE (Priority Ceiling Emulation), were proposed 
-  in \cite{journals/tc/ShaRL90}. PCE is less convenient to use because it requires 
+  in \cite{Sha90}. PCE is less convenient to use because it requires 
   static analysis of programs. Therefore, PI is more commonly used in 
   practice\cite{locke-july02}. However, as pointed out in the literature, 
   the analysis of priority inheritance protocol is quite subtle\cite{yodaiken-july02}.