--- 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,268 +456,6 @@
vat_s.le_cp)
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 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"
- 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' = th"
- proof(rule preced_unique)
- show "preced th' (t @ s) = preced th (t @ s)" (is "?L = ?R")
- proof -
- 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)
- finally show ?thesis .
- qed
- qed (auto simp: th'_in th_kept)
- moreover have "th' \<noteq> th" using neq_th' .
- ultimately show ?thesis by simp
- qed
-qed
-
-lemmas pv_blocked = pv_blocked_pre[folded detached_eq]
-
-lemma runing_precond_pre: (* ddd *)
- fixes th'
- assumes th'_in: "th' \<in> threads s"
- and eq_pv: "cntP s th' = cntV s th'"
- and neq_th': "th' \<noteq> th"
- shows "th' \<in> threads (t@s) \<and>
- cntP (t@s) th' = cntV (t@s) th'"
-proof(induct rule:ind)
- 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 \<noteq> th'"
- proof -
- have "step (t@s) (P thread cs)" using Cons P by auto
- thus ?thesis
- 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)
- 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' \<in> 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 \<noteq> th'"
- proof -
- have "step (t@s) (V thread cs)" using Cons V by auto
- thus ?thesis
- 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)
- 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' \<in> 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 \<noteq> 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' \<in> 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 \<noteq> 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.pv_blocked_pre)
- 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' \<in> 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)
- qed
-next
- case Nil
- with assms
- show ?case by auto
-qed
-
-text {* Changing counting balance to detachedness *}
-lemmas runing_precond_pre_dtc = runing_precond_pre
- [folded vat_t.detached_eq vat_s.detached_eq]
-
-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 -
- have "cntP s th' \<noteq> cntV s th'"
- by (metis is_runing neq_th' pv_blocked_pre runing_precond_pre th'_in)
- moreover have "cntV s th' \<le> cntP s th'" using vat_s.cnp_cnv_cncs by auto
- ultimately show ?thesis by auto
-qed
-
-lemma moment_blocked_pre:
- assumes neq_th': "th' \<noteq> th"
- and th'_in: "th' \<in> 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' \<and>
- th' \<in> 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 \<in> 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' \<in> set (moment j (restm i t))"
- thus "prio' \<le> 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' \<in> set (moment j (restm i t))"
- thus "th' \<noteq> th \<and> prio' \<le> prio"
- by (metis Un_iff add.commute h_j.set_diff_low moment_plus_split set_append)
- next
- fix th'
- assume "Exit th' \<in> set (moment j (restm i t))"
- thus "th' \<noteq> 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.runing_precond_pre
- moment_plus_split neq_th' th'_in)
-qed
-
-lemma moment_blocked_eqpv: (* ddd *)
- assumes neq_th': "th' \<noteq> th"
- and th'_in: "th' \<in> threads ((moment i t)@s)"
- and eq_pv: "cntP ((moment i t)@s) th' = cntV ((moment i t)@s) th'"
- and le_ij: "i \<le> j"
- shows "cntP ((moment j t)@s) th' = cntV ((moment j t)@s) th' \<and>
- th' \<in> threads ((moment j t)@s) \<and>
- th' \<notin> 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' \<in> threads ((moment j t)@s)" by auto
- moreover have "th' \<notin> runing ((moment j t)@s)"
- proof -
- interpret h: red_extend_highest_gen _ _ _ _ _ j by (unfold_locales)
- show ?thesis
- using h.pv_blocked_pre 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"
- and th'_in: "th' \<in> threads ((moment i t)@s)"
- and dtc: "detached (moment i t @ s) th'"
- and le_ij: "i \<le> j"
- shows "detached (moment j t @ s) th' \<and>
- th' \<in> threads ((moment j t)@s) \<and>
- th' \<notin> 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 that the @{term cp}-value
of the blocking thread @{text th'} equals to the highest
precedence in the whole system.
@@ -735,67 +471,190 @@
finally show ?thesis .
qed
+section {* The `blocking 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 following lemma shows that the counting controls whether
+ a thread is running or not.
+*} (* 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)
+ -- {* 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)
+ moreover have "th' \<noteq> th" using neq_th' .
+ ultimately show ?thesis by simp
+ qed
+qed
+
+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' \<noteq> th"
+ and eq_pv: "cntP s th' = cntV s th'"
+ 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)
+ -- {* 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' \<noteq> 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' \<in> 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' \<notin> runing (t@s)"
+ using vat_t.eq_pv_blocked[OF neq_th' Cons(5)] .
+ -- {* Contradiction is finally derived: *}
+ ultimately show False by simp
+ 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' \<noteq> 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' \<in> runing (t@s)" by (cases e, auto)
+ moreover have "th' \<notin> 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)
+
+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' \<noteq> th"
+ and eq_pv: "cntP s th' = cntV s th'"
+ shows "th' \<notin> 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
+ 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.
+*}
+lemma runing_cntP_cntV_inv: (* ddd *)
+ assumes is_runing: "th' \<in> runing (t@s)"
+ and neq_th': "th' \<noteq> th"
+ shows "cntP s th' > cntV s th'"
+ using assms
+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' \<noteq> cntV s th'"
+ proof
+ -- {* The proof goes by contradiction, suppose otherwise: *}
+ assume otherwise: "cntP s th' = cntV s th'"
+ -- {* 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' \<notin> 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' \<le> 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
+
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 *)
+lemma runing_threads_inv:
assumes runing': "th' \<in> runing (t@s)"
and neq_th': "th' \<noteq> th"
shows "th' \<in> threads s"
-proof -
- -- {* The proof is by contradiction: *}
- { assume otherwise: "\<not> ?thesis"
- have "th' \<notin> runing (t @ s)"
- proof -
- -- {* Since @{term "th'"} is running at time @{term "t@s"}, so it exists that time. *}
- have th'_in: "th' \<in> 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' \<notin> 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 \<le> i"
- and pre: " th' \<notin> threads (moment i t @ s)" (is "th' \<notin> threads ?pre")
- and post: "(\<forall>i'>i. th' \<in> 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 \<le> 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' \<in> 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' \<in> runing (t@s)`
- have False by simp
- } thus ?thesis by auto
+proof(rule ccontr) -- {* Proof by contradiction: *}
+ assume otherwise: "th' \<notin> threads s"
+ have "th' \<notin> 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' \<in> runing (t@s)"
and neq_th: "th' \<noteq> th"
shows "th' \<in> threads s"
@@ -805,13 +664,15 @@
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']
+ from runing_cntP_cntV_inv[OF runing' neq_th]
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
+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'"}
@@ -822,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 \<notin> runing (t@s)"
obtains th' where "Th th' \<in> ancestors (RAG (t @ s)) (Th th)"
"th' \<in> runing (t@s)"
@@ -898,6 +759,3 @@
end
end
-
-
-