--- 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 ((\<lambda> 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' \<in> 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 "\<dots> = ?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' \<in> threads (t@s)"
- and neq_th': "th' \<noteq> th"
+*} (* ccc *)
+
+lemma eq_pv_blocked: (* ddd *)
+ assumes neq_th': "th' \<noteq> th"
and eq_pv: "cntP (t@s) th' = cntV (t@s) th'"
shows "th' \<notin> runing (t@s)"
proof
assume otherwise: "th' \<in> runing (t@s)"
show False
proof -
+ have th'_in: "th' \<in> 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' \<in> threads s"
and eq_pv: "cntP s th' = cntV s th'"
and neq_th': "th' \<noteq> th"
@@ -521,7 +547,7 @@
proof(cases)
assume "thread \<in> runing (t@s)"
moreover have "th' \<notin> 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 \<in> runing (t@s)"
moreover have "th' \<notin> 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' \<in> threads s"
and neq_th': "th' \<noteq> th"
and is_runing: "th' \<in> 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' \<noteq> 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' \<notin> runing (t@s)"
+ proof(rule eq_pv_blocked)
+ show "th' \<noteq> 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' \<le> 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' \<noteq> 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' \<in> 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 "\<dots> = ?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' \<noteq> th"
- and runing': "th' \<in> runing (t@s)"
+ and neq_th': "th' \<noteq> th"
shows "th' \<in> 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' \<noteq> th"
- and runing': "th' \<in> runing (t@s)"
- -- {* thread @{term "th'"} is a live on in state @{term "s"} and
- it has some unreleased resource. *}
- shows "th' \<in> threads s \<and> 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' \<in> 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' \<in> runing (t@s)"
- shows "th' = th \<or> (th' \<noteq> th \<and> th' \<in> threads s \<and> 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' \<in> runing (t@s)"
- and neq_th: "th' \<noteq> th"
- shows "th' \<in> threads s \<and> (cntV s th' < cntP s th' \<and> 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' \<in> runing (t@s)"
and neq_th: "th' \<noteq> th"
shows "th' \<in> threads s"
and "\<not>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' \<in> threads s" .
+next
+ from runing_cntP_cntV_inv[OF runing_threads_inv[OF assms] neq_th runing']
+ show "\<not>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