--- a/prio/Paper/Paper.thy	Sat Feb 04 00:14:41 2012 +0000
+++ b/prio/Paper/Paper.thy	Sat Feb 04 22:56:14 2012 +0000
@@ -46,12 +46,13 @@
   priority task locking a resource prevented a high priority process
   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} in the scheduling software.
+  (PIP) \cite{Sha90}\footnote{Sha et al.~call it the
+  \emph{Basic Priority Inheritance Protocol}.} 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
   section by unlocking the resource. This solves the problem of $H$
-  having to wait indefinitely, because $L$ cannot, for example, be
+  having to wait indefinitely, because $L$ cannot be
   blocked by processes having priority $M$. While a few other
   solutions exist for the Priority Inversion problem, PIP is one that is widely deployed
   and implemented. This includes VxWorks (a proprietary real-time OS
@@ -107,9 +108,9 @@
   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 by
-  Sha et al. They specify in \cite{Sha90} that after the process whose
-  priority has been raised completes its critical section and releases
+  \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
@@ -117,35 +118,32 @@
   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'$. The correct 
-  behaviour for $L$
-  is to revert to the highest remaining priority of processes which it
-  blocks. The advantage of a formalisation of PIP in a theorem prover 
-  is that such issues clearly show up and cannot be overlooked as in
-  informal reasoning.
+  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).
 
   There have been earlier formal investigations into PIP, but ...\cite{Faria08}
+*}
 
-  \bigskip
-  Priority Inversion problem has been known since 1980
-  \cite{Lampson80}, 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}.}
+section {* Preliminaries *}
 
-   POSIX.4: programming for the real world (Google eBook)
+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
 
-  However, there are further subtleties: just lowering the priority 
-  of the process $L$ to its low priority, as proposed in ???, is 
-  incorrect.\bigskip
-
-  
+  To define events, the identifiers of {\em threads},
+  {\em priority} and {\em critical resources } (abbreviated as @{text "cs"}) 
+  need to be represented. All three are represetned using standard 
+  Isabelle/HOL type @{typ "nat"}:
+*}
 
-  very little on implementations, not to mention implementations informed by 
-  formal correctness proofs.
-
-  
-
+text {*
+  \bigskip
   The priority inversion phenomenon was first published in \cite{Lampson80}. 
   The two protocols widely used to eliminate priority inversion, namely 
   PI (Priority Inheritance) and PCE (Priority Ceiling Emulation), were proposed