--- a/prio/Paper/Paper.thy	Wed Feb 01 12:00:37 2012 +0000
+++ b/prio/Paper/Paper.thy	Wed Feb 01 15:00:17 2012 +0000
@@ -52,15 +52,55 @@
   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 to the Priority
-  Inversion problem exists \cite{Lampson:Redell:cacm:1980}, PIP is one
-  that is widely adopted and implemented [???Book] (where implemented???). 
-  One advantage of PIP is that raising the priority of a process
-  having a lock can be dynamically calculated. This is in contrast,
-  for example, to Priority Ceiling which requires static analysis 
-  of the program in order to avoid Priority Inversion.
+  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.
+
+  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:
+
+  \begin{quote}
+  \it{}``Priority inheritance is neither efficient nor reliable. Implementations
+  are either incomplete (and unreliable) or surprisingly complex and intrusive.''
+  \end{quote}
 
-  However there has also been strong criticism against PIP
+  \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:
+
+  \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.''
+  \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
+
+
 
   Priority Inversion problem has been known since 1980
   \cite{Lampson:Redell:cacm:1980}, but Sha et al.~give the first
@@ -68,18 +108,23 @@
   .\footnote{Sha et al.~call it the
   \emph{Basic Priority Inheritance Protocol}.}
 
+   POSIX.4: programming for the real world (Google eBook)
+
   However, there are further subtleties: just lowering the priority 
   of the process $L$ to its low priority, as proposed in ???, is 
   incorrect.\bigskip
 
-  \begin{quote}
-  \it{}``Priority inheritance is neither efficient nor reliable. Implementations
-  are either incomplete (and unreliable) or surprisingly complex and intrusive.''
-  \end{quote}
+  
 
   book: page 135, sec 5.6.5
 
-  do you need axioms in the formalisation?
+ 
+
+  
+
+  very little on implementations, not to mention implementations informed by 
+  formal correctness proofs.
+
   
   \noindent
   Priority inversion referrers to the phenomena where tasks with higher