diff -r 2af87bb52fca -r 25fd656667a7 Correctness.thy~ --- a/Correctness.thy~ Thu Jan 07 22:10:06 2016 +0800 +++ b/Correctness.thy~ Sat Jan 09 22:19:27 2016 +0800 @@ -79,7 +79,6 @@ ultimately show ?thesis by auto qed -(* ccc *) 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) @@ -135,7 +134,6 @@ apply (unfold extend_highest_gen_def extend_highest_gen_axioms_def, clarsimp) by (unfold highest_gen_def, auto dest:step_back_vt_app) - context extend_highest_gen begin @@ -458,6 +456,23 @@ vat_s.le_cp) text {* + The following lemmas shows that the @{term cp}-value + of the blocking thread @{text th'} equals to the highest + precedence in the whole system. +*} +lemma runing_preced_inversion: + assumes runing': "th' \ runing (t@s)" + shows "cp (t@s) th' = preced th s" (is "?L = ?R") +proof - + have "?L = Max (cp (t @ s) ` readys (t @ s))" using assms + by (unfold runing_def, auto) + also have "\ = ?R" + by (metis th_cp_max th_cp_preced vat_t.max_cp_readys_threads) + finally show ?thesis . +qed + + +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 @@ -465,27 +480,37 @@ The following lemma shows that the counting controls whether a thread is running or not. -*} - -lemma pv_blocked_pre: (* ddd *) - assumes th'_in: "th' \ threads (t@s)" - and neq_th': "th' \ th" +*} (* ccc *) + +lemma eq_pv_blocked: (* ddd *) + assumes neq_th': "th' \ th" and eq_pv: "cntP (t@s) th' = cntV (t@s) th'" shows "th' \ runing (t@s)" proof assume otherwise: "th' \ runing (t@s)" show False proof - + have th'_in: "th' \ threads (t@s)" + using otherwise readys_threads runing_def by auto have "th' = th" proof(rule preced_unique) + -- {* The proof goes like this: + it is first shown that the @{term preced}-value of @{term th'} + equals to that of @{term th}, then by uniqueness + of @{term preced}-values (given by lemma @{thm preced_unique}), + @{term th'} equals to @{term th}: *} show "preced th' (t @ s) = preced th (t @ s)" (is "?L = ?R") proof - + -- {* Since the counts of @{term th'} are balanced, the subtree + of it contains only itself, so, its @{term cp}-value + 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) - also have "... = cp (t @ s) th" using otherwise - by (metis (mono_tags, lifting) mem_Collect_eq - runing_def th_cp_max vat_t.max_cp_readys_threads) - also have "... = ?R" by (metis th_cp_preced th_kept) + -- {* 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}. *} + also have "... = ?R" + using runing_preced_inversion[OF otherwise] th_kept by simp finally show ?thesis . qed qed (auto simp: th'_in th_kept) @@ -494,10 +519,11 @@ qed qed -lemmas pv_blocked = pv_blocked_pre[folded detached_eq] +lemmas eq_pv_blocked_dtc = eq_pv_blocked[folded detached_eq] + -lemma runing_precond_pre: (* ddd *) - fixes th' + +lemma eq_pv_kept: (* ddd *) assumes th'_in: "th' \ threads s" and eq_pv: "cntP s th' = cntV s th'" and neq_th': "th' \ th" @@ -521,7 +547,7 @@ proof(cases) assume "thread \ runing (t@s)" moreover have "th' \ runing (t@s)" using Cons(5) - by (metis neq_th' vat_t.pv_blocked_pre) + by (metis neq_th' vat_t.eq_pv_blocked) ultimately show ?thesis by auto qed qed with Cons show ?thesis @@ -543,7 +569,7 @@ proof(cases) assume "thread \ runing (t@s)" moreover have "th' \ runing (t@s)" using Cons(5) - by (metis neq_th' vat_t.pv_blocked_pre) + by (metis neq_th' vat_t.eq_pv_blocked) ultimately show ?thesis by auto qed qed with Cons show ?thesis @@ -576,7 +602,7 @@ 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.pv_blocked_pre) + 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) @@ -596,20 +622,53 @@ show ?case by auto qed +(* runing_precond has changed to eq_pv_kept *) + text {* Changing counting balance to detachedness *} -lemmas runing_precond_pre_dtc = runing_precond_pre +lemmas eq_pv_kept_dtc = eq_pv_kept [folded vat_t.detached_eq vat_s.detached_eq] -lemma runing_precond: (* ddd *) - fixes th' +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. + + 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" and neq_th': "th' \ th" and is_runing: "th' \ runing (t@s)" shows "cntP s th' > cntV s th'" using assms -proof - +proof - (* ccc *) + -- {* 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'" - by (metis is_runing neq_th' pv_blocked_pre runing_precond_pre th'_in) + proof + 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 + -- {* This is obvious in contradiction with assumption @{thm is_runing} *} + thus False using is_runing by simp + qed moreover have "cntV s th' \ cntP s th'" using vat_s.cnp_cnv_cncs by auto ultimately show ?thesis by auto qed @@ -656,7 +715,7 @@ 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.runing_precond_pre + by (metis add.commute append_assoc eq_pv h.eq_pv_kept moment_plus_split neq_th' th'_in) qed @@ -676,13 +735,14 @@ proof - interpret h: red_extend_highest_gen _ _ _ _ _ j by (unfold_locales) show ?thesis - using h.pv_blocked_pre h1 h2 neq_th' by auto + 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" @@ -701,31 +761,13 @@ show ?thesis by (metis h_j.detached_intro) qed -lemma runing_preced_inversion: +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}. +*} +lemma runing_threads_inv: (* ddd *) (* ccc *) assumes runing': "th' \ runing (t@s)" - shows "cp (t@s) th' = preced th s" (is "?L = ?R") -proof - - have "?L = Max (cp (t @ s) ` readys (t @ s))" using assms - by (unfold runing_def, auto) - also have "\ = ?R" - by (metis th_cp_max th_cp_preced vat_t.max_cp_readys_threads) - finally show ?thesis . -qed - -text {* - The situation when @{term "th"} is blocked is analyzed by the following lemmas. -*} - -text {* - The following lemmas shows the running thread @{text "th'"}, if it is different from - @{term th}, must be live at the very beginning. By the term {\em the very beginning}, - we mean the moment where the formal investigation starts, i.e. the moment (or state) - @{term s}. -*} - -lemma runing_inversion_0: - assumes neq_th': "th' \ th" - and runing': "th' \ runing (t@s)" + and neq_th': "th' \ th" shows "th' \ threads s" proof - -- {* The proof is by contradiction: *} @@ -774,61 +816,26 @@ } thus ?thesis by auto qed -text {* - The second lemma says, if the running thread @{text th'} is different from - @{term th}, then this @{text th'} must in the possession of some resources - at the very beginning. - - To ease the reasoning of resource possession of one particular thread, - we used two auxiliary functions @{term cntV} and @{term cntP}, - which are the counters of @{term P}-operations and - @{term V}-operations respectively. - If the number of @{term V}-operation is less than the number of - @{term "P"}-operations, the thread must have some unreleased resource. +text {* + The following lemma summarizes several foregoing + lemmas to give an overall picture of the blocking thread @{text "th'"}: *} - -lemma runing_inversion_1: (* ddd *) - assumes neq_th': "th' \ th" - and runing': "th' \ runing (t@s)" - -- {* thread @{term "th'"} is a live on in state @{term "s"} and - it has some unreleased resource. *} - shows "th' \ threads s \ cntV s th' < cntP s th'" -proof - - -- {* The proof is a simple composition of @{thm runing_inversion_0} and - @{thm runing_precond}: *} - -- {* By applying @{thm runing_inversion_0} to assumptions, - it can be shown that @{term th'} is live in state @{term s}: *} - have "th' \ threads s" using runing_inversion_0[OF assms(1,2)] . - -- {* Then the thesis is derived easily by applying @{thm runing_precond}: *} - with runing_precond [OF this neq_th' runing'] show ?thesis by simp -qed - -text {* - The following lemma is just a rephrasing of @{thm runing_inversion_1}: -*} -lemma runing_inversion_2: - assumes runing': "th' \ runing (t@s)" - shows "th' = th \ (th' \ th \ th' \ threads s \ cntV s th' < cntP s th')" -proof - - from runing_inversion_1[OF _ runing'] - show ?thesis by auto -qed - -lemma runing_inversion_3: - assumes runing': "th' \ runing (t@s)" - and neq_th: "th' \ th" - shows "th' \ threads s \ (cntV s th' < cntP s th' \ cp (t@s) th' = preced th s)" - by (metis neq_th runing' runing_inversion_2 runing_preced_inversion) - -lemma runing_inversion_4: +lemma runing_inversion: assumes runing': "th' \ runing (t@s)" and neq_th: "th' \ th" shows "th' \ threads s" and "\detached s th'" and "cp (t@s) th' = preced th s" - apply (metis neq_th runing' runing_inversion_2) - apply (metis neq_th pv_blocked runing' runing_inversion_2 runing_precond_pre_dtc) - by (metis neq_th runing' runing_inversion_3) +proof - + 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'] + 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 text {* Suppose @{term th} is not running, it is first shown that