--- a/prio/Paper/Paper.thy	Wed Feb 01 08:16:00 2012 +0000
+++ b/prio/Paper/Paper.thy	Wed Feb 01 12:00:37 2012 +0000
@@ -3,6 +3,7 @@
 imports CpsG ExtGG (* "~~/src/HOL/Library/LaTeXsugar" *) LaTeXsugar
 begin
 ML {*
+  open Printer;
   show_question_marks_default := false;
   *}
 (*>*)
@@ -10,10 +11,10 @@
 section {* Introduction *}
 
 text {*
-  Many realtime systems need to support processes with priorities and
+  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 hard deadlines.
+  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
@@ -31,7 +32,7 @@
   \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, realtime systems
+  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
@@ -46,18 +47,39 @@
   it was rectified by enabling the Priority Inheritance Protocol in
   the scheduling software.
 
-  The idea behind the \emph{Priority Inheritance Protocol} (PIP) 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$. This solution to the Priority
-  Inversion problem has been known since \cite{Lampson:Redell:cacm:1980}
-  but Lui et al give the first thorough analysis and present a correctness
-  proof for an algorithm \cite{journals/tc/ShaRL90}.
+  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 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.
+
+  However there has also been strong criticism against PIP
+
+  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
+  .\footnote{Sha et al.~call it the
+  \emph{Basic Priority Inheritance Protocol}.}
 
   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?
   
   \noindent
   Priority inversion referrers to the phenomena where tasks with higher 
@@ -109,6 +131,12 @@
   which can be used for guidelines of implementation. Section \ref{related} discusses 
   related works. Section \ref{conclusion} concludes the whole paper.
 
+  The basic priority inheritance protocol has two problems:
+
+  It does not prevent a deadlock from happening in a program with circular lock dependencies.
+  
+  A chain of blocking may be formed; blocking duration can be substantial, though bounded.
+
 
   Contributions