
diff -r d9b0a2fd0db7 -r bd05c5011c0f prio/Paper/Paper.thy
--- a/prio/Paper/Paper.thy	Sun Feb 12 15:12:50 2012 +0000
+++ b/prio/Paper/Paper.thy	Sun Feb 12 23:20:06 2012 +0000
@@ -103,7 +103,8 @@
   \noindent
   He suggests to avoid PIP altogether by not allowing critical
   sections to be preempted. Unfortunately, this solution does not
-  help in real-time systems with low latency \emph{requirements}.
+  help in real-time systems with hard deadlines for high-priority 
+  threads.
 
   In our opinion, there is clearly a need for investigating correct
   algorithms for PIP. A few specifications for PIP exist (in English)
@@ -150,38 +151,16 @@
 
   \noindent
   {\bf Contributions:} There have been earlier formal investigations
-  into PIP \cite{conf/fase/JahierHR09,WellingsBSB07,Faria08}, but they
-  are using model checking technology. As far as we are aware, this is
-  the first formalised proof for the correctness of PIP. In contrast
-  to model checking, our formalisation provides insight into why PIP
-  is correct and allows us to prove stronger properties. For this Isar
-  and Isabelle/HOL is an attractive tool for exploring definitions and
-  keeping proofs consistent.
-
-  For example, we find through formalization that the choice of next 
-  thread to take a lock when a resource is released is irrelevant for 
-  the very basic property of PIP to hold.
-
-  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.
-
-  vt (valid trace) was introduced earlier, cite
-  
-  
-  Paulson's method has not been used outside security field, except
-  work by Zhang et al.
-
-  How did Sha et al prove it....they did not use Paulson's method.
+  into PIP \cite{Faria08,Jahier09,Wellings07}, but they employ model
+  checking techniques. This paper presents a formalised and
+  mechanically checked proof for the correctness of PIP (to our
+  knowledge the first one; an 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, inform an
+  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.
 *}
 
 section {* Formal Model of the Priority Inheritance Protocol *}
@@ -528,7 +507,7 @@
   @{term threads} is empty and therefore there is no thread ready nor a 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 possibilites.
+  threads. We use the set-comprehension to capture both possibilities.
   We can now also define the set of resources that are locked by a thread in any
   given state.
 
@@ -539,10 +518,11 @@
   \noindent
   These resources are given by the holding edges in the RAG.
 
-  Finally we can define what a \emph{valid state} is in our PIP. For example we cannot exptect to
-  be able to exit a thread, if it was not created yet. These validity constraints
-  are characterised by the inductive predicate @{term "step"}. We give five 
-  inference rules relating a state and an event that can happen next.
+  Finally we can define what a \emph{valid state} is in our PIP. For
+  example we cannot expect to be able to exit a thread, if it was not
+  created yet. These validity constraints are characterised by the
+  inductive predicate @{term "step"}. We give five inference rules
+  relating a state and an event that can happen next.
 
   \begin{center}
   \begin{tabular}{c}
@@ -622,9 +602,23 @@
     @{thm highest}.
   \item The precedence of @{term "th"} is @{term "Prc prio tm"} (@{text "preced_th"}):
     @{thm preced_th}.
+ 
+  \item @{term "t"} is a valid extension of @{term "s"} (@{text "vt_t"}): @{thm vt_t}.
+  \item Any thread created in @{term "t"} has priority no higher than @{term "prio"}, therefore
+    its precedence can not be higher than @{term "th"},  therefore
+    @{term "th"} remain to be the one with the highest precedence
+    (@{text "create_low"}):
+    @{thm [display] create_low}
+  \item Any adjustment of priority in 
+    @{term "t"} does not happen to @{term "th"} and 
+    the priority set is no higher than @{term "prio"}, therefore
+    @{term "th"} remain to be the one with the highest precedence (@{text "set_diff_low"}):
+    @{thm [display] set_diff_low}
+  \item Since we are investigating what happens to @{term "th"}, it is assumed 
+    @{term "th"} does not exit during @{term "t"} (@{text "exit_diff"}):
+    @{thm [display] exit_diff}
   \end{enumerate}
 
-
   \begin{lemma}
   @{thm[mode=IfThen] moment_blocked}
   \end{lemma}
@@ -633,6 +627,9 @@
   @{thm[mode=IfThen] runing_inversion_2}
   \end{theorem}
 
+  \begin{theorem}
+  @{thm[mode=IfThen] runing_inversion_3}
+  \end{theorem}
   
 
 
@@ -660,6 +657,10 @@
   has finally be reduced to the very first principle to be checked
   mechanically.
 
+  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. 
+
   TO DO 
 
   no clue about multi-processor case according to \cite{Steinberg10} 
@@ -679,7 +680,7 @@
   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{conf/fase/JahierHR09,WellingsBSB07,Faria08} are based on the
+  \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
@@ -1038,7 +1039,7 @@
   Section 5.6.5 of \cite{Vahalia96}, the implementation of Priority Inheritance in Solaris 
   uses sophisticated linking data structure. Except discussing two scenarios to show how
   the data structure should be manipulated, a lot of details of the implementation are missing. 
-  In \cite{Faria08,conf/fase/JahierHR09,WellingsBSB07} the protocol is described formally 
+  In \cite{Faria08,Jahier09,Wellings07} the protocol is described formally 
   using different notations, but little information is given on how this protocol can be 
   implemented efficiently, especially there is no information on how these data structure 
   should be manipulated. 
@@ -1307,7 +1308,7 @@
 text {*
   \begin{enumerate}
   \item {\em Integrating Priority Inheritance Algorithms in the Real-Time Specification for Java}
-    \cite{WellingsBSB07} models and verifies the combination of Priority Inheritance (PI) and 
+    \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 
@@ -1320,7 +1321,7 @@
     \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{conf/fase/JahierHR09}. Gives a formal model
+    \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. 




