# HG changeset patch # User xingyuan zhang # Date 1446208811 -28800 # Node ID b85cfbd58f59116aff4e080adea66cdf27a1d72d # Parent fee01b2858a2c48358149e8062f32f68ee32078c Comments for Set-operation finished diff -r fee01b2858a2 -r b85cfbd58f59 CpsG.thy --- a/CpsG.thy Sat Oct 17 16:14:30 2015 +0800 +++ b/CpsG.thy Fri Oct 30 20:40:11 2015 +0800 @@ -6,6 +6,9 @@ imports PrioG Max begin +lemma eq_dependants: "dependants (wq s) = dependants s" + by (simp add: s_dependants_abv wq_def) + (* obvious lemma *) lemma not_thread_holdents: fixes th s @@ -312,14 +315,14 @@ qed qed -text {* (* ??? *) +text {* (* ddd *) *} lemma child_RAG_eq: assumes vt: "vt s" shows "(Th th1, Th th2) \ (child s)^+ \ (Th th1, Th th2) \ (RAG s)^+" by (auto intro: RAG_child[OF vt] child_RAG_p) -text {* (* ??? *) +text {* (* ddd *) *} lemma children_no_dep: fixes s th th1 th2 th3 @@ -354,7 +357,7 @@ qed qed -text {* (* ??? *) +text {* (* ddd *) *} lemma unique_RAG_p: assumes vt: "vt s" @@ -367,7 +370,7 @@ show "\a b c. \(a, b) \ RAG s; (a, c) \ RAG s\ \ b = c" by auto qed -text {* (* ??? *) +text {* (* ddd *) *} lemma dependants_child_unique: fixes s th th1 th2 th3 @@ -405,7 +408,7 @@ apply (unfold children_def) by (metis assms(2) children_def RAG_children eq_RAG) -text {* (* ??? *) +text {* (* ddd *) *} lemma dependants_expand: assumes "vt s" @@ -447,7 +450,9 @@ shows "(\x \ A. {f y | y. Q y x}) = ({f y | y. (\x \ A. Q y x)})" by auto -text {* (* ??? *) +text {* (* ddd *) + This is the recursive equation used to compute the current precedence of + a thread (the @{text "th"}) here. *} lemma cp_rec: fixes s th @@ -514,17 +519,112 @@ qed qed +lemma next_waiting: + assumes vt: "vt s" + and nxt: "next_th s th cs th'" + shows "waiting s th' cs" +proof - + from assms show ?thesis + apply (auto simp:next_th_def s_waiting_def[folded wq_def]) + proof - + fix rest + assume ni: "hd (SOME q. distinct q \ set q = set rest) \ set rest" + and eq_wq: "wq s cs = th # rest" + and ne: "rest \ []" + have "set (SOME q. distinct q \ set q = set rest) = set rest" + proof(rule someI2) + from wq_distinct[OF vt, of cs] eq_wq + show "distinct rest \ set rest = set rest" by auto + next + show "\x. distinct x \ set x = set rest \ set x = set rest" by auto + qed + with ni + have "hd (SOME q. distinct q \ set q = set rest) \ set (SOME q. distinct q \ set q = set rest)" + by simp + moreover have "(SOME q. distinct q \ set q = set rest) \ []" + proof(rule someI2) + from wq_distinct[OF vt, of cs] eq_wq + show "distinct rest \ set rest = set rest" by auto + next + from ne show "\x. distinct x \ set x = set rest \ x \ []" by auto + qed + ultimately show "hd (SOME q. distinct q \ set q = set rest) = th" by auto + next + fix rest + assume eq_wq: "wq s cs = hd (SOME q. distinct q \ set q = set rest) # rest" + and ne: "rest \ []" + have "(SOME q. distinct q \ set q = set rest) \ []" + proof(rule someI2) + from wq_distinct[OF vt, of cs] eq_wq + show "distinct rest \ set rest = set rest" by auto + next + from ne show "\x. distinct x \ set x = set rest \ x \ []" by auto + qed + hence "hd (SOME q. distinct q \ set q = set rest) \ set (SOME q. distinct q \ set q = set rest)" + by auto + moreover have "set (SOME q. distinct q \ set q = set rest) = set rest" + proof(rule someI2) + from wq_distinct[OF vt, of cs] eq_wq + show "distinct rest \ set rest = set rest" by auto + next + show "\x. distinct x \ set x = set rest \ set x = set rest" by auto + qed + ultimately have "hd (SOME q. distinct q \ set q = set rest) \ set rest" by simp + with eq_wq and wq_distinct[OF vt, of cs] + show False by auto + qed +qed + 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 + obvious facts are derived as lemmas, rather than asserted as axioms. +*} + +text {* + However, the lemmas in the forthcoming several locales are no longer + obvious. These lemmas show how the current precedences should be recalculated + after every execution step (in our model, every step is represented by an event, + which in turn, represents a system call, or operation). Each operation is + treated in a separate locale. + + The complication of current precedence recalculation comes + because the changing of RAG needs to be taken into account, + in addition to the changing of precedence. + The reason RAG changing affects current precedence is that, + according to the definition, current precedence + of a thread is the maximum of the precedences of its dependants, + where the dependants are defined in terms of RAG. + + Therefore, each operation, lemmas concerning the change of the precedences + and RAG are derived first, so that the lemmas about + current precedence recalculation can be based on. +*} + +text {* (* ddd *) + The following locale @{text "step_set_cps"} investigates the recalculation + after the @{text "Set"} operation. +*} locale step_set_cps = fixes s' th prio s - defines s_def : "s \ (Set th prio#s')" + -- {* @{text "s'"} is the system state before the operation *} + -- {* @{text "s"} is the system state after the operation *} + defines s_def : "s \ (Set th prio#s')" + -- {* @{text "s"} is assumed to be a legitimate state, from which + the legitimacy of @{text "s"} can be derived. *} assumes vt_s: "vt s" context step_set_cps begin +text {* (* ddd *) + The following lemma confirms that @{text "Set"}-operating only changes the precedence + of initiating thread. +*} + lemma eq_preced: fixes th' assumes "th' \ th" @@ -534,69 +634,115 @@ by (unfold s_def, auto simp:preced_def) qed +text {* (* ddd *) + The following lemma assures that the resetting of priority does not change the RAG. +*} + lemma eq_dep: "RAG s = RAG s'" by (unfold s_def RAG_set_unchanged, auto) +text {* + Th following lemma @{text "eq_cp_pre"} circumscribe a rough range of recalculation. + It says, thread other than the initiating thread @{text "th"} does not need recalculation + unless it lies upstream of @{text "th"} in the RAG. + + The reason behind this lemma is that: + the change of precedence of one thread can only affect it's upstream threads, according to + lemma @{text "eq_preced"}. Since the only thread which might change precedence is + @{text "th"}, so only @{text "th"} and its upstream threads need recalculation. + (* ccc *) +*} + lemma eq_cp_pre: fixes th' assumes neq_th: "th' \ th" and nd: "th \ dependants s th'" shows "cp s th' = cp s' th'" - apply (unfold cp_eq_cpreced cpreced_def) proof - - have eq_dp: "\ th. dependants (wq s) th = dependants (wq s') th" - by (unfold cs_dependants_def, auto simp:eq_dep eq_RAG) - moreover { - fix th1 - assume "th1 \ {th'} \ dependants (wq s') th'" - hence "th1 = th' \ th1 \ dependants (wq s') th'" by auto - hence "preced th1 s = preced th1 s'" - proof - assume "th1 = th'" - with eq_preced[OF neq_th] - show "preced th1 s = preced th1 s'" by simp - next - assume "th1 \ dependants (wq s') th'" - with nd and eq_dp have "th1 \ th" - by (auto simp:eq_RAG cs_dependants_def s_dependants_def eq_dep) - from eq_preced[OF this] show "preced th1 s = preced th1 s'" by simp - qed - } ultimately have "((\th. preced th s) ` ({th'} \ dependants (wq s) th')) = - ((\th. preced th s') ` ({th'} \ dependants (wq s') th'))" - by (auto simp:image_def) - thus "Max ((\th. preced th s) ` ({th'} \ dependants (wq s) th')) = - Max ((\th. preced th s') ` ({th'} \ dependants (wq s') th'))" by simp + -- {* This is what we need to prove after expanding the definition of @{text "cp"} *} + have "Max ((\th. preced th s) ` ({th'} \ dependants (wq s) th')) = + Max ((\th. preced th s') ` ({th'} \ dependants (wq s') th'))" + (is "Max (?f1 ` ({th'} \ ?A)) = Max (?f2 ` ({th'} \ ?B))") + proof - + -- {* Since RAG is not changed by @{text "Set"}-operation, the dependants of + any threads are not changed, this is one of key facts underpinning this + lemma *} + have eq_ab: "?A = ?B" by (unfold cs_dependants_def, auto simp:eq_dep eq_RAG) + have "(?f1 ` ({th'} \ ?A)) = (?f2 ` ({th'} \ ?B))" + proof(rule image_cong) + show "{th'} \ ?A = {th'} \ ?B" by (simp only:eq_ab) + next + fix x + assume x_in: "x \ {th'} \ ?B" + show "?f1 x = ?f2 x" + proof(rule eq_preced) -- {* The other key fact underpinning this lemma is @{text "eq_preced"} *} + from x_in[folded eq_ab, unfolded eq_dependants] + have "x \ {th'} \ dependants s th'" . + thus "x \ th" + proof + assume "x \ {th'}" + with `th' \ th` show ?thesis by simp + next + assume "x \ dependants s th'" + with `th \ dependants s th'` show ?thesis by auto + qed + qed + qed + thus ?thesis by simp + qed + thus ?thesis by (unfold cp_eq_cpreced cpreced_def) qed +text {* + The following lemma shows that no thread lies upstream of the initiating thread @{text "th"}. + The reason for this is that only no-blocked thread can initiate + a system call. Since thread @{text "th"} is non-blocked, it is not waiting for any + critical resource. Therefore, there is edge leading out of @{text "th"} in the RAG. + Consequently, there is no node (neither resource nor thread) upstream of @{text "th"}. +*} lemma no_dependants: - assumes "th' \ th" shows "th \ dependants s th'" proof - assume h: "th \ dependants s th'" - from step_back_step [OF vt_s[unfolded s_def]] - have "step s' (Set th prio)" . - hence "th \ runing s'" by (cases, simp) - hence rd_th: "th \ readys s'" - by (simp add:readys_def runing_def) - from h have "(Th th, Th th') \ (RAG s')\<^sup>+" + assume "th \ dependants s th'" + from `th \ dependants s th'` have "(Th th, Th th') \ (RAG s')\<^sup>+" by (unfold s_dependants_def, unfold eq_RAG, unfold eq_dep, auto) from tranclD[OF this] obtain z where "(Th th, z) \ RAG s'" by auto - with rd_th show "False" + moreover have "th \ readys s'" + proof - + from step_back_step [OF vt_s[unfolded s_def]] + have "step s' (Set th prio)" . + hence "th \ runing s'" by (cases, simp) + thus ?thesis by (simp add:readys_def runing_def) + qed + ultimately show "False" apply (case_tac z, auto simp:readys_def s_RAG_def s_waiting_def cs_waiting_def) by (fold wq_def, blast) qed (* Result improved *) +text {* + A simple combination of @{text "eq_cp_pre"} and @{text "no_dependants"} + gives the main lemma of this locale, which shows that + only the initiating thread needs a recalculation of current precedence. +*} lemma eq_cp: - fixes th' - assumes neq_th: "th' \ th" + fixes th' + assumes "th' \ th" shows "cp s th' = cp s' th'" -proof(rule eq_cp_pre [OF neq_th]) - from no_dependants[OF neq_th] - show "th \ dependants s th'" . -qed + 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. + + The foregoing lemma says only those threads which +*} lemma eq_up: fixes th' th'' assumes dp1: "th \ dependants s th'" @@ -733,6 +879,20 @@ 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. +*} + lemma eq_up_self: fixes th' th'' assumes dp: "th \ dependants s th''" @@ -859,63 +1019,6 @@ qed end -lemma next_waiting: - assumes vt: "vt s" - and nxt: "next_th s th cs th'" - shows "waiting s th' cs" -proof - - from assms show ?thesis - apply (auto simp:next_th_def s_waiting_def[folded wq_def]) - proof - - fix rest - assume ni: "hd (SOME q. distinct q \ set q = set rest) \ set rest" - and eq_wq: "wq s cs = th # rest" - and ne: "rest \ []" - have "set (SOME q. distinct q \ set q = set rest) = set rest" - proof(rule someI2) - from wq_distinct[OF vt, of cs] eq_wq - show "distinct rest \ set rest = set rest" by auto - next - show "\x. distinct x \ set x = set rest \ set x = set rest" by auto - qed - with ni - have "hd (SOME q. distinct q \ set q = set rest) \ set (SOME q. distinct q \ set q = set rest)" - by simp - moreover have "(SOME q. distinct q \ set q = set rest) \ []" - proof(rule someI2) - from wq_distinct[OF vt, of cs] eq_wq - show "distinct rest \ set rest = set rest" by auto - next - from ne show "\x. distinct x \ set x = set rest \ x \ []" by auto - qed - ultimately show "hd (SOME q. distinct q \ set q = set rest) = th" by auto - next - fix rest - assume eq_wq: "wq s cs = hd (SOME q. distinct q \ set q = set rest) # rest" - and ne: "rest \ []" - have "(SOME q. distinct q \ set q = set rest) \ []" - proof(rule someI2) - from wq_distinct[OF vt, of cs] eq_wq - show "distinct rest \ set rest = set rest" by auto - next - from ne show "\x. distinct x \ set x = set rest \ x \ []" by auto - qed - hence "hd (SOME q. distinct q \ set q = set rest) \ set (SOME q. distinct q \ set q = set rest)" - by auto - moreover have "set (SOME q. distinct q \ set q = set rest) = set rest" - proof(rule someI2) - from wq_distinct[OF vt, of cs] eq_wq - show "distinct rest \ set rest = set rest" by auto - next - show "\x. distinct x \ set x = set rest \ set x = set rest" by auto - qed - ultimately have "hd (SOME q. distinct q \ set q = set rest) \ set rest" by simp - with eq_wq and wq_distinct[OF vt, of cs] - show False by auto - qed -qed - - locale step_v_cps = fixes s' th cs s defines s_def : "s \ (V th cs#s')" diff -r fee01b2858a2 -r b85cfbd58f59 PrioG.thy --- a/PrioG.thy Sat Oct 17 16:14:30 2015 +0800 +++ b/PrioG.thy Fri Oct 30 20:40:11 2015 +0800 @@ -210,7 +210,7 @@ lemma \thread \ set (wq_fun cs1 s); thread \ set (wq_fun cs2 s)\ \ cs1 = cs2" *) -text {* (* ??? *) +text {* (* ddd *) The nature of the work is like this: since it starts from a very simple and basic model, even intuitively very `basic` and `obvious` properties need to derived from scratch. For instance, the fact @@ -842,7 +842,7 @@ qed qed -text {* (* ??? *) +text {* (* ddd *) The following @{text "step_RAG_v"} lemma charaterizes how @{text "RAG"} is changed with the happening of @{text "V"}-events: *} @@ -1544,7 +1544,7 @@ ultimately show ?thesis by (simp add:cntCS_def) qed -text {* (* ??? *) \noindent +text {* (* ddd *) \noindent The relationship between @{text "cntP"}, @{text "cntV"} and @{text "cntCS"} of one particular thread. *}