--- a/prio/Paper/Paper.thy	Fri Jan 27 23:19:10 2012 +0000
+++ b/prio/Paper/Paper.thy	Sun Jan 29 09:31:03 2012 +0000
@@ -2,6 +2,9 @@
 theory Paper
 imports CpsG ExtGG LaTeXsugar
 begin
+ML {*
+  show_question_marks_default := false;
+  *}
 (*>*)
 
 section {* Introduction *}
@@ -380,7 +383,7 @@
   *}
 
 text {* \noindent
-  The main theorem is to characterizing the running thread during @{term "t"} 
+  The main theorem of this part is to characterizing the running thread during @{term "t"} 
   (@{text "runing_inversion_2"}):
   @{thm [display] runing_inversion_2}
   According to this, if a thread is running, it is either @{term "th"} or was
@@ -400,12 +403,89 @@
 section {* Properties to guide implementation \label{implement} *}
 
 text {*
-  The properties (especially @{text "runing_inversion_2"}) convinced us that model defined 
-  in section \ref{model} does prevent indefinite priority inversion and therefore fulfills 
+  The properties (especially @{text "runing_inversion_2"}) convinced us that the model defined 
+  in Section \ref{model} does prevent indefinite priority inversion and therefore fulfills 
   the fundamental requirement of Priority Inheritance protocol. Another purpose of this paper 
-  is to show how this model can be used to guide a concrete implementation.
+  is to show how this model can be used to guide a concrete implementation. As discussed in
+  Section 5.6.5 of \cite{Vahalia:1996:UI}, 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 
+  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. 
+
+  Because the scheduling of threads is based on current precedence, 
+  the central issue in implementation of Priority Inheritance is how to compute the precedence
+  correctly and efficiently. As long as the precedence is correct, it is very easy to 
+  modify the scheduling algorithm to select the correct thread to execute. 
+
+  First, it can be proved that the computation of current precedence @{term "cp"} of a threads
+  only involves its children (@{text "cp_rec"}):
+  @{thm [display] cp_rec} 
+  where @{term "children s th"} represents the set of children of @{term "th"} in the current
+  RAG: 
+  \[
+  @{thm (lhs) children_def} @{text "\<equiv>"} @{thm (rhs) children_def}
+  \]
+  where the definition of @{term "child"} is: 
+  \[ @{thm (lhs) child_def} @{text "\<equiv>"}  @{thm (rhs) child_def}
+  \]
+
+  The aim of this section is to fill the missing details of how current precedence should
+  be changed with the happening of events, with each event type treated by one subsection,
+  where the computation of @{term "cp"} uses lemma @{text "cp_rec"}.
+  *}
+ 
+subsection {* Event @{text "Set th prio"} *}
+
+(*<*)
+context step_set_cps
+begin
+(*>*)
+
+text {*
+  The context under which event @{text "Set th prio"} happens is formalized as follows:
+  \begin{enumerate}
+    \item The formation of @{term "s"} (@{text "s_def"}): @{thm s_def}.
+    \item State @{term "s"} is a valid state (@{text "vt_s"}): @{thm vt_s}. This implies 
+      event @{text "Set th prio"} is eligible to happen under state @{term "s'"} and
+      state @{term "s'"} is a valid state.
+  \end{enumerate}
   *}
 
+text {* \noindent
+  Under such a context, we investigated how the current precedence @{term "cp"} of 
+  threads change from state @{term "s'"} to @{term "s"} and obtained the following
+  conclusions:
+  \begin{enumerate}
+  %% \item The RAG does not change (@{text "eq_dep"}): @{thm "eq_dep"}.
+  \item All threads with no dependence relation with thread @{term "th"} have their
+    @{term "cp"}-value unchanged (@{text "eq_cp"}):
+    @{thm [display] eq_cp}
+    This lemma implies the @{term "cp"}-value of @{term "th"}
+    and those threads which have a dependence relation with @{term "th"} might need
+    to be recomputed. The way to do this is to start from @{term "th"} 
+    and follow the @{term "depend"}-chain to recompute the @{term "cp"}-value of every 
+    encountered thread using lemma @{text "cp_rec"}. 
+    Since the @{term "depend"}-relation is loop free, this procedure 
+    can always stop. The the following lemma shows this procedure actually could stop earlier.
+  \item The following two lemma shows, if a thread the re-computation of which
+    gives an unchanged @{term "cp"}-value, the procedure described above can stop. 
+    \begin{enumerate}
+      \item Lemma @{text "eq_up_self"} shows if the re-computation of
+        @{term "th"}'s @{term "cp"} gives the same result, the procedure can stop:
+        @{thm [display] eq_up_self}
+      \item Lemma @{text "eq_up"}) shows if the re-computation at intermediate threads
+        gives unchanged result, the procedure can stop:
+        @{thm [display] eq_up}
+  \end{enumerate}
+  \end{enumerate}
+  *}
+
+(*<*)
+end
+(*>*)
 
 section {* Related works \label{related} *}