diff -r 23632f329e10 -r 09281ccb31bd prio/Paper/Paper.thy
--- a/prio/Paper/Paper.thy	Mon Feb 13 10:57:47 2012 +0000
+++ b/prio/Paper/Paper.thy	Mon Feb 13 15:35:08 2012 +0000
@@ -709,9 +709,12 @@
 
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
-  %@{thm[mode=IfThen] }\\
-  %@{thm[mode=IfThen] }\\
-  %@{thm[mode=IfThen] }
+  @{text If}~@{thm (prem 1) acyclic_depend}~@{text "then"}:\\
+  \hspace{5mm}@{thm (concl) acyclic_depend},
+  @{thm (concl) finite_depend} and
+  @{thm (concl) wf_dep_converse},\\
+  \hspace{5mm}@{text "if"}~@{thm (prem 2) dm_depend_threads}~@{text "then"}~@{thm (concl) dm_depend_threads}\\
+  \hspace{5mm}@{text "if"}~@{thm (prem 2) range_in}~@{text "then"}~@{thm (concl) range_in}
   \end{tabular}
   \end{isabelle}
 
@@ -811,280 +814,242 @@
 end
 (*>*)
 
-section {* Properties for an Implementation \label{implement}*}
+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. 
+  While a formal correctness proof for our model of PIP is certainly
+  attractive (especially in light of the flawed proof by Sha et
+  al.~\cite{Sha90}), we found that the formalisation can even help us
+  with efficiently implementing PIP.
 
-  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. 
+  For example Baker complained that calculating the current precedence
+  in PIP is quite ``heavy weight'' in Linux (see our 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
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  \begin{tabular}{@ {}l}
+  @{thm children_def2}
+  \end{tabular}
+  \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
 
-  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.
+  \begin{lemma}\label{childrenlem}
+  @{text "If"} @{thm (prem 1) cp_rec} @{text "then"}
+  \begin{center}
+  @{thm (concl) cp_rec}.
+  \end{center}
+  \end{lemma}
   
-  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. 
+  \noindent
+  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 
+  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.
 
-  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"} *}
+  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
+*}
 
 (*<*)
+context step_create_cps
+begin
+(*>*)
+text {*
+  \noindent
+  @{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[mode=IfThen] eq_cp}
+  \end{tabular}
+  \end{isabelle}
+
+  \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))"}.
+  \smallskip
+  *}
+(*<*)
+end
+context step_exit_cps
+begin
+(*>*)
+text {*
+  \noindent
+  @{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[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
+  alive anymore in state @{term "s"}, there is no need to calculate its
+  current precedence.
+  \smallskip
+*}
+(*<*)
+end
 context step_set_cps
 begin
 (*>*)
+text {*
+  \noindent
+  @{term "Set th prio"}: We assume that @{text s'} and 
+  @{term "s \<equiv> Set th prio#s'"} are both valid. We can show that
 
-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}
-  *}
+  \begin{isabelle}\ \ \ \ \ %%%
+  \begin{tabular}{@ {}l}
+  @{thm[mode=IfThen] eq_dep}\\
+  @{thm[mode=IfThen] eq_cp}
+  \end{tabular}
+  \end{isabelle}
 
-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}
+  \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
+  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.
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  \begin{tabular}{@ {}l}
+  @{thm[mode=IfThen] eq_up_self}\\
+  @{text "If"} @{thm (prem 1) eq_up}, @{thm (prem 2) eq_up} and @{thm (prem 3) eq_up}\\
+  @{text "then"} @{thm (concl) eq_up}.
+  \end{tabular}
+  \end{isabelle}
+
+  \noindent
+  The first states that if the current precedence of @{text th} is unchanged,
+  then the procedure can stop immediately (all dependent threads have their @{term cp}-value unchanged).
+  The second states that if an intermediate @{term cp}-value does not change, then
+  the procedure can also stop, because none of its dependent threads will
+  have their current precedence changed.
+  \smallskip
   *}
 
 (*<*)
 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"}. 
+  \noindent
+  @{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
+  in turn. Suppose in state @{text s}, the thread @{text th'} takes over
+  resource @{text cs} from thread @{text th}. We can show
 
 
-  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}
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{thm depend_s}
+  \end{isabelle}
+  
+  \noindent
+  which shows how the @{text RAG} needs to be changed. This also suggests
+  how the current precedences need to be recalculated. For threads that are
+  not @{text "th"} and @{text "th'"} nothing needs to be changed, since we
+  can show
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{thm[mode=IfThen] cp_kept}
+  \end{isabelle}
+  
+  \noindent
+  For @{text th} and @{text th'} we need to use Lemma~\ref{childrenlem} to
+  recalculate their current prcedence since their children have changed. *}(*<*)end context step_v_cps_nnt begin (*>*)text {*
+  \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).
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  \begin{tabular}{@ {}l}
+  @{thm depend_s}\\
+  @{thm eq_cp}
+  \end{tabular}
+  \end{isabelle}
   *}
-
 (*<*)
 end
-
-context step_v_cps_nnt
-begin
-(*>*)
-
-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
+  \noindent
+  @{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
+  
+  \begin{isabelle}\ \ \ \ \ %%%
+  \begin{tabular}{@ {}l}
+  @{thm depend_s}\\
+  @{thm eq_cp}
+  \end{tabular}
+  \end{isabelle}
 
-context step_P_cps_ne
-begin
-(*>*)
+  \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 {*
+  \noindent
+  In the second case we know that resouce @{text cs} is locked. We can show that
+  
+  \begin{isabelle}\ \ \ \ \ %%%
+  \begin{tabular}{@ {}l}
+  @{thm depend_s}\\
+  @{thm[mode=IfThen] eq_cp}
+  \end{tabular}
+  \end{isabelle}
 
-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}
-
+  \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 
+  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
+  values do not change.
   *}
-
 (*<*)
 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}
-
+  \noindent
+  TO DO a few sentences summarising what has been achieved.
 *}
 
-
-(*<*)
-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 *}
 
 text {* 
@@ -1224,10 +1189,12 @@
   Priority Inheritance is just such a byproduct. 
   *}
 
+(*
 section {* Formal model of Priority Inheritance \label{model} *}
 text {*
   \input{../../generated/PrioGDef}
 *}
+*)
 
 section {* General properties of Priority Inheritance \label{general} *}
 
@@ -1353,279 +1320,6 @@
 end
 (*>*)
 
-section {* Properties to guide implementation \label{implement} *}
-
-text {*
-  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. As discussed in
-  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,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. 
-
-  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
-(*>*)
-
-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 {*
-  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 {* Related works \label{related} *}