--- a/prio/Paper/Paper.thy	Sun Feb 12 11:30:17 2012 +0000
+++ b/prio/Paper/Paper.thy	Sun Feb 12 14:58:47 2012 +0000
@@ -1,6 +1,6 @@
 (*<*)
 theory Paper
-imports CpsG ExtGG "~~/src/HOL/Library/LaTeXsugar"
+imports "../CpsG" "../ExtGG" "~~/src/HOL/Library/LaTeXsugar"
 begin
 ML {*
   open Printer;
@@ -149,17 +149,39 @@
   of threads, i.e.~\emph{traces}, that could possibly happen).\medskip
 
   \noindent
-  {\bf Contributions:} There have been earlier formal investigations 
-  into PIP, but ...\cite{Faria08}
+  {\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
   
-  distributed PIP
-
+  
   Paulson's method has not been used outside security field, except
   work by Zhang et al.
 
-  no clue about multi-processor case according to \cite{Steinberg10} 
+  How did Sha et al prove it....they did not use Paulson's method.
 *}
 
 section {* Formal Model of the Priority Inheritance Protocol *}
@@ -284,7 +306,7 @@
   empty list for every resource.
 
   \begin{isabelle}\ \ \ \ \ %%%
-  @{abbrev all_unlocked}
+  @{abbrev all_unlocked}\hfill\numbered{allunlocked}
   \end{isabelle}
 
   \noindent
@@ -383,7 +405,7 @@
   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 and the
+  In the initial state, the scheduler starts with all resources unlocked (see \eqref{allunlocked}) and the
   current precedence of every thread is initialised with @{term "Prc 0 0"}; that means 
   \mbox{@{abbrev initial_cprec}}. Therefore
   we have
@@ -435,7 +457,8 @@
 
   \noindent
   The clause for event @{term "V th cs"} is similar, except that we need to update the waiting queue function
-  so that the thread that possessed the lock is deleted from the corresponding thread list. For this we use
+  so that the thread that possessed the lock is deleted from the corresponding thread list. For this 
+  list transformation, we use
   the auxiliary function @{term release}. A simple version of @{term release} would
   just delete this thread and return the rest, namely
 
@@ -531,7 +554,7 @@
   \noindent
   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. The event @{text Set} can happen
+  running and does not lock any resources anymore (to simplify ). The event @{text Set} can happen
   if the corresponding thread is running. 
 
   \begin{center}
@@ -539,11 +562,19 @@
   \end{center}
 
   \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 doe not lead to a cycle in the 
-  RAG. Similarly, if a thread wants to release a lock on a resource, then it must 
-  be running and in the possession of that lock. This is formally given by the 
-  last two inference rules of @{term step}.
+  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.  Here in our formal
+  model we just exclude such problematic cases in order 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, we need to perform an occurs
+  check; but in practice the occurs check is ommited and the
+  responsibility to avoid problems rests with the programmer.}
+  Similarly, if a thread wants to release a lock on a resource, then
+  it must be running and in the possession of that lock. This is
+  formally given by the last two inference rules of @{term step}.
 
   \begin{center}
   \begin{tabular}{c}
@@ -569,7 +600,49 @@
 
 section {* Correctness Proof *}
 
-text {* TO DO *}
+
+(*<*)
+context extend_highest_gen
+begin
+(*>*)
+
+print_locale extend_highest_gen
+thm extend_highest_gen_def
+thm extend_highest_gen_axioms_def
+thm highest_gen_def
+text {* 
+  Main lemma
+
+  \begin{enumerate}
+  \item @{term "s"} is a valid state (@{text "vt_s"}):
+    @{thm  vt_s}.
+  \item @{term "th"} is a living thread in @{term "s"} (@{text "threads_s"}):
+    @{thm threads_s}.
+  \item @{term "th"} has the highest precedence in @{term "s"} (@{text "highest"}):
+    @{thm highest}.
+  \item The precedence of @{term "th"} is @{term "Prc prio tm"} (@{text "preced_th"}):
+    @{thm preced_th}.
+  \end{enumerate}
+
+
+  \begin{lemma}
+  @{thm[mode=IfThen] moment_blocked}
+  \end{lemma}
+
+  \begin{theorem}
+  @{thm[mode=IfThen] runing_inversion_2}
+  \end{theorem}
+
+  
+
+
+TO DO 
+
+*}
+
+(*<*)
+end
+(*>*)
 
 section {* Properties for an Implementation *}
 
@@ -582,8 +655,15 @@
   used in real-time systems in order to avoid the problem of Priority
   Inversion.
 
+  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.
+
   TO DO 
 
+  no clue about multi-processor case according to \cite{Steinberg10} 
+
 *}
 
 text {*

Binary file prio/paper.pdf has changed