--- 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"})