# HG changeset patch # User zhangx # Date 1452558936 -28800 # Node ID db196b066b97e77ffd299dc200669f1cd6a44d1e # Parent 25fd656667a7a20c3a111d7370adf16ccf87789c Before retrofiting PIPBasics.thy 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 @@ -79,17 +79,15 @@ ultimately show ?thesis by auto qed -lemma highest_cp_preced: "cp s th = Max ((\ th'. preced th' s) ` threads s)" - by (fold max_cp_eq, unfold eq_cp_s_th, insert highest, simp) +lemma highest_cp_preced: "cp s th = Max (the_preced s ` threads s)" + using eq_cp_s_th highest max_cp_eq the_preced_def by presburger + -lemma highest_preced_thread: "preced th s = Max ((\ th'. preced th' s) ` threads s)" +lemma highest_preced_thread: "preced th s = Max (the_preced s ` threads s)" by (fold eq_cp_s_th, unfold highest_cp_preced, simp) lemma highest': "cp s th = Max (cp s ` threads s)" -proof - - from highest_cp_preced max_cp_eq[symmetric] - show ?thesis by simp -qed + by (simp add: eq_cp_s_th highest) end @@ -125,7 +123,6 @@ qed qed - locale red_extend_highest_gen = extend_highest_gen + fixes i::nat @@ -248,16 +245,15 @@ operations of PIP. All cases follow the same pattern rendered by the generalized introduction rule @{thm "image_Max_eqI"}. - The very essence is to show that precedences, no matter whether they are newly introduced - or modified, are always lower than the one held by @{term "th"}, - which by @{thm th_kept} is preserved along the way. + The very essence is to show that precedences, no matter whether they + are newly introduced or modified, are always lower than the one held + by @{term "th"}, which by @{thm th_kept} is preserved along the way. *} lemma max_kept: "Max (the_preced (t @ s) ` (threads (t@s))) = preced th s" proof(induct rule:ind) case Nil from highest_preced_thread - show ?case - by (unfold the_preced_def, simp) + show ?case by simp next case (Cons e t) interpret h_e: extend_highest_gen _ _ _ _ "(e # t)" using Cons by auto @@ -285,7 +281,8 @@ assume "x = thread" thus ?thesis apply (simp add:Create the_preced_def preced_def, fold preced_def) - using Create h_e.create_low h_t.th_kept lt_tm preced_leI2 preced_th by force + using Create h_e.create_low h_t.th_kept lt_tm preced_leI2 + preced_th by force next assume h: "x \ threads (t @ s)" from Cons(2)[unfolded Create] @@ -440,10 +437,25 @@ finally show ?thesis . qed -lemma th_cp_max: "cp (t@s) th = Max (cp (t@s) ` threads (t@s))" +lemma th_cp_max[simp]: "Max (cp (t@s) ` threads (t@s)) = cp (t@s) th" using max_cp_eq th_cp_max_preced the_preced_def vt_t by presburger -lemma th_cp_preced: "cp (t@s) th = preced th s" +lemma [simp]: "Max (cp (t@s) ` threads (t@s)) = Max (the_preced (t@s) ` threads (t@s))" + by (simp add: th_cp_max_preced) + +lemma [simp]: "Max (the_preced (t@s) ` threads (t@s)) = the_preced (t@s) th" + using max_kept th_kept the_preced_def by auto + +lemma [simp]: "the_preced (t@s) th = preced th (t@s)" + using the_preced_def by auto + +lemma [simp]: "preced th (t@s) = preced th s" + by (simp add: th_kept) + +lemma [simp]: "cp s th = preced th s" + by (simp add: eq_cp_s_th) + +lemma th_cp_preced [simp]: "cp (t@s) th = preced th s" by (fold max_kept, unfold th_cp_max_preced, simp) lemma preced_less: @@ -455,6 +467,21 @@ preced_linorder rev_image_eqI threads_s vat_s.finite_threads vat_s.le_cp) +section {* The `blocking thread` *} + +text {* + The purpose of PIP is to ensure that the most + urgent thread @{term th} is not blocked unreasonably. + Therefore, a clear picture of the blocking thread is essential + to assure people that the purpose is fulfilled. + + In this section, we are going to derive a series of lemmas + with finally give rise to a picture of the blocking thread. + + By `blocking thread`, we mean a thread in running state but + different from thread @{term th}. +*} + text {* The following lemmas shows that the @{term cp}-value of the blocking thread @{text th'} equals to the highest @@ -471,17 +498,31 @@ finally show ?thesis . qed -section {* The `blocking thread` *} +text {* + The following lemma shows how the counting of + @{term "P"} and @{term "V"} operations affects + the running state of threads in @{term t}. + + The lemma shows that if a thread's @{term "P"}-count equals + its @{term "V"}-count (which means it no longer has any + resource in its possession), it can not be in running thread. -text {* - Counting of the number of @{term "P"} and @{term "V"} operations - is the cornerstone of a large number of the following proofs. - The reason is that this counting is quite easy to calculate and - convenient to use in the reasoning. + The proof is by contraction with the assumption @{text "th' \ th"}. + The key is the use of @{thm count_eq_dependants} + to derive the emptiness of @{text th'}s @{term dependants}-set + from the balance of its @{term P} @{term V} counts. + From this, it can be shown @{text th'}s @{term cp}-value + equals to its own precedence. - The following lemma shows that the counting controls whether - a thread is running or not. -*} (* ccc *) + On the other hand, since @{text th'} is running, by + @{thm runing_preced_inversion}, its @{term cp}-value + equals to the precedence of @{term th}. + + Combining the above two we have that @{text th'} and + @{term th} have the same precedence. By uniqueness of precedence, we + have @{text "th' = th"}, which is in contradiction with the + assumption @{text "th' \ th"}. +*} lemma eq_pv_blocked: (* ddd *) assumes neq_th': "th' \ th" @@ -507,16 +548,16 @@ equals its @{term preced}-value: *} have "?L = cp (t@s) th'" by (unfold cp_eq_cpreced cpreced_def count_eq_dependants[OF eq_pv], simp) - -- {* Since @{term "th'"} is running by @{thm otherwise}, - it has the highest @{term cp}-value, by definition, - which in turn equals to the @{term cp}-value of @{term th}. *} + -- {* Since @{term "th'"} is running, by @{thm runing_preced_inversion}, + its @{term cp}-value equals @{term "preced th s"}, + which equals to @{term "?R"} by simplification: *} also have "... = ?R" - using runing_preced_inversion[OF otherwise] th_kept by simp + thm runing_preced_inversion + using runing_preced_inversion[OF otherwise] by simp finally show ?thesis . qed qed (auto simp: th'_in th_kept) - moreover have "th' \ th" using neq_th' . - ultimately show ?thesis by simp + with `th' \ th` show ?thesis by simp qed qed @@ -589,15 +630,6 @@ using assms by (simp add: eq_pv_blocked eq_pv_persist) -text {* - The purpose of PIP is to ensure that the most - urgent thread @{term th} is not blocked unreasonably. - Therefore, a clear picture of the blocking thread is essential - to assure people that the purpose is fulfilled. - - The following lemmas will give us such a picture: -*} - text {* The following lemma shows the blocking thread @{term th'} must hold some resource in the very beginning. 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 - - - diff -r 25fd656667a7 -r db196b066b97 Implementation.thy --- a/Implementation.thy Sat Jan 09 22:19:27 2016 +0800 +++ b/Implementation.thy Tue Jan 12 08:35:36 2016 +0800 @@ -22,16 +22,19 @@ 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. + of a thread is the maximum of the precedences of every threads in its subtree, + where the notion of sub-tree in RAG is defined in RTree.thy. - 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. + Therefore, for each operation, lemmas about the change of precedences + and RAG are derived first, on which lemmas about current precedence + recalculation are based on. *} +section {* The @{term Set} operation *} + text {* (* ddd *) The following locale @{text "step_set_cps"} investigates the recalculation after the @{text "Set"} operation. @@ -59,8 +62,9 @@ begin text {* (* ddd *) - The following two lemmas confirm that @{text "Set"}-operating only changes the precedence - of the initiating thread. + The following two lemmas confirm that @{text "Set"}-operation + only changes the precedence of the initiating thread (or actor) + of the operation (or event). *} lemma eq_preced: @@ -72,7 +76,6 @@ qed lemma eq_the_preced: - fixes th' assumes "th' \ th" shows "the_preced s th' = the_preced s' th'" using assms @@ -86,14 +89,14 @@ by (unfold s_def RAG_set_unchanged, auto) text {* (* ddd *) - Th following lemma @{text "eq_cp_pre"} says the priority change of @{text "th"} + Th following lemma @{text "eq_cp_pre"} says that the priority change of @{text "th"} only affects those threads, which as @{text "Th th"} in their sub-trees. - The proof of this lemma is simplified by using the alternative definition of @{text "cp"}. + The proof of this lemma is simplified by using the alternative definition + of @{text "cp"}. *} lemma eq_cp_pre: - fixes th' assumes nd: "Th th \ subtree (RAG s') (Th th')" shows "cp s th' = cp s' th'" proof - @@ -147,13 +150,14 @@ of the initiating thread @{text "th"}. *} lemma eq_cp: - fixes th' assumes "th' \ th" shows "cp s th' = cp s' th'" by (rule eq_cp_pre[OF th_in_no_subtree[OF assms]]) end +section {* The @{term V} operation *} + text {* The following @{text "step_v_cps"} is the locale for @{text "V"}-operation. *} @@ -301,7 +305,7 @@ and nt show ?thesis by (auto intro:next_th_unique) qed -lemma subtree_kept: +lemma subtree_kept: (* ddd *) assumes "th1 \ {th, th'}" shows "subtree (RAG s) (Th th1) = subtree (RAG s') (Th th1)" (is "_ = ?R") proof - @@ -429,7 +433,6 @@ by (unfold cp_alt_def subtree_th preced_kept, auto) lemma eq_cp: - fixes th' shows "cp s th' = cp s' th'" using cp_kept_1 cp_kept_2 by (cases "th' = th", auto) @@ -446,6 +449,8 @@ from vt_s show "vt s" . qed +section {* The @{term P} operation *} + sublocale step_P_cps < vat_s' : valid_trace "s'" proof from step_back_vt[OF vt_s[unfolded s_def]] show "vt s'" . @@ -727,6 +732,8 @@ end +section {* The @{term Create} operation *} + locale step_create_cps = fixes s' th prio s defines s_def : "s \ (Create th prio#s')" diff -r 25fd656667a7 -r db196b066b97 Implementation.thy~ --- a/Implementation.thy~ Sat Jan 09 22:19:27 2016 +0800 +++ b/Implementation.thy~ Tue Jan 12 08:35:36 2016 +0800 @@ -3,732 +3,9 @@ after every system call (or system operation) *} theory Implementation -imports PIPBasics Max RTree -begin - -text {* @{text "the_preced"} is also the same as @{text "preced"}, the only - difference is the order of arguemts. *} -definition "the_preced s th = preced th s" - -lemma inj_the_preced: - "inj_on (the_preced s) (threads s)" - by (metis inj_onI preced_unique the_preced_def) - -text {* @{term "the_thread"} extracts thread out of RAG node. *} -fun the_thread :: "node \ thread" where - "the_thread (Th th) = th" - -text {* The following @{text "wRAG"} is the waiting sub-graph of @{text "RAG"}. *} -definition "wRAG (s::state) = {(Th th, Cs cs) | th cs. waiting s th cs}" - -text {* The following @{text "hRAG"} is the holding sub-graph of @{text "RAG"}. *} -definition "hRAG (s::state) = {(Cs cs, Th th) | th cs. holding s th cs}" - -text {* The following lemma splits @{term "RAG"} graph into the above two sub-graphs. *} -lemma RAG_split: "RAG s = (wRAG s \ hRAG s)" - by (unfold s_RAG_abv wRAG_def hRAG_def s_waiting_abv - s_holding_abv cs_RAG_def, auto) - -text {* - The following @{text "tRAG"} is the thread-graph derived from @{term "RAG"}. - It characterizes the dependency between threads when calculating current - precedences. It is defined as the composition of the above two sub-graphs, - names @{term "wRAG"} and @{term "hRAG"}. - *} -definition "tRAG s = wRAG s O hRAG s" - -(* ccc *) - -definition "cp_gen s x = - Max ((the_preced s \ the_thread) ` subtree (tRAG s) x)" - -lemma tRAG_alt_def: - "tRAG s = {(Th th1, Th th2) | th1 th2. - \ cs. (Th th1, Cs cs) \ RAG s \ (Cs cs, Th th2) \ RAG s}" - by (auto simp:tRAG_def RAG_split wRAG_def hRAG_def) - -lemma tRAG_Field: - "Field (tRAG s) \ Field (RAG s)" - by (unfold tRAG_alt_def Field_def, auto) - -lemma tRAG_ancestorsE: - assumes "x \ ancestors (tRAG s) u" - obtains th where "x = Th th" -proof - - from assms have "(u, x) \ (tRAG s)^+" - by (unfold ancestors_def, auto) - from tranclE[OF this] obtain c where "(c, x) \ tRAG s" by auto - then obtain th where "x = Th th" - by (unfold tRAG_alt_def, auto) - from that[OF this] show ?thesis . -qed - -lemma tRAG_mono: - assumes "RAG s' \ RAG s" - shows "tRAG s' \ tRAG s" - using assms - by (unfold tRAG_alt_def, auto) - -lemma holding_next_thI: - assumes "holding s th cs" - and "length (wq s cs) > 1" - obtains th' where "next_th s th cs th'" -proof - - from assms(1)[folded eq_holding, unfolded cs_holding_def] - have " th \ set (wq s cs) \ th = hd (wq s cs)" . - then obtain rest where h1: "wq s cs = th#rest" - by (cases "wq s cs", auto) - with assms(2) have h2: "rest \ []" by auto - let ?th' = "hd (SOME q. distinct q \ set q = set rest)" - have "next_th s th cs ?th'" using h1(1) h2 - by (unfold next_th_def, auto) - from that[OF this] show ?thesis . -qed - -lemma RAG_tRAG_transfer: - assumes "vt s'" - assumes "RAG s = RAG s' \ {(Th th, Cs cs)}" - and "(Cs cs, Th th'') \ RAG s'" - shows "tRAG s = tRAG s' \ {(Th th, Th th'')}" (is "?L = ?R") -proof - - interpret vt_s': valid_trace "s'" using assms(1) - by (unfold_locales, simp) - interpret rtree: rtree "RAG s'" - proof - show "single_valued (RAG s')" - apply (intro_locales) - by (unfold single_valued_def, - auto intro:vt_s'.unique_RAG) - - show "acyclic (RAG s')" - by (rule vt_s'.acyclic_RAG) - qed - { fix n1 n2 - assume "(n1, n2) \ ?L" - from this[unfolded tRAG_alt_def] - obtain th1 th2 cs' where - h: "n1 = Th th1" "n2 = Th th2" - "(Th th1, Cs cs') \ RAG s" - "(Cs cs', Th th2) \ RAG s" by auto - from h(4) and assms(2) have cs_in: "(Cs cs', Th th2) \ RAG s'" by auto - from h(3) and assms(2) - have "(Th th1, Cs cs') = (Th th, Cs cs) \ - (Th th1, Cs cs') \ RAG s'" by auto - hence "(n1, n2) \ ?R" - proof - assume h1: "(Th th1, Cs cs') = (Th th, Cs cs)" - hence eq_th1: "th1 = th" by simp - moreover have "th2 = th''" - proof - - from h1 have "cs' = cs" by simp - from assms(3) cs_in[unfolded this] rtree.sgv - show ?thesis - by (unfold single_valued_def, auto) - qed - ultimately show ?thesis using h(1,2) by auto - next - assume "(Th th1, Cs cs') \ RAG s'" - with cs_in have "(Th th1, Th th2) \ tRAG s'" - by (unfold tRAG_alt_def, auto) - from this[folded h(1, 2)] show ?thesis by auto - qed - } moreover { - fix n1 n2 - assume "(n1, n2) \ ?R" - hence "(n1, n2) \tRAG s' \ (n1, n2) = (Th th, Th th'')" by auto - hence "(n1, n2) \ ?L" - proof - assume "(n1, n2) \ tRAG s'" - moreover have "... \ ?L" - proof(rule tRAG_mono) - show "RAG s' \ RAG s" by (unfold assms(2), auto) - qed - ultimately show ?thesis by auto - next - assume eq_n: "(n1, n2) = (Th th, Th th'')" - from assms(2, 3) have "(Cs cs, Th th'') \ RAG s" by auto - moreover have "(Th th, Cs cs) \ RAG s" using assms(2) by auto - ultimately show ?thesis - by (unfold eq_n tRAG_alt_def, auto) - qed - } ultimately show ?thesis by auto -qed - -context valid_trace -begin - -lemmas RAG_tRAG_transfer = RAG_tRAG_transfer[OF vt] - -end - -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 cp_gen_alt_def: - "cp_gen s = (Max \ (\x. (the_preced s \ the_thread) ` subtree (tRAG s) x))" - by (auto simp:cp_gen_def) - -lemma tRAG_nodeE: - assumes "(n1, n2) \ tRAG s" - obtains th1 th2 where "n1 = Th th1" "n2 = Th th2" - using assms - by (auto simp: tRAG_def wRAG_def hRAG_def tRAG_def) - -lemma subtree_nodeE: - assumes "n \ subtree (tRAG s) (Th th)" - obtains th1 where "n = Th th1" -proof - - show ?thesis - proof(rule subtreeE[OF assms]) - assume "n = Th th" - from that[OF this] show ?thesis . - next - assume "Th th \ ancestors (tRAG s) n" - hence "(n, Th th) \ (tRAG s)^+" by (auto simp:ancestors_def) - hence "\ th1. n = Th th1" - proof(induct) - case (base y) - from tRAG_nodeE[OF this] show ?case by metis - next - case (step y z) - thus ?case by auto - qed - with that show ?thesis by auto - qed -qed - -lemma tRAG_star_RAG: "(tRAG s)^* \ (RAG s)^*" -proof - - have "(wRAG s O hRAG s)^* \ (RAG s O RAG s)^*" - by (rule rtrancl_mono, auto simp:RAG_split) - also have "... \ ((RAG s)^*)^*" - by (rule rtrancl_mono, auto) - also have "... = (RAG s)^*" by simp - finally show ?thesis by (unfold tRAG_def, simp) -qed - -lemma tRAG_subtree_RAG: "subtree (tRAG s) x \ subtree (RAG s) x" -proof - - { fix a - assume "a \ subtree (tRAG s) x" - hence "(a, x) \ (tRAG s)^*" by (auto simp:subtree_def) - with tRAG_star_RAG[of s] - have "(a, x) \ (RAG s)^*" by auto - hence "a \ subtree (RAG s) x" by (auto simp:subtree_def) - } thus ?thesis by auto -qed - -lemma tRAG_trancl_eq: - "{th'. (Th th', Th th) \ (tRAG s)^+} = - {th'. (Th th', Th th) \ (RAG s)^+}" - (is "?L = ?R") -proof - - { fix th' - assume "th' \ ?L" - hence "(Th th', Th th) \ (tRAG s)^+" by auto - from tranclD[OF this] - obtain z where h: "(Th th', z) \ tRAG s" "(z, Th th) \ (tRAG s)\<^sup>*" by auto - from tRAG_subtree_RAG[of s] and this(2) - have "(z, Th th) \ (RAG s)^*" by (meson subsetCE tRAG_star_RAG) - moreover from h(1) have "(Th th', z) \ (RAG s)^+" using tRAG_alt_def by auto - ultimately have "th' \ ?R" by auto - } moreover - { fix th' - assume "th' \ ?R" - hence "(Th th', Th th) \ (RAG s)^+" by (auto) - from plus_rpath[OF this] - obtain xs where rp: "rpath (RAG s) (Th th') xs (Th th)" "xs \ []" by auto - hence "(Th th', Th th) \ (tRAG s)^+" - proof(induct xs arbitrary:th' th rule:length_induct) - case (1 xs th' th) - then obtain x1 xs1 where Cons1: "xs = x1#xs1" by (cases xs, auto) - show ?case - proof(cases "xs1") - case Nil - from 1(2)[unfolded Cons1 Nil] - have rp: "rpath (RAG s) (Th th') [x1] (Th th)" . - hence "(Th th', x1) \ (RAG s)" by (cases, simp) - then obtain cs where "x1 = Cs cs" - by (unfold s_RAG_def, auto) - from rpath_nnl_lastE[OF rp[unfolded this]] - show ?thesis by auto - next - case (Cons x2 xs2) - from 1(2)[unfolded Cons1[unfolded this]] - have rp: "rpath (RAG s) (Th th') (x1 # x2 # xs2) (Th th)" . - from rpath_edges_on[OF this] - have eds: "edges_on (Th th' # x1 # x2 # xs2) \ RAG s" . - have "(Th th', x1) \ edges_on (Th th' # x1 # x2 # xs2)" - by (simp add: edges_on_unfold) - with eds have rg1: "(Th th', x1) \ RAG s" by auto - then obtain cs1 where eq_x1: "x1 = Cs cs1" by (unfold s_RAG_def, auto) - have "(x1, x2) \ edges_on (Th th' # x1 # x2 # xs2)" - by (simp add: edges_on_unfold) - from this eds - have rg2: "(x1, x2) \ RAG s" by auto - from this[unfolded eq_x1] - obtain th1 where eq_x2: "x2 = Th th1" by (unfold s_RAG_def, auto) - from rg1[unfolded eq_x1] rg2[unfolded eq_x1 eq_x2] - have rt1: "(Th th', Th th1) \ tRAG s" by (unfold tRAG_alt_def, auto) - from rp have "rpath (RAG s) x2 xs2 (Th th)" - by (elim rpath_ConsE, simp) - from this[unfolded eq_x2] have rp': "rpath (RAG s) (Th th1) xs2 (Th th)" . - show ?thesis - proof(cases "xs2 = []") - case True - from rpath_nilE[OF rp'[unfolded this]] - have "th1 = th" by auto - from rt1[unfolded this] show ?thesis by auto - next - case False - from 1(1)[rule_format, OF _ rp' this, unfolded Cons1 Cons] - have "(Th th1, Th th) \ (tRAG s)\<^sup>+" by simp - with rt1 show ?thesis by auto - qed - qed - qed - hence "th' \ ?L" by auto - } ultimately show ?thesis by blast -qed - -lemma tRAG_trancl_eq_Th: - "{Th th' | th'. (Th th', Th th) \ (tRAG s)^+} = - {Th th' | th'. (Th th', Th th) \ (RAG s)^+}" - using tRAG_trancl_eq by auto - -lemma dependants_alt_def: - "dependants s th = {th'. (Th th', Th th) \ (tRAG s)^+}" - by (metis eq_RAG s_dependants_def tRAG_trancl_eq) - -context valid_trace +imports PIPBasics begin -lemma count_eq_tRAG_plus: - assumes "cntP s th = cntV s th" - shows "{th'. (Th th', Th th) \ (tRAG s)^+} = {}" - using assms count_eq_dependants dependants_alt_def eq_dependants by auto - -lemma count_eq_RAG_plus: - assumes "cntP s th = cntV s th" - shows "{th'. (Th th', Th th) \ (RAG s)^+} = {}" - using assms count_eq_dependants cs_dependants_def eq_RAG by auto - -lemma count_eq_RAG_plus_Th: - assumes "cntP s th = cntV s th" - shows "{Th th' | th'. (Th th', Th th) \ (RAG s)^+} = {}" - using count_eq_RAG_plus[OF assms] by auto - -lemma count_eq_tRAG_plus_Th: - assumes "cntP s th = cntV s th" - shows "{Th th' | th'. (Th th', Th th) \ (tRAG s)^+} = {}" - using count_eq_tRAG_plus[OF assms] by auto - -end - -lemma tRAG_subtree_eq: - "(subtree (tRAG s) (Th th)) = {Th th' | th'. Th th' \ (subtree (RAG s) (Th th))}" - (is "?L = ?R") -proof - - { fix n - assume h: "n \ ?L" - hence "n \ ?R" - by (smt mem_Collect_eq subsetCE subtree_def subtree_nodeE tRAG_subtree_RAG) - } moreover { - fix n - assume "n \ ?R" - then obtain th' where h: "n = Th th'" "(Th th', Th th) \ (RAG s)^*" - by (auto simp:subtree_def) - from rtranclD[OF this(2)] - have "n \ ?L" - proof - assume "Th th' \ Th th \ (Th th', Th th) \ (RAG s)\<^sup>+" - with h have "n \ {Th th' | th'. (Th th', Th th) \ (RAG s)^+}" by auto - thus ?thesis using subtree_def tRAG_trancl_eq by fastforce - qed (insert h, auto simp:subtree_def) - } ultimately show ?thesis by auto -qed - -lemma threads_set_eq: - "the_thread ` (subtree (tRAG s) (Th th)) = - {th'. Th th' \ (subtree (RAG s) (Th th))}" (is "?L = ?R") - by (auto intro:rev_image_eqI simp:tRAG_subtree_eq) - -lemma cp_alt_def1: - "cp s th = Max ((the_preced s o the_thread) ` (subtree (tRAG s) (Th th)))" -proof - - have "(the_preced s ` the_thread ` subtree (tRAG s) (Th th)) = - ((the_preced s \ the_thread) ` subtree (tRAG s) (Th th))" - by auto - thus ?thesis by (unfold cp_alt_def, fold threads_set_eq, auto) -qed - -lemma cp_gen_def_cond: - assumes "x = Th th" - shows "cp s th = cp_gen s (Th th)" -by (unfold cp_alt_def1 cp_gen_def, simp) - -lemma cp_gen_over_set: - assumes "\ x \ A. \ th. x = Th th" - shows "cp_gen s ` A = (cp s \ the_thread) ` A" -proof(rule f_image_eq) - fix a - assume "a \ A" - from assms[rule_format, OF this] - obtain th where eq_a: "a = Th th" by auto - show "cp_gen s a = (cp s \ the_thread) a" - by (unfold eq_a, simp, unfold cp_gen_def_cond[OF refl[of "Th th"]], simp) -qed - - -context valid_trace -begin - -lemma RAG_threads: - assumes "(Th th) \ Field (RAG s)" - shows "th \ threads s" - using assms - by (metis Field_def UnE dm_RAG_threads range_in vt) - -lemma subtree_tRAG_thread: - assumes "th \ threads s" - shows "subtree (tRAG s) (Th th) \ Th ` threads s" (is "?L \ ?R") -proof - - have "?L = {Th th' |th'. Th th' \ subtree (RAG s) (Th th)}" - by (unfold tRAG_subtree_eq, simp) - also have "... \ ?R" - proof - fix x - assume "x \ {Th th' |th'. Th th' \ subtree (RAG s) (Th th)}" - then obtain th' where h: "x = Th th'" "Th th' \ subtree (RAG s) (Th th)" by auto - from this(2) - show "x \ ?R" - proof(cases rule:subtreeE) - case 1 - thus ?thesis by (simp add: assms h(1)) - next - case 2 - thus ?thesis by (metis ancestors_Field dm_RAG_threads h(1) image_eqI) - qed - qed - finally show ?thesis . -qed - -lemma readys_root: - assumes "th \ readys s" - shows "root (RAG s) (Th th)" -proof - - { fix x - assume "x \ ancestors (RAG s) (Th th)" - hence h: "(Th th, x) \ (RAG s)^+" by (auto simp:ancestors_def) - from tranclD[OF this] - obtain z where "(Th th, z) \ RAG s" by auto - with assms(1) have False - apply (case_tac z, auto simp:readys_def s_RAG_def s_waiting_def cs_waiting_def) - by (fold wq_def, blast) - } thus ?thesis by (unfold root_def, auto) -qed - -lemma readys_in_no_subtree: - assumes "th \ readys s" - and "th' \ th" - shows "Th th \ subtree (RAG s) (Th th')" -proof - assume "Th th \ subtree (RAG s) (Th th')" - thus False - proof(cases rule:subtreeE) - case 1 - with assms show ?thesis by auto - next - case 2 - with readys_root[OF assms(1)] - show ?thesis by (auto simp:root_def) - qed -qed - -lemma not_in_thread_isolated: - assumes "th \ threads s" - shows "(Th th) \ Field (RAG s)" -proof - assume "(Th th) \ Field (RAG s)" - with dm_RAG_threads and range_in assms - show False by (unfold Field_def, blast) -qed - -lemma wf_RAG: "wf (RAG s)" -proof(rule finite_acyclic_wf) - from finite_RAG show "finite (RAG s)" . -next - from acyclic_RAG show "acyclic (RAG s)" . -qed - -lemma sgv_wRAG: "single_valued (wRAG s)" - using waiting_unique - by (unfold single_valued_def wRAG_def, auto) - -lemma sgv_hRAG: "single_valued (hRAG s)" - using holding_unique - by (unfold single_valued_def hRAG_def, auto) - -lemma sgv_tRAG: "single_valued (tRAG s)" - by (unfold tRAG_def, rule single_valued_relcomp, - insert sgv_wRAG sgv_hRAG, auto) - -lemma acyclic_tRAG: "acyclic (tRAG s)" -proof(unfold tRAG_def, rule acyclic_compose) - show "acyclic (RAG s)" using acyclic_RAG . -next - show "wRAG s \ RAG s" unfolding RAG_split by auto -next - show "hRAG s \ RAG s" unfolding RAG_split by auto -qed - -lemma sgv_RAG: "single_valued (RAG s)" - using unique_RAG by (auto simp:single_valued_def) - -lemma rtree_RAG: "rtree (RAG s)" - using sgv_RAG acyclic_RAG - by (unfold rtree_def rtree_axioms_def sgv_def, auto) - -end - - -sublocale valid_trace < rtree_RAG: rtree "RAG s" -proof - show "single_valued (RAG s)" - apply (intro_locales) - by (unfold single_valued_def, - auto intro:unique_RAG) - - show "acyclic (RAG s)" - by (rule acyclic_RAG) -qed - -sublocale valid_trace < rtree_s: rtree "tRAG s" -proof(unfold_locales) - from sgv_tRAG show "single_valued (tRAG s)" . -next - from acyclic_tRAG show "acyclic (tRAG s)" . -qed - -sublocale valid_trace < fsbtRAGs : fsubtree "RAG s" -proof - - show "fsubtree (RAG s)" - proof(intro_locales) - show "fbranch (RAG s)" using finite_fbranchI[OF finite_RAG] . - next - show "fsubtree_axioms (RAG s)" - proof(unfold fsubtree_axioms_def) - from wf_RAG show "wf (RAG s)" . - qed - qed -qed - -sublocale valid_trace < fsbttRAGs: fsubtree "tRAG s" -proof - - have "fsubtree (tRAG s)" - proof - - have "fbranch (tRAG s)" - proof(unfold tRAG_def, rule fbranch_compose) - show "fbranch (wRAG s)" - proof(rule finite_fbranchI) - from finite_RAG show "finite (wRAG s)" - by (unfold RAG_split, auto) - qed - next - show "fbranch (hRAG s)" - proof(rule finite_fbranchI) - from finite_RAG - show "finite (hRAG s)" by (unfold RAG_split, auto) - qed - qed - moreover have "wf (tRAG s)" - proof(rule wf_subset) - show "wf (RAG s O RAG s)" using wf_RAG - by (fold wf_comp_self, simp) - next - show "tRAG s \ (RAG s O RAG s)" - by (unfold tRAG_alt_def, auto) - qed - ultimately show ?thesis - by (unfold fsubtree_def fsubtree_axioms_def,auto) - qed - from this[folded tRAG_def] show "fsubtree (tRAG s)" . -qed - -lemma Max_UNION: - assumes "finite A" - and "A \ {}" - and "\ M \ f ` A. finite M" - and "\ M \ f ` A. M \ {}" - shows "Max (\x\ A. f x) = Max (Max ` f ` A)" (is "?L = ?R") - using assms[simp] -proof - - have "?L = Max (\(f ` A))" - by (fold Union_image_eq, simp) - also have "... = ?R" - by (subst Max_Union, simp+) - finally show ?thesis . -qed - -lemma max_Max_eq: - assumes "finite A" - and "A \ {}" - and "x = y" - shows "max x (Max A) = Max ({y} \ A)" (is "?L = ?R") -proof - - have "?R = Max (insert y A)" by simp - also from assms have "... = ?L" - by (subst Max.insert, simp+) - finally show ?thesis by simp -qed - -context valid_trace -begin - -(* ddd *) -lemma cp_gen_rec: - assumes "x = Th th" - shows "cp_gen s x = Max ({the_preced s th} \ (cp_gen s) ` children (tRAG s) x)" -proof(cases "children (tRAG s) x = {}") - case True - show ?thesis - by (unfold True cp_gen_def subtree_children, simp add:assms) -next - case False - hence [simp]: "children (tRAG s) x \ {}" by auto - note fsbttRAGs.finite_subtree[simp] - have [simp]: "finite (children (tRAG s) x)" - by (intro rev_finite_subset[OF fsbttRAGs.finite_subtree], - rule children_subtree) - { fix r x - have "subtree r x \ {}" by (auto simp:subtree_def) - } note this[simp] - have [simp]: "\x\children (tRAG s) x. subtree (tRAG s) x \ {}" - proof - - from False obtain q where "q \ children (tRAG s) x" by blast - moreover have "subtree (tRAG s) q \ {}" by simp - ultimately show ?thesis by blast - qed - have h: "Max ((the_preced s \ the_thread) ` - ({x} \ \(subtree (tRAG s) ` children (tRAG s) x))) = - Max ({the_preced s th} \ cp_gen s ` children (tRAG s) x)" - (is "?L = ?R") - proof - - let "Max (?f ` (?A \ \ (?g ` ?B)))" = ?L - let "Max (_ \ (?h ` ?B))" = ?R - let ?L1 = "?f ` \(?g ` ?B)" - have eq_Max_L1: "Max ?L1 = Max (?h ` ?B)" - proof - - have "?L1 = ?f ` (\ x \ ?B.(?g x))" by simp - also have "... = (\ x \ ?B. ?f ` (?g x))" by auto - finally have "Max ?L1 = Max ..." by simp - also have "... = Max (Max ` (\x. ?f ` subtree (tRAG s) x) ` ?B)" - by (subst Max_UNION, simp+) - also have "... = Max (cp_gen s ` children (tRAG s) x)" - by (unfold image_comp cp_gen_alt_def, simp) - finally show ?thesis . - qed - show ?thesis - proof - - have "?L = Max (?f ` ?A \ ?L1)" by simp - also have "... = max (the_preced s (the_thread x)) (Max ?L1)" - by (subst Max_Un, simp+) - also have "... = max (?f x) (Max (?h ` ?B))" - by (unfold eq_Max_L1, simp) - also have "... =?R" - by (rule max_Max_eq, (simp)+, unfold assms, simp) - finally show ?thesis . - qed - qed thus ?thesis - by (fold h subtree_children, unfold cp_gen_def, simp) -qed - -lemma cp_rec: - "cp s th = Max ({the_preced s th} \ - (cp s o the_thread) ` children (tRAG s) (Th th))" -proof - - have "Th th = Th th" by simp - note h = cp_gen_def_cond[OF this] cp_gen_rec[OF this] - show ?thesis - proof - - have "cp_gen s ` children (tRAG s) (Th th) = - (cp s \ the_thread) ` children (tRAG s) (Th th)" - proof(rule cp_gen_over_set) - show " \x\children (tRAG s) (Th th). \th. x = Th th" - by (unfold tRAG_alt_def, auto simp:children_def) - qed - thus ?thesis by (subst (1) h(1), unfold h(2), simp) - qed -qed - -end - -(* keep *) -lemma next_th_holding: - assumes vt: "vt s" - and nxt: "next_th s th cs th'" - shows "holding (wq s) th cs" -proof - - from nxt[unfolded next_th_def] - obtain rest where h: "wq s cs = th # rest" - "rest \ []" - "th' = hd (SOME q. distinct q \ set q = set rest)" by auto - thus ?thesis - by (unfold cs_holding_def, auto) -qed - -context valid_trace -begin - -lemma next_th_waiting: - assumes nxt: "next_th s th cs th'" - shows "waiting (wq s) th' cs" -proof - - from nxt[unfolded next_th_def] - obtain rest where h: "wq s cs = th # rest" - "rest \ []" - "th' = hd (SOME q. distinct q \ set q = set rest)" by auto - from wq_distinct[of cs, unfolded h] - have dst: "distinct (th # rest)" . - have in_rest: "th' \ set rest" - proof(unfold h, rule someI2) - show "distinct rest \ set rest = set rest" using dst by auto - next - fix x assume "distinct x \ set x = set rest" - with h(2) - show "hd x \ set (rest)" by (cases x, auto) - qed - hence "th' \ set (wq s cs)" by (unfold h(1), auto) - moreover have "th' \ hd (wq s cs)" - by (unfold h(1), insert in_rest dst, auto) - ultimately show ?thesis by (auto simp:cs_waiting_def) -qed - -lemma next_th_RAG: - assumes nxt: "next_th (s::event list) th cs th'" - shows "{(Cs cs, Th th), (Th th', Cs cs)} \ RAG s" - using vt assms next_th_holding next_th_waiting - by (unfold s_RAG_def, simp) - -end - --- {* 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 diff -r 25fd656667a7 -r db196b066b97 PIPBasics.thy --- a/PIPBasics.thy Sat Jan 09 22:19:27 2016 +0800 +++ b/PIPBasics.thy Tue Jan 12 08:35:36 2016 +0800 @@ -30,6 +30,13 @@ "cs \ cs' \ wq (V thread cs#s) cs' = wq s cs'" by (auto simp:wq_def Let_def cp_def split:list.splits) +lemma runing_head: + assumes "th \ runing s" + and "th \ set (wq_fun (schs s) cs)" + shows "th = hd (wq_fun (schs s) cs)" + using assms + by (simp add:runing_def readys_def s_waiting_def wq_def) + context valid_trace begin @@ -60,39 +67,70 @@ qed lemma wq_distinct: "distinct (wq s cs)" -proof(rule ind, simp add:wq_def) - fix s e - assume h1: "step s e" - and h2: "distinct (wq s cs)" - thus "distinct (wq (e # s) cs)" - proof(induct rule:step.induct, auto simp: wq_def Let_def split:list.splits) - fix thread s - assume h1: "(Cs cs, Th thread) \ (RAG s)\<^sup>+" - and h2: "thread \ set (wq_fun (schs s) cs)" - and h3: "thread \ runing s" - show "False" - proof - - from h3 have "\ cs. thread \ set (wq_fun (schs s) cs) \ - thread = hd ((wq_fun (schs s) cs))" - by (simp add:runing_def readys_def s_waiting_def wq_def) - from this [OF h2] have "thread = hd (wq_fun (schs s) cs)" . - with h2 - have "(Cs cs, Th thread) \ (RAG s)" - by (simp add:s_RAG_def s_holding_def wq_def cs_holding_def) - with h1 show False by auto +proof(induct rule:ind) + case (Cons s e) + from Cons(4,3) + show ?case + proof(induct) + case (thread_P th s cs1) + show ?case + proof(cases "cs = cs1") + case True + thus ?thesis (is "distinct ?L") + proof - + have "?L = wq_fun (schs s) cs1 @ [th]" using True + by (simp add:wq_def wf_def Let_def split:list.splits) + moreover have "distinct ..." + proof - + have "th \ set (wq_fun (schs s) cs1)" + proof + assume otherwise: "th \ set (wq_fun (schs s) cs1)" + from runing_head[OF thread_P(1) this] + have "th = hd (wq_fun (schs s) cs1)" . + hence "(Cs cs1, Th th) \ (RAG s)" using otherwise + by (simp add:s_RAG_def s_holding_def wq_def cs_holding_def) + with thread_P(2) show False by auto + qed + moreover have "distinct (wq_fun (schs s) cs1)" + using True thread_P wq_def by auto + ultimately show ?thesis by auto + qed + ultimately show ?thesis by simp + qed + next + case False + with thread_P(3) + show ?thesis + by (auto simp:wq_def wf_def Let_def split:list.splits) qed next - fix thread s a list - assume dst: "distinct list" - show "distinct (SOME q. distinct q \ set q = set list)" - proof(rule someI2) - from dst show "distinct list \ set list = set list" by auto + case (thread_V th s cs1) + thus ?case + proof(cases "cs = cs1") + case True + show ?thesis (is "distinct ?L") + proof(cases "(wq s cs)") + case Nil + thus ?thesis + by (auto simp:wq_def wf_def Let_def split:list.splits) + next + case (Cons w_hd w_tl) + moreover have "distinct (SOME q. distinct q \ set q = set w_tl)" + proof(rule someI2) + from thread_V(3)[unfolded Cons] + show "distinct w_tl \ set w_tl = set w_tl" by auto + qed auto + ultimately show ?thesis + by (auto simp:wq_def wf_def Let_def True split:list.splits) + qed next - fix q assume "distinct q \ set q = set list" - thus "distinct q" by auto + case False + with thread_V(3) + show ?thesis + by (auto simp:wq_def wf_def Let_def split:list.splits) qed - qed -qed + qed (insert Cons, auto simp: wq_def Let_def split:list.splits) +qed (unfold wq_def Let_def, simp) end @@ -108,56 +146,34 @@ *} lemma block_pre: - assumes s_ni: "thread \ set (wq s cs)" + assumes s_ni: "thread \ set (wq s cs)" and s_i: "thread \ set (wq (e#s) cs)" shows "e = P thread cs" -proof - - show ?thesis - proof(cases e) - case (P th cs) - with assms +proof(cases e) + -- {* This is the only non-trivial case: *} + case (V th cs1) + have False + proof(cases "cs1 = cs") + case True show ?thesis - by (auto simp:wq_def Let_def split:if_splits) - next - case (Create th prio) - with assms show ?thesis - by (auto simp:wq_def Let_def split:if_splits) - next - case (Exit th) - with assms show ?thesis - by (auto simp:wq_def Let_def split:if_splits) - next - case (Set th prio) - with assms show ?thesis - by (auto simp:wq_def Let_def split:if_splits) - next - case (V th cs) - with vt_e assms show ?thesis - apply (auto simp:wq_def Let_def split:if_splits) - proof - - fix q qs - assume h1: "thread \ set (wq_fun (schs s) cs)" - and h2: "q # qs = wq_fun (schs s) cs" - and h3: "thread \ set (SOME q. distinct q \ set q = set qs)" - and vt: "vt (V th cs # s)" - from h1 and h2[symmetric] have "thread \ set (q # qs)" by simp - moreover have "thread \ set qs" + proof(cases "(wq s cs1)") + case (Cons w_hd w_tl) + have "set (wq (e#s) cs) \ set (wq s cs)" proof - - have "set (SOME q. distinct q \ set q = set qs) = set qs" + have "(wq (e#s) cs) = (SOME q. distinct q \ set q = set w_tl)" + using Cons V by (auto simp:wq_def Let_def True split:if_splits) + moreover have "set ... \ set (wq s cs)" proof(rule someI2) - from wq_distinct [of cs] - and h2[symmetric, folded wq_def] - show "distinct qs \ set qs = set qs" by auto - next - fix x assume "distinct x \ set x = set qs" - thus "set x = set qs" by auto - qed - with h3 show ?thesis by simp + show "distinct w_tl \ set w_tl = set w_tl" + by (metis distinct.simps(2) local.Cons wq_distinct) + qed (insert Cons True, auto) + ultimately show ?thesis by simp qed - ultimately show "False" by auto - qed - qed -qed + with assms show ?thesis by auto + qed (insert assms V True, auto simp:wq_def Let_def split:if_splits) + qed (insert assms V, auto simp:wq_def Let_def split:if_splits) + thus ?thesis by auto +qed (insert assms, auto simp:wq_def Let_def split:if_splits) end @@ -233,10 +249,10 @@ end + context valid_trace begin - -lemma vt_moment: "\ t. vt (moment t s)" +lemma vt_moment: "\ t. vt (moment t s)" proof(induct rule:ind) case Nil thus ?case by (simp add:vt_nil) @@ -260,10 +276,17 @@ ultimately show ?thesis by simp qed qed +end -(* Wrong: - lemma \thread \ set (wq_fun cs1 s); thread \ set (wq_fun cs2 s)\ \ cs1 = cs2" -*) +locale valid_moment = valid_trace + + fixes i :: nat + +sublocale valid_moment < vat_moment: valid_trace "(moment i s)" + by (unfold_locales, insert vt_moment, auto) + +context valid_trace +begin + text {* (* ddd *) The nature of the work is like this: since it starts from a very simple and basic @@ -292,13 +315,13 @@ @{text "th"} got blocked on @{text "cs1"} and @{text "cs2"} and kept on blocked on them respectively ever since. - Without lose of generality, we assume @{text "t1"} is earlier than @{text "t2"}. + Without lost of generality, we assume @{text "t1"} is earlier than @{text "t2"}. However, since @{text "th"} was blocked ever since memonent @{text "t1"}, so it was still in blocked state at moment @{text "t2"} and could not make any request and get blocked the second time: Contradiction. *} -lemma waiting_unique_pre: +lemma waiting_unique_pre: (* ccc *) assumes h11: "thread \ set (wq s cs1)" and h12: "thread \ hd (wq s cs1)" assumes h21: "thread \ set (wq s cs2)" @@ -519,7 +542,6 @@ (* An aux lemma used later *) lemma unique_minus: - fixes x y z r assumes unique: "\ a b c. \(a, b) \ r; (a, c) \ r\ \ b = c" and xy: "(x, y) \ r" and xz: "(x, z) \ r^+" @@ -547,7 +569,6 @@ qed lemma unique_base: - fixes r x y z assumes unique: "\ a b c. \(a, b) \ r; (a, c) \ r\ \ b = c" and xy: "(x, y) \ r" and xz: "(x, z) \ r^+" @@ -574,7 +595,6 @@ qed lemma unique_chain: - fixes r x y z assumes unique: "\ a b c. \(a, b) \ r; (a, c) \ r\ \ b = c" and xy: "(x, y) \ r^+" and xz: "(x, z) \ r^+" @@ -914,7 +934,6 @@ with the happening of @{text "V"}-events: *} lemma step_RAG_v: -fixes th::thread assumes vt: "vt (V th cs#s)" shows " @@ -1342,7 +1361,6 @@ by (auto intro:wq_threads) lemma readys_v_eq: - fixes th thread cs rest assumes neq_th: "th \ thread" and eq_wq: "wq s cs = thread#rest" and not_in: "th \ set rest" @@ -1511,7 +1529,6 @@ lemma step_holdents_p_add: - fixes th cs s assumes vt: "vt (P th cs#s)" and "wq s cs = []" shows "holdents (P th cs#s) th = holdents s th \ {cs}" @@ -1521,7 +1538,6 @@ qed lemma step_holdents_p_eq: - fixes th cs s assumes vt: "vt (P th cs#s)" and "wq s cs \ []" shows "holdents (P th cs#s) th = holdents s th" @@ -1551,7 +1567,6 @@ qed lemma cntCS_v_dec: - fixes s thread cs assumes vtv: "vt (V thread cs#s)" shows "(cntCS (V thread cs#s) thread + 1) = cntCS s thread" proof - diff -r 25fd656667a7 -r db196b066b97 PIPBasics.thy~ --- a/PIPBasics.thy~ Sat Jan 09 22:19:27 2016 +0800 +++ b/PIPBasics.thy~ Tue Jan 12 08:35:36 2016 +0800 @@ -33,6 +33,13 @@ context valid_trace begin +lemma actor_inv: + assumes "PIP s e" + and "\ isCreate e" + shows "actor e \ runing s" + using assms + by (induct, auto) + lemma ind [consumes 0, case_names Nil Cons, induct type]: assumes "PP []" and "(\s e. valid_trace s \ valid_trace (e#s) \ @@ -1620,6 +1627,52 @@ ultimately show ?thesis by (simp add:cntCS_def) qed +lemma count_rec1 [simp]: + assumes "Q e" + shows "count Q (e#es) = Suc (count Q es)" + using assms + by (unfold count_def, auto) + +lemma count_rec2 [simp]: + assumes "\Q e" + shows "count Q (e#es) = (count Q es)" + using assms + by (unfold count_def, auto) + +lemma count_rec3 [simp]: + shows "count Q [] = 0" + by (unfold count_def, auto) + +lemma cntP_diff_inv: + assumes "cntP (e#s) th \ cntP s th" + shows "isP e \ actor e = th" +proof(cases e) + case (P th' pty) + show ?thesis + by (cases "(\e. \cs. e = P th cs) (P th' pty)", + insert assms P, auto simp:cntP_def) +qed (insert assms, auto simp:cntP_def) + +lemma isP_E: + assumes "isP e" + obtains cs where "e = P (actor e) cs" + using assms by (cases e, auto) + +lemma isV_E: + assumes "isV e" + obtains cs where "e = V (actor e) cs" + using assms by (cases e, auto) (* ccc *) + +lemma cntV_diff_inv: + assumes "cntV (e#s) th \ cntV s th" + shows "isV e \ actor e = th" +proof(cases e) + case (V th' pty) + show ?thesis + by (cases "(\e. \cs. e = V th cs) (V th' pty)", + insert assms V, auto simp:cntV_def) +qed (insert assms, auto simp:cntV_def) + context valid_trace begin