
diff -r eb2fc3ac934d -r a40a35d1bc91 prio/Paper/Paper.thy
--- a/prio/Paper/Paper.thy	Mon Apr 16 12:54:08 2012 +0000
+++ b/prio/Paper/Paper.thy	Mon Apr 16 15:08:24 2012 +0000
@@ -53,8 +53,8 @@
   can interact in subtle ways leading to a problem, called
   \emph{Priority Inversion}. Suppose three threads having priorities
   $H$(igh), $M$(edium) and $L$(ow). We would expect that the thread
-  $H$ blocks any other thread with lower priority and itself cannot
-  be blocked by any thread with lower priority. Alas, in a naive
+  $H$ blocks any other thread with lower priority and the thread itself cannot
+  be blocked indefinitely by any thread with lower priority. Alas, in a naive
   implementation of resource locking and priorities this property can
   be violated. Even worse, $H$ can be delayed indefinitely by
   threads with lower priorities. For this let $L$ be in the
@@ -168,15 +168,15 @@
   checking techniques. This paper presents a formalised and
   mechanically checked proof for the correctness of PIP (to our
   knowledge the first one). 
-  %; the earlier informal proof by Sha et
-  %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
   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---a fact
-  that has not been mentioned in the literature.
+  that has not been mentioned in the literature. This is important
+  for an efficient implementation, because we can give the lock to the
+  thread with the highest priority so that it terminates more quickly.
 *}
 
 section {* Formal Model of the Priority Inheritance Protocol *}
@@ -184,10 +184,12 @@
 text {*
   The Priority Inheritance Protocol, short PIP, is a scheduling
   algorithm for a single-processor system.\footnote{We shall come back
-  later to the case of PIP on multi-processor systems.} Our model of
-  PIP is based on Paulson's inductive approach to protocol
-  verification \cite{Paulson98}, where the \emph{state} of a system is
-  given by a list of events that happened so far.  \emph{Events} of PIP fall
+  later to the case of PIP on multi-processor systems.} 
+  Following good experience in earlier work \cite{Wang09},  
+  our model of PIP is based on Paulson's inductive approach to protocol
+  verification \cite{Paulson98}. In this approach a \emph{state} of a system is
+  given by a list of events that happened so far (with new events prepended to the list). 
+  \emph{Events} of PIP fall
   into five categories defined as the datatype:
 
   \begin{isabelle}\ \ \ \ \ %%%
@@ -369,7 +371,12 @@
   in turn needs to wait for @{text "th\<^isub>0"} to finish). If there is a circle of dependencies 
   in a RAG, then clearly
   we have a deadlock. Therefore when a thread requests a resource,
-  we must ensure that the resulting RAG is not circular. 
+  we must ensure that the resulting RAG is not circular. In practice, the 
+  programmer has to ensure this.
+
+
+  {\bf define detached}
+
 
   Next we introduce the notion of the \emph{current precedence} of a thread @{text th} in a 
   state @{text s}. It is defined as
@@ -380,7 +387,7 @@
 
   \noindent
   where the dependants of @{text th} are given by the waiting queue function.
-  While the precedence @{term prec} of a thread is determined by the programmer 
+  While the precedence @{term prec} of a thread is determined statically 
   (for example when the thread is
   created), the point of the current precedence is to let the scheduler increase this
   precedence, if needed according to PIP. Therefore the current precedence of @{text th} is
@@ -567,14 +574,15 @@
   \noindent
   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
-  the responsibility of the programmer.  In our formal
+  not lead to a cycle in the RAG. In practice, ensuring the latter
+  is 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 \emph{occurs check} in Prolog: In order to say
   anything meaningful about unification, one needs to perform an occurs
   check. But in practice the occurs check is omitted and the
   responsibility for avoiding problems rests with the programmer.}
+
  
   \begin{center}
   @{thm[mode=Rule] thread_P[where thread=th]}
@@ -638,7 +646,8 @@
 
   Even when fixed, their proof idea does not seem to go through for
   us, because of the way we have set up our formal model of PIP.  One
-  reason is that we allow critical sections to intersect
+  reason is that we allow critical sections, which start with a @{text P}-event
+  and finish with a corresponding @{text V}-event, to arbitrarily overlap
   (something Sha et al.~explicitly exclude).  Therefore we have
   designed a different correctness criterion for PIP. The idea behind
   our criterion is as follows: for all states @{text s}, we know the
@@ -658,9 +667,8 @@
 
   \begin{quote}
   {\bf Assumptions on the states {\boldmath@{text s}} and 
-  {\boldmath@{text "s' @ s"}:}} In order to make 
-  any meaningful statement, we need to require that @{text "s"} and 
-  @{text "s' @ s"} are valid states, namely
+  {\boldmath@{text "s' @ s"}:}} We need to require that @{text "s"} and 
+  @{text "s' @ s"} are valid states:
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{l}
   @{term "vt s"}\\
@@ -960,10 +968,8 @@
 section {* Properties for an Implementation\label{implement} *}
 
 text {*
-  While a formal correctness proof for our model of PIP is certainly
-  attractive (especially in light of the flawed proof by Sha et
-  al.~\cite{Sha90}), we found that the formalisation can even help us
-  with efficiently implementing PIP.
+  While our formalised proof gives us confidence about the correctness of our model of PIP, 
+  we found that the formalisation can even help us with efficiently implementing it.
 
   For example Baker complained that calculating the current precedence
   in PIP is quite ``heavy weight'' in Linux (see the Introduction).
@@ -1068,36 +1074,42 @@
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
   @{thm[mode=IfThen] eq_dep}, and\\
-  @{thm[mode=IfThen] eq_cp}
+  @{thm[mode=IfThen] eq_cp_pre}
   \end{tabular}
   \end{isabelle}
 
   \noindent
-  The first property is again telling us we do not need to change the @{text RAG}. The second
-  however states that only threads that are \emph{not} dependants of @{text th} have their
-  current precedence unchanged. For the others we have to recalculate the current
-  precedence. To do this we can start from @{term "th"} 
-  and follow the @{term "depend"}-edges to recompute  using Lemma~\ref{childrenlem} 
-  the @{term "cp"} of every 
-  thread encountered on the way. Since the @{term "depend"}
-  is assumed to be loop free, this procedure will always stop. The following two lemmas show, however, 
-  that this procedure can actually stop often earlier without having to consider all
-  dependants.
+  The first property is again telling us we do not need to change the @{text RAG}. 
+  The second shows that the @{term cp}-values of all threads other than @{text th} 
+  are unchanged. The reason is that @{text th} is running; therefore it is not in 
+  the @{term dependants} relation of any thread. This in turn means that the 
+  change of its priority cannot affect the threads.
 
-  \begin{isabelle}\ \ \ \ \ %%%
-  \begin{tabular}{@ {}l}
-  @{thm[mode=IfThen] eq_up_self}\\
-  @{text "If"} @{thm (prem 1) eq_up}, @{thm (prem 2) eq_up} and @{thm (prem 3) eq_up}\\
-  @{text "then"} @{thm (concl) eq_up}.
-  \end{tabular}
-  \end{isabelle}
-
-  \noindent
-  The first lemma states that if the current precedence of @{text th} is unchanged,
-  then the procedure can stop immediately (all dependent threads have their @{term cp}-value unchanged).
-  The second states that if an intermediate @{term cp}-value does not change, then
-  the procedure can also stop, because none of its dependent threads will
-  have their current precedence changed.
+  %The second
+  %however states that only threads that are \emph{not} dependants of @{text th} have their
+  %current precedence unchanged. For the others we have to recalculate the current
+  %precedence. To do this we can start from @{term "th"} 
+  %and follow the @{term "depend"}-edges to recompute  using Lemma~\ref{childrenlem} 
+  %the @{term "cp"} of every 
+  %thread encountered on the way. Since the @{term "depend"}
+  %is assumed to be loop free, this procedure will always stop. The following two lemmas show, however, 
+  %that this procedure can actually stop often earlier without having to consider all
+  %dependants.
+  %
+  %\begin{isabelle}\ \ \ \ \ %%%
+  %\begin{tabular}{@ {}l}
+  %@{thm[mode=IfThen] eq_up_self}\\
+  %@{text "If"} @{thm (prem 1) eq_up}, @{thm (prem 2) eq_up} and @{thm (prem 3) eq_up}\\
+  %@{text "then"} @{thm (concl) eq_up}.
+  %\end{tabular}
+  %\end{isabelle}
+  %
+  %\noindent
+  %The first lemma states that if the current precedence of @{text th} is unchanged,
+  %then the procedure can stop immediately (all dependent threads have their @{term cp}-value unchanged).
+  %The second states that if an intermediate @{term cp}-value does not change, then
+  %the procedure can also stop, because none of its dependent threads will
+  %have their current precedence changed.
   \smallskip
   *}
 (*<*)
@@ -1153,7 +1165,7 @@
   \noindent
   \colorbox{mygrey}{@{term "P th cs"}:} We assume that @{text s'} and 
   @{term "s \<equiv> P th cs#s'"} are both valid. We again have to analyse two subcases, namely
-  the one where @{text cs} is locked, and where it is not. We treat the second case
+  the one where @{text cs} is not locked, and one where it is. We treat the former case
   first by showing that
   
   \begin{isabelle}\ \ \ \ \ %%%
@@ -1210,13 +1222,11 @@
   that a mechanically checked proof avoids the flaws that crept into their
   informal reasoning. We achieved this goal: 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/HOL. We can also confirm that Paulson's
+  sometimes quite intricate and tedious, has been checked by Isabelle/HOL. 
+  We can also confirm that Paulson's
   inductive method for 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}.
+  area of this method is security protocols. 
 
   The second goal of our formalisation is to provide a specification for actually
   implementing PIP. Textbooks, for example \cite[Section 5.6.5]{Vahalia96},
@@ -1237,6 +1247,8 @@
   provide this kind of ``deep understanding'' about the principles behind 
   PIP and its correctness.
 
+  {\bf rewrite the following slightly}
+
   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 any relevance in such a world beyond
@@ -1260,11 +1272,12 @@
   area, not even informal or flawed ones.
 
   The most closely related work to ours is the formal verification in
-  PVS of the Priority Ceiling Protocol done by Dutertre 
-  \cite{dutertre99b}---another solution to the Priority Inversion 
-  problem, which however needs
-  static analysis of programs in order to avoid it.
-  His formalisation consists of 407 lemmas and 2500 lines of (PVS) code.  Our formalisation
+  PVS of the Priority Ceiling Protocol done by Dutertre
+  \cite{dutertre99b}---another solution to the Priority Inversion
+  problem, which however needs static analysis of programs in order to
+  avoid it. {\bf mention model-checking approaches}
+
+  Our formalisation
   consists of around 210 lemmas and overall 6950 lines of readable Isabelle/Isar
   code with a few apply-scripts interspersed. The formal model of PIP
   is 385 lines long; the formal correctness proof 3800 lines. Some auxiliary
@@ -1273,6 +1286,13 @@
   can be downloaded from
   \url{http://www.inf.kcl.ac.uk/staff/urbanc/pip.html}.
 
+  {\bf say:
+  So this paper is a good witness for one
+of the major reasons to be interested in machine checked reasoning:
+gaining deeper understanding of the subject matter.
+  }
+
+
   \bibliographystyle{plain}
   \bibliography{root}
 *}




