
diff -r 3d154253d5fe -r ccb6c0601614 prio/Paper/Paper.thy
--- a/prio/Paper/Paper.thy	Mon Feb 13 15:42:45 2012 +0000
+++ b/prio/Paper/Paper.thy	Mon Feb 13 19:33:03 2012 +0000
@@ -158,7 +158,7 @@
   al.~\cite{Sha90} is flawed).  In contrast to model checking, our
   formalisation provides insight into why PIP is correct and allows us
   to prove stronger properties that, as we will show, can inform an
-  implementation.  For example, we found by ``playing'' with the formalisation
+  efficient implementation.  For example, we found by ``playing'' with the formalisation
   that the choice of the next thread to take over a lock when a
   resource is released is irrelevant for PIP being correct. Something
   which has not been mentioned in the relevant literature.
@@ -384,10 +384,12 @@
   \end{isabelle}
 
   \noindent
-  The first function is a waiting queue function (that is, it takes a resource @{text "cs"} and returns the
-  corresponding list of threads that wait for it), the second is a function that takes
-  a thread and returns its current precedence (see \eqref{cpreced}). We assume the usual getter and 
-  setter methods for such records.
+  The first function is a waiting queue function (that is, it takes a
+  resource @{text "cs"} and returns the corresponding list of threads
+  that lock, respectively wait for, it); the second is a function that
+  takes a thread and returns its current precedence (see
+  \eqref{cpreced}). We assume the usual getter and setter methods for
+  such records.
 
   In the initial state, the scheduler starts with all resources unlocked (the corresponding 
   function is defined in \eqref{allunlocked}) and the
@@ -428,7 +430,7 @@
   More interesting are the cases where a resource, say @{text cs}, is locked or released. In these cases
   we need to calculate a new waiting queue function. For the event @{term "P th cs"}, we have to update
   the function so that the new thread list for @{text cs} is the old thread list plus the thread @{text th} 
