--- a/prio/Paper/Paper.thy	Mon Feb 13 19:33:03 2012 +0000
+++ b/prio/Paper/Paper.thy	Mon Feb 13 20:57:02 2012 +0000
@@ -1128,74 +1128,74 @@
 
 text {* 
   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.
+  algorithm used in real-time operating systems in order to avoid the problem of
+  Priority Inversion.  Although classic and widely used, PIP does have
+  its faults: for example it does not prevent deadlocks where threads
+  have circular lock dependencies.
 
-  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
+  We had two aims in mind with our formalisation of PIP: One is to
+  make the notions in the correctness proof by Sha et al.~\cite{Sha90}
+  precise so that they can be processed by a theorem prover, because a
+  mechanically checked proof avoids the flaws that crept into their
+  informal reasoning. We achieved this aim: The correctness of PIP now
+  only hinges on the assumptions behind our formal model. 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}.
+  reasonable doubt by Isabelle/HOL. We can also confirm that Paulson's
+  inductive method to protocol verification~\cite{Paulson98} is quite
+  suitable for our formal model and proof. The traditional application
+  area of this method is security protocols.  The only other
+  application of Paulson's method we know of outside this area is
+  \cite{Wang09}.
 
-  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
+  The second aim is to provide a specification for actually
+  implementing PIP. Textbooks, like \cite[Section 5.6.5]{Vahalia96},
+  explain how to use various implementations of PIP and abstractly
+  discuss its properties, but surprisingly lack most details for a
+  programmer.  That this is an issue in practice is illustrated by the
+  email from Baker we cited in the Introduction. We achieved also this
+  aim: The formalisation gives the first author enough data to enable
+  his undergraduate students to implement as part of their OS course
+  PIP on top of PINTOS, a small operating system for teaching
+  purposes. A byproduct of our formalisation effort is that nearly all
   design choices for the PIP scheduler are backed up with a proved
-  lemma.
+  lemma. We were also able to prove the property that the choice of
+  the next thread taking over a lock is irrelevant for the correctness
+  of PIP. Earlier model checking techniques
+  \cite{Faria08,Jahier09,Wellings07} were not able to provided this
+  kind of ``deep understanding'' into PIP.
+
+  PIP is a scheduling algorithm for single-processor systems. We are
+  now living in a multi-processor world. So the question naturally arises 
+  whether PIP has nowadays any relevance beyond teaching. 
+  
+   The work in this paper only deals with single CPU configurations. The
+  "one CPU" assumption is essential for our formalisation, because the
+  main lemma fails in multi-CPU configuration. The lemma says that any
+  runing thead must be the one with the highest prioirty or already held
+  some resource when the highest priority thread was initiated. When
+  there are multiple CPUs, it may well be the case that a threads did
+  not hold any resource when the highest priority thread was initiated,
+  but that thread still runs after that moment on a separate CPU. In
+  this way, the main lemma does not hold anymore.
 
 
-
- 
+  There are some works deals with priority inversion in multi-CPU
+  configurations[???], but none of them have given a formal correctness
+  proof. The extension of our formal proof to deal with multi-CPU
+  configurations is not obvious. One possibility, as suggested in paper
+  [???], is change our formal model (the defiintion of "schs") to give
+  the released resource to the thread with the highest prioirty. In this
+  way, indefinite prioirty inversion can be avoided, but for a quite
+  different reason from the one formalized in this paper (because the
+  "mail lemma" will be different). This means a formal correctness proof
+  for milt-CPU configuration would be quite different from the one given
+  in this paper. The solution of prioirty inversion problem in mult-CPU
+  configurations is a different problem which needs different solutions
+  which is outside the scope of this paper.
 
   no clue about multi-processor case according to \cite{Steinberg10} 
 
-
-  \begin{enumerate}
-  \item The correctness of the protocol model itself. A series of desirable properties is 
-    derived until we are fully convinced that the formal model of PI does 
-    eliminate priority inversion. And a better understanding of PI is so obtained 
-    in due course. For example, we find through formalization that the choice of 
-    next thread to take hold when a 
-    resource is released is irrelevant for the very basic property of PI to hold. 
-    A point never mentioned in literature. 
-  \item The correctness of the implementation. A series of properties is derived the meaning 
-    of which can be used as guidelines on how PI can be implemented efficiently and correctly. 
-  \end{enumerate} 
-
  
-   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. 
-  All existing verification are based on model checking technology. Full automatic
-  verification gives little help to understand why the protocol is correct. 
-  And results such obtained only apply to models of limited size. 
-  This paper presents a formal verification based on theorem proving. 
-  Machine checked formal proof does help to get deeper understanding. We found 
-  the fact which is not mentioned in the literature, that the choice of next 
-  thread to take over when an critical resource is release does not affect the correctness
-  of the protocol. The paper also shows how formal proof can help to construct 
-  correct and efficient implementation.\bigskip 
 
 *}
 
@@ -1248,13 +1248,6 @@
   Priority Inheritance is just such a byproduct. 
   *}
 
-(*
-section {* Formal model of Priority Inheritance \label{model} *}
-text {*
-  \input{../../generated/PrioGDef}
-*}
-*)
-
 section {* General properties of Priority Inheritance \label{general} *}
 
 text {*
@@ -1426,30 +1419,7 @@
 section {* Conclusions \label{conclusion} *}
 
 text {*
-  The work in this paper only deals with single CPU configurations. The
-  "one CPU" assumption is essential for our formalisation, because the
-  main lemma fails in multi-CPU configuration. The lemma says that any
-  runing thead must be the one with the highest prioirty or already held
-  some resource when the highest priority thread was initiated. When
-  there are multiple CPUs, it may well be the case that a threads did
-  not hold any resource when the highest priority thread was initiated,
-  but that thread still runs after that moment on a separate CPU. In
-  this way, the main lemma does not hold anymore.
-
-
-  There are some works deals with priority inversion in multi-CPU
-  configurations[???], but none of them have given a formal correctness
-  proof. The extension of our formal proof to deal with multi-CPU
-  configurations is not obvious. One possibility, as suggested in paper
-  [???], is change our formal model (the defiintion of "schs") to give
-  the released resource to the thread with the highest prioirty. In this
-  way, indefinite prioirty inversion can be avoided, but for a quite
-  different reason from the one formalized in this paper (because the
-  "mail lemma" will be different). This means a formal correctness proof
-  for milt-CPU configuration would be quite different from the one given
-  in this paper. The solution of prioirty inversion problem in mult-CPU
-  configurations is a different problem which needs different solutions
-  which is outside the scope of this paper.
+ 
 
 *}
 

Binary file prio/paper.pdf has changed