
diff -r 83b0317370c2 -r 22b6bd498419 prio/Paper/Paper.thy
--- a/prio/Paper/Paper.thy	Wed Feb 01 15:00:17 2012 +0000
+++ b/prio/Paper/Paper.thy	Wed Feb 01 17:40:00 2012 +0000
@@ -13,62 +13,63 @@
 text {*
   Many real-time systems need to support processes with priorities and
   locking of resources. Locking of resources ensures mutual exclusion
-  when accessing shared data or devices. Priorities allow scheduling
-  of processes that need to finish their work within deadlines.
-  Unfortunately, both features can interact in subtle ways leading to
-  a problem, called \emph{Priority Inversion}. Suppose three processes
-  having priorities $H$(igh), $M$(edium) and $L$(ow). We would expect
-  that the process $H$ blocks any other process with lower priority
-  and itself cannot be blocked by a process with lower priority. Alas,
-  in a naive implementation of resource looking and priorities this
-  property can be violated. Even worse, $H$ can be delayed
-  indefinitely by processes with lower priorities. For this let $L$ be
-  in the possession of a lock for a resource that also $H$ needs. $H$
-  must therefore wait for $L$ to release this lock. The problem is
-  that $L$ might in turn be blocked by any 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 Mesa
-  programming language designed for concurrent programming.
+  when accessing shared data or devices that cannot be
+  preempted. Priorities allow scheduling of processes that need to
+  finish their work within deadlines.  Unfortunately, both features
+  can interact in subtle ways leading to a problem, called
+  \emph{Priority Inversion}. Suppose three processes having priorities
+  $H$(igh), $M$(edium) and $L$(ow). We would expect that the process
+  $H$ blocks any other process with lower priority and itself cannot
+  be blocked by any process with lower priority. Alas, in a naive
+  implementation of resource looking and priorities this property can
+  be violated. Even worse, $H$ can be delayed indefinitely by
+  processes with lower priorities. For this let $L$ be in the
+  possession of a lock for a resource that also $H$ needs. $H$ must
+  therefore wait for $L$ to exit the critical section and release this
+  lock. The problem is that $L$ might in turn be blocked by any
+  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
+  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
-  shut down at irregular intervals leading to loss of project time, as
+  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
   of a clever system design).  The reason for the shutdowns was that
   the scheduling software fell victim of Priority Inversion: a low
   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 Priority Inheritance Protocol in
-  the scheduling software.
+  it was rectified by enabling the \emph{Priority Inheritance Protocol} 
+  (PIP) \cite{journals/tc/ShaRL90} in the scheduling software.
 
-  The idea behind the \emph{Priority Inheritance Protocol} (PIP)
-  \cite{journals/tc/ShaRL90} is to let the process $L$ temporarily
-  inherit the high priority from $H$ until $L$ releases the locked
-  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 and implemented, including in
-  VxWorks (a proprietary real-time OS used in the Mars Pathfinder
-  mission, in Boeing's 787 Dreamliner, Honda's ASIMO robot, etc.), but
-  also as POSIX 1003.1c Standard, realised for example in libraries
-  for FreeBSD, Solaris and Linux. One advantage of PIP is that
-  increasing the priority of a process can be dynamically
-  calculated. This is in contrast to, for example, \emph{Priority Ceiling}---another 
-  solution to the Priority Inversion problem, which however
-  requires static analysis of the program in order to be helpful.
+  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
+  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 example in libraries for FreeBSD, Solaris and Linux.
 
-  However there has also been strong criticism against using PIP. For
-  example it cannot prevent deathlocks and also blocking times can be
-  substantial (more than just the duration of a critical section).
-  However, most criticism of PIP centres around unreliabale
-  implementations of PIP and PIP being complex. For example, Y...writes:
+  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}:
 
   \begin{quote}
   \it{}``Priority inheritance is neither efficient nor reliable. Implementations
@@ -76,32 +77,36 @@
   \end{quote}
 
   \noindent
-  His solution is to avoid PIP altogether by not allowing critical sections to be 
-  pre-empted. While this might have been a sensible solution in 198..., in our
-  modern multiprocessor world, this seems out of date. 
-  While there exists 
-   That there is a practical need
-
-   Baker wrote on 13 July 2009 in the Linux Kernel mailing list:
+  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:
 
   \begin{quote}
-  \it{}``I observed in the kernel code
-  (to my disgust), the Linux PIP implementation is a nightmare:
-  extremely heavy weight, involving maintenance of a full wait-for
-  graph, and requiring updates for a range of events, including
-  priority changes and interruptions of wait operations.''
+  \it{}``I observed in the kernel code (to my disgust), the Linux PIP
+  implementation is a nightmare: extremely heavy weight, involving
+  maintenance of a full wait-for graph, and requiring updates for a
+  range of events, including priority changes and interruptions of
+  wait operations.''
   \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 efficient implementation) 
-  and makes it an ideal candidate for a formal verification. One reason
-  is of course that the original presentation of PIP, including a correcness ``proof'',
-  is flawed. Y... points out a subletly that has been overlooked by Sha et al.
-  But this is too simplistic. Consider
+  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.
 
-
-
+  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
   thorough analysis and present an informal correctness proof for PIP
@@ -116,12 +121,6 @@
 
   
 
-  book: page 135, sec 5.6.5
-
- 
-
-  
-
   very little on implementations, not to mention implementations informed by 
   formal correctness proofs.
 




