--- a/prio/ExtGG.thy	Mon Feb 13 10:44:42 2012 +0000
+++ b/prio/ExtGG.thy	Mon Feb 13 10:57:47 2012 +0000
@@ -892,15 +892,39 @@
   show ?thesis by auto
 qed
 
+lemma runing_preced_inversion:
+  assumes runing': "th' \<in> runing (t@s)"
+  shows "cp (t@s) th' = preced th s"
+proof -
+  from runing' have "cp (t@s) th' = Max (cp (t @ s) ` readys (t @ s))"
+    by (unfold runing_def, auto)
+  also have "\<dots> = preced th s"
+  proof -
+    from max_cp_readys_threads[OF vt_t]
+    have "\<dots> =  Max (cp (t @ s) ` threads (t @ s))" .
+    also have "\<dots> = preced th s"
+    proof -
+      from max_kept
+      and max_cp_eq [OF vt_t]
+      show ?thesis by auto
+    qed
+    finally show ?thesis .
+  qed
+  finally show ?thesis .
+qed
+
 lemma runing_inversion_3:
   assumes runing': "th' \<in> runing (t@s)"
   and neq_th: "th' \<noteq> th"
-  shows "th' \<in> threads s \<and> cntV s th' < cntP s th'"
+  shows "th' \<in> threads s \<and> (cntV s th' < cntP s th' \<and> cp (t@s) th' = preced th s)"
 proof -
-  from runing_inversion_2 [OF runing'] and neq_th
+  from runing_inversion_2 [OF runing'] 
+    and neq_th 
+    and runing_preced_inversion[OF runing']
   show ?thesis by auto
 qed
 
+
 lemma live: "runing (t@s) \<noteq> {}"
 proof(cases "th \<in> runing (t@s)")
   case True thus ?thesis by auto

--- a/prio/Paper/Paper.thy	Mon Feb 13 10:44:42 2012 +0000
+++ b/prio/Paper/Paper.thy	Mon Feb 13 10:57:47 2012 +0000
@@ -811,9 +811,279 @@
 end
 (*>*)
 
-section {* Properties for an Implementation *}
+section {* Properties for an Implementation \label{implement}*}
+
+text {*
+  The properties (centered around @{text "runing_inversion_2"} in particular) 
+  convinced us that the formal model 
+  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. 
+
+  The difficult part of implementation is the calculation of current precedence. 
+  Once current precedence is computed efficiently and correctly, 
+  the selection of the thread with highest precedence from ready threads is a 
+  standard scheduling mechanism implemented in most operating systems. 
+
+  Our implementation related formalization focuses on how to compute 
+  current precedence. 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}
+  \]
+  which corresponds a two hop link between threads in the RAG, with a resource in the middle.
+  
+  Lemma @{text "cp_rec"} means, the current precedence of threads can be computed locally, 
+  i.e. the current precedence of one thread only needs to be recomputed when some of its
+  children change their current precedence. 
+
+  Each of the following subsections discusses one event type, investigating 
+  which parts in the RAG need current precedence re-computation when that type of event
+  happens.
+  *}
+ 
+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
+  results:
+  \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
+(*>*)
+
+subsection {* Event @{text "V th cs"} *}
+
+(*<*)
+context step_v_cps_nt
+begin
+(*>*)
+
+text {*
+  The context under which event @{text "V th cs"} 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 "V th cs"} 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"}. 
+
+
+  Two subcases are considerted, 
+  where the first is that there exits @{term "th'"} 
+  such that 
+  @{thm [display] nt} 
+  holds, which means there exists a thread @{term "th'"} to take over
+  the resource release by thread @{term "th"}. 
+  In this sub-case, the following results are obtained:
+  \begin{enumerate}
+  \item The change of RAG is given by lemma @{text "depend_s"}: 
+  @{thm [display] "depend_s"}
+  which shows two edges are removed while one is added. These changes imply how
+  the current precedences should be re-computed.
+  \item First all threads different from @{term "th"} and @{term "th'"} have their
+  @{term "cp"}-value kept, therefore do not need a re-computation
+  (@{text "cp_kept"}): @{thm [display] cp_kept}
+  This lemma also implies, only the @{term "cp"}-values of @{term "th"} and @{term "th'"}
+  need to be recomputed.
+  \end{enumerate}
+  *}
+
+(*<*)
+end
+
+context step_v_cps_nnt
+begin
+(*>*)
 
-text {* TO DO *}
+text {*
+  The other sub-case is when for all @{text "th'"}
+  @{thm [display] nnt}
+  holds, no such thread exists. The following results can be obtained for this 
+  sub-case:
+  \begin{enumerate}
+  \item The change of RAG is given by lemma @{text "depend_s"}:
+  @{thm [display] depend_s}
+  which means only one edge is removed.
+  \item In this case, no re-computation is needed (@{text "eq_cp"}):
+  @{thm [display] eq_cp}
+  \end{enumerate}
+  *}
+
+(*<*)
+end
+(*>*)
+
+
+subsection {* Event @{text "P th cs"} *}
+
+(*<*)
+context step_P_cps_e
+begin
+(*>*)
+
+text {*
+  The context under which event @{text "P th cs"} 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 "P th cs"} is eligible to happen under state @{term "s'"} and
+      state @{term "s'"} is a valid state.
+  \end{enumerate}
+
+  This case is further divided into two sub-cases. The first is when @{thm ee} holds.
+  The following results can be obtained:
+  \begin{enumerate}
+  \item One edge is added to the RAG (@{text "depend_s"}):
+    @{thm [display] depend_s}
+  \item No re-computation is needed (@{text "eq_cp"}):
+    @{thm [display] eq_cp}
+  \end{enumerate}
+*}
+
+(*<*)
+end
+
+context step_P_cps_ne
+begin
+(*>*)
+
+text {*
+  The second is when @{thm ne} holds.
+  The following results can be obtained:
+  \begin{enumerate}
+  \item One edge is added to the RAG (@{text "depend_s"}):
+    @{thm [display] depend_s}
+  \item Threads with no dependence relation with @{term "th"} do not need a re-computation
+    of their @{term "cp"}-values (@{text "eq_cp"}):
+    @{thm [display] eq_cp}
+    This lemma implies all threads with a dependence relation with @{term "th"} may need 
+    re-computation.
+  \item Similar to the case of @{term "Set"}, the computation procedure could stop earlier
+    (@{text "eq_up"}):
+    @{thm [display] eq_up}
+  \end{enumerate}
+
+  *}
+
+(*<*)
+end
+(*>*)
+
+subsection {* Event @{text "Create th prio"} *}
+
+(*<*)
+context step_create_cps
+begin
+(*>*)
+
+text {*
+  The context under which event @{text "Create 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 "Create th prio"} is eligible to happen under state @{term "s'"} and
+      state @{term "s'"} is a valid state.
+  \end{enumerate}
+  The following results can be obtained under this context:
+  \begin{enumerate}
+  \item The RAG does not change (@{text "eq_dep"}):
+    @{thm [display] eq_dep}
+  \item All threads other than @{term "th"} do not need re-computation (@{text "eq_cp"}):
+    @{thm [display] eq_cp}
+  \item The @{term "cp"}-value of @{term "th"} equals its precedence 
+    (@{text "eq_cp_th"}):
+    @{thm [display] eq_cp_th}
+  \end{enumerate}
+
+*}
+
+
+(*<*)
+end
+(*>*)
+
+subsection {* Event @{text "Exit th"} *}
+
+(*<*)
+context step_exit_cps
+begin
+(*>*)
+
+text {*
+  The context under which event @{text "Exit th"} 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 "Exit th"} is eligible to happen under state @{term "s'"} and
+      state @{term "s'"} is a valid state.
+  \end{enumerate}
+  The following results can be obtained under this context:
+  \begin{enumerate}
+  \item The RAG does not change (@{text "eq_dep"}):
+    @{thm [display] eq_dep}
+  \item All threads other than @{term "th"} do not need re-computation (@{text "eq_cp"}):
+    @{thm [display] eq_cp}
+  \end{enumerate}
+  Since @{term th} does not live in state @{term "s"}, there is no need to compute 
+  its @{term cp}-value.
+*}
+
+(*<*)
+end
+(*>*)
 
 section {* Conclusion *}
 

Binary file prio/paper.pdf has changed