-  appended to the end of that list (remember the head of this list is seen to be in the possession of this
+  appended to the end of that list (remember the head of this list is assigned to be in the possession of this
   resource). This gives the clause
 
   \begin{isabelle}\ \ \ \ \ %%%
@@ -512,7 +514,7 @@
   @{term threads} is empty and therefore there is neither a thread ready nor running.
   If there is one or more threads ready, then there can only be \emph{one} thread
   running, namely the one whose current precedence is equal to the maximum of all ready 
-  threads. We use the set-comprehension to capture both possibilities.
+  threads. We use sets to capture both possibilities.
   We can now also conveniently define the set of resources that are locked by a thread in a
   given state.
 
@@ -537,7 +539,7 @@
   The first rule states that a thread can only be created, if it does not yet exists.
   Similarly, the second rule states that a thread can only be terminated if it was
   running and does not lock any resources anymore (this simplifies slightly our model;
-  in practice we would expect the operating system releases all held lock of a
+  in practice we would expect the operating system releases all locks held by a
   thread that is about to exit). The event @{text Set} can happen
   if the corresponding thread is running. 
 
@@ -549,8 +551,8 @@
   If a thread wants to lock a resource, then the thread needs to be
   running and also we have to make sure that the resource lock does
   not lead to a cycle in the RAG. In practice, ensuring the latter is
-  of course the responsibility of the programmer.  In our formal
-  model we just exclude such problematic cases in order to be able to make
+  the responsibility of the programmer.  In our formal
+  model we brush aside these problematic cases in order to be able to make
   some meaningful statements about PIP.\footnote{This situation is
   similar to the infamous occurs check in Prolog: In order to say
   anything meaningful about unification, one needs to perform an occurs
@@ -886,7 +888,7 @@
 (*>*)
 
 
-section {* Properties for an Implementation\label{implement}*}
+section {* Properties for an Implementation\label{implement} *}
 
 text {*
   While a formal correctness proof for our model of PIP is certainly
@@ -1125,50 +1127,48 @@
 section {* Conclusion *}
 
 text {* 
-  The Priority Inheritance Protocol is a classic textbook algorithm
-  used in real-time systems in order to avoid the problem of Priority
-  Inversion.
+  The Priority Inheritance Protocol (PIP) is a classic textbook
+  algorithm used in real-time systems in order to avoid the problem of
+  Priority Inversion.  While classic and widely used, PIP does have its faults: for
+  example it does not prevent deadlocks where threads have circular
+  lock dependencies.
 
-  A clear and simple understanding of the problem at hand is both a
-  prerequisite and a byproduct of such an effort, because everything
-  has finally be reduced to the very first principle to be checked
-  mechanically.
+  We had two aims in mind with our formalisation
+  of PIP: One is to understand the relevant literature and to make the
+  notions in its correctness proof precise so that they can be
+  processed by a theorem prover, because a mechanically checked proof
+  avoids the flaws that crept into the informal reasoning by Sha et
+  al.~\cite{Sha90}. We achieved this aim: The correctness of PIP now
+  hinges only on the assumptions behind our formal model, which can
+  now be debated and potentially be modified. The reasoning, which is
+  sometimes quite intricate and tedious, has been checked beyond any
+  reasonable doubt by Isabelle. We can confirm that Paulson's
+  inductive approach to protocol verification \cite{Paulson98} is
+  quite suitable for our formal model and proof. The traditianal
+  application area of this approach are security protocols.
+  The only other application of Paulson's approach outside this area we know of 
+  is \cite{Wang09}.
 
-  Our formalisation and the one presented
-  in \cite{Wang09} are the only ones that employ Paulson's method for
-  verifying protocols which are \emph{not} security related. 
+  The second aim is to provide a specification for PIP so that it can
+  actually be implemented. Textbooks, like \cite[Section
+  5.6.5]{Vahalia96}, explain how to use various implementations of PIP
+  and abstractly discuss its properties, but surprisinly lack many
+  details for an implementor.  That this is an issue in practice is
+  illustrated by the email from Baker we cited in the
+  Introduction. The formalisation gives the first author enough data
+  to enable his undergraduate students to implement PIP on top of
+  PINTOS, an small operating system for teaching purposes.  Given the
+  results in Section~\ref{implement}, we also succeeded with this
+  aim. A byproduct of our formalisation effort is that nearly all
+  design choices for the PIP scheduler are backed up with a proved
+  lemma.
 
-  TO DO 
+
+
+ 
 
   no clue about multi-processor case according to \cite{Steinberg10} 
 
-*}
-
-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 in \cite{Sha90}. PCE is
-  less convenient to use because it requires static analysis of
-  programs. Therefore, PI is more commonly used in
-  practice\cite{locke-july02}. However, as pointed out in the
-  literature, the analysis of priority inheritance protocol is quite
-  subtle\cite{yodaiken-july02}.  A formal analysis will certainly be
-  helpful for us to understand and correctly implement PI. All
-  existing formal analysis of PI
-  \cite{Jahier09,Wellings07,Faria08} are based on the
-  model checking technology. Because of the state explosion problem,
-  model check is much like an exhaustive testing of finite models with
-  limited size.  The results obtained can not be safely generalized to
-  models with arbitrarily large size. Worse still, since model
-  checking is fully automatic, it give little insight on why the
-  formal model is correct. It is therefore definitely desirable to
-  analyze PI using theorem proving, which gives more general results
-  as well as deeper insight. And this is the purpose of this paper
-  which gives a formal analysis of PI in the interactive theorem
-  prover Isabelle using Higher Order Logic (HOL). The formalization
-  focuses on on two issues:
 
   \begin{enumerate}
   \item The correctness of the protocol model itself. A series of desirable properties is 
@@ -1182,21 +1182,8 @@
     of which can be used as guidelines on how PI can be implemented efficiently and correctly. 
   \end{enumerate} 
 
-  The rest of the paper is organized as follows: Section \ref{overview} gives an overview 
-  of PI. Section \ref{model} introduces the formal model of PI. Section \ref{general} 
-  discusses a series of basic properties of PI. Section \ref{extension} shows formally 
-  how priority inversion is controlled by PI. Section \ref{implement} gives properties 
-  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
+ 
+   Contributions
 
   Despite the wide use of Priority Inheritance Protocol in real time operating
   system, it's correctness has never been formally proved and mechanically checked. 




