--- a/prio/Paper/Paper.thy Mon Jan 30 09:44:33 2012 +0000
+++ b/prio/Paper/Paper.thy Wed Feb 01 08:16:00 2012 +0000
@@ -1,9 +1,9 @@
(*<*)
theory Paper
-imports CpsG ExtGG "~~/src/HOL/Library/LaTeXsugar"
+imports CpsG ExtGG (* "~~/src/HOL/Library/LaTeXsugar" *) LaTeXsugar
begin
ML {*
- Printer.show_question_marks_default := false;
+ show_question_marks_default := false;
*}
(*>*)
@@ -507,6 +507,193 @@
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} *}
text {*