--- a/PIPBasics.thy Sun Jan 31 18:15:13 2016 +0800
+++ b/PIPBasics.thy Mon Feb 01 20:56:39 2016 +0800
@@ -86,6 +86,12 @@
finally show ?thesis by simp
qed
+lemma rel_eqI:
+ assumes "\<And> x y. (x,y) \<in> A \<Longrightarrow> (x,y) \<in> B"
+ and "\<And> x y. (x,y) \<in> B \<Longrightarrow> (x, y) \<in> A"
+ shows "A = B"
+ using assms by auto
+
section {* Lemmas do not depend on trace validity *}
lemma birth_time_lt:
@@ -206,6 +212,67 @@
with eq_wq that show ?thesis by metis
qed
+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)
+
+
+text {*
+ Every thread can only be blocked on one critical resource,
+ symmetrically, every critical resource can only be held by one thread.
+ This fact is much more easier according to our definition.
+*}
+lemma held_unique:
+ assumes "holding (s::event list) th1 cs"
+ and "holding s th2 cs"
+ shows "th1 = th2"
+ by (insert assms, unfold s_holding_def, auto)
+
+lemma last_set_lt: "th \<in> threads s \<Longrightarrow> last_set th s < length s"
+ apply (induct s, auto)
+ by (case_tac a, auto split:if_splits)
+
+lemma last_set_unique:
+ "\<lbrakk>last_set th1 s = last_set th2 s; th1 \<in> threads s; th2 \<in> threads s\<rbrakk>
+ \<Longrightarrow> th1 = th2"
+ apply (induct s, auto)
+ by (case_tac a, auto split:if_splits dest:last_set_lt)
+
+lemma preced_unique :
+ assumes pcd_eq: "preced th1 s = preced th2 s"
+ and th_in1: "th1 \<in> threads s"
+ and th_in2: " th2 \<in> threads s"
+ shows "th1 = th2"
+proof -
+ from pcd_eq have "last_set th1 s = last_set th2 s" by (simp add:preced_def)
+ from last_set_unique [OF this th_in1 th_in2]
+ show ?thesis .
+qed
+
+lemma preced_linorder:
+ assumes neq_12: "th1 \<noteq> th2"
+ and th_in1: "th1 \<in> threads s"
+ and th_in2: " th2 \<in> threads s"
+ shows "preced th1 s < preced th2 s \<or> preced th1 s > preced th2 s"
+proof -
+ from preced_unique [OF _ th_in1 th_in2] and neq_12
+ have "preced th1 s \<noteq> preced th2 s" by auto
+ thus ?thesis by auto
+qed
+
+lemma in_RAG_E:
+ assumes "(n1, n2) \<in> RAG (s::state)"
+ obtains (waiting) th cs where "n1 = Th th" "n2 = Cs cs" "waiting s th cs"
+ | (holding) th cs where "n1 = Cs cs" "n2 = Th th" "holding s th cs"
+ using assms[unfolded s_RAG_def, folded waiting_eq holding_eq]
+ by auto
+
(* ccc *)
section {* Locales used to investigate the execution of PIP *}
@@ -479,9 +546,29 @@
locale valid_moment = valid_trace +
fixes i :: nat
-sublocale valid_moment < vat_moment: valid_trace "(moment i s)"
+sublocale valid_moment < vat_moment!: valid_trace "(moment i s)"
by (unfold_locales, insert vt_moment, auto)
+locale valid_moment_e = valid_moment +
+ assumes less_i: "i < length s"
+begin
+ definition "next_e = hd (moment (Suc i) s)"
+
+ lemma trace_e:
+ "moment (Suc i) s = next_e#moment i s"
+ proof -
+ from less_i have "Suc i \<le> length s" by auto
+ from moment_plus[OF this, folded next_e_def]
+ show ?thesis .
+ qed
+
+end
+
+sublocale valid_moment_e < vat_moment_e!: valid_trace_e "moment i s" "next_e"
+ using vt_moment[of "Suc i", unfolded trace_e]
+ by (unfold_locales, simp)
+
+section {* Distinctiveness of waiting queues *}
context valid_trace_create
begin
@@ -511,7 +598,7 @@
using assms by simp
end
-context valid_trace_p (* ccc *)
+context valid_trace_p
begin
lemma wq_neq_simp [simp]:
@@ -527,31 +614,6 @@
show ?thesis by (cases, simp)
qed
-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 live_th_es: "th \<in> threads (e#s)"
- using live_th_s
- by (unfold is_p, simp)
-
-lemma th_not_waiting:
- "\<not> waiting s th c"
-proof -
- have "th \<in> readys s"
- using runing_ready runing_th_s by blast
- thus ?thesis
- by (unfold readys_def, auto)
-qed
-
-lemma waiting_neq_th:
- assumes "waiting s t c"
- shows "t \<noteq> th"
- using assms using th_not_waiting by blast
-
lemma th_not_in_wq:
shows "th \<notin> set (wq s cs)"
proof
@@ -595,27 +657,6 @@
using assms unfolding is_v wq_def
by (auto simp:Let_def)
-lemma runing_th_s:
- shows "th \<in> runing s"
-proof -
- from pip_e[unfolded is_v]
- show ?thesis by (cases, simp)
-qed
-
-lemma th_not_waiting:
- "\<not> waiting s th c"
-proof -
- have "th \<in> readys s"
- using runing_ready runing_th_s by blast
- thus ?thesis
- by (unfold readys_def, auto)
-qed
-
-lemma waiting_neq_th:
- assumes "waiting s t c"
- shows "t \<noteq> th"
- using assms using th_not_waiting by blast
-
lemma wq_s_cs:
"wq s cs = th#rest"
proof -
@@ -665,23 +706,6 @@
context valid_trace
begin
-lemma actor_inv: (* ccc *)
- assumes "PIP s e"
- and "\<not> isCreate e"
- shows "actor e \<in> runing s"
- using assms
- by (induct, auto)
-
-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)
-
lemma wq_distinct: "distinct (wq s cs)"
proof(induct rule:ind)
case (Cons s e)
@@ -715,47 +739,12 @@
end
+section {* Waiting queues and threads *}
+
context valid_trace_e
begin
-text {*
- The following lemma shows that only the @{text "P"}
- operation can add new thread into waiting queues.
- Such kind of lemmas are very obvious, but need to be checked formally.
- This is a kind of confirmation that our modelling is correct.
-*}
-
-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)
-
-lemma wq_out_inv: (* ccc *)
+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)"
@@ -788,248 +777,173 @@
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)
+ 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)
+ 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}"
+ 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)
+ 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"
+proof
+ assume otherwise: "th \<in> set rest"
+ have "distinct (wq s cs)" by (simp add: wq_distinct)
+ from this[unfolded wq_s_cs] and otherwise
+ show False by auto
+qed
+
+lemma (in valid_trace_v) distinct_rest: "distinct rest"
+ by (simp add: distinct_tl rest_def wq_distinct)
+
+lemma (in valid_trace_v)
+ 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"
+ by (simp add: distinct_rest)
+next
+ fix x
+ assume "distinct x \<and> set x = set rest"
+ thus "set x = set (wq s cs) - {th}"
+ by (unfold wq_s_cs, simp)
+qed
+
+lemma (in valid_trace_exit)
+ 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 (in valid_trace) wq_threads:
+ assumes "th \<in> set (wq s cs)"
+ shows "th \<in> threads s"
+ using assms
+proof(induct rule:ind)
+ case (Nil)
+ thus ?case by (auto simp:wq_def)
+next
+ case (Cons s e)
+ interpret vt_e: valid_trace_e s e using Cons by simp
+ show ?case
+ proof(cases e)
+ 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
+ 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
+ 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
+ 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
+ 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)
+ qed
+qed
+
+section {* RAG and threads *}
context valid_trace
begin
-
-text {* (* ddd *)
- The nature of the work is like this: since it starts from a very simple and basic
- model, even intuitively very `basic` and `obvious` properties need to derived from scratch.
- For instance, the fact
- that one thread can not be blocked by two critical resources at the same time
- is obvious, because only running threads can make new requests, if one is waiting for
- a critical resource and get blocked, it can not make another resource request and get
- blocked the second time (because it is not running).
-
- To derive this fact, one needs to prove by contraction and
- reason about time (or @{text "moement"}). The reasoning is based on a generic theorem
- named @{text "p_split"}, which is about status changing along the time axis. It says if
- a condition @{text "Q"} is @{text "True"} at a state @{text "s"},
- but it was @{text "False"} at the very beginning, then there must exits a moment @{text "t"}
- in the history of @{text "s"} (notice that @{text "s"} itself is essentially the history
- of events leading to it), such that @{text "Q"} switched
- from being @{text "False"} to @{text "True"} and kept being @{text "True"}
- till the last moment of @{text "s"}.
-
- Suppose a thread @{text "th"} is blocked
- on @{text "cs1"} and @{text "cs2"} in some state @{text "s"},
- since no thread is blocked at the very beginning, by applying
- @{text "p_split"} to these two blocking facts, there exist
- two moments @{text "t1"} and @{text "t2"} in @{text "s"}, such that
- @{text "th"} got blocked on @{text "cs1"} and @{text "cs2"}
- and kept on blocked on them respectively ever since.
-
- 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: (* ddd *)
- assumes h11: "thread \<in> set (wq s cs1)"
- and h12: "thread \<noteq> hd (wq s cs1)"
- assumes h21: "thread \<in> set (wq s cs2)"
- and h22: "thread \<noteq> hd (wq s cs2)"
- and neq12: "cs1 \<noteq> cs2"
- shows "False"
+lemma dm_RAG_threads:
+ assumes in_dom: "(Th th) \<in> Domain (RAG s)"
+ shows "th \<in> threads s"
proof -
- let "?Q" = "\<lambda> cs s. thread \<in> set (wq s cs) \<and> thread \<noteq> hd (wq s cs)"
- from h11 and h12 have q1: "?Q cs1 s" by simp
- from h21 and h22 have q2: "?Q cs2 s" by simp
- have nq1: "\<not> ?Q cs1 []" by (simp add:wq_def)
- have nq2: "\<not> ?Q cs2 []" by (simp add:wq_def)
- from p_split [of "?Q cs1", OF q1 nq1]
- obtain t1 where lt1: "t1 < length s"
- and np1: "\<not> ?Q cs1 (moment t1 s)"
- and nn1: "(\<forall>i'>t1. ?Q cs1 (moment i' s))" by auto
- from p_split [of "?Q cs2", OF q2 nq2]
- obtain t2 where lt2: "t2 < length s"
- and np2: "\<not> ?Q cs2 (moment t2 s)"
- and nn2: "(\<forall>i'>t2. ?Q cs2 (moment i' s))" by auto
- { fix s cs
- assume q: "?Q cs s"
- have "thread \<notin> runing s"
- proof
- assume "thread \<in> runing s"
- hence " \<forall>cs. \<not> (thread \<in> set (wq_fun (schs s) cs) \<and>
- thread \<noteq> hd (wq_fun (schs s) cs))"
- by (unfold runing_def s_waiting_def readys_def, auto)
- from this[rule_format, of cs] q
- show False by (simp add: wq_def)
- qed
- } note q_not_runing = this
- { fix t1 t2 cs1 cs2
- assume lt1: "t1 < length s"
- and np1: "\<not> ?Q cs1 (moment t1 s)"
- and nn1: "(\<forall>i'>t1. ?Q cs1 (moment i' s))"
- and lt2: "t2 < length s"
- and np2: "\<not> ?Q cs2 (moment t2 s)"
- and nn2: "(\<forall>i'>t2. ?Q cs2 (moment i' s))"
- and lt12: "t1 < t2"
- let ?t3 = "Suc t2"
- from lt2 have le_t3: "?t3 \<le> length s" by auto
- from moment_plus [OF this]
- obtain e where eq_m: "moment ?t3 s = e#moment t2 s" by auto
- have "t2 < ?t3" by simp
- from nn2 [rule_format, OF this] and eq_m
- have h1: "thread \<in> set (wq (e#moment t2 s) cs2)" and
- h2: "thread \<noteq> hd (wq (e#moment t2 s) cs2)" by auto
- have "vt (e#moment t2 s)"
- proof -
- from vt_moment
- have "vt (moment ?t3 s)" .
- with eq_m show ?thesis by simp
- qed
- then interpret vt_e: valid_trace_e "moment t2 s" "e"
- by (unfold_locales, auto, cases, simp)
- have ?thesis
- proof -
- have "thread \<in> runing (moment t2 s)"
- proof(cases "thread \<in> set (wq (moment t2 s) cs2)")
- case True
- have "e = V thread cs2"
- proof -
- have eq_th: "thread = hd (wq (moment t2 s) cs2)"
- using True and np2 by auto
- from vt_e.wq_out_inv[OF True this h2]
- show ?thesis .
- qed
- thus ?thesis using vt_e.actor_inv[OF vt_e.pip_e] by auto
- next
- case False
- have "e = P thread cs2" using vt_e.wq_in_inv[OF False h1] .
- with vt_e.actor_inv[OF vt_e.pip_e]
- show ?thesis by auto
- qed
- moreover have "thread \<notin> runing (moment t2 s)"
- by (rule q_not_runing[OF nn1[rule_format, OF lt12]])
- ultimately show ?thesis by simp
- qed
- } note lt_case = this
- show ?thesis
- proof -
- { assume "t1 < t2"
- from lt_case[OF lt1 np1 nn1 lt2 np2 nn2 this]
- have ?thesis .
- } moreover {
- assume "t2 < t1"
- from lt_case[OF lt2 np2 nn2 lt1 np1 nn1 this]
- have ?thesis .
- } moreover {
- assume eq_12: "t1 = t2"
- let ?t3 = "Suc t2"
- from lt2 have le_t3: "?t3 \<le> length s" by auto
- from moment_plus [OF this]
- obtain e where eq_m: "moment ?t3 s = e#moment t2 s" by auto
- have lt_2: "t2 < ?t3" by simp
- from nn2 [rule_format, OF this] and eq_m
- have h1: "thread \<in> set (wq (e#moment t2 s) cs2)" and
- h2: "thread \<noteq> hd (wq (e#moment t2 s) cs2)" by auto
- from nn1[rule_format, OF lt_2[folded eq_12]] eq_m[folded eq_12]
- have g1: "thread \<in> set (wq (e#moment t1 s) cs1)" and
- g2: "thread \<noteq> hd (wq (e#moment t1 s) cs1)" by auto
- have "vt (e#moment t2 s)"
- proof -
- from vt_moment
- have "vt (moment ?t3 s)" .
- with eq_m show ?thesis by simp
- qed
- then interpret vt_e: valid_trace_e "moment t2 s" "e"
- by (unfold_locales, auto, cases, simp)
- have "e = V thread cs2 \<or> e = P thread cs2"
- proof(cases "thread \<in> set (wq (moment t2 s) cs2)")
- case True
- have "e = V thread cs2"
- proof -
- have eq_th: "thread = hd (wq (moment t2 s) cs2)"
- using True and np2 by auto
- from vt_e.wq_out_inv[OF True this h2]
- show ?thesis .
- qed
- thus ?thesis by auto
- next
- case False
- have "e = P thread cs2" using vt_e.wq_in_inv[OF False h1] .
- thus ?thesis by auto
- qed
- moreover have "e = V thread cs1 \<or> e = P thread cs1"
- proof(cases "thread \<in> set (wq (moment t1 s) cs1)")
- case True
- have eq_th: "thread = hd (wq (moment t1 s) cs1)"
- using True and np1 by auto
- from vt_e.wq_out_inv[folded eq_12, OF True this g2]
- have "e = V thread cs1" .
- thus ?thesis by auto
- next
- case False
- have "e = P thread cs1" using vt_e.wq_in_inv[folded eq_12, OF False g1] .
- thus ?thesis by auto
- qed
- ultimately have ?thesis using neq12 by auto
- } ultimately show ?thesis using nat_neq_iff by blast
- qed
+ from in_dom obtain n where "(Th th, n) \<in> RAG s" by auto
+ moreover from RAG_target_th[OF this] obtain cs where "n = Cs cs" by auto
+ ultimately have "(Th th, Cs cs) \<in> RAG s" by simp
+ hence "th \<in> set (wq s cs)"
+ by (unfold s_RAG_def, auto simp:cs_waiting_def)
+ from wq_threads [OF this] show ?thesis .
qed
-text {*
- This lemma is a simple corrolary of @{text "waiting_unique_pre"}.
-*}
-
-lemma waiting_unique:
- assumes "waiting s th cs1"
- and "waiting s th cs2"
- shows "cs1 = cs2"
- using waiting_unique_pre assms
- unfolding wq_def s_waiting_def
- by auto
+lemma rg_RAG_threads:
+ assumes "(Th th) \<in> Range (RAG s)"
+ shows "th \<in> threads s"
+ using assms
+ by (unfold s_RAG_def cs_waiting_def cs_holding_def,
+ auto intro:wq_threads)
+
+lemma RAG_threads:
+ assumes "(Th th) \<in> Field (RAG s)"
+ shows "th \<in> threads s"
+ using assms
+ by (metis Field_def UnE dm_RAG_threads rg_RAG_threads)
end
-(* not used *)
-text {*
- Every thread can only be blocked on one critical resource,
- symmetrically, every critical resource can only be held by one thread.
- This fact is much more easier according to our definition.
-*}
-lemma held_unique:
- assumes "holding (s::event list) th1 cs"
- and "holding s th2 cs"
- shows "th1 = th2"
- by (insert assms, unfold s_holding_def, auto)
-
-lemma last_set_lt: "th \<in> threads s \<Longrightarrow> last_set th s < length s"
- apply (induct s, auto)
- by (case_tac a, auto split:if_splits)
-
-lemma last_set_unique:
- "\<lbrakk>last_set th1 s = last_set th2 s; th1 \<in> threads s; th2 \<in> threads s\<rbrakk>
- \<Longrightarrow> th1 = th2"
- apply (induct s, auto)
- by (case_tac a, auto split:if_splits dest:last_set_lt)
-
-lemma preced_unique :
- assumes pcd_eq: "preced th1 s = preced th2 s"
- and th_in1: "th1 \<in> threads s"
- and th_in2: " th2 \<in> threads s"
- shows "th1 = th2"
-proof -
- from pcd_eq have "last_set th1 s = last_set th2 s" by (simp add:preced_def)
- from last_set_unique [OF this th_in1 th_in2]
- show ?thesis .
-qed
-
-lemma preced_linorder:
- assumes neq_12: "th1 \<noteq> th2"
- and th_in1: "th1 \<in> threads s"
- and th_in2: " th2 \<in> threads s"
- shows "preced th1 s < preced th2 s \<or> preced th1 s > preced th2 s"
-proof -
- from preced_unique [OF _ th_in1 th_in2] and neq_12
- have "preced th1 s \<noteq> preced th2 s" by auto
- thus ?thesis by auto
-qed
+section {* The change of @{term RAG} *}
text {*
The following three lemmas show that @{text "RAG"} does not change
@@ -1037,36 +951,18 @@
events, respectively.
*}
-lemma RAG_set_unchanged: "(RAG (Set th prio # s)) = RAG s"
-apply (unfold s_RAG_def s_waiting_def wq_def)
-by (simp add:Let_def)
-
-lemma (in valid_trace_set)
- RAG_unchanged: "(RAG (e # s)) = RAG s"
- by (unfold is_set RAG_set_unchanged, simp)
-
-lemma RAG_create_unchanged: "(RAG (Create th prio # s)) = RAG s"
-apply (unfold s_RAG_def s_waiting_def wq_def)
-by (simp add:Let_def)
-
-lemma (in valid_trace_create)
- RAG_unchanged: "(RAG (e # s)) = RAG s"
- by (unfold is_create RAG_create_unchanged, simp)
-
-lemma RAG_exit_unchanged: "(RAG (Exit th # s)) = RAG s"
-apply (unfold s_RAG_def s_waiting_def wq_def)
-by (simp add:Let_def)
-
-lemma (in valid_trace_exit)
- RAG_unchanged: "(RAG (e # s)) = RAG s"
- by (unfold is_exit RAG_exit_unchanged, simp)
+lemma (in valid_trace_set) RAG_unchanged [simp]: "(RAG (e # s)) = RAG s"
+ by (unfold is_set s_RAG_def s_waiting_def wq_def, simp add:Let_def)
+
+lemma (in valid_trace_create) RAG_unchanged [simp]: "(RAG (e # s)) = RAG s"
+ by (unfold is_create s_RAG_def s_waiting_def wq_def, simp add:Let_def)
+
+lemma (in valid_trace_exit) RAG_unchanged[simp]: "(RAG (e # s)) = RAG s"
+ by (unfold is_exit s_RAG_def s_waiting_def wq_def, simp add:Let_def)
context valid_trace_v
begin
-lemma distinct_rest: "distinct rest"
- by (simp add: distinct_tl rest_def wq_distinct)
-
lemma holding_cs_eq_th:
assumes "holding s t cs"
shows "t = th"
@@ -1084,14 +980,20 @@
by (metis (mono_tags, lifting) distinct_rest some_eq_ex wq'_def)
lemma set_wq': "set wq' = set rest"
- by (metis (mono_tags, lifting) distinct_rest rest_def
- some_eq_ex wq'_def)
+ by (metis (mono_tags, lifting) distinct_rest some_eq_ex wq'_def)
lemma th'_in_inv:
assumes "th' \<in> set wq'"
shows "th' \<in> set rest"
using assms set_wq' by simp
+lemma runing_th_s:
+ shows "th \<in> runing s"
+proof -
+ from pip_e[unfolded is_v]
+ show ?thesis by (cases, simp)
+qed
+
lemma neq_t_th:
assumes "waiting (e#s) t c"
shows "t \<noteq> th"
@@ -1114,7 +1016,7 @@
by (simp add: cs_waiting_def waiting_eq)
hence "t \<notin> readys s" by (unfold readys_def, auto)
hence "t \<notin> runing s" using runing_ready by auto
- with runing_th_s[folded otherwise] show ?thesis by auto
+ with runing_th_s[folded otherwise] show ?thesis by auto
qed
qed
@@ -1367,18 +1269,6 @@
end
-lemma rel_eqI:
- assumes "\<And> x y. (x,y) \<in> A \<Longrightarrow> (x,y) \<in> B"
- and "\<And> x y. (x,y) \<in> B \<Longrightarrow> (x, y) \<in> A"
- shows "A = B"
- using assms by auto
-
-lemma in_RAG_E:
- assumes "(n1, n2) \<in> RAG (s::state)"
- obtains (waiting) th cs where "n1 = Th th" "n2 = Cs cs" "waiting s th cs"
- | (holding) th cs where "n1 = Cs cs" "n2 = Th th" "holding s th cs"
- using assms[unfolded s_RAG_def, folded waiting_eq holding_eq]
- by auto
context valid_trace_v
begin
@@ -1565,183 +1455,29 @@
qed
qed
-end
-
-lemma step_RAG_v:
-assumes vt:
- "vt (V th cs#s)"
-shows "
- RAG (V th cs # s) =
- RAG s - {(Cs cs, Th th)} -
- {(Th th', Cs cs) |th'. next_th s th cs th'} \<union>
- {(Cs cs, Th th') |th'. next_th s th cs th'}" (is "?L = ?R")
-proof -
- interpret vt_v: valid_trace_v s "V th cs"
- using assms step_back_vt by (unfold_locales, auto)
- show ?thesis using vt_v.RAG_es .
-qed
-
-lemma (in valid_trace_create)
- 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)
- 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}"
- 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)
- 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"
-proof
- assume otherwise: "th \<in> set rest"
- have "distinct (wq s cs)" by (simp add: wq_distinct)
- from this[unfolded wq_s_cs] and otherwise
- show False by auto
-qed
-
-lemma (in valid_trace_v)
- 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"
- by (simp add: distinct_rest)
+lemma
+ finite_RAG_kept:
+ assumes "finite (RAG s)"
+ shows "finite (RAG (e#s))"
+proof(cases "rest = []")
+ case True
+ interpret vt: valid_trace_v_e using True
+ by (unfold_locales, simp)
+ show ?thesis using assms
+ by (unfold RAG_es vt.waiting_set_eq vt.holding_set_eq, simp)
next
- fix x
- assume "distinct x \<and> set x = set rest"
- thus "set x = set (wq s cs) - {th}"
- by (unfold wq_s_cs, simp)
-qed
-
-lemma (in valid_trace_exit)
- 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)
+ case False
+ interpret vt: valid_trace_v_n using False
+ by (unfold_locales, simp)
+ show ?thesis using assms
+ by (unfold RAG_es vt.waiting_set_eq vt.holding_set_eq, simp)
qed
-lemma (in valid_trace) wq_threads:
- assumes "th \<in> set (wq s cs)"
- shows "th \<in> threads s"
- using assms
-proof(induct rule:ind)
- case (Nil)
- thus ?case by (auto simp:wq_def)
-next
- case (Cons s e)
- interpret vt_e: valid_trace_e s e using Cons by simp
- show ?case
- proof(cases e)
- 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
- 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
- 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
- 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
- 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)
- qed
-qed
-
-context valid_trace
-begin
-
-lemma dm_RAG_threads:
- assumes in_dom: "(Th th) \<in> Domain (RAG s)"
- shows "th \<in> threads s"
-proof -
- from in_dom obtain n where "(Th th, n) \<in> RAG s" by auto
- moreover from RAG_target_th[OF this] obtain cs where "n = Cs cs" by auto
- ultimately have "(Th th, Cs cs) \<in> RAG s" by simp
- hence "th \<in> set (wq s cs)"
- by (unfold s_RAG_def, auto simp:cs_waiting_def)
- from wq_threads [OF this] show ?thesis .
-qed
-
-lemma rg_RAG_threads:
- assumes "(Th th) \<in> Range (RAG s)"
- shows "th \<in> threads s"
- using assms
- by (unfold s_RAG_def cs_waiting_def cs_holding_def,
- auto intro:wq_threads)
-
-lemma RAG_threads:
- assumes "(Th th) \<in> Field (RAG s)"
- shows "th \<in> threads s"
- using assms
- by (metis Field_def UnE dm_RAG_threads rg_RAG_threads)
-
end
-lemma (in valid_trace_v)
- preced_es [simp]: "preced th (e#s) = preced th s"
- by (unfold is_v preced_def, simp)
-
-lemma the_preced_v[simp]: "the_preced (V th cs#s) = the_preced s"
-proof
- fix th'
- show "the_preced (V th cs # s) th' = the_preced s th'"
- by (unfold the_preced_def preced_def, simp)
-qed
-
-lemma (in valid_trace_v)
- the_preced_es: "the_preced (e#s) = the_preced s"
- by (unfold is_v preced_def, simp)
-
context valid_trace_p
begin
-lemma not_holding_s_th_cs: "\<not> holding s th cs"
-proof
- assume otherwise: "holding s th cs"
- from pip_e[unfolded is_p]
- show False
- proof(cases)
- case (thread_P)
- moreover have "(Cs cs, Th th) \<in> RAG s"
- using otherwise cs_holding_def
- holding_eq th_not_in_wq by auto
- ultimately show ?thesis by auto
- qed
-qed
-
lemma waiting_kept:
assumes "waiting s th' cs'"
shows "waiting (e#s) th' cs'"
@@ -1749,7 +1485,7 @@
by (metis cs_waiting_def hd_append2 list.sel(1) list.set_intros(2)
rotate1.simps(2) self_append_conv2 set_rotate1
th_not_in_wq waiting_eq wq_es_cs wq_neq_simp)
-
+
lemma holding_kept:
assumes "holding s th' cs'"
shows "holding (e#s) th' cs'"
@@ -1767,116 +1503,16 @@
thus ?thesis
by (simp add: cs_holding_def holding_eq)
qed
-
-end
-
-
-context valid_trace_p_w
-begin
-
-lemma wq_s_cs: "wq s cs = holder#waiters"
- by (simp add: holder_def waiters_def wne)
-
-lemma wq_es_cs': "wq (e#s) cs = holder#waiters@[th]"
- by (simp add: wq_es_cs wq_s_cs)
-
-lemma waiting_es_th_cs: "waiting (e#s) th cs"
- using cs_waiting_def th_not_in_wq waiting_eq wq_es_cs' wq_s_cs by auto
-
-lemma RAG_edge: "(Th th, Cs cs) \<in> RAG (e#s)"
- by (unfold s_RAG_def, fold waiting_eq, insert waiting_es_th_cs, auto)
-
-lemma holding_esE:
- assumes "holding (e#s) th' cs'"
- obtains "holding s th' cs'"
- using assms
-proof(cases "cs' = cs")
- case False
- hence "wq (e#s) cs' = wq s cs'" by simp
- with assms show ?thesis
- using cs_holding_def holding_eq that by auto
-next
- case True
- with assms show ?thesis
- by (metis cs_holding_def holding_eq list.sel(1) list.set_intros(1) that
- wq_es_cs' wq_s_cs)
-qed
-
-lemma waiting_esE:
- assumes "waiting (e#s) th' cs'"
- obtains "th' \<noteq> th" "waiting s th' cs'"
- | "th' = th" "cs' = cs"
-proof(cases "waiting s th' cs'")
- case True
- have "th' \<noteq> th"
- proof
- assume otherwise: "th' = th"
- from True[unfolded this]
- show False by (simp add: th_not_waiting)
- qed
- from that(1)[OF this True] show ?thesis .
-next
- case False
- hence "th' = th \<and> cs' = cs"
- by (metis assms cs_waiting_def holder_def list.sel(1) rotate1.simps(2)
- set_ConsD set_rotate1 waiting_eq wq_es_cs wq_es_cs' wq_neq_simp)
- with that(2) show ?thesis by metis
+end
+
+lemma (in valid_trace_p) th_not_waiting: "\<not> waiting s th c"
+proof -
+ have "th \<in> readys s"
+ using runing_ready runing_th_s by blast
+ thus ?thesis
+ by (unfold readys_def, auto)
qed
-lemma RAG_es: "RAG (e # s) = RAG s \<union> {(Th th, Cs cs)}" (is "?L = ?R")
-proof(rule rel_eqI)
- fix n1 n2
- assume "(n1, n2) \<in> ?L"
- thus "(n1, n2) \<in> ?R"
- proof(cases rule:in_RAG_E)
- case (waiting th' cs')
- from this(3)
- show ?thesis
- proof(cases rule:waiting_esE)
- case 1
- thus ?thesis using waiting(1,2)
- by (unfold s_RAG_def, fold waiting_eq, auto)
- next
- case 2
- thus ?thesis using waiting(1,2) by auto
- qed
- next
- case (holding th' cs')
- from this(3)
- show ?thesis
- proof(cases rule:holding_esE)
- case 1
- with holding(1,2)
- show ?thesis by (unfold s_RAG_def, fold holding_eq, auto)
- qed
- qed
-next
- fix n1 n2
- assume "(n1, n2) \<in> ?R"
- hence "(n1, n2) \<in> RAG s \<or> (n1 = Th th \<and> n2 = Cs cs)" by auto
- thus "(n1, n2) \<in> ?L"
- proof
- assume "(n1, n2) \<in> RAG s"
- thus ?thesis
- proof(cases rule:in_RAG_E)
- case (waiting th' cs')
- from waiting_kept[OF this(3)]
- show ?thesis using waiting(1,2)
- by (unfold s_RAG_def, fold waiting_eq, auto)
- next
- case (holding th' cs')
- from holding_kept[OF this(3)]
- show ?thesis using holding(1,2)
- by (unfold s_RAG_def, fold holding_eq, auto)
- qed
- next
- assume "n1 = Th th \<and> n2 = Cs cs"
- thus ?thesis using RAG_edge by auto
- qed
-qed
-
-end
-
context valid_trace_p_h
begin
@@ -1973,10 +1609,116 @@
end
+context valid_trace_p_w
+begin
+
+lemma wq_s_cs: "wq s cs = holder#waiters"
+ by (simp add: holder_def waiters_def wne)
+
+lemma wq_es_cs': "wq (e#s) cs = holder#waiters@[th]"
+ by (simp add: wq_es_cs wq_s_cs)
+
+lemma waiting_es_th_cs: "waiting (e#s) th cs"
+ using cs_waiting_def th_not_in_wq waiting_eq wq_es_cs' wq_s_cs by auto
+
+lemma RAG_edge: "(Th th, Cs cs) \<in> RAG (e#s)"
+ by (unfold s_RAG_def, fold waiting_eq, insert waiting_es_th_cs, auto)
+
+lemma holding_esE:
+ assumes "holding (e#s) th' cs'"
+ obtains "holding s th' cs'"
+ using assms
+proof(cases "cs' = cs")
+ case False
+ hence "wq (e#s) cs' = wq s cs'" by simp
+ with assms show ?thesis
+ using cs_holding_def holding_eq that by auto
+next
+ case True
+ with assms show ?thesis
+ by (metis cs_holding_def holding_eq list.sel(1) list.set_intros(1) that
+ wq_es_cs' wq_s_cs)
+qed
+
+lemma waiting_esE:
+ assumes "waiting (e#s) th' cs'"
+ obtains "th' \<noteq> th" "waiting s th' cs'"
+ | "th' = th" "cs' = cs"
+proof(cases "waiting s th' cs'")
+ case True
+ have "th' \<noteq> th"
+ proof
+ assume otherwise: "th' = th"
+ from True[unfolded this]
+ show False by (simp add: th_not_waiting)
+ qed
+ from that(1)[OF this True] show ?thesis .
+next
+ case False
+ hence "th' = th \<and> cs' = cs"
+ by (metis assms cs_waiting_def holder_def list.sel(1) rotate1.simps(2)
+ set_ConsD set_rotate1 waiting_eq wq_es_cs wq_es_cs' wq_neq_simp)
+ with that(2) show ?thesis by metis
+qed
+
+lemma RAG_es: "RAG (e # s) = RAG s \<union> {(Th th, Cs cs)}" (is "?L = ?R")
+proof(rule rel_eqI)
+ fix n1 n2
+ assume "(n1, n2) \<in> ?L"
+ thus "(n1, n2) \<in> ?R"
+ proof(cases rule:in_RAG_E)
+ case (waiting th' cs')
+ from this(3)
+ show ?thesis
+ proof(cases rule:waiting_esE)
+ case 1
+ thus ?thesis using waiting(1,2)
+ by (unfold s_RAG_def, fold waiting_eq, auto)
+ next
+ case 2
+ thus ?thesis using waiting(1,2) by auto
+ qed
+ next
+ case (holding th' cs')
+ from this(3)
+ show ?thesis
+ proof(cases rule:holding_esE)
+ case 1
+ with holding(1,2)
+ show ?thesis by (unfold s_RAG_def, fold holding_eq, auto)
+ qed
+ qed
+next
+ fix n1 n2
+ assume "(n1, n2) \<in> ?R"
+ hence "(n1, n2) \<in> RAG s \<or> (n1 = Th th \<and> n2 = Cs cs)" by auto
+ thus "(n1, n2) \<in> ?L"
+ proof
+ assume "(n1, n2) \<in> RAG s"
+ thus ?thesis
+ proof(cases rule:in_RAG_E)
+ case (waiting th' cs')
+ from waiting_kept[OF this(3)]
+ show ?thesis using waiting(1,2)
+ by (unfold s_RAG_def, fold waiting_eq, auto)
+ next
+ case (holding th' cs')
+ from holding_kept[OF this(3)]
+ show ?thesis using holding(1,2)
+ by (unfold s_RAG_def, fold holding_eq, auto)
+ qed
+ next
+ assume "n1 = Th th \<and> n2 = Cs cs"
+ thus ?thesis using RAG_edge by auto
+ qed
+qed
+
+end
+
context valid_trace_p
begin
-lemma RAG_es': "RAG (e # s) = (if (wq s cs = []) then RAG s \<union> {(Cs cs, Th th)}
+lemma RAG_es: "RAG (e # s) = (if (wq s cs = []) then RAG s \<union> {(Cs cs, Th th)}
else RAG s \<union> {(Th th, Cs cs)})"
proof(cases "wq s cs = []")
case True
@@ -1992,6 +1734,252 @@
end
+section {* Finiteness of RAG *}
+
+context valid_trace
+begin
+
+lemma finite_RAG:
+ shows "finite (RAG s)"
+proof(induct rule:ind)
+ case Nil
+ show ?case
+ by (auto simp: s_RAG_def cs_waiting_def
+ cs_holding_def wq_def acyclic_def)
+next
+ case (Cons s e)
+ interpret vt_e: valid_trace_e s e using Cons by simp
+ show ?case
+ proof(cases e)
+ case (Create th prio)
+ interpret vt: valid_trace_create s e th prio using Create
+ by (unfold_locales, simp)
+ show ?thesis using Cons by simp
+ next
+ case (Exit th)
+ interpret vt: valid_trace_exit s e th using Exit
+ by (unfold_locales, simp)
+ show ?thesis using Cons by simp
+ next
+ case (P th cs)
+ interpret vt: valid_trace_p s e th cs using P
+ by (unfold_locales, simp)
+ show ?thesis using Cons using vt.RAG_es 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 by (simp add: vt.finite_RAG_kept)
+ next
+ case (Set th prio)
+ interpret vt: valid_trace_set s e th prio using Set
+ by (unfold_locales, simp)
+ show ?thesis using Cons by simp
+ qed
+qed
+end
+
+section {* RAG is acyclic *}
+
+text {* (* ddd *)
+ The nature of the work is like this: since it starts from a very simple and basic
+ model, even intuitively very `basic` and `obvious` properties need to derived from scratch.
+ For instance, the fact
+ that one thread can not be blocked by two critical resources at the same time
+ is obvious, because only running threads can make new requests, if one is waiting for
+ a critical resource and get blocked, it can not make another resource request and get
+ blocked the second time (because it is not running).
+
+ To derive this fact, one needs to prove by contraction and
+ reason about time (or @{text "moement"}). The reasoning is based on a generic theorem
+ named @{text "p_split"}, which is about status changing along the time axis. It says if
+ a condition @{text "Q"} is @{text "True"} at a state @{text "s"},
+ but it was @{text "False"} at the very beginning, then there must exits a moment @{text "t"}
+ in the history of @{text "s"} (notice that @{text "s"} itself is essentially the history
+ of events leading to it), such that @{text "Q"} switched
+ from being @{text "False"} to @{text "True"} and kept being @{text "True"}
+ till the last moment of @{text "s"}.
+
+ Suppose a thread @{text "th"} is blocked
+ on @{text "cs1"} and @{text "cs2"} in some state @{text "s"},
+ since no thread is blocked at the very beginning, by applying
+ @{text "p_split"} to these two blocking facts, there exist
+ two moments @{text "t1"} and @{text "t2"} in @{text "s"}, such that
+ @{text "th"} got blocked on @{text "cs1"} and @{text "cs2"}
+ and kept on blocked on them respectively ever since.
+
+ 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.
+*}
+
+
+context valid_trace
+begin
+
+lemma waiting_unique_pre: (* ddd *)
+ assumes h11: "thread \<in> set (wq s cs1)"
+ and h12: "thread \<noteq> hd (wq s cs1)"
+ assumes h21: "thread \<in> set (wq s cs2)"
+ and h22: "thread \<noteq> hd (wq s cs2)"
+ and neq12: "cs1 \<noteq> cs2"
+ shows "False"
+proof -
+ let "?Q" = "\<lambda> cs s. thread \<in> set (wq s cs) \<and> thread \<noteq> hd (wq s cs)"
+ from h11 and h12 have q1: "?Q cs1 s" by simp
+ from h21 and h22 have q2: "?Q cs2 s" by simp
+ have nq1: "\<not> ?Q cs1 []" by (simp add:wq_def)
+ have nq2: "\<not> ?Q cs2 []" by (simp add:wq_def)
+ from p_split [of "?Q cs1", OF q1 nq1]
+ obtain t1 where lt1: "t1 < length s"
+ and np1: "\<not> ?Q cs1 (moment t1 s)"
+ and nn1: "(\<forall>i'>t1. ?Q cs1 (moment i' s))" by auto
+ from p_split [of "?Q cs2", OF q2 nq2]
+ obtain t2 where lt2: "t2 < length s"
+ and np2: "\<not> ?Q cs2 (moment t2 s)"
+ and nn2: "(\<forall>i'>t2. ?Q cs2 (moment i' s))" by auto
+ { fix s cs
+ assume q: "?Q cs s"
+ have "thread \<notin> runing s"
+ proof
+ assume "thread \<in> runing s"
+ hence " \<forall>cs. \<not> (thread \<in> set (wq_fun (schs s) cs) \<and>
+ thread \<noteq> hd (wq_fun (schs s) cs))"
+ by (unfold runing_def s_waiting_def readys_def, auto)
+ from this[rule_format, of cs] q
+ show False by (simp add: wq_def)
+ qed
+ } note q_not_runing = this
+ { fix t1 t2 cs1 cs2
+ assume lt1: "t1 < length s"
+ and np1: "\<not> ?Q cs1 (moment t1 s)"
+ and nn1: "(\<forall>i'>t1. ?Q cs1 (moment i' s))"
+ and lt2: "t2 < length s"
+ and np2: "\<not> ?Q cs2 (moment t2 s)"
+ and nn2: "(\<forall>i'>t2. ?Q cs2 (moment i' s))"
+ and lt12: "t1 < t2"
+ let ?t3 = "Suc t2"
+ interpret ve2: valid_moment_e _ t2 using lt2
+ by (unfold_locales, simp)
+ let ?e = ve2.next_e
+ have "t2 < ?t3" by simp
+ from nn2 [rule_format, OF this] and ve2.trace_e
+ have h1: "thread \<in> set (wq (?e#moment t2 s) cs2)" and
+ h2: "thread \<noteq> hd (wq (?e#moment t2 s) cs2)" by auto
+ have ?thesis
+ proof -
+ have "thread \<in> runing (moment t2 s)"
+ proof(cases "thread \<in> set (wq (moment t2 s) cs2)")
+ case True
+ have "?e = V thread cs2"
+ proof -
+ have eq_th: "thread = hd (wq (moment t2 s) cs2)"
+ using True and np2 by auto
+ thus ?thesis
+ using True h2 ve2.vat_moment_e.wq_out_inv by blast
+ qed
+ thus ?thesis
+ using step.cases ve2.vat_moment_e.pip_e by auto
+ next
+ case False
+ hence "?e = P thread cs2"
+ using h1 ve2.vat_moment_e.wq_in_inv by blast
+ thus ?thesis
+ using step.cases ve2.vat_moment_e.pip_e by auto
+ qed
+ moreover have "thread \<notin> runing (moment t2 s)"
+ by (rule q_not_runing[OF nn1[rule_format, OF lt12]])
+ ultimately show ?thesis by simp
+ qed
+ } note lt_case = this
+ show ?thesis
+ proof -
+ { assume "t1 < t2"
+ from lt_case[OF lt1 np1 nn1 lt2 np2 nn2 this]
+ have ?thesis .
+ } moreover {
+ assume "t2 < t1"
+ from lt_case[OF lt2 np2 nn2 lt1 np1 nn1 this]
+ have ?thesis .
+ } moreover {
+ assume eq_12: "t1 = t2"
+ let ?t3 = "Suc t2"
+ interpret ve2: valid_moment_e _ t2 using lt2
+ by (unfold_locales, simp)
+ let ?e = ve2.next_e
+ have "t2 < ?t3" by simp
+ from nn2 [rule_format, OF this] and ve2.trace_e
+ have h1: "thread \<in> set (wq (?e#moment t2 s) cs2)" by auto
+ have lt_2: "t2 < ?t3" by simp
+ from nn2 [rule_format, OF this] and ve2.trace_e
+ have h1: "thread \<in> set (wq (?e#moment t2 s) cs2)" and
+ h2: "thread \<noteq> hd (wq (?e#moment t2 s) cs2)" by auto
+ from nn1[rule_format, OF lt_2[folded eq_12], unfolded ve2.trace_e[folded eq_12]]
+ eq_12[symmetric]
+ have g1: "thread \<in> set (wq (?e#moment t1 s) cs1)" and
+ g2: "thread \<noteq> hd (wq (?e#moment t1 s) cs1)" by auto
+ have "?e = V thread cs2 \<or> ?e = P thread cs2"
+ using h1 h2 np2 ve2.vat_moment_e.wq_in_inv
+ ve2.vat_moment_e.wq_out_inv by blast
+ moreover have "?e = V thread cs1 \<or> ?e = P thread cs1"
+ using eq_12 g1 g2 np1 ve2.vat_moment_e.wq_in_inv
+ ve2.vat_moment_e.wq_out_inv by blast
+ ultimately have ?thesis using neq12 by auto
+ } ultimately show ?thesis using nat_neq_iff by blast
+ qed
+qed
+
+text {*
+ This lemma is a simple corrolary of @{text "waiting_unique_pre"}.
+*}
+
+lemma waiting_unique:
+ assumes "waiting s th cs1"
+ and "waiting s th cs2"
+ shows "cs1 = cs2"
+ using waiting_unique_pre assms
+ unfolding wq_def s_waiting_def
+ by auto
+
+end
+
+lemma (in valid_trace_v)
+ preced_es [simp]: "preced th (e#s) = preced th s"
+ by (unfold is_v preced_def, simp)
+
+lemma the_preced_v[simp]: "the_preced (V th cs#s) = the_preced s"
+proof
+ fix th'
+ show "the_preced (V th cs # s) th' = the_preced s th'"
+ by (unfold the_preced_def preced_def, simp)
+qed
+
+
+lemma (in valid_trace_v)
+ the_preced_es: "the_preced (e#s) = the_preced s"
+ by (unfold is_v preced_def, simp)
+
+context valid_trace_p
+begin
+
+lemma not_holding_s_th_cs: "\<not> holding s th cs"
+proof
+ assume otherwise: "holding s th cs"
+ from pip_e[unfolded is_p]
+ show False
+ proof(cases)
+ case (thread_P)
+ moreover have "(Cs cs, Th th) \<in> RAG s"
+ using otherwise cs_holding_def
+ holding_eq th_not_in_wq by auto
+ ultimately show ?thesis by auto
+ qed
+qed
+
+end
+
+
lemma (in valid_trace_v_n) finite_waiting_set:
"finite {(Th th', Cs cs) |th'. next_th s th cs th'}"
by (simp add: waiting_set_eq)
@@ -2008,28 +1996,6 @@
"finite {(Cs cs, Th th') |th'. next_th s th cs th'}"
by (simp add: holding_set_eq)
-context valid_trace_v
-begin
-
-lemma
- finite_RAG_kept:
- assumes "finite (RAG s)"
- shows "finite (RAG (e#s))"
-proof(cases "rest = []")
- case True
- interpret vt: valid_trace_v_e using True
- by (unfold_locales, simp)
- show ?thesis using assms
- by (unfold RAG_es vt.waiting_set_eq vt.holding_set_eq, simp)
-next
- case False
- interpret vt: valid_trace_v_n using False
- by (unfold_locales, simp)
- show ?thesis using assms
- by (unfold RAG_es vt.waiting_set_eq vt.holding_set_eq, simp)
-qed
-
-end
context valid_trace_v_e
begin
@@ -2074,7 +2040,7 @@
by (unfold s_RAG_def, auto)
from this(2) have "waiting s taker cs'"
by (unfold s_RAG_def, fold waiting_eq, auto)
- from waiting_unique[OF this waiting_taker]
+ from waiting_unique[OF this waiting_taker]
have "cs' = cs" .
from h(1)[unfolded this] show False by auto
qed
@@ -2109,7 +2075,7 @@
by (unfold s_RAG_def, auto)
hence "waiting s th cs'"
by (unfold s_RAG_def, fold waiting_eq, auto)
- with th_not_waiting show False by auto
+ with th_not_waiting show False by auto (* ccc *)
qed
ultimately show ?thesis by auto
qed
@@ -2153,45 +2119,6 @@
context valid_trace
begin
-lemma finite_RAG:
- shows "finite (RAG s)"
-proof(induct rule:ind)
- case Nil
- show ?case
- by (auto simp: s_RAG_def cs_waiting_def
- cs_holding_def wq_def acyclic_def)
-next
- case (Cons s e)
- interpret vt_e: valid_trace_e s e using Cons by simp
- show ?case
- proof(cases e)
- case (Create th prio)
- interpret vt: valid_trace_create s e th prio using Create
- by (unfold_locales, simp)
- show ?thesis using Cons by (simp add: vt.RAG_unchanged)
- next
- case (Exit th)
- interpret vt: valid_trace_exit s e th using Exit
- by (unfold_locales, simp)
- show ?thesis using Cons by (simp add: vt.RAG_unchanged)
- next
- case (P th cs)
- interpret vt: valid_trace_p s e th cs using P
- by (unfold_locales, simp)
- show ?thesis using Cons using vt.RAG_es' 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 by (simp add: vt.finite_RAG_kept)
- next
- case (Set th prio)
- interpret vt: valid_trace_set s e th prio using Set
- by (unfold_locales, simp)
- show ?thesis using Cons by (simp add: vt.RAG_unchanged)
- qed
-qed
-
lemma acyclic_RAG:
shows "acyclic (RAG s)"
proof(induct rule:ind)
@@ -2207,12 +2134,12 @@
case (Create th prio)
interpret vt: valid_trace_create s e th prio using Create
by (unfold_locales, simp)
- show ?thesis using Cons by (simp add: vt.RAG_unchanged)
+ show ?thesis using Cons by simp
next
case (Exit th)
interpret vt: valid_trace_exit s e th using Exit
by (unfold_locales, simp)
- show ?thesis using Cons by (simp add: vt.RAG_unchanged)
+ show ?thesis using Cons by simp
next
case (P th cs)
interpret vt: valid_trace_p s e th cs using P
@@ -2249,10 +2176,31 @@
case (Set th prio)
interpret vt: valid_trace_set s e th prio using Set
by (unfold_locales, simp)
- show ?thesis using Cons by (simp add: vt.RAG_unchanged)
+ show ?thesis using Cons by simp
qed
qed
+end
+
+section {* RAG is single-valued *}
+
+context valid_trace
+begin
+
+lemma unique_RAG: "\<lbrakk>(n, n1) \<in> RAG s; (n, n2) \<in> RAG s\<rbrakk> \<Longrightarrow> n1 = n2"
+ apply(unfold s_RAG_def, auto, fold waiting_eq holding_eq)
+ by(auto elim:waiting_unique held_unique)
+
+lemma sgv_RAG: "single_valued (RAG s)"
+ using unique_RAG by (auto simp:single_valued_def)
+
+end
+
+section {* RAG is well-founded *}
+
+context valid_trace
+begin
+
lemma wf_RAG: "wf (RAG s)"
proof(rule finite_acyclic_wf)
from finite_RAG show "finite (RAG s)" .
@@ -2260,6 +2208,59 @@
from acyclic_RAG show "acyclic (RAG s)" .
qed
+lemma wf_RAG_converse:
+ shows "wf ((RAG s)^-1)"
+proof(rule finite_acyclic_wf_converse)
+ from finite_RAG
+ show "finite (RAG s)" .
+next
+ from acyclic_RAG
+ show "acyclic (RAG s)" .
+qed
+
+end
+
+section {* RAG forms a forest (or tree) *}
+
+context valid_trace
+begin
+
+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"
+ using rtree_RAG .
+
+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
+
+section {* Derived properties for parts of RAG *}
+
+context valid_trace
+begin
+
+lemma acyclic_tRAG: "acyclic (tRAG s)"
+proof(unfold tRAG_def, rule acyclic_compose)
+ show "acyclic (RAG s)" using acyclic_RAG .
+next
+ show "wRAG s \<subseteq> RAG s" unfolding RAG_split by auto
+next
+ show "hRAG s \<subseteq> RAG s" unfolding RAG_split by auto
+qed
+
lemma sgv_wRAG: "single_valued (wRAG s)"
using waiting_unique
by (unfold single_valued_def wRAG_def, auto)
@@ -2272,39 +2273,8 @@
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 \<subseteq> RAG s" unfolding RAG_split by auto
-next
- show "hRAG s \<subseteq> RAG s" unfolding RAG_split by auto
-qed
-
-lemma unique_RAG: "\<lbrakk>(n, n1) \<in> RAG s; (n, n2) \<in> RAG s\<rbrakk> \<Longrightarrow> n1 = n2"
- apply(unfold s_RAG_def, auto, fold waiting_eq holding_eq)
- by(auto elim:waiting_unique held_unique)
-
-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)" .
@@ -2312,24 +2282,6 @@
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
-
-lemma tRAG_alt_def:
- "tRAG s = {(Th th1, Th th2) | th1 th2.
- \<exists> cs. (Th th1, Cs cs) \<in> RAG s \<and> (Cs cs, Th th2) \<in> RAG s}"
- by (auto simp:tRAG_def RAG_split wRAG_def hRAG_def)
-
sublocale valid_trace < fsbttRAGs: fsubtree "tRAG s"
proof -
have "fsubtree (tRAG s)"
@@ -2363,6 +2315,70 @@
qed
+(* ccc *)
+
+context valid_trace_p
+begin
+
+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 live_th_es: "th \<in> threads (e#s)"
+ using live_th_s
+ by (unfold is_p, simp)
+
+
+lemma waiting_neq_th:
+ assumes "waiting s t c"
+ shows "t \<noteq> th"
+ using assms using th_not_waiting by blast
+
+end
+
+context valid_trace_v
+begin
+
+lemma th_not_waiting:
+ "\<not> waiting s th c"
+proof -
+ have "th \<in> readys s"
+ using runing_ready runing_th_s by blast
+ thus ?thesis
+ by (unfold readys_def, auto)
+qed
+
+lemma waiting_neq_th:
+ assumes "waiting s t c"
+ shows "t \<noteq> th"
+ using assms using th_not_waiting by blast
+
+end
+
+
+context valid_trace_e
+begin
+
+lemma actor_inv:
+ assumes "\<not> isCreate e"
+ shows "actor e \<in> runing s"
+ using pip_e assms
+ by (induct, auto)
+
+end
+
+
+(* ccc *)
+
+(* drag more from before to here *)
+
+
+section {* ccc *}
+
+
context valid_trace
begin
@@ -2393,10 +2409,9 @@
by (simp add: subtree_def the_preced_def)
qed
-
-lemma (in valid_trace) finite_threads:
+lemma finite_threads:
shows "finite (threads s)"
-using vt by (induct) (auto elim: step.cases)
+ using vt by (induct) (auto elim: step.cases)
lemma cp_le:
assumes th_in: "th \<in> threads s"
@@ -2432,16 +2447,6 @@
ultimately show ?thesis by auto
qed
-lemma wf_RAG_converse:
- shows "wf ((RAG s)^-1)"
-proof(rule finite_acyclic_wf_converse)
- from finite_RAG
- show "finite (RAG s)" .
-next
- from acyclic_RAG
- show "acyclic (RAG s)" .
-qed
-
lemma chain_building:
assumes "node \<in> Domain (RAG s)"
obtains th' where "th' \<in> readys s" "(node, Th th') \<in> (RAG s)^+"
@@ -2487,7 +2492,7 @@
text {* \noindent
The following is just an instance of @{text "chain_building"}.
-*}
+*}
lemma th_chain_to_ready:
assumes th_in: "th \<in> threads s"
shows "th \<in> readys s \<or> (\<exists> th'. th' \<in> readys s \<and> (Th th, Th th') \<in> (RAG s)^+)"
@@ -2585,13 +2590,6 @@
apply (unfold children_RAG_alt_def cntCS_def holdents_def)
by (rule card_image[symmetric], auto simp:inj_on_def)
-context valid_trace
-begin
-
-lemma finite_holdents: "finite (holdents s th)"
- by (unfold holdents_alt_def, insert fsbtRAGs.finite_children, auto)
-
-end
context valid_trace_p_w
begin
@@ -2655,6 +2653,9 @@
end
+lemma (in valid_trace) finite_holdents: "finite (holdents s th)"
+ by (unfold holdents_alt_def, insert fsbtRAGs.finite_children, auto)
+
context valid_trace_p_h
begin
@@ -2874,7 +2875,7 @@
end
-context valid_trace_v (* ccc *)
+context valid_trace_v
begin
lemma holding_th_cs_s:
@@ -2905,7 +2906,7 @@
proof -
have "cs \<in> holdents s th" using holding_th_cs_s
by (unfold holdents_def, simp)
- moreover have "finite (holdents s th)" using finite_holdents
+ moreover have "finite (holdents s th)" using finite_holdents (* ccc *)
by simp
ultimately show ?thesis
by (unfold cntCS_def,
@@ -4630,10 +4631,6 @@
context valid_trace
begin
-thm th_chain_to_ready
-
-find_theorems subtree Th RAG
-
lemma threads_alt_def:
"(threads s) = (\<Union> th \<in> readys s. {th'. Th th' \<in> subtree (RAG s) (Th th)})"
(is "?L = ?R")