# HG changeset patch
# User urbanc
# Date 1328097637 0
# Node ID 039711ba6cf9152eca9ac375daf4e35299abf61f
# Parent  ee4611c1e13cf0fb3f0aa4cfe950751bd6d0e3f0
slightly more on text

diff -r ee4611c1e13c -r 039711ba6cf9 prio/Paper/Paper.thy
--- 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
 
diff -r ee4611c1e13c -r 039711ba6cf9 prio/Paper/document/root.tex
--- 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}
diff -r ee4611c1e13c -r 039711ba6cf9 prio/paper.pdf
Binary file prio/paper.pdf has changed