diff -r b85cfbd58f59 -r 0fd478e14e87 CpsG.thy --- a/CpsG.thy Fri Oct 30 20:40:11 2015 +0800 +++ b/CpsG.thy Thu Dec 03 14:34:00 2015 +0800 @@ -3,9 +3,47 @@ after every system call (or system operation) *} theory CpsG -imports PrioG Max +imports PrioG Max RTree +begin + +locale pip = + fixes s + assumes vt: "vt s" + +context pip begin +interpretation rtree_RAG: rtree "RAG s" +proof + show "single_valued (RAG s)" + apply (intro_locales) + by (unfold single_valued_def, auto intro: unique_RAG[OF vt]) + + show "acyclic (RAG s)" + by (rule acyclic_RAG[OF vt]) +qed + +end + + + +definition "the_preced s th = preced th s" + +lemma cp_alt_def: + "cp s th = + Max ((the_preced s) ` {th'. Th th' \ (subtree (RAG s) (Th th))})" +proof - + have "Max (the_preced s ` ({th} \ dependants (wq s) th)) = + Max (the_preced s ` {th'. Th th' \ subtree (RAG s) (Th th)})" + (is "Max (_ ` ?L) = Max (_ ` ?R)") + proof - + have "?L = ?R" + by (auto dest:rtranclD simp:cs_dependants_def cs_RAG_def s_RAG_def subtree_def) + thus ?thesis by simp + qed + thus ?thesis by (unfold cp_eq_cpreced cpreced_def, fold the_preced_def, simp) +qed + lemma eq_dependants: "dependants (wq s) = dependants s" by (simp add: s_dependants_abv wq_def) @@ -575,9 +613,11 @@ qed qed +-- {* A useless definition *} definition cps:: "state \ (thread \ precedence) set" where "cps s = {(th, cp s th) | th . th \ threads s}" + text {* (* ddd *) One beauty of our modelling is that we follow the definitional extension tradition of HOL. The benefit of such a concise and miniature model is that large number of intuitively @@ -620,6 +660,27 @@ context step_set_cps begin +interpretation rtree_RAGs: rtree "RAG s" +proof + show "single_valued (RAG s)" + apply (intro_locales) + by (unfold single_valued_def, auto intro: unique_RAG[OF vt_s]) + + show "acyclic (RAG s)" + by (rule acyclic_RAG[OF vt_s]) +qed + +interpretation rtree_RAGs': rtree "RAG s'" +proof + show "single_valued (RAG s')" + apply (intro_locales) + by (unfold single_valued_def, + auto intro: unique_RAG[OF step_back_vt[OF vt_s[unfolded s_def]]]) + + show "acyclic (RAG s')" + by (rule acyclic_RAG[OF step_back_vt[OF vt_s[unfolded s_def]]]) +qed + text {* (* ddd *) The following lemma confirms that @{text "Set"}-operating only changes the precedence of initiating thread. @@ -732,305 +793,73 @@ shows "cp s th' = cp s' th'" by (rule eq_cp_pre[OF assms no_dependants]) - -text {* (* ddd *) \noindent - The following @{text "eq_up"} was originally designed to save the recalculations - of current precedence going upstream from thread @{text "th"} can stop earlier. - If at a certain point along way, the recalculation results in the same - result, the recalculation can stop there. - This lemma is obsolete because we found that @{text "th"} is not contained in - any thread's dependants set. +end - The foregoing lemma says only those threads which -*} -lemma eq_up: - fixes th' th'' - assumes dp1: "th \ dependants s th'" - and dp2: "th' \ dependants s th''" - and eq_cps: "cp s th' = cp s' th'" - shows "cp s th'' = cp s' th''" -proof - - from dp2 - have "(Th th', Th th'') \ (RAG (wq s))\<^sup>+" by (simp add:s_dependants_def) - from RAG_child[OF vt_s this[unfolded eq_RAG]] - have ch_th': "(Th th', Th th'') \ (child s)\<^sup>+" . - moreover { fix n th'' - have "\(Th th', n) \ (child s)^+\ \ - (\ th'' . n = Th th'' \ cp s th'' = cp s' th'')" - proof(erule trancl_induct, auto) - fix y th'' - assume y_ch: "(y, Th th'') \ child s" - and ih: "\th''. y = Th th'' \ cp s th'' = cp s' th''" - and ch': "(Th th', y) \ (child s)\<^sup>+" - from y_ch obtain thy where eq_y: "y = Th thy" by (auto simp:child_def) - with ih have eq_cpy:"cp s thy = cp s' thy" by blast - from dp1 have "(Th th, Th th') \ (RAG s)^+" by (auto simp:s_dependants_def eq_RAG) - moreover from child_RAG_p[OF ch'] and eq_y - have "(Th th', Th thy) \ (RAG s)^+" by simp - ultimately have dp_thy: "(Th th, Th thy) \ (RAG s)^+" by auto - show "cp s th'' = cp s' th''" - apply (subst cp_rec[OF vt_s]) - proof - - have "preced th'' s = preced th'' s'" - proof(rule eq_preced) - show "th'' \ th" - proof - assume "th'' = th" - with dp_thy y_ch[unfolded eq_y] - have "(Th th, Th th) \ (RAG s)^+" - by (auto simp:child_def) - with wf_trancl[OF wf_RAG[OF vt_s]] - show False by auto - qed - qed - moreover { - fix th1 - assume th1_in: "th1 \ children s th''" - have "cp s th1 = cp s' th1" - proof(cases "th1 = thy") - case True - with eq_cpy show ?thesis by simp - next - case False - have neq_th1: "th1 \ th" - proof - assume eq_th1: "th1 = th" - with dp_thy have "(Th th1, Th thy) \ (RAG s)^+" by simp - from children_no_dep[OF vt_s _ _ this] and - th1_in y_ch eq_y show False by (auto simp:children_def) - qed - have "th \ dependants s th1" - proof - assume h:"th \ dependants s th1" - from eq_y dp_thy have "th \ dependants s thy" by (auto simp:s_dependants_def eq_RAG) - from dependants_child_unique[OF vt_s _ _ h this] - th1_in y_ch eq_y have "th1 = thy" by (auto simp:children_def child_def) - with False show False by auto - qed - from eq_cp_pre[OF neq_th1 this] - show ?thesis . - qed - } - ultimately have "{preced th'' s} \ (cp s ` children s th'') = - {preced th'' s'} \ (cp s' ` children s th'')" by (auto simp:image_def) - moreover have "children s th'' = children s' th''" - by (unfold children_def child_def s_def RAG_set_unchanged, simp) - ultimately show "Max ({preced th'' s} \ cp s ` children s th'') = cp s' th''" - by (simp add:cp_rec[OF step_back_vt[OF vt_s[unfolded s_def]]]) - qed - next - fix th'' - assume dp': "(Th th', Th th'') \ child s" - show "cp s th'' = cp s' th''" - apply (subst cp_rec[OF vt_s]) - proof - - have "preced th'' s = preced th'' s'" - proof(rule eq_preced) - show "th'' \ th" - proof - assume "th'' = th" - with dp1 dp' - have "(Th th, Th th) \ (RAG s)^+" - by (auto simp:child_def s_dependants_def eq_RAG) - with wf_trancl[OF wf_RAG[OF vt_s]] - show False by auto - qed - qed - moreover { - fix th1 - assume th1_in: "th1 \ children s th''" - have "cp s th1 = cp s' th1" - proof(cases "th1 = th'") - case True - with eq_cps show ?thesis by simp - next - case False - have neq_th1: "th1 \ th" - proof - assume eq_th1: "th1 = th" - with dp1 have "(Th th1, Th th') \ (RAG s)^+" - by (auto simp:s_dependants_def eq_RAG) - from children_no_dep[OF vt_s _ _ this] - th1_in dp' - show False by (auto simp:children_def) - qed - thus ?thesis - proof(rule eq_cp_pre) - show "th \ dependants s th1" - proof - assume "th \ dependants s th1" - from dependants_child_unique[OF vt_s _ _ this dp1] - th1_in dp' have "th1 = th'" - by (auto simp:children_def) - with False show False by auto - qed - qed - qed - } - ultimately have "{preced th'' s} \ (cp s ` children s th'') = - {preced th'' s'} \ (cp s' ` children s th'')" by (auto simp:image_def) - moreover have "children s th'' = children s' th''" - by (unfold children_def child_def s_def RAG_set_unchanged, simp) - ultimately show "Max ({preced th'' s} \ cp s ` children s th'') = cp s' th''" - by (simp add:cp_rec[OF step_back_vt[OF vt_s[unfolded s_def]]]) - qed - qed - } - ultimately show ?thesis by auto -qed - -text {* (* ddd *) - For those @{text "th''"}, @{text "th \ dependants s th''"} means that - the current precedence of such @{text "th''"} might possibly be boosted if the - current precedence of @{text "th"} somehow get raised. The following lemma - says that if the resetting of its own priority by thread @{text "th"} does not - change its current precedence, then the current precedence of such @{text "th''"} - will remain unchanged. The situation such that @{text "th"}'s current - precedence does not change with the resetting of its priority might happen in many - different cases. For example, if the current precedence of @{text "th"} is already an inherited one, - the lowering of its priority will not change its current precedence, and the increasing - of its priority will not change its current precedence neither, if - incidental rising of its own precedence is not large enough to surpass the inherited precedence. +text {* + The following @{text "step_v_cps"} is the locale for @{text "V"}-operation. *} -lemma eq_up_self: - fixes th' th'' - assumes dp: "th \ dependants s th''" - and eq_cps: "cp s th = cp s' th" - shows "cp s th'' = cp s' th''" -proof - - from dp - have "(Th th, Th th'') \ (RAG (wq s))\<^sup>+" by (simp add:s_dependants_def) - from RAG_child[OF vt_s this[unfolded eq_RAG]] - have ch_th': "(Th th, Th th'') \ (child s)\<^sup>+" . - moreover { fix n th'' - have "\(Th th, n) \ (child s)^+\ \ - (\ th'' . n = Th th'' \ cp s th'' = cp s' th'')" - proof(erule trancl_induct, auto) - fix y th'' - assume y_ch: "(y, Th th'') \ child s" - and ih: "\th''. y = Th th'' \ cp s th'' = cp s' th''" - and ch': "(Th th, y) \ (child s)\<^sup>+" - from y_ch obtain thy where eq_y: "y = Th thy" by (auto simp:child_def) - with ih have eq_cpy:"cp s thy = cp s' thy" by blast - from child_RAG_p[OF ch'] and eq_y - have dp_thy: "(Th th, Th thy) \ (RAG s)^+" by simp - show "cp s th'' = cp s' th''" - apply (subst cp_rec[OF vt_s]) - proof - - have "preced th'' s = preced th'' s'" - proof(rule eq_preced) - show "th'' \ th" - proof - assume "th'' = th" - with dp_thy y_ch[unfolded eq_y] - have "(Th th, Th th) \ (RAG s)^+" - by (auto simp:child_def) - with wf_trancl[OF wf_RAG[OF vt_s]] - show False by auto - qed - qed - moreover { - fix th1 - assume th1_in: "th1 \ children s th''" - have "cp s th1 = cp s' th1" - proof(cases "th1 = thy") - case True - with eq_cpy show ?thesis by simp - next - case False - have neq_th1: "th1 \ th" - proof - assume eq_th1: "th1 = th" - with dp_thy have "(Th th1, Th thy) \ (RAG s)^+" by simp - from children_no_dep[OF vt_s _ _ this] and - th1_in y_ch eq_y show False by (auto simp:children_def) - qed - have "th \ dependants s th1" - proof - assume h:"th \ dependants s th1" - from eq_y dp_thy have "th \ dependants s thy" by (auto simp:s_dependants_def eq_RAG) - from dependants_child_unique[OF vt_s _ _ h this] - th1_in y_ch eq_y have "th1 = thy" by (auto simp:children_def child_def) - with False show False by auto - qed - from eq_cp_pre[OF neq_th1 this] - show ?thesis . - qed - } - ultimately have "{preced th'' s} \ (cp s ` children s th'') = - {preced th'' s'} \ (cp s' ` children s th'')" by (auto simp:image_def) - moreover have "children s th'' = children s' th''" - by (unfold children_def child_def s_def RAG_set_unchanged, simp) - ultimately show "Max ({preced th'' s} \ cp s ` children s th'') = cp s' th''" - by (simp add:cp_rec[OF step_back_vt[OF vt_s[unfolded s_def]]]) - qed - next - fix th'' - assume dp': "(Th th, Th th'') \ child s" - show "cp s th'' = cp s' th''" - apply (subst cp_rec[OF vt_s]) - proof - - have "preced th'' s = preced th'' s'" - proof(rule eq_preced) - show "th'' \ th" - proof - assume "th'' = th" - with dp dp' - have "(Th th, Th th) \ (RAG s)^+" - by (auto simp:child_def s_dependants_def eq_RAG) - with wf_trancl[OF wf_RAG[OF vt_s]] - show False by auto - qed - qed - moreover { - fix th1 - assume th1_in: "th1 \ children s th''" - have "cp s th1 = cp s' th1" - proof(cases "th1 = th") - case True - with eq_cps show ?thesis by simp - next - case False - assume neq_th1: "th1 \ th" - thus ?thesis - proof(rule eq_cp_pre) - show "th \ dependants s th1" - proof - assume "th \ dependants s th1" - hence "(Th th, Th th1) \ (RAG s)^+" by (auto simp:s_dependants_def eq_RAG) - from children_no_dep[OF vt_s _ _ this] - and th1_in dp' show False - by (auto simp:children_def) - qed - qed - qed - } - ultimately have "{preced th'' s} \ (cp s ` children s th'') = - {preced th'' s'} \ (cp s' ` children s th'')" by (auto simp:image_def) - moreover have "children s th'' = children s' th''" - by (unfold children_def child_def s_def RAG_set_unchanged, simp) - ultimately show "Max ({preced th'' s} \ cp s ` children s th'') = cp s' th''" - by (simp add:cp_rec[OF step_back_vt[OF vt_s[unfolded s_def]]]) - qed - qed - } - ultimately show ?thesis by auto -qed -end - locale step_v_cps = - fixes s' th cs s - defines s_def : "s \ (V th cs#s')" + -- {* @{text "th"} is the initiating thread *} + -- {* @{text "cs"} is the critical resource release by the @{text "V"}-operation *} + fixes s' th cs s -- {* @{text "s'"} is the state before operation*} + defines s_def : "s \ (V th cs#s')" -- {* @{text "s"} is the state after operation*} + -- {* @{text "s"} is assumed to be valid, which implies the validity of @{text "s'"} *} assumes vt_s: "vt s" +text {* + The following @{text "step_v_cps_nt"} is the sub-locale for @{text "V"}-operation, + which represents the case when there is another thread @{text "th'"} + to take over the critical resource released by the initiating thread @{text "th"}. +*} locale step_v_cps_nt = step_v_cps + fixes th' - assumes nt: "next_th s' th cs th'" + -- {* @{text "th'"} is assumed to take over @{text "cs"} *} + assumes nt: "next_th s' th cs th'" context step_v_cps_nt begin +text {* + Lemma @{text "RAG_s"} confirms the change of RAG: + two edges removed and one added, as shown by the following diagram. +*} + +(* + RAG before the V-operation + th1 ----| + | + th' ----| + |----> cs -----| + th2 ----| | + | | + th3 ----| | + |------> th + th4 ----| | + | | + th5 ----| | + |----> cs'-----| + th6 ----| + | + th7 ----| + + RAG after the V-operation + th1 ----| + | + |----> cs ----> th' + th2 ----| + | + th3 ----| + + th4 ----| + | + th5 ----| + |----> cs'----> th + th6 ----| + | + th7 ----| +*) + lemma RAG_s: "RAG s = (RAG s' - {(Cs cs, Th th), (Th th', Cs cs)}) \ {(Cs cs, Th th')}" @@ -1039,12 +868,16 @@ and nt show ?thesis by (auto intro:next_th_unique) qed +text {* + Lemma @{text "dependants_kept"} shows only @{text "th"} and @{text "th'"} + have their dependants changed. +*} lemma dependants_kept: fixes th'' assumes neq1: "th'' \ th" and neq2: "th'' \ th'" shows "dependants (wq s) th'' = dependants (wq s') th''" -proof(auto) +proof(auto) (* ccc *) fix x assume "x \ dependants (wq s) th''" hence dp: "(Th x, Th th'') \ (RAG s)^+" @@ -1529,6 +1362,7 @@ show ?thesis by (simp add:s_def) qed + lemma eq_child_left: assumes nd: "(Th th, Th th') \ (child s)^+" shows "(n1, Th th') \ (child s)^+ \ (n1, Th th') \ (child s')^+"