# HG changeset patch
# User urbanc
# Date 1327913156 0
# Node ID 1baf8d0c709393c0ab0e59de6f6f1d178590f77a
# Parent  83fb18cadd2bc44ef892bea658f8dcfb31861b38
more text

diff -r 83fb18cadd2b -r 1baf8d0c7093 prio/Paper/Paper.thy
--- a/prio/Paper/Paper.thy	Mon Jan 30 06:46:47 2012 +0000
+++ b/prio/Paper/Paper.thy	Mon Jan 30 08:45:56 2012 +0000
@@ -14,8 +14,8 @@
   locking of resources. Locking of resources ensures mutual exclusion
   when accessing shared data or devices. Priorities allow schedulling
   of processes that need to finish their work within hard deadlines.
-  Unfortunately, both features can interact in subtle ways leading to a
-  problem, called \emph{Priority Inversion}. Suppose three processes
+  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,
@@ -23,29 +23,37 @@
   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 be in turn 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.
+  must therefore wait for $L$ to release this lock. The problem is
+  that $L$ might be in turn 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 to support concurrent programming.
 
   If the problem of Priority Inversion is ignored, realtime 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.  Once the spacecraft
-  landed, the software 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 was
-  fortunately not lost, because of a clever system design).  The
-  problem was that the schedulling software fell victim of Priority
-  Inversion: a low priority task locking a resource prevented a high
-  priority process from running.  Once found, the problem could be
-  rectified by enabling the Priority Inheritance Protocol in the
-  schedulling software.
+  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
+  normal operation of the craft could only resume the next day (the
+  mission and data already collected was fortunately not lost, because
+  of a clever system design).  The reason for the shutdowns was that
+  the schedulling software fell victim of Priority Inversion: a low
+  priority task locking a resource prevented a high priority process
+  from running leading to a system reset. Once the problem was found,
+  it was rectified by enabling the Priority Inheritance Protocol in
+  the schedulling software.
 
   The idea behind the \emph{Priority Inheritance Protocol} (PIP) is to
-  temporarily inherit the low priority process the higher priority
-  until it released the locked resource.
+  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 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 thourough analysis and present a correctness
+  proof for an algorithm \cite{journals/tc/ShaRL90}.
 
   However, there are further subtleties: just lowering the priority 
   of the process $L$ to its low priority, as proposed in ???, is 
diff -r 83fb18cadd2b -r 1baf8d0c7093 prio/Paper/document/root.tex
--- a/prio/Paper/document/root.tex	Mon Jan 30 06:46:47 2012 +0000
+++ b/prio/Paper/document/root.tex	Mon Jan 30 08:45:56 2012 +0000
@@ -3,8 +3,8 @@
 \usepackage{isabellesym}
 \usepackage{amsmath}
 \usepackage{amssymb}
-\usepackage{tikz}
-\usepackage{pgf}
+%\usepackage{tikz}
+%\usepackage{pgf}
 %\usetikzlibrary{arrows,automata,decorations,fit,calc}
 %\usetikzlibrary{shapes,shapes.arrows,snakes,positioning}
 %\usepgflibrary{shapes.misc} % LATEX and plain TEX and pure pgf
@@ -17,7 +17,7 @@
 \usepackage{stmaryrd}
 \usepackage{url}
 
-\titlerunning{Myhill-Nerode using Regular Expressions}
+\titlerunning{Proving the Priority Inheritance Protocol Correct}
 
 
 \urlstyle{rm}
@@ -45,23 +45,23 @@
 \maketitle
 
 \begin{abstract}
-In realtime systems with support for resource locking and processes
-involving priorities, one faces the problem of priority
+In realtime 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
 Priority Inheritance Protocol is one solution implemented in many
 systems for solving this problem, but the correctness of this solution
 has never been formally verified in a theorem prover. As already
-pointed out in the literature, the original description of the
-Property Inheritance Protocol presents an informal correctness
-``proof'' for an \emph{incorrect} algorithm. In this paper we fix the
-problem of the original proof by making all notions precise and
-implementing a variant of a solution proposed earlier. Our
-formalisation in Isabelle/HOL uncovered facts not mentioned in the
-literature, but also shows how to efficiently implement this
-protocol. Earlier correct implementations were criticised as too
-inefficient. Our formalisation is based on Paulson's inductive
-approach to verifying protocols.\medskip
+pointed out in the literature, the original informal investigation of
+the Property Inheritance Protocol presents a correctness ``proof'' for
+an \emph{incorrect} algorithm. In this paper we fix the problem of the
+original proof by making all notions precise and implementing a
+variant of a solution proposed earlier. Our formalisation in
+Isabelle/HOL uncovered facts not mentioned in the literature, but also
+shows how to efficiently implement this protocol. Earlier correct
+implementations were criticised as too inefficient. Our formalisation
+is based on Paulson's inductive approach to verifying
+protocols.\medskip
 
 {\bf Keywords:} Priority Inheritance Protocol, formal connectness proof, 
 realtime systems
diff -r 83fb18cadd2b -r 1baf8d0c7093 prio/document/root.tex
--- a/prio/document/root.tex	Mon Jan 30 06:46:47 2012 +0000
+++ b/prio/document/root.tex	Mon Jan 30 08:45:56 2012 +0000
@@ -16,7 +16,7 @@
 %%\usepackage{mathabx}
 \usepackage{stmaryrd}
 
-\titlerunning{Myhill-Nerode using Regular Expressions}
+\titlerunning{Proving the Priority Inheritance Protocol Correct}
 
 
 \urlstyle{rm}
diff -r 83fb18cadd2b -r 1baf8d0c7093 prio/paper.pdf
Binary file prio/paper.pdf has changed