
diff -r 630754a81bdb -r 6a4249608ad0 prio/Paper/Paper.thy
--- a/prio/Paper/Paper.thy	Mon Feb 13 22:45:06 2012 +0000
+++ b/prio/Paper/Paper.thy	Mon Feb 13 23:31:40 2012 +0000
@@ -897,12 +897,12 @@
   with efficiently implementing PIP.
 
   For example Baker complained that calculating the current precedence
-  in PIP is quite ``heavy weight'' in Linux (see our Introduction).
+  in PIP is quite ``heavy weight'' in Linux (see the Introduction).
   In our model of PIP the current precedence of a thread in a state s
   depends on all its dependants---a ``global'' transitive notion,
   which is indeed heavy weight (see Def.~shown in \eqref{cpreced}).
-  We can however prove how to improve upon this. For this let us
-  define the notion of @{term children} of a thread as
+  We can however improve upon this. For this let us define the notion
+  of @{term children} of a thread @{text th} in a state @{text s} as
 
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
@@ -911,8 +911,9 @@
   \end{isabelle}
 
   \noindent
-  where a child is a thread that is one ``hop'' away in the @{term RAG} from the 
-  tread @{text th} (and waiting for @{text th} to release a resource). We can prove that
+  where a child is a thread that is one ``hop'' away from the tread
+  @{text th} in the @{term RAG} (and waiting for @{text th} to release
+  a resource). We can prove that
 
   \begin{lemma}\label{childrenlem}
   @{text "If"} @{thm (prem 1) cp_rec} @{text "then"}
@@ -925,17 +926,16 @@
   That means the current precedence of a thread @{text th} can be
   computed locally by considering only the children of @{text th}. In
   effect, it only needs to be recomputed for @{text th} when one of
-  its children change their current precedence.  Once the current 
+  its children changes its current precedence.  Once the current 
   precedence is computed in this more efficient manner, the selection
   of the thread with highest precedence from a set of ready threads is
   a standard scheduling operation implemented in most operating
   systems.
 
-  Of course the main implementation work for PIP involves the scheduler
-  and coding how it should react to the events, for example which 
-  datastructures need to be modified (mainly @{text RAG} and @{text cprec}).
-  Below we outline how our formalisation guides this implementation for each 
-  event.\smallskip
+  Of course the main implementation work for PIP involves the
+  scheduler and coding how it should react to events.  Below we
+  outline how our formalisation guides this implementation for each
+  kind of event.\smallskip
 *}
 
 (*<*)
