--- a/PIPBasics.thy Thu Feb 04 14:45:30 2016 +0800
+++ b/PIPBasics.thy Fri Feb 05 20:11:12 2016 +0800
@@ -322,8 +322,9 @@
text {*
The following lemmas are the simplification rules
for @{term count}, @{term cntP}, @{term cntV}.
- It is a major technical in this development to use
- the counter of @{term "P"} and @{term "V"} (* ccc *)
+ It is part of the scheme to use the counting
+ of @{term "P"} and @{term "V"} operations to reason about
+ the number of resources occupied by one thread.
*}
lemma count_rec1 [simp]:
@@ -374,6 +375,12 @@
using assms
by (unfold cntV_def, cases e, simp+)
+text {*
+ The following two lemmas show that only @{term P}
+ and @{term V} operation can change the value
+ of @{term cntP} and @{term cntV}, which is true
+ obviously.
+*}
lemma cntP_diff_inv:
assumes "cntP (e#s) th \<noteq> cntP s th"
shows "isP e \<and> actor e = th"
@@ -394,8 +401,6 @@
insert assms V, auto simp:cntV_def)
qed (insert assms, auto simp:cntV_def)
-(* ccc *)
-
section {* Locales used to investigate the execution of PIP *}
text {*
@@ -689,14 +694,23 @@
using vt_moment[of "Suc i", unfolded trace_e]
by (unfold_locales, simp)
-section {* Distinctiveness of waiting queues *}
-
-lemma (in valid_trace) finite_threads:
- shows "finite (threads s)"
- using vt by (induct) (auto elim: step.cases)
-
-lemma (in valid_trace) finite_readys [simp]: "finite (readys s)"
- using finite_threads readys_threads rev_finite_subset by blast
+section {* Waiting queues are distinct *}
+
+text {*
+ This section proofs that every waiting queue in the system
+ is distinct, given in lemma @{text wq_distinct}.
+
+ The proof is split into the locales for events (or operations),
+ all contain a lemma named @{text "wq_distinct_kept"} to show that
+ the distinctiveness is preserved by the respective operation. All lemmas
+ before are to facilitate the proof of @{text "wq_distinct_kept"}.
+
+ The proof also demonstrates the common pattern to prove
+ invariant properties over valid traces, i.e. to spread the
+ invariant proof into locales and to assemble the results of all
+ locales to complete the final proof.
+
+*}
context valid_trace_create
begin
@@ -760,7 +774,7 @@
with cs_th_RAG show ?thesis by auto
qed
qed
-
+
lemma wq_es_cs:
"wq (e#s) cs = wq s cs @ [th]"
by (unfold is_p wq_def, auto simp:Let_def)
@@ -834,6 +848,13 @@
context valid_trace
begin
+text {*
+ The proof of @{text "wq_distinct"} shows how the results
+ proved in the foregoing locales are assembled in
+ a overall structure of induction and case analysis
+ to get the final conclusion. This scheme will be
+ used repeatedly in the following.
+*}
lemma wq_distinct: "distinct (wq s cs)"
proof(induct rule:ind)
case (Cons s e)
@@ -869,99 +890,96 @@
section {* Waiting queues and threads *}
-context valid_trace_e
+text {*
+ This section shows that all threads withing waiting queues are
+ in the @{term threads}-set. In other words, @{term threads} covers
+ all the threads in waiting queue.
+
+ The proof follows the same pattern as @{thm valid_trace.wq_distinct}.
+ The desired property is shown to be kept by all operations (or events)
+ in their respective locales, and finally the main lemmas is
+ derived by assembling the invariant keeping results of the locales.
+*}
+
+context valid_trace_create
begin
-lemma wq_out_inv:
- assumes s_in: "thread \<in> set (wq s cs)"
- and s_hd: "thread = hd (wq s cs)"
- and s_i: "thread \<noteq> hd (wq (e#s) cs)"
- shows "e = V thread cs"
-proof(cases e)
--- {* There are only two non-trivial cases: *}
- case (V th cs1)
- show ?thesis
- proof(cases "cs1 = cs")
- case True
- have "PIP s (V th cs)" using pip_e[unfolded V[unfolded True]] .
- thus ?thesis
- proof(cases)
- case (thread_V)
- moreover have "th = thread" using thread_V(2) s_hd
- by (unfold s_holding_def wq_def, simp)
- ultimately show ?thesis using V True by simp
- qed
- qed (insert assms V, auto simp:wq_def Let_def split:if_splits)
-next
- case (P th cs1)
- show ?thesis
- proof(cases "cs1 = cs")
- case True
- with P have "wq (e#s) cs = wq_fun (schs s) cs @ [th]"
- by (auto simp:wq_def Let_def split:if_splits)
- with s_i s_hd s_in have False
- by (metis empty_iff hd_append2 list.set(1) wq_def)
- thus ?thesis by simp
- qed (insert assms P, auto simp:wq_def Let_def split:if_splits)
-qed (insert assms, auto simp:wq_def Let_def split:if_splits)
-
-lemma wq_in_inv:
- assumes s_ni: "thread \<notin> set (wq s cs)"
- and s_i: "thread \<in> set (wq (e#s) cs)"
- shows "e = P thread cs"
-proof(cases e)
- -- {* This is the only non-trivial case: *}
- case (V th cs1)
- have False
- proof(cases "cs1 = cs")
- case True
- show ?thesis
- proof(cases "(wq s cs1)")
- case (Cons w_hd w_tl)
- have "set (wq (e#s) cs) \<subseteq> set (wq s cs)"
- proof -
- have "(wq (e#s) cs) = (SOME q. distinct q \<and> set q = set w_tl)"
- using Cons V by (auto simp:wq_def Let_def True split:if_splits)
- moreover have "set ... \<subseteq> set (wq s cs)"
- proof(rule someI2)
- show "distinct w_tl \<and> 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
- 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
-
-lemma (in valid_trace_create)
+lemma
th_not_in_threads: "th \<notin> threads s"
proof -
from pip_e[unfolded is_create]
show ?thesis by (cases, simp)
qed
-lemma (in valid_trace_create)
+lemma
threads_es [simp]: "threads (e#s) = threads s \<union> {th}"
by (unfold is_create, simp)
-lemma (in valid_trace_exit)
- threads_es [simp]: "threads (e#s) = threads s - {th}"
+lemma wq_threads_kept:
+ assumes "\<And> th' cs'. th' \<in> set (wq s cs') \<Longrightarrow> th' \<in> threads s"
+ and "th' \<in> set (wq (e#s) cs')"
+ shows "th' \<in> threads (e#s)"
+proof -
+ have "th' \<in> threads s"
+ proof -
+ from assms(2)[unfolded wq_kept]
+ have "th' \<in> set (wq s cs')" .
+ from assms(1)[OF this] show ?thesis .
+ qed
+ with threads_es show ?thesis by simp
+qed
+
+end
+
+context valid_trace_exit
+begin
+
+lemma threads_es [simp]: "threads (e#s) = threads s - {th}"
by (unfold is_exit, simp)
-lemma (in valid_trace_p)
- threads_es [simp]: "threads (e#s) = threads s"
- by (unfold is_p, simp)
-
-lemma (in valid_trace_v)
+lemma
+ th_not_in_wq: "th \<notin> set (wq s cs)"
+proof -
+ from pip_e[unfolded is_exit]
+ show ?thesis
+ by (cases, unfold holdents_def s_holding_def, fold wq_def,
+ auto elim!:runing_wqE)
+qed
+
+lemma wq_threads_kept:
+ assumes "\<And> th' cs'. th' \<in> set (wq s cs') \<Longrightarrow> th' \<in> threads s"
+ and "th' \<in> set (wq (e#s) cs')"
+ shows "th' \<in> threads (e#s)"
+proof -
+ have "th' \<in> threads s"
+ proof -
+ from assms(2)[unfolded wq_kept]
+ have "th' \<in> set (wq s cs')" .
+ from assms(1)[OF this] show ?thesis .
+ qed
+ moreover have "th' \<noteq> th"
+ proof
+ assume otherwise: "th' = th"
+ from assms(2)[unfolded wq_kept]
+ have "th' \<in> set (wq s cs')" .
+ with th_not_in_wq[folded otherwise]
+ show False by simp
+ qed
+ ultimately show ?thesis
+ by (unfold threads_es, simp)
+qed
+
+end
+
+context valid_trace_v
+begin
+
+lemma
threads_es [simp]: "threads (e#s) = threads s"
by (unfold is_v, simp)
-lemma (in valid_trace_v)
- th_not_in_rest[simp]: "th \<notin> set rest"
+lemma
+ th_not_in_rest: "th \<notin> set rest"
proof
assume otherwise: "th \<in> set rest"
have "distinct (wq s cs)" by (simp add: wq_distinct)
@@ -969,10 +987,10 @@
show False by auto
qed
-lemma (in valid_trace_v) distinct_rest: "distinct rest"
+lemma distinct_rest: "distinct rest"
by (simp add: distinct_tl rest_def wq_distinct)
-lemma (in valid_trace_v)
+lemma
set_wq_es_cs [simp]: "set (wq (e#s) cs) = set (wq s cs) - {th}"
proof(unfold wq_es_cs wq'_def, rule someI2)
show "distinct rest \<and> set rest = set rest"
@@ -981,23 +999,117 @@
fix x
assume "distinct x \<and> set x = set rest"
thus "set x = set (wq s cs) - {th}"
- by (unfold wq_s_cs, simp)
+ by (unfold wq_s_cs, simp add:th_not_in_rest)
+qed
+
+lemma wq_threads_kept:
+ assumes "\<And> th' cs'. th' \<in> set (wq s cs') \<Longrightarrow> th' \<in> threads s"
+ and "th' \<in> set (wq (e#s) cs')"
+ shows "th' \<in> threads (e#s)"
+proof(cases "cs' = cs")
+ case True
+ have " th' \<in> threads s"
+ proof -
+ from assms(2)[unfolded True set_wq_es_cs]
+ have "th' \<in> set (wq s cs) - {th}" .
+ hence "th' \<in> set (wq s cs)" by simp
+ from assms(1)[OF this]
+ show ?thesis .
+ qed
+ with threads_es show ?thesis by simp
+next
+ case False
+ have "th' \<in> threads s"
+ proof -
+ from wq_neq_simp[OF False]
+ have "wq (e # s) cs' = wq s cs'" .
+ from assms(2)[unfolded this]
+ have "th' \<in> set (wq s cs')" .
+ from assms(1)[OF this]
+ show ?thesis .
+ qed
+ with threads_es show ?thesis by simp
qed
-
-lemma (in valid_trace_exit)
- th_not_in_wq: "th \<notin> set (wq s cs)"
+end
+
+context valid_trace_p
+begin
+
+lemma threads_es [simp]: "threads (e#s) = threads s"
+ by (unfold is_p, simp)
+
+lemma ready_th_s: "th \<in> readys s"
+ using runing_th_s
+ by (unfold runing_def, auto)
+
+lemma live_th_s: "th \<in> threads s"
+ using readys_threads ready_th_s by auto
+
+lemma wq_threads_kept:
+ assumes "\<And> th' cs'. th' \<in> set (wq s cs') \<Longrightarrow> th' \<in> threads s"
+ and "th' \<in> set (wq (e#s) cs')"
+ shows "th' \<in> threads (e#s)"
+proof(cases "cs' = cs")
+ case True
+ from assms(2)[unfolded True wq_es_cs]
+ have "th' \<in> set (wq s cs) \<or> th' = th" by auto
+ thus ?thesis
+ proof
+ assume "th' \<in> set (wq s cs)"
+ from assms(1)[OF this] have "th' \<in> threads s" .
+ with threads_es
+ show ?thesis by simp
+ next
+ assume "th' = th"
+ with live_th_s have "th' \<in> threads s" by simp
+ with threads_es show ?thesis by simp
+ qed
+next
+ case False
+ have "th' \<in> threads s"
+ proof -
+ from wq_neq_simp[OF False]
+ have "wq (e # s) cs' = wq s cs'" .
+ from assms(2)[unfolded this]
+ have "th' \<in> set (wq s cs')" .
+ from assms(1)[OF this]
+ show ?thesis .
+ qed
+ with threads_es show ?thesis by simp
+qed
+
+end
+
+context valid_trace_set
+begin
+
+lemma threads_kept[simp]:
+ "threads (e#s) = threads s"
+ by (unfold is_set, simp)
+
+lemma wq_threads_kept:
+ assumes "\<And> th' cs'. th' \<in> set (wq s cs') \<Longrightarrow> th' \<in> threads s"
+ and "th' \<in> set (wq (e#s) cs')"
+ shows "th' \<in> threads (e#s)"
proof -
- from pip_e[unfolded is_exit]
- show ?thesis
- by (cases, unfold holdents_def s_holding_def, fold wq_def,
- auto elim!:runing_wqE)
+ have "th' \<in> threads s"
+ using assms(1)[OF assms(2)[unfolded wq_kept]] .
+ with threads_kept show ?thesis by simp
qed
+end
+
+text {*
+ The is the main lemma of this section, which is derived
+ by induction, case analysis on event @{text e} and
+ assembling the @{text "wq_threads_kept"}-results of
+ all possible cases of @{text "e"}.
+*}
lemma (in valid_trace) wq_threads:
assumes "th \<in> set (wq s cs)"
shows "th \<in> threads s"
using assms
-proof(induct rule:ind)
+proof(induct arbitrary:th cs rule:ind)
case (Nil)
thus ?case by (auto simp:wq_def)
next
@@ -1008,42 +1120,41 @@
case (Create th' prio')
interpret vt: valid_trace_create s e th' prio'
using Create by (unfold_locales, simp)
- show ?thesis
- using Cons.hyps(2) Cons.prems by auto
+ show ?thesis using vt.wq_threads_kept Cons by auto
next
case (Exit th')
interpret vt: valid_trace_exit s e th'
using Exit by (unfold_locales, simp)
- show ?thesis
- using Cons.hyps(2) Cons.prems vt.th_not_in_wq by auto
+ show ?thesis using vt.wq_threads_kept Cons by auto
next
case (P th' cs')
interpret vt: valid_trace_p s e th' cs'
using P by (unfold_locales, simp)
- show ?thesis
- using Cons.hyps(2) Cons.prems readys_threads
- runing_ready vt.is_p vt.runing_th_s vt_e.wq_in_inv
- by fastforce
+ show ?thesis using vt.wq_threads_kept Cons by auto
next
case (V th' cs')
interpret vt: valid_trace_v s e th' cs'
using V by (unfold_locales, simp)
- show ?thesis using Cons
- using vt.is_v vt.threads_es vt_e.wq_in_inv by blast
+ show ?thesis using vt.wq_threads_kept Cons by auto
next
case (Set th' prio)
interpret vt: valid_trace_set s e th' prio
using Set by (unfold_locales, simp)
- show ?thesis using Cons.hyps(2) Cons.prems vt.is_set
- by (auto simp:wq_def Let_def)
+ show ?thesis using vt.wq_threads_kept Cons by auto
qed
qed
-section {* RAG and threads *}
+subsection {* RAG and threads *}
context valid_trace
begin
+text {*
+ As corollaries of @{thm wq_threads}, it is shown in this subsection
+ that the fields (including both domain
+ and range) of @{term RAG} are covered by @{term threads}.
+*}
+
lemma dm_RAG_threads:
assumes in_dom: "(Th th) \<in> Domain (RAG s)"
shows "th \<in> threads s"
@@ -1669,8 +1780,8 @@
assumes "waiting (e#s) th' cs'"
obtains "waiting s th' cs'"
using assms
- by (metis cs_waiting_def event.distinct(15) is_p list.sel(1)
- set_ConsD waiting_eq we wq_es_cs' wq_neq_simp wq_out_inv)
+ by (metis empty_iff list.sel(1) list.set(1) s_waiting_def
+ set_ConsD wq_def wq_es_cs' wq_neq_simp)
lemma holding_esE:
assumes "holding (e#s) th' cs'"
@@ -1771,9 +1882,7 @@
next
case True
with assms show ?thesis
- using event.inject(3) holder_def is_p s_holding_def s_waiting_def that
- waiting_es_th_cs wq_def wq_es_cs' wq_in_inv
- by(force)
+ using s_holding_def that wq_def wq_es_cs' wq_s_cs by auto
qed
lemma waiting_esE:
@@ -1870,7 +1979,7 @@
end
-section {* Finiteness of RAG *}
+section {* RAG is finite *}
context valid_trace
begin
@@ -2952,6 +3061,9 @@
by (simp add: subtree_def the_preced_def)
qed
+lemma finite_threads:
+ shows "finite (threads s)"
+ using vt by (induct) (auto elim: step.cases)
lemma cp_le:
assumes th_in: "th \<in> threads s"
@@ -3016,6 +3128,8 @@
} ultimately show ?thesis by auto
qed
+lemma finite_readys: "finite (readys s)"
+ using finite_threads readys_threads rev_finite_subset by blast
text {* (* ccc *) \noindent
Since the current precedence of the threads in ready queue will always be boosted,
@@ -3038,7 +3152,7 @@
show "\<forall>M\<in>(\<lambda>x. the_preced s `
{th'. Th th' \<in> subtree (RAG s) (Th x)}) ` readys s. finite M"
using finite_subtree_threads by auto
- qed (auto simp:False subtree_def)
+ qed (auto simp:False subtree_def finite_readys)
also have "... =
Max ((Max \<circ> (\<lambda>th. the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)})) ` readys s)"
by (unfold image_comp, simp)
@@ -3132,9 +3246,6 @@
using runing_th_s
by (unfold runing_def, auto)
-lemma live_th_s: "th \<in> threads s"
- using readys_threads ready_th_s by auto
-
lemma live_th_es: "th \<in> threads (e#s)"
using live_th_s
by (unfold is_p, simp)