# HG changeset patch # User zhang # Date 1328084160 0 # Node ID ee4611c1e13cf0fb3f0aa4cfe950751bd6d0e3f0 # Parent 78523b3ae2ad8a343d8477270a0f0b6acc1af1b1 All comments added. diff -r 78523b3ae2ad -r ee4611c1e13c prio/CpsG.thy --- a/prio/CpsG.thy Mon Jan 30 09:44:33 2012 +0000 +++ b/prio/CpsG.thy Wed Feb 01 08:16:00 2012 +0000 @@ -1356,6 +1356,142 @@ locale step_P_cps_ne =step_P_cps + assumes ne: "wq s' cs \ []" +locale step_P_cps_e =step_P_cps + + assumes ee: "wq s' cs = []" + +context step_P_cps_e +begin + +lemma depend_s: "depend s = depend s' \ {(Cs cs, Th th)}" +proof - + from ee and step_depend_p[OF vt_s[unfolded s_def], folded s_def] + show ?thesis by auto +qed + +lemma child_kept_left: + assumes + "(n1, n2) \ (child s')^+" + shows "(n1, n2) \ (child s)^+" +proof - + from assms show ?thesis + proof(induct rule: converse_trancl_induct) + case (base y) + from base obtain th1 cs1 th2 + where h1: "(Th th1, Cs cs1) \ depend s'" + and h2: "(Cs cs1, Th th2) \ depend s'" + and eq_y: "y = Th th1" and eq_n2: "n2 = Th th2" by (auto simp:child_def) + have "cs1 \ cs" + proof + assume eq_cs: "cs1 = cs" + with h1 have "(Th th1, Cs cs) \ depend s'" by simp + with ee show False + by (auto simp:s_depend_def cs_waiting_def) + qed + with h1 h2 depend_s have + h1': "(Th th1, Cs cs1) \ depend s" and + h2': "(Cs cs1, Th th2) \ depend s" by auto + hence "(Th th1, Th th2) \ child s" by (auto simp:child_def) + with eq_y eq_n2 have "(y, n2) \ child s" by simp + thus ?case by auto + next + case (step y z) + have "(y, z) \ child s'" by fact + then obtain th1 cs1 th2 + where h1: "(Th th1, Cs cs1) \ depend s'" + and h2: "(Cs cs1, Th th2) \ depend s'" + and eq_y: "y = Th th1" and eq_z: "z = Th th2" by (auto simp:child_def) + have "cs1 \ cs" + proof + assume eq_cs: "cs1 = cs" + with h1 have "(Th th1, Cs cs) \ depend s'" by simp + with ee show False + by (auto simp:s_depend_def cs_waiting_def) + qed + with h1 h2 depend_s have + h1': "(Th th1, Cs cs1) \ depend s" and + h2': "(Cs cs1, Th th2) \ depend s" by auto + hence "(Th th1, Th th2) \ child s" by (auto simp:child_def) + with eq_y eq_z have "(y, z) \ child s" by simp + moreover have "(z, n2) \ (child s)^+" by fact + ultimately show ?case by auto + qed +qed + +lemma child_kept_right: + assumes + "(n1, n2) \ (child s)^+" + shows "(n1, n2) \ (child s')^+" +proof - + from assms show ?thesis + proof(induct) + case (base y) + from base and depend_s + have "(n1, y) \ child s'" + apply (auto simp:child_def) + proof - + fix th' + assume "(Th th', Cs cs) \ depend s'" + with ee have "False" + by (auto simp:s_depend_def cs_waiting_def) + thus "\cs. (Th th', Cs cs) \ depend s' \ (Cs cs, Th th) \ depend s'" by auto + qed + thus ?case by auto + next + case (step y z) + have "(y, z) \ child s" by fact + with depend_s have "(y, z) \ child s'" + apply (auto simp:child_def) + proof - + fix th' + assume "(Th th', Cs cs) \ depend s'" + with ee have "False" + by (auto simp:s_depend_def cs_waiting_def) + thus "\cs. (Th th', Cs cs) \ depend s' \ (Cs cs, Th th) \ depend s'" by auto + qed + moreover have "(n1, y) \ (child s')\<^sup>+" by fact + ultimately show ?case by auto + qed +qed + +lemma eq_child: "(child s)^+ = (child s')^+" + by (insert child_kept_left child_kept_right, auto) + +lemma eq_cp: + fixes th' + shows "cp s th' = cp s' th'" + apply (unfold cp_eq_cpreced cpreced_def) +proof - + have eq_dp: "\ th. dependents (wq s) th = dependents (wq s') th" + apply (unfold cs_dependents_def, unfold eq_depend) + proof - + from eq_child + have "\th. {th'. (Th th', Th th) \ (child s)\<^sup>+} = {th'. (Th th', Th th) \ (child s')\<^sup>+}" + by auto + with child_depend_eq[OF vt_s] child_depend_eq[OF step_back_vt[OF vt_s[unfolded s_def]]] + show "\th. {th'. (Th th', Th th) \ (depend s)\<^sup>+} = {th'. (Th th', Th th) \ (depend s')\<^sup>+}" + by simp + qed + moreover { + fix th1 + assume "th1 \ {th'} \ dependents (wq s') th'" + hence "th1 = th' \ th1 \ dependents (wq s') th'" by auto + hence "preced th1 s = preced th1 s'" + proof + assume "th1 = th'" + show "preced th1 s = preced th1 s'" by (simp add:s_def preced_def) + next + assume "th1 \ dependents (wq s') th'" + show "preced th1 s = preced th1 s'" by (simp add:s_def preced_def) + qed + } ultimately have "((\th. preced th s) ` ({th'} \ dependents (wq s) th')) = + ((\th. preced th s') ` ({th'} \ dependents (wq s') th'))" + by (auto simp:image_def) + thus "Max ((\th. preced th s) ` ({th'} \ dependents (wq s) th')) = + Max ((\th. preced th s') ` ({th'} \ dependents (wq s') th'))" by simp +qed + +end + context step_P_cps_ne begin diff -r 78523b3ae2ad -r ee4611c1e13c prio/Paper/Paper.thy --- 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 {* diff -r 78523b3ae2ad -r ee4611c1e13c prio/paper.pdf Binary file prio/paper.pdf has changed