--- a/prio/Paper/Paper.thy	Sun Feb 05 21:00:12 2012 +0000
+++ b/prio/Paper/Paper.thy	Mon Feb 06 12:08:35 2012 +0000
@@ -47,7 +47,7 @@
   from running in time leading to a system reset. Once the problem was found,
   it was rectified by enabling the \emph{Priority Inheritance Protocol} 
   (PIP) \cite{Sha90}\footnote{Sha et al.~call it the
-  \emph{Basic Priority Inheritance Protocol}.} in the scheduling software.
+  \emph{Basic Priority Inheritance Protocol} \cite{Sha90}.} in the scheduling software.
 
   The idea behind PIP is to let the process $L$ temporarily
   inherit the high priority from $H$ until $L$ leaves the critical
@@ -90,7 +90,7 @@
   and also a few high-level descriptions of implementations (e.g.~in
   the textbook \cite[Section 5.6.5]{Vahalia96}), but they help little
   with actual implementations. That this is a problem in practise is
-  proved by an email by Baker, who wrote on 13 July 2009 on the Linux
+  proved by an email from Baker, who wrote on 13 July 2009 on the Linux
   Kernel mailing list:
 
   \begin{quote}
@@ -107,34 +107,49 @@
   to inform an implementation) and makes PIP an ideal candidate for a
   formal verification. One reason, of course, is that the original
   presentation of PIP \cite{Sha90}, despite being informally
-  ``proved'' correct, is actually \emph{flawed}. Yodaiken
-  \cite{Yodaiken02} points to a subtlety that had been overlooked in
-  the informal proof by Sha et al. They specify in \cite{Sha90} that after the process (whose
-  priority has been raised) completes its critical section and releases
-  the lock, it ``returns to its original priority level.'' This leads
-  them to believe that an implementation of PIP is ``rather
-  straightforward'' \cite{Sha90}.  Unfortunately, as Yodaiken pointed
-  out, this behaviour is too simplistic.  Consider the case where the
-  low priority process $L$ locks \emph{two} resources, and two
-  high-priority processes $H$ and $H'$ each wait for one of
-  them.  If $L$ then releases one resource so that $H$, say, can
-  proceed, then we still have Priority Inversion with $H'$ (which waits for
-  the other resource). The correct behaviour for $L$
-  is to revert to the highest remaining priority of processes that it
-  blocks. The advantage of a formalisation of the correctness of PIP 
-  in a theorem prover is that such issues clearly show up and cannot
-  be overlooked as in informal reasoning (since we have to analyse all
-  \emph{traces} that could possibly happen).
+  ``proved'' correct, is actually \emph{flawed}. 
+
+  Yodaiken \cite{Yodaiken02} points to a subtlety that had been
+  overlooked in the informal proof by Sha et al. They specify in
+  \cite{Sha90} that after the process (whose priority has been raised)
+  completes its critical section and releases the lock, it ``returns
+  to its original priority level.'' This leads them to believe that an
+  implementation of PIP is ``rather straightforward'' \cite{Sha90}.
+  Unfortunately, as Yodaiken pointed out, this behaviour is too
+  simplistic.  Consider the case where the low priority process $L$
+  locks \emph{two} resources, and two high-priority processes $H$ and
+  $H'$ each wait for one of them.  If $L$ then releases one resource
+  so that $H$, say, can proceed, then we still have Priority Inversion
+  with $H'$ (which waits for the other resource). The correct
+  behaviour for $L$ is to revert to the highest remaining priority of
+  processes that it blocks. The advantage of a formalisation in a
+  theorem prover for the correctness of a high-level specification of
+  PIP is that such issues clearly show up and cannot be overlooked as
+  in informal reasoning (since we have to analyse all possible program
+  behaviours, i.e.~\emph{traces}, that could possibly happen).
 
   There have been earlier formal investigations into PIP, but ...\cite{Faria08}
 *}
 
-section {* Preliminaries *}
+section {* Formal Model of the Priority Inheritance Protocol *}
 
 text {*
   Our formal model of PIP is based on Paulson's inductive approach to protocol 
-  verification, where the state of the system is modelled as a list of events 
-  that happened so far. \emph{Events} will use
+  verification \cite{Paulson98}, where the state of the system is modelled as a list of events 
+  that happened so far. \emph{Events} fall into four categories defined as the datatype
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{7mm}}l}
+  \isacommand{datatype} event & @{text "="} & @{term "Create thread priority"}\\
+  & @{text "|"} & @{term "Exit thread"}\\
+  & @{text "|"} & @{term "P thread cs"} & {\rm Request of a resource} @{text "cs"} {\rm by} @{text "thread"}\\
+  & @{text "|"} & @{term "V thread cs"} & {\rm Release of a resource} @{text "cs"} {\rm by} @{text "thread"}
+  \end{tabular}
+  \end{isabelle}
+
+  \noindent
+  whereby threads, priorities and resources are represented as natural numbers.
+  A \emph{state} is a list of events.
 
   To define events, the identifiers of {\em threads},
   {\em priority} and {\em critical resources } (abbreviated as @{text "cs"}) 

--- a/prio/Paper/document/root.bib	Sun Feb 05 21:00:12 2012 +0000
+++ b/prio/Paper/document/root.bib	Mon Feb 06 12:08:35 2012 +0000
@@ -52,7 +52,15 @@
 }
 
 
-
+@Article{Paulson98,
+  author =       {L.~C.~Paulson},
+  title =        {{T}he {I}nductive {A}pproach to {V}erifying {C}ryptographic {P}rotocols},
+  journal =      {Journal of Computer Security},
+  year =         {1998},
+  volume =       {6},
+  number =       {1--2},
+  pages =        {85--128}
+}
 
 @MISC{locke-july02,
 author = {D. Locke},

--- a/prio/Paper/document/root.tex	Sun Feb 05 21:00:12 2012 +0000
+++ b/prio/Paper/document/root.tex	Mon Feb 06 12:08:35 2012 +0000
@@ -45,8 +45,8 @@
 
 \begin{abstract}
 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
+processes with priorities, one faces the problem of Priority
+IBnversion. 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

Binary file prio/paper.pdf has changed