# HG changeset patch # User urbanc # Date 1335799954 0 # Node ID e6b13c7b94946f38f310c2ff9361546652ea6961 # Parent 8ce9a432680b75d59840a3f3cc625a9fb3f355f7 slightly changed the definition of holdends and detached diff -r 8ce9a432680b -r e6b13c7b9494 prio/CpsG.thy --- a/prio/CpsG.thy Mon Apr 23 08:01:37 2012 +0000 +++ b/prio/CpsG.thy Mon Apr 30 15:32:34 2012 +0000 @@ -21,7 +21,7 @@ assume eq_e: "e = Create thread prio" and not_in': "thread \ threads s" have "holdents (e # s) th = holdents s th" - apply (unfold eq_e holdents_def) + apply (unfold eq_e holdents_test) by (simp add:depend_create_unchanged) moreover have "th \ threads s" proof - @@ -37,13 +37,13 @@ case True with nh eq_e show ?thesis - by (auto simp:holdents_def depend_exit_unchanged) + by (auto simp:holdents_test depend_exit_unchanged) next case False with not_in and eq_e have "th \ threads s" by simp from ih[OF this] False eq_e show ?thesis - by (auto simp:holdents_def depend_exit_unchanged) + by (auto simp:holdents_test depend_exit_unchanged) qed next case (thread_P thread cs) @@ -58,7 +58,7 @@ ultimately show ?thesis by auto qed hence "holdents (e # s) th = holdents s th " - apply (unfold cntCS_def holdents_def eq_e) + apply (unfold cntCS_def holdents_test eq_e) by (unfold step_depend_p[OF vtp], auto) moreover have "holdents s th = {}" proof(rule ih) @@ -101,7 +101,7 @@ qed moreover note neq_th eq_wq ultimately have "holdents (e # s) th = holdents s th" - by (unfold eq_e cntCS_def holdents_def step_depend_v[OF vtv], auto) + by (unfold eq_e cntCS_def holdents_test step_depend_v[OF vtv], auto) moreover have "holdents s th = {}" proof(rule ih) from not_in eq_e show "th \ threads s" by simp @@ -115,13 +115,13 @@ from not_in and eq_e have "th \ threads s" by auto from ih [OF this] and eq_e show ?thesis - apply (unfold eq_e cntCS_def holdents_def) + apply (unfold eq_e cntCS_def holdents_test) by (simp add:depend_set_unchanged) qed next case vt_nil show ?case - by (auto simp:count_def holdents_def s_depend_def wq_def cs_holding_def) + by (auto simp:count_def holdents_test s_depend_def wq_def cs_holding_def) qed qed @@ -1919,7 +1919,7 @@ from tranclE[OF this] obtain cs' where "(Cs cs', Th th) \ depend s'" by (auto simp:s_depend_def) with hdn - have False by (auto simp:holdents_def) + have False by (auto simp:holdents_test) } thus ?thesis by auto qed thus ?thesis diff -r 8ce9a432680b -r e6b13c7b9494 prio/ExtGG.thy --- a/prio/ExtGG.thy Mon Apr 23 08:01:37 2012 +0000 +++ b/prio/ExtGG.thy Mon Apr 30 15:32:34 2012 +0000 @@ -952,6 +952,20 @@ show ?thesis by auto qed +lemma runing_inversion_4: + assumes runing': "th' \ runing (t@s)" + and neq_th: "th' \ th" + shows "th' \ threads s" + and "\detached s th'" + and "cp (t@s) th' = preced th s" +using runing_inversion_3 [OF runing'] + and neq_th + and runing_preced_inversion[OF runing'] +apply(auto simp add: detached_eq[OF vt_s]) +done + + + lemma live: "runing (t@s) \ {}" proof(cases "th \ runing (t@s)") case True thus ?thesis by auto diff -r 8ce9a432680b -r e6b13c7b9494 prio/Paper/Paper.thy --- a/prio/Paper/Paper.thy Mon Apr 23 08:01:37 2012 +0000 +++ b/prio/Paper/Paper.thy Mon Apr 30 15:32:34 2012 +0000 @@ -375,13 +375,6 @@ programmer has to ensure this. - {\bf ??? define detached} - \begin{isabelle}\ \ \ \ \ %%% - @{thm detached_def} - \end{isabelle} - - - Next we introduce the notion of the \emph{current precedence} of a thread @{text th} in a state @{text s}. It is defined as @@ -543,12 +536,22 @@ running, namely the one whose current precedence is equal to the maximum of all ready threads. We use sets to capture both possibilities. We can now also conveniently define the set of resources that are locked by a thread in a - given state. + given state \begin{isabelle}\ \ \ \ \ %%% @{thm holdents_def} \end{isabelle} + \noindent + and also when a thread is detached + + \begin{isabelle}\ \ \ \ \ %%% + @{thm detached_def} + \end{isabelle} + + \noindent + which means that @{text th} neither holds nor waits for a resource in @{text s}. + Finally we can define what a \emph{valid state} is in our model of PIP. For example we cannot expect to be able to exit a thread, if it was not created yet. @@ -1211,6 +1214,18 @@ be recalculated for an event. This information is provided by the lemmas we proved. We confirmened that our observations translate into practice by implementing a PIP-scheduler on top of PINTOS, a small operating system for teaching purposes \cite{PINTOS}. + Our events translate in PINTOS to the following function interface: + + \begin{center} + \begin{tabular}{|l|l|} + \hline + {\bf Event} & {\bf PINTOS function} \\ + \hline + @{text Create} & \\ + @{text Exit} & \\ + \end{tabular} + \end{center} + *} section {* Conclusion *} diff -r 8ce9a432680b -r e6b13c7b9494 prio/PrioG.thy --- a/prio/PrioG.thy Mon Apr 23 08:01:37 2012 +0000 +++ b/prio/PrioG.thy Mon Apr 30 15:32:34 2012 +0000 @@ -1114,7 +1114,7 @@ apply (ind_cases "step s (Exit th')") apply (auto simp:runing_def readys_def s_holding_def s_waiting_def holdents_def s_depend_def s_holding_def cs_holding_def) - by (fold wq_def, auto) + done next case (V th' cs') show ?thesis @@ -1354,7 +1354,7 @@ shows "holdents (P th cs#s) th = holdents s th \ {cs}" proof - from assms show ?thesis - unfolding holdents_def step_depend_p[OF vt] by auto + unfolding holdents_test step_depend_p[OF vt] by (auto) qed lemma step_holdents_p_eq: @@ -1364,7 +1364,7 @@ shows "holdents (P th cs#s) th = holdents s th" proof - from assms show ?thesis - unfolding holdents_def step_depend_p[OF vt] by auto + unfolding holdents_test step_depend_p[OF vt] by auto qed @@ -1386,7 +1386,7 @@ ultimately have "x \ (\(x, y). the_cs x) ` depend s" by simp } thus ?thesis by auto qed - ultimately show ?thesis by (unfold holdents_def, auto intro:finite_subset) + ultimately show ?thesis by (unfold holdents_test, auto intro:finite_subset) qed lemma cntCS_v_dec: @@ -1396,12 +1396,12 @@ proof - from step_back_step[OF vtv] have cs_in: "cs \ holdents s thread" - apply (cases, unfold holdents_def s_depend_def, simp) + apply (cases, unfold holdents_test s_depend_def, simp) by (unfold cs_holding_def s_holding_def wq_def, auto) moreover have cs_not_in: "(holdents (V thread cs#s) thread) = holdents s thread - {cs}" apply (insert wq_distinct[OF step_back_vt[OF vtv], of cs]) - apply (unfold holdents_def, unfold step_depend_v[OF vtv], + apply (unfold holdents_test, unfold step_depend_v[OF vtv], auto simp:next_th_def) proof - fix rest @@ -1492,7 +1492,7 @@ from eq_e have eq_cnp: "cntP (e#s) th = cntP s th" by (simp add:cntP_def count_def) from eq_e have eq_cnv: "cntV (e#s) th = cntV s th" by (simp add:cntV_def count_def) have eq_cncs: "cntCS (e#s) th = cntCS s th" - unfolding cntCS_def holdents_def + unfolding cntCS_def holdents_test by (simp add:depend_create_unchanged eq_e) { assume "th \ thread" with eq_readys eq_e @@ -1517,7 +1517,7 @@ from eq_e have eq_cnp: "cntP (e#s) th = cntP s th" by (simp add:cntP_def count_def) from eq_e have eq_cnv: "cntV (e#s) th = cntV s th" by (simp add:cntV_def count_def) have eq_cncs: "cntCS (e#s) th = cntCS s th" - unfolding cntCS_def holdents_def + unfolding cntCS_def holdents_test by (simp add:depend_exit_unchanged eq_e) { assume "th \ thread" with eq_e @@ -1559,7 +1559,7 @@ apply (erule_tac x = cs in allE, auto) by (case_tac "(wq_fun (schs s) cs)", auto) moreover from neq_th eq_e have "cntCS (e # s) th = cntCS s th" - apply (simp add:cntCS_def holdents_def) + apply (simp add:cntCS_def holdents_test) by (unfold step_depend_p [OF vtp], auto) moreover from eq_e neq_th have "cntP (e # s) th = cntP s th" by (simp add:cntP_def count_def) @@ -1594,7 +1594,7 @@ proof(rule card_insert) from finite_holding [OF vt, of thread] show " finite {cs. (Cs cs, Th thread) \ depend s}" - by (unfold holdents_def, simp) + by (unfold holdents_test, simp) qed moreover have "?R - {cs} = ?R" proof - @@ -1609,7 +1609,7 @@ qed thus ?thesis apply (unfold eq_e eq_th cntCS_def) - apply (simp add: holdents_def) + apply (simp add: holdents_test) by (unfold step_depend_p [OF vtp], auto simp:True) qed moreover from is_runing have "th \ readys s" @@ -1637,7 +1637,7 @@ moreover from is_runing have "th \ threads (e#s)" by (unfold eq_e, auto simp:runing_def readys_def eq_th) moreover have "cntCS (e # s) th = cntCS s th" - apply (unfold cntCS_def holdents_def eq_e step_depend_p[OF vtp]) + apply (unfold cntCS_def holdents_test eq_e step_depend_p[OF vtp]) by (auto simp:False) moreover note eq_cnp eq_cnv ih[of th] moreover from is_runing have "th \ readys s" @@ -1734,7 +1734,7 @@ apply (insert step_back_vt[OF vtv]) by (unfold eq_e, rule readys_v_eq [OF _ neq_th eq_wq False], auto) moreover have "cntCS (e#s) th = cntCS s th" - apply (insert neq_th, unfold eq_e cntCS_def holdents_def step_depend_v[OF vtv], auto) + apply (insert neq_th, unfold eq_e cntCS_def holdents_test step_depend_v[OF vtv], auto) proof - have "{csa. (Cs csa, Th th) \ depend s \ csa = cs \ next_th s thread cs th} = {cs. (Cs cs, Th th) \ depend s}" @@ -1796,7 +1796,7 @@ from eq_wq and th_in and neq_hd have "(holdents (e # s) th) = (holdents s th)" apply (unfold eq_e step_depend_v[OF vtv], - auto simp:next_th_def eq_set s_depend_def holdents_def wq_def + auto simp:next_th_def eq_set s_depend_def holdents_test wq_def Let_def cs_holding_def) by (insert wq_distinct[OF step_back_vt[OF vtv], of cs], auto simp:wq_def) thus ?thesis by (simp add:cntCS_def) @@ -1861,7 +1861,7 @@ ultimately show ?thesis using ih by auto qed moreover from True neq_th have "cntCS (e # s) th = 1 + cntCS s th" - apply (unfold cntCS_def holdents_def eq_e step_depend_v[OF vtv], auto) + apply (unfold cntCS_def holdents_test eq_e step_depend_v[OF vtv], auto) proof - show "card {csa. (Cs csa, Th th) \ depend s \ csa = cs} = Suc (card {cs. (Cs cs, Th th) \ depend s})" @@ -1903,7 +1903,7 @@ from eq_e have eq_cnp: "cntP (e#s) th = cntP s th" by (simp add:cntP_def count_def) from eq_e have eq_cnv: "cntV (e#s) th = cntV s th" by (simp add:cntV_def count_def) have eq_cncs: "cntCS (e#s) th = cntCS s th" - unfolding cntCS_def holdents_def + unfolding cntCS_def holdents_test by (simp add:depend_set_unchanged eq_e) from eq_e have eq_readys: "readys (e#s) = readys s" by (simp add:readys_def cs_waiting_def s_waiting_def wq_def, @@ -1930,7 +1930,7 @@ case vt_nil show ?case by (unfold cntP_def cntV_def cntCS_def, - auto simp:count_def holdents_def s_depend_def wq_def cs_holding_def) + auto simp:count_def holdents_test s_depend_def wq_def cs_holding_def) qed qed @@ -1953,7 +1953,7 @@ assume eq_e: "e = Create thread prio" and not_in': "thread \ threads s" have "cntCS (e # s) th = cntCS s th" - apply (unfold eq_e cntCS_def holdents_def) + apply (unfold eq_e cntCS_def holdents_test) by (simp add:depend_create_unchanged) moreover have "th \ threads s" proof - @@ -1965,7 +1965,7 @@ assume eq_e: "e = Exit thread" and nh: "holdents s thread = {}" have eq_cns: "cntCS (e # s) th = cntCS s th" - apply (unfold eq_e cntCS_def holdents_def) + apply (unfold eq_e cntCS_def holdents_test) by (simp add:depend_exit_unchanged) show ?thesis proof(cases "th = thread") @@ -1991,7 +1991,7 @@ ultimately show ?thesis by auto qed hence "cntCS (e # s) th = cntCS s th " - apply (unfold cntCS_def holdents_def eq_e) + apply (unfold cntCS_def holdents_test eq_e) by (unfold step_depend_p[OF vtp], auto) moreover have "cntCS s th = 0" proof(rule ih) @@ -2034,7 +2034,7 @@ qed moreover note neq_th eq_wq ultimately have "cntCS (e # s) th = cntCS s th" - by (unfold eq_e cntCS_def holdents_def step_depend_v[OF vtv], auto) + by (unfold eq_e cntCS_def holdents_test step_depend_v[OF vtv], auto) moreover have "cntCS s th = 0" proof(rule ih) from not_in eq_e show "th \ threads s" by simp @@ -2048,14 +2048,14 @@ from not_in and eq_e have "th \ threads s" by auto from ih [OF this] and eq_e show ?thesis - apply (unfold eq_e cntCS_def holdents_def) + apply (unfold eq_e cntCS_def holdents_test) by (simp add:depend_set_unchanged) qed next case vt_nil show ?case by (unfold cntCS_def, - auto simp:count_def holdents_def s_depend_def wq_def cs_holding_def) + auto simp:count_def holdents_test s_depend_def wq_def cs_holding_def) qed qed @@ -2425,10 +2425,10 @@ moreover have "finite {cs. (Cs cs, Th th) \ depend s}" proof - from finite_holding[OF vt, of th] show ?thesis - by (simp add:holdents_def) + by (simp add:holdents_test) qed ultimately have h: "{cs. (Cs cs, Th th) \ depend s} = {}" - by (unfold cntCS_def holdents_def cs_dependents_def, auto) + by (unfold cntCS_def holdents_test cs_dependents_def, auto) show ?thesis proof(unfold cs_dependents_def) { assume "{th'. (Th th', Th th) \ (depend (wq s))\<^sup>+} \ {}" @@ -2773,10 +2773,20 @@ by (rule image_subsetI, auto intro:h[symmetric]) qed + definition detached :: "state \ thread \ bool" - where "detached s th \ (Th th \ Field (depend s))" + where "detached s th \ (\(\ cs. holding s th cs)) \ (\(\cs. waiting s th cs))" + -thm Field_def +lemma detached_test: + shows "detached s th = (Th th \ Field (depend s))" +apply(simp add: detached_def Field_def) +apply(simp add: s_depend_def) +apply(simp add: s_holding_abv s_waiting_abv) +apply(simp add: Domain_iff Range_iff) +apply(simp add: wq_def) +apply(auto) +done lemma detached_intro: fixes s th @@ -2796,7 +2806,7 @@ assume "th \ threads s" with range_in[OF vt] dm_depend_threads[OF vt] show ?thesis - by (auto simp:detached_def Field_def Domain_def Range_def) + by (auto simp add: detached_def s_depend_def s_waiting_abv s_holding_abv wq_def Domain_iff Range_iff) next assume "th \ readys s" moreover have "Th th \ Range (depend s)" @@ -2805,15 +2815,13 @@ have "holdents s th = {}" by (simp add:cntCS_def) thus ?thesis - apply(auto simp:holdents_def) + apply(auto simp:holdents_test) apply(case_tac a) - apply(auto simp:holdents_def s_depend_def) + apply(auto simp:holdents_test s_depend_def) done qed ultimately show ?thesis - apply (auto simp:detached_def Field_def Domain_def readys_def) - apply (case_tac b, auto simp:s_depend_def) - by (erule_tac x = "nat" in allE, simp add: eq_waiting) + by (auto simp add: detached_def s_depend_def s_waiting_abv s_holding_abv wq_def readys_def) qed qed @@ -2829,7 +2837,8 @@ have cncs_z: "cntCS s th = 0" proof - from dtc have "holdents s th = {}" - by (unfold detached_def holdents_def, auto simp:Field_def Domain_def Range_def) + unfolding detached_def holdents_test s_depend_def + by (simp add: s_waiting_abv wq_def s_holding_abv Domain_iff Range_iff) thus ?thesis by (auto simp:cntCS_def) qed show ?thesis diff -r 8ce9a432680b -r e6b13c7b9494 prio/PrioGDef.thy --- a/prio/PrioGDef.thy Mon Apr 23 08:01:37 2012 +0000 +++ b/prio/PrioGDef.thy Mon Apr 30 15:32:34 2012 +0000 @@ -361,7 +361,15 @@ @{text "th"} in state @{text "s"}. *} definition holdents :: "state \ thread \ cs set" - where "holdents s th \ {cs . (Cs cs, Th th) \ depend s}" + where "holdents s th \ {cs . holding s th cs}" + +lemma holdents_test: + "holdents s th = {cs . (Cs cs, Th th) \ depend s}" +unfolding holdents_def +unfolding s_depend_def +unfolding s_holding_abv +unfolding wq_def +by (simp) text {* \noindent @{text "cntCS s th"} returns the number of resources held by thread @{text "th"} in diff -r 8ce9a432680b -r e6b13c7b9494 prio/paper.pdf Binary file prio/paper.pdf has changed