--- a/prio/CpsG.thy Mon Feb 13 10:57:47 2012 +0000
+++ b/prio/CpsG.thy Mon Feb 13 15:35:08 2012 +0000
@@ -245,12 +245,15 @@
qed
definition child :: "state \<Rightarrow> (node \<times> node) set"
- where "child s =
+ where "child s \<equiv>
{(Th th', Th th) | th th'. \<exists> cs. (Th th', Cs cs) \<in> depend s \<and> (Cs cs, Th th) \<in> depend s}"
definition children :: "state \<Rightarrow> thread \<Rightarrow> thread set"
- where "children s th = {th'. (Th th', Th th) \<in> child s}"
+ where "children s th \<equiv> {th'. (Th th', Th th) \<in> child s}"
+lemma children_def2:
+ "children s th \<equiv> {th'. \<exists> cs. (Th th', Cs cs) \<in> depend s \<and> (Cs cs, Th th) \<in> depend s}"
+unfolding child_def children_def by simp
lemma children_dependents: "children s th \<subseteq> dependents (wq s) th"
by (unfold children_def child_def cs_dependents_def, auto simp:eq_depend)
@@ -1004,7 +1007,7 @@
begin
lemma depend_s:
- "depend s = (depend s' - {(Cs cs, Th th)} - {(Th th', Cs cs)}) \<union>
+ "depend s = (depend s' - {(Cs cs, Th th), (Th th', Cs cs)}) \<union>
{(Cs cs, Th th')}"
proof -
from step_depend_v[OF vt_s[unfolded s_def], folded s_def]
--- 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} *}