@@ -944,14 +944,14 @@
 (*>*)
 text {*
   \noindent
-  @{term "Create th prio"}: We assume that the current state @{text s'} and 
+  \colorbox{mygrey}{@{term "Create th prio"}:} We assume that the current state @{text s'} and 
   the next state @{term "s \<equiv> Create th prio#s'"} are both valid (meaning the event
   is allowed to occur). In this situation we can show that
 
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
-  @{thm eq_dep}\\
-  @{thm eq_cp_th}\\
+  @{thm eq_dep},\\
+  @{thm eq_cp_th}, and\\
   @{thm[mode=IfThen] eq_cp}
   \end{tabular}
   \end{isabelle}
@@ -959,7 +959,7 @@
   \noindent
   This means we do not have recalculate the @{text RAG} and also none of the
   current precedences of the other threads. The current precedence of the created
-  thread is just its precedence, that is the pair @{term "(prio, length (s::event list))"}.
+  thread @{text th} is just its precedence, namely the pair @{term "(prio, length (s::event list))"}.
   \smallskip
   *}
 (*<*)
@@ -969,19 +969,19 @@
 (*>*)
 text {*
   \noindent
-  @{term "Exit th"}: We again assume that the current state @{text s'} and 
+  \colorbox{mygrey}{@{term "Exit th"}:} We again assume that the current state @{text s'} and 
   the next state @{term "s \<equiv> Exit th#s'"} are both valid. We can show that
 
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
-  @{thm eq_dep}\\
+  @{thm eq_dep}, and\\
   @{thm[mode=IfThen] eq_cp}
   \end{tabular}
   \end{isabelle}
 
   \noindent
-  This means also we do not have to recalculate the @{text RAG} and
-  not the current precedences for the other threads. Since @{term th} is not
+  This means again we do not have to recalculate the @{text RAG} and
+  also not the current precedences for the other threads. Since @{term th} is not
   alive anymore in state @{term "s"}, there is no need to calculate its
   current precedence.
   \smallskip
@@ -993,25 +993,26 @@
 (*>*)
 text {*
   \noindent
-  @{term "Set th prio"}: We assume that @{text s'} and 
+  \colorbox{mygrey}{@{term "Set th prio"}:} We assume that @{text s'} and 
   @{term "s \<equiv> Set th prio#s'"} are both valid. We can show that
 
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
-  @{thm[mode=IfThen] eq_dep}\\
+  @{thm[mode=IfThen] eq_dep}, and\\
   @{thm[mode=IfThen] eq_cp}
   \end{tabular}
   \end{isabelle}
 
   \noindent
-  The first is again telling us we do not need to change the @{text RAG}. The second
-  however states that only threads that are \emph{not} dependent on @{text th} have their
+  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"}-chains to recompute the @{term "cp"} of every 
   thread encountered on the way using Lemma~\ref{childrenlem}. Since the @{term "depend"}
-  is loop free, this procedure always stop. The the following two lemmas show this 
-  procedure can actually stop often earlier.
+  is 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}
@@ -1029,7 +1030,6 @@
   have their current precedence changed.
   \smallskip
   *}
-
 (*<*)
 end
 context step_v_cps_nt
@@ -1037,10 +1037,10 @@
 (*>*)
 text {*
   \noindent
-  @{term "V th cs"}: We assume that @{text s'} and 
+  \colorbox{mygrey}{@{term "V th cs"}:} We assume that @{text s'} and 
   @{term "s \<equiv> V th cs#s'"} are both valid. We have to consider two
   subcases: one where there is a thread to ``take over'' the released
-  resource @{text cs}, and where there is not. Let us consider them
+  resource @{text cs}, and one where there is not. Let us consider them
   in turn. Suppose in state @{text s}, the thread @{text th'} takes over
   resource @{text cs} from thread @{text th}. We can show
 
@@ -1065,7 +1065,7 @@
   \noindent
   In the other case where there is no thread that takes over @{text cs}, we can show how
   to recalculate the @{text RAG} and also show that no current precedence needs
-  to be recalculated, except for @{text th} (like in the case above).
+  to be recalculated.
 
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
@@ -1082,7 +1082,7 @@
 
 text {*
   \noindent
-  @{term "P th cs"}: We assume that @{text s'} and 
+  \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
   first by showing that
@@ -1096,7 +1096,7 @@
 
   \noindent
   This means we do not need to add a holding edge to the @{text RAG} and no
-  current precedence must be recalculated (including that for @{text th}).*}(*<*)end context step_P_cps_ne begin(*>*) text {*
+  current precedence needs to be recalculated.*}(*<*)end context step_P_cps_ne begin(*>*) text {*
   \noindent
   In the second case we know that resouce @{text cs} is locked. We can show that
   
@@ -1109,19 +1109,21 @@
 
   \noindent
   That means we have to add a waiting edge to the @{text RAG}. Furthermore
-  the current precedence for all threads that are not dependent on @{text th}
-  are unchanged. For the others we need to follow the @{term "depend"}-chains 
+  the current precedence for all threads that are not dependants of @{text th}
+  are unchanged. For the others we need to follow the edges 
   in the @{text RAG} and recompute the @{term "cp"}. However, like in the 
-  @{text Set}-event, this operation can stop often earlier, namely when intermediate
+  @case of {text Set}, this operation can stop often earlier, namely when intermediate
   values do not change.
   *}
 (*<*)
 end
 (*>*)
-
 text {*
   \noindent
-  TO DO a few sentences summarising what has been achieved.
+  A pleasing result of our formalisation is that the properties in
+  this section closely inform an implementation of PIP:  Whether the
+  @{text RAG} needs to be reconfigured or current precedences need to
+  recalculated for an event is given by a lemma we proved.
 *}
 
 section {* Conclusion *}
@@ -1141,7 +1143,7 @@
   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
-  inductive method to protocol verification~\cite{Paulson98} is quite
+  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
@@ -1169,30 +1171,37 @@
   now living in a multi-processor world. So the question naturally
   arises whether PIP has any relevance in such a world beyond
   teaching. Priority Inversion certainly occurs also in
-  multi-processor systems.  However, the surprising answer, according to
-  \cite{Steinberg10}, is that except for one unsatisfactory proposal
-  nobody has a good idea for how PIP should be modified to work
-  correctly on multi-processor systems. The difficulties become clear
-  when considering that locking and releasing a resource always
-  requires a some small amount of time. If processes work independently, then a
-  low priority process can ``steal'' in this unguarded moment a lock for a
-  resource that was supposed allow a high-priority process to run next. Thus
-  the problem of Priority Inversion is not really prevented. It seems 
-  difficult to design a PIP-algorithm with a meaningful correctness 
-  property on independent multi-processor systems.  We can imagine PIP 
-  to be of use in a situation where
-  processes are not independent, but coordinated via a master
-  process that distributes work over some slave processes. However a
-  formal investigation of this is beyond the scope of this paper.
-  We are not aware of any proofs in this area, not even informal ones.
- 
-  Our formalisation consists of 6894 of readable Isabelle/Isar code, with some
-  apply-scripts interspersed. The formal model is 385 lines long; the 
-  formal correctness proof 3777 lines. The properties relevant for an
-  implementation are 1964 lines long; Auxlliary definitions and notions are 
-  768 lines.
-  
+  multi-processor systems.  However, the surprising answer, according
+  to \cite{Steinberg10}, is that except for one unsatisfactory
+  proposal nobody has a good idea for how PIP should be modified to
+  work correctly on multi-processor systems. The difficulties become
+  clear when considering that locking and releasing a resource always
+  requires a small amount of time. If processes work independently,
+  then a low priority process can ``steal'' in such an unguarded
+  moment a lock for a resource that was supposed allow a high-priority
+  process to run next. Thus the problem of Priority Inversion is not
+  really prevented. It seems difficult to design a PIP-algorithm with
+  a meaningful correctness property on a multi-processor systems where
+  processes work independently.  We can imagine PIP to be of use in
+  situations where processes are \emph{not} independent, but
+  coordinated via a master process that distributes work over some
+  slave processes. However, a formal investigation of this is beyond
+  the scope of this paper.  We are not aware of any proofs in this
+  area, not even informal ones.
 
+  The most closely related work to ours is the formal verification in
+  PVS for Priority Ceiling done by Dutertre \cite{dutertre99b}. His formalisation
+  consists of 407 lemmas and 2500 lines of ``specification'' (we do not
+  know whether this includes also code for proofs).  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
+  definitions and proofs took 770 lines of code. The properties relevant
+  for an implementation took 2000 lines.  Our code can be downloaded from
+  ...
+
+  \bibliographystyle{plain}
+  \bibliography{root}
 *}
 
 section {* Key properties \label{extension} *}
@@ -1311,53 +1320,6 @@
 
 (*<*)
 end
-(*>*)
 
-
-section {* Related works \label{related} *}
-
-text {*
-  \begin{enumerate}
-  \item {\em Integrating Priority Inheritance Algorithms in the Real-Time Specification for Java}
-    \cite{Wellings07} models and verifies the combination of Priority Inheritance (PI) and 
-    Priority Ceiling Emulation (PCE) protocols in the setting of Java virtual machine 
-    using extended Timed Automata(TA) formalism of the UPPAAL tool. Although a detailed 
-    formal model of combined PI and PCE is given, the number of properties is quite 
-    small and the focus is put on the harmonious working of PI and PCE. Most key features of PI 
-    (as well as PCE) are not shown. Because of the limitation of the model checking technique
-    used there, properties are shown only for a small number of scenarios. Therefore, 
-    the verification does not show the correctness of the formal model itself in a 
-    convincing way.  
-  \item {\em Formal Development of Solutions for Real-Time Operating Systems with TLA+/TLC}
-    \cite{Faria08}. A formal model of PI is given in TLA+. Only 3 properties are shown 
-    for PI using model checking. The limitation of model checking is intrinsic to the work.
-  \item {\em Synchronous modeling and validation of priority inheritance schedulers}
-    \cite{Jahier09}. Gives a formal model
-    of PI and PCE in AADL (Architecture Analysis \& Design Language) and checked 
-    several properties using model checking. The number of properties shown there is 
-    less than here and the scale is also limited by the model checking technique. 
-  \item {\em The Priority Ceiling Protocol: Formalization and Analysis Using PVS}
-    \cite{dutertre99b}. Formalized another protocol for Priority Inversion in the 
-    interactive theorem proving system PVS.
-\end{enumerate}
-
-
-  There are several works on inversion avoidance:
-  \begin{enumerate}
-  \item {\em Solving the group priority inversion problem in a timed asynchronous system}
-    \cite{Wang:2002:SGP}. The notion of Group Priority Inversion is introduced. The main 
-    strategy is still inversion avoidance. The method is by reordering requests 
-    in the setting of Client-Server.
-  \item {\em A Formalization of Priority Inversion} \cite{journals/rts/BabaogluMS93}. 
-    Formalized the notion of Priority 
-    Inversion and proposes methods to avoid it. 
-  \end{enumerate}
-
-  {\em Examples of inaccurate specification of the protocol ???}.
-
-*}
-
-
-(*<*)
 end
 (*>*)
\ No newline at end of file




