diff -r 25fd656667a7 -r db196b066b97 Correctness.thy~ --- a/Correctness.thy~ Sat Jan 09 22:19:27 2016 +0800 +++ b/Correctness.thy~ Tue Jan 12 08:35:36 2016 +0800 @@ -471,6 +471,7 @@ finally show ?thesis . qed +section {* The `blocking thread` *} text {* Counting of the number of @{term "P"} and @{term "V"} operations @@ -519,116 +520,74 @@ qed qed -lemmas eq_pv_blocked_dtc = eq_pv_blocked[folded detached_eq] - - - -lemma eq_pv_kept: (* ddd *) - assumes th'_in: "th' \ threads s" +text {* + The following lemma is the extrapolation of @{thm eq_pv_blocked}. + It says if a thread, different from @{term th}, + does not hold any resource at the very beginning, + it will keep hand-emptied in the future @{term "t@s"}. +*} +lemma eq_pv_persist: (* ddd *) + assumes neq_th': "th' \ th" and eq_pv: "cntP s th' = cntV s th'" - and neq_th': "th' \ th" - shows "th' \ threads (t@s) \ - cntP (t@s) th' = cntV (t@s) th'" -proof(induct rule:ind) + shows "cntP (t@s) th' = cntV (t@s) th'" +proof(induction rule:ind) -- {* The proof goes by induction. *} + -- {* The nontrivial case is for the @{term Cons}: *} case (Cons e t) - interpret vat_t: extend_highest_gen s th prio tm t using Cons by simp - interpret vat_e: extend_highest_gen s th prio tm "(e # t)" using Cons by simp - show ?case - proof(cases e) - case (P thread cs) - show ?thesis - proof - - have "cntP ((e # t) @ s) th' = cntV ((e # t) @ s) th'" - proof - - have "thread \ th'" - proof - - have "step (t@s) (P thread cs)" using Cons P by auto - thus ?thesis - proof(cases) - assume "thread \ runing (t@s)" - moreover have "th' \ runing (t@s)" using Cons(5) - by (metis neq_th' vat_t.eq_pv_blocked) - ultimately show ?thesis by auto - qed - qed with Cons show ?thesis - by (unfold P, simp add:cntP_def cntV_def count_def) - qed - moreover have "th' \ threads ((e # t) @ s)" using Cons by (unfold P, simp) - ultimately show ?thesis by auto - qed - next - case (V thread cs) - show ?thesis - proof - - have "cntP ((e # t) @ s) th' = cntV ((e # t) @ s) th'" - proof - - have "thread \ th'" - proof - - have "step (t@s) (V thread cs)" using Cons V by auto - thus ?thesis - proof(cases) - assume "thread \ runing (t@s)" - moreover have "th' \ runing (t@s)" using Cons(5) - by (metis neq_th' vat_t.eq_pv_blocked) - ultimately show ?thesis by auto - qed - qed with Cons show ?thesis - by (unfold V, simp add:cntP_def cntV_def count_def) - qed - moreover have "th' \ threads ((e # t) @ s)" using Cons by (unfold V, simp) - ultimately show ?thesis by auto - qed - next - case (Create thread prio') - show ?thesis - proof - - have "cntP ((e # t) @ s) th' = cntV ((e # t) @ s) th'" - proof - - have "thread \ th'" - proof - - have "step (t@s) (Create thread prio')" using Cons Create by auto - thus ?thesis using Cons(5) by (cases, auto) - qed with Cons show ?thesis - by (unfold Create, simp add:cntP_def cntV_def count_def) - qed - moreover have "th' \ threads ((e # t) @ s)" using Cons by (unfold Create, simp) - ultimately show ?thesis by auto - qed - next - case (Exit thread) - show ?thesis - proof - - have neq_thread: "thread \ th'" - proof - - have "step (t@s) (Exit thread)" using Cons Exit by auto - thus ?thesis apply (cases) using Cons(5) - by (metis neq_th' vat_t.eq_pv_blocked) - qed - hence "cntP ((e # t) @ s) th' = cntV ((e # t) @ s) th'" using Cons - by (unfold Exit, simp add:cntP_def cntV_def count_def) - moreover have "th' \ threads ((e # t) @ s)" using Cons neq_thread - by (unfold Exit, simp) - ultimately show ?thesis by auto - qed - next - case (Set thread prio') - with Cons - show ?thesis - by (auto simp:cntP_def cntV_def count_def) + -- {* All results derived so far hold for both @{term s} and @{term "t@s"}: *} + interpret vat_t: extend_highest_gen s th prio tm t using Cons by simp + interpret vat_e: extend_highest_gen s th prio tm "(e # t)" using Cons by simp + show ?case + proof - + -- {* It can be proved that @{term cntP}-value of @{term th'} does not change + by the happening of event @{term e}: *} + have "cntP ((e#t)@s) th' = cntP (t@s) th'" + proof(rule ccontr) -- {* Proof by contradiction. *} + -- {* Suppose @{term cntP}-value of @{term th'} is changed by @{term e}: *} + assume otherwise: "cntP ((e # t) @ s) th' \ cntP (t @ s) th'" + -- {* Then the actor of @{term e} must be @{term th'} and @{term e} + must be a @{term P}-event: *} + hence "isP e" "actor e = th'" by (auto simp:cntP_diff_inv) + with vat_t.actor_inv[OF Cons(2)] + -- {* According to @{thm actor_inv}, @{term th'} must be running at + the moment @{term "t@s"}: *} + have "th' \ runing (t@s)" by (cases e, auto) + -- {* However, an application of @{thm eq_pv_blocked} to induction hypothesis + shows @{term th'} can not be running at moment @{term "t@s"}: *} + moreover have "th' \ runing (t@s)" + using vat_t.eq_pv_blocked[OF neq_th' Cons(5)] . + -- {* Contradiction is finally derived: *} + ultimately show False by simp qed -next - case Nil - with assms - show ?case by auto -qed + -- {* It can also be proved that @{term cntV}-value of @{term th'} does not change + by the happening of event @{term e}: *} + -- {* The proof follows exactly the same pattern as the case for @{term cntP}-value: *} + moreover have "cntV ((e#t)@s) th' = cntV (t@s) th'" + proof(rule ccontr) -- {* Proof by contradiction. *} + assume otherwise: "cntV ((e # t) @ s) th' \ cntV (t @ s) th'" + hence "isV e" "actor e = th'" by (auto simp:cntV_diff_inv) + with vat_t.actor_inv[OF Cons(2)] + have "th' \ runing (t@s)" by (cases e, auto) + moreover have "th' \ runing (t@s)" + using vat_t.eq_pv_blocked[OF neq_th' Cons(5)] . + ultimately show False by simp + qed + -- {* Finally, it can be shown that the @{term cntP} and @{term cntV} + value for @{term th'} are still in balance, so @{term th'} + is still hand-emptied after the execution of event @{term e}: *} + ultimately show ?thesis using Cons(5) by metis + qed +qed (auto simp:eq_pv) -(* runing_precond has changed to eq_pv_kept *) - -text {* Changing counting balance to detachedness *} -lemmas eq_pv_kept_dtc = eq_pv_kept - [folded vat_t.detached_eq vat_s.detached_eq] - -section {* The blocking thread *} +text {* + By combining @{thm eq_pv_blocked} and @{thm eq_pv_persist}, + it can be derived easily that @{term th'} can not be running in the future: +*} +lemma eq_pv_blocked_persist: + assumes neq_th': "th' \ th" + and eq_pv: "cntP s th' = cntV s th'" + shows "th' \ runing (t@s)" + using assms + by (simp add: eq_pv_blocked eq_pv_persist) text {* The purpose of PIP is to ensure that the most @@ -639,188 +598,63 @@ The following lemmas will give us such a picture: *} -(* ccc *) - text {* The following lemma shows the blocking thread @{term th'} must hold some resource in the very beginning. *} lemma runing_cntP_cntV_inv: (* ddd *) - assumes th'_in: "th' \ threads s" + assumes is_runing: "th' \ runing (t@s)" and neq_th': "th' \ th" - and is_runing: "th' \ runing (t@s)" shows "cntP s th' > cntV s th'" using assms -proof - (* ccc *) +proof - -- {* First, it can be shown that the number of @{term P} and @{term V} operations can not be equal for thred @{term th'} *} have "cntP s th' \ cntV s th'" proof + -- {* The proof goes by contradiction, suppose otherwise: *} assume otherwise: "cntP s th' = cntV s th'" - -- {* The proof goes by contradiction. *} - -- {* We can show that @{term th'} can not be running at moment @{term "t@s"}: *} - have "th' \ runing (t@s)" - proof(rule eq_pv_blocked) - show "th' \ th" using neq_th' by simp - next - show "cntP (t @ s) th' = cntV (t @ s) th'" - using eq_pv_kept[OF th'_in otherwise neq_th'] by simp - qed + -- {* By applying @{thm eq_pv_blocked_persist} to this: *} + from eq_pv_blocked_persist[OF neq_th' otherwise] + -- {* we have that @{term th'} can not be running at moment @{term "t@s"}: *} + have "th' \ runing (t@s)" . -- {* This is obvious in contradiction with assumption @{thm is_runing} *} thus False using is_runing by simp qed + -- {* However, the number of @{term V} is always less or equal to @{term P}: *} moreover have "cntV s th' \ cntP s th'" using vat_s.cnp_cnv_cncs by auto + -- {* Thesis is finally derived by combining the these two results: *} ultimately show ?thesis by auto qed -lemma moment_blocked_pre: - assumes neq_th': "th' \ th" - and th'_in: "th' \ threads ((moment i t)@s)" - and eq_pv: "cntP ((moment i t)@s) th' = cntV ((moment i t)@s) th'" - shows "cntP ((moment (i+j) t)@s) th' = cntV ((moment (i+j) t)@s) th' \ - th' \ threads ((moment (i+j) t)@s)" -proof - - interpret h_i: red_extend_highest_gen _ _ _ _ _ i - by (unfold_locales) - interpret h_j: red_extend_highest_gen _ _ _ _ _ "i+j" - by (unfold_locales) - interpret h: extend_highest_gen "((moment i t)@s)" th prio tm "moment j (restm i t)" - proof(unfold_locales) - show "vt (moment i t @ s)" by (metis h_i.vt_t) - next - show "th \ threads (moment i t @ s)" by (metis h_i.th_kept) - next - show "preced th (moment i t @ s) = - Max (cp (moment i t @ s) ` threads (moment i t @ s))" - by (metis h_i.th_cp_max h_i.th_cp_preced h_i.th_kept) - next - show "preced th (moment i t @ s) = Prc prio tm" by (metis h_i.th_kept preced_th) - next - show "vt (moment j (restm i t) @ moment i t @ s)" - using moment_plus_split by (metis add.commute append_assoc h_j.vt_t) - next - fix th' prio' - assume "Create th' prio' \ set (moment j (restm i t))" - thus "prio' \ prio" using assms - by (metis Un_iff add.commute h_j.create_low moment_plus_split set_append) - next - fix th' prio' - assume "Set th' prio' \ set (moment j (restm i t))" - thus "th' \ th \ prio' \ prio" - by (metis Un_iff add.commute h_j.set_diff_low moment_plus_split set_append) - next - fix th' - assume "Exit th' \ set (moment j (restm i t))" - thus "th' \ th" - by (metis Un_iff add.commute h_j.exit_diff moment_plus_split set_append) - qed - show ?thesis - by (metis add.commute append_assoc eq_pv h.eq_pv_kept - moment_plus_split neq_th' th'_in) -qed - -lemma moment_blocked_eqpv: (* ddd *) - assumes neq_th': "th' \ th" - and th'_in: "th' \ threads ((moment i t)@s)" - and eq_pv: "cntP ((moment i t)@s) th' = cntV ((moment i t)@s) th'" - and le_ij: "i \ j" - shows "cntP ((moment j t)@s) th' = cntV ((moment j t)@s) th' \ - th' \ threads ((moment j t)@s) \ - th' \ runing ((moment j t)@s)" -proof - - from moment_blocked_pre [OF neq_th' th'_in eq_pv, of "j-i"] and le_ij - have h1: "cntP ((moment j t)@s) th' = cntV ((moment j t)@s) th'" - and h2: "th' \ threads ((moment j t)@s)" by auto - moreover have "th' \ runing ((moment j t)@s)" - proof - - interpret h: red_extend_highest_gen _ _ _ _ _ j by (unfold_locales) - show ?thesis - using h.eq_pv_blocked h1 h2 neq_th' by auto - qed - ultimately show ?thesis by auto -qed - -(* The foregoing two lemmas are preparation for this one, but - in long run can be combined. Maybe I am wrong. - This one is useless (* XY *) -*) -lemma moment_blocked: - assumes neq_th': "th' \ th" - and th'_in: "th' \ threads ((moment i t)@s)" - and dtc: "detached (moment i t @ s) th'" - and le_ij: "i \ j" - shows "detached (moment j t @ s) th' \ - th' \ threads ((moment j t)@s) \ - th' \ runing ((moment j t)@s)" -proof - - interpret h_i: red_extend_highest_gen _ _ _ _ _ i by (unfold_locales) - interpret h_j: red_extend_highest_gen _ _ _ _ _ j by (unfold_locales) - have cnt_i: "cntP (moment i t @ s) th' = cntV (moment i t @ s) th'" - by (metis dtc h_i.detached_elim) - from moment_blocked_eqpv[OF neq_th' th'_in cnt_i le_ij] - show ?thesis by (metis h_j.detached_intro) -qed text {* The following lemmas shows the blocking thread @{text th'} must be live at the very beginning, i.e. the moment (or state) @{term s}. + + The proof is a simple combination of the results above: *} -lemma runing_threads_inv: (* ddd *) (* ccc *) +lemma runing_threads_inv: assumes runing': "th' \ runing (t@s)" and neq_th': "th' \ th" shows "th' \ threads s" -proof - - -- {* The proof is by contradiction: *} - { assume otherwise: "\ ?thesis" - have "th' \ runing (t @ s)" - proof - - -- {* Since @{term "th'"} is running at time @{term "t@s"}, so it exists that time. *} - have th'_in: "th' \ threads (t@s)" using runing' by (simp add:runing_def readys_def) - -- {* However, @{text "th'"} does not exist at very beginning. *} - have th'_notin: "th' \ threads (moment 0 t @ s)" using otherwise - by (metis append.simps(1) moment_zero) - -- {* Therefore, there must be a moment during @{text "t"}, when - @{text "th'"} came into being. *} - -- {* Let us suppose the moment being @{text "i"}: *} - from p_split_gen[OF th'_in th'_notin] - obtain i where lt_its: "i < length t" - and le_i: "0 \ i" - and pre: " th' \ threads (moment i t @ s)" (is "th' \ threads ?pre") - and post: "(\i'>i. th' \ threads (moment i' t @ s))" by (auto) - interpret h_i: red_extend_highest_gen _ _ _ _ _ i by (unfold_locales) - interpret h_i': red_extend_highest_gen _ _ _ _ _ "(Suc i)" by (unfold_locales) - from lt_its have "Suc i \ length t" by auto - -- {* Let us also suppose the event which makes this change is @{text e}: *} - from moment_head[OF this] obtain e where - eq_me: "moment (Suc i) t = e # moment i t" by blast - hence "vt (e # (moment i t @ s))" by (metis append_Cons h_i'.vt_t) - hence "PIP (moment i t @ s) e" by (cases, simp) - -- {* It can be derived that this event @{text "e"}, which - gives birth to @{term "th'"} must be a @{term "Create"}: *} - from create_pre[OF this, of th'] - obtain prio where eq_e: "e = Create th' prio" - by (metis append_Cons eq_me lessI post pre) - have h1: "th' \ threads (moment (Suc i) t @ s)" using post by auto - have h2: "cntP (moment (Suc i) t @ s) th' = cntV (moment (Suc i) t@ s) th'" - proof - - have "cntP (moment i t@s) th' = cntV (moment i t@s) th'" - by (metis h_i.cnp_cnv_eq pre) - thus ?thesis by (simp add:eq_me eq_e cntP_def cntV_def count_def) - qed - show ?thesis - using moment_blocked_eqpv [OF neq_th' h1 h2, of "length t"] lt_its moment_ge - by auto - qed - with `th' \ runing (t@s)` - have False by simp - } thus ?thesis by auto +proof(rule ccontr) -- {* Proof by contradiction: *} + assume otherwise: "th' \ threads s" + have "th' \ runing (t @ s)" + proof - + from vat_s.cnp_cnv_eq[OF otherwise] + have "cntP s th' = cntV s th'" . + from eq_pv_blocked_persist[OF neq_th' this] + show ?thesis . + qed + with runing' show False by simp qed text {* The following lemma summarizes several foregoing lemmas to give an overall picture of the blocking thread @{text "th'"}: *} -lemma runing_inversion: +lemma runing_inversion: (* ddd, one of the main lemmas to present *) assumes runing': "th' \ runing (t@s)" and neq_th: "th' \ th" shows "th' \ threads s" @@ -830,13 +664,15 @@ from runing_threads_inv[OF assms] show "th' \ threads s" . next - from runing_cntP_cntV_inv[OF runing_threads_inv[OF assms] neq_th runing'] + from runing_cntP_cntV_inv[OF runing' neq_th] show "\detached s th'" using vat_s.detached_eq by simp next from runing_preced_inversion[OF runing'] show "cp (t@s) th' = preced th s" . qed +section {* The existence of `blocking thread` *} + text {* Suppose @{term th} is not running, it is first shown that there is a path in RAG leading from node @{term th} to another thread @{text "th'"} @@ -847,7 +683,7 @@ is the @{term runing}-thread. However, we are going to show more: this running thread is exactly @{term "th'"}. *} -lemma th_blockedE: (* ddd *) +lemma th_blockedE: (* ddd, the other main lemma to be presented: *) assumes "th \ runing (t@s)" obtains th' where "Th th' \ ancestors (RAG (t @ s)) (Th th)" "th' \ runing (t@s)" @@ -923,6 +759,3 @@ end end - - -