--- 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
 

--- a/prio/Paper/document/root.tex	Wed Feb 01 08:16:00 2012 +0000
+++ b/prio/Paper/document/root.tex	Wed Feb 01 12:00:37 2012 +0000
@@ -45,7 +45,7 @@
 \maketitle
 
 \begin{abstract}
-In realtime systems with support for resource locking and for
+In real-time systems with support for resource locking and for
 processes with priorities, one faces the problem of priority
 inversion. This problem can make the behaviour of processes
 unpredictable and the resulting bugs can be hard to find.  The
@@ -63,7 +63,7 @@
 Paulson's inductive approach to verifying protocols.\medskip
 
 {\bf Keywords:} Priority Inheritance Protocol, formal connectness proof, 
-realtime systems
+real-time systems
 \end{abstract}
 
 \input{session}

Binary file prio/paper.pdf has changed