--- a/Test.thy Sat May 24 12:39:12 2014 +0100
+++ b/Test.thy Fri May 30 07:56:39 2014 +0100
@@ -4,7 +4,7 @@
type_synonym thread = nat -- {* Type for thread identifiers. *}
type_synonym priority = nat -- {* Type for priorities. *}
-type_synonym cs = nat -- {* Type for critical sections (or critical resources). *}
+type_synonym cs = nat -- {* Type for critical sections (or resources). *}
datatype event =
Create thread priority
@@ -98,8 +98,11 @@
definition wq :: "state \<Rightarrow> cs \<Rightarrow> thread list"
where "wq s = wq_fun (schs s)"
-definition cp :: "state \<Rightarrow> thread \<Rightarrow> precedence"
- where "cp s \<equiv> cprec_fun (schs s)"
+definition cpreced2 :: "state \<Rightarrow> thread \<Rightarrow> precedence"
+ where "cpreced2 s \<equiv> cprec_fun (schs s)"
+
+abbreviation
+ "cpreceds2 s ths \<equiv> {cpreced2 s th | th. th \<in> ths}"
definition
"holds2 s \<equiv> holds (wq_fun (schs s))"
@@ -113,24 +116,33 @@
definition
"dependants2 s \<equiv> dependants (wq_fun (schs s))"
+(* ready -> is a thread that is not waiting for any resource *)
definition readys :: "state \<Rightarrow> thread set"
where "readys s \<equiv> {th . th \<in> threads s \<and> (\<forall> cs. \<not> waits2 s th cs)}"
definition runing :: "state \<Rightarrow> thread set"
- where "runing s \<equiv> {th . th \<in> readys s \<and> cp s th = Max ((cp s) ` (readys s))}"
+ where "runing s \<equiv> {th . th \<in> readys s \<and> cpreced2 s th = Max (cpreceds2 s (readys s))}"
+(* all resources a thread hols in a state *)
definition holding :: "state \<Rightarrow> thread \<Rightarrow> cs set"
where "holding s th \<equiv> {cs . holds2 s th cs}"
abbreviation
"next_to_run ths \<equiv> hd (SOME q::thread list. distinct q \<and> set q = set ths)"
+lemma exists_distinct:
+ obtains ys where "distinct ys" "set ys = set xs"
+by (metis List.finite_set finite_distinct_list)
+
+lemma next_to_run_set [simp]:
+ "wts \<noteq> [] \<Longrightarrow> next_to_run wts \<in> set wts"
+apply(rule exists_distinct[of wts])
+by (metis (mono_tags, lifting) hd_in_set set_empty some_eq_ex)
+
lemma holding_RAG:
"holding s th = {cs . (Cs cs, Th th) \<in> RAG2 s}"
-unfolding holding_def
-unfolding holds2_def
-unfolding RAG2_def RAG_def
-unfolding holds_def waits_def
+unfolding holding_def RAG2_def RAG_def
+unfolding holds2_def holds_def waits_def
by auto
inductive step :: "state \<Rightarrow> event \<Rightarrow> bool"
@@ -141,6 +153,7 @@
| step_V: "\<lbrakk>th \<in> runing s; holds2 s th cs\<rbrakk> \<Longrightarrow> step s (V th cs)"
| step_Set: "\<lbrakk>th \<in> runing s\<rbrakk> \<Longrightarrow> step s (Set th prio)"
+(* valid states *)
inductive vt :: "state \<Rightarrow> bool"
where
vt_nil[intro]: "vt []"
@@ -160,9 +173,10 @@
assumes "step s e" "distinct (wq s cs)"
shows "distinct (wq (e # s) cs)"
using assms
+unfolding wq_def
apply(induct)
-apply(auto simp add: wq_def Let_def)
-apply(auto simp add: wq_def Let_def RAG2_def RAG_def holds_def runing_def waits2_def waits_def readys_def)[1]
+apply(auto simp add: RAG2_def RAG_def Let_def)[1]
+apply(auto simp add: wq_def Let_def RAG2_def RAG_def holds_def runing_def waits2_def waits_def readys_def)
apply(auto split: list.split)
apply(rule someI2)
apply(auto)
@@ -225,7 +239,7 @@
lemma RAG_v2:
assumes vt:"vt s" "wq s cs = th # wts \<and> wts \<noteq> []"
shows "RAG2 (V th cs # s) \<subseteq>
- RAG2 s - {(Cs cs, Th th)} - {(Th (next_to_run wts), Cs cs)} \<union> {(Cs cs, Th (next_to_run wts))}"
+ RAG2 s - {(Cs cs, Th th), (Th (next_to_run wts), Cs cs)} \<union> {(Cs cs, Th (next_to_run wts))}"
unfolding RAG2_def RAG_def waits_def holds_def
using assms wq_distinct[OF vt(1), of"cs"]
by (auto simp add: Let_def wq_def)
@@ -235,7 +249,22 @@
and "waits2 s th cs1"
and "waits2 s th cs2"
shows "cs1 = cs2"
-sorry
+using assms
+apply(induct)
+apply(simp add: waits2_def waits_def)
+apply(erule step.cases)
+apply(auto simp add: Let_def waits2_def waits_def holds_def RAG2_def RAG_def
+ readys_def runing_def split: if_splits)
+apply (metis Nil_is_append_conv hd_append2 list.distinct(1) split_list)
+apply (metis Nil_is_append_conv hd_append2 list.distinct(1) split_list)
+apply (metis distinct.simps(2) distinct_length_2_or_more list.sel(1) wq_def wq_distinct)
+by (metis (full_types, hide_lams) distinct.simps(2) distinct_length_2_or_more list.sel(1) wq_def wq_distinct)
+
+
+lemma rtrancl_eq_trancl [simp]:
+ assumes "x \<noteq> y"
+ shows "(x, y) \<in> r\<^sup>* \<longleftrightarrow> (x, y) \<in> r\<^sup>+"
+using assms by (metis rtrancl_eq_or_trancl)
lemma acyclic_RAG_step:
assumes vt: "vt s"
@@ -247,39 +276,35 @@
case (step_P th s cs)
have ac: "acyclic (RAG2 s)" by fact
have ds: "(Cs cs, Th th) \<notin> (RAG2 s)\<^sup>+" by fact
- { assume a: "wq s cs = []" -- "case waiting queue is empty"
- have "(Th th, Cs cs) \<notin> (RAG2 s)\<^sup>*"
- proof
- assume "(Th th, Cs cs) \<in> (RAG2 s)\<^sup>*"
- then have "(Th th, Cs cs) \<in> (RAG2 s)\<^sup>+" by (simp add: rtrancl_eq_or_trancl)
+ { assume wq_empty: "wq s cs = []" -- "case waiting queue is empty"
+ then have "(Th th, Cs cs) \<notin> (RAG2 s)\<^sup>+"
+ proof (rule_tac notI)
+ assume "(Th th, Cs cs) \<in> (RAG2 s)\<^sup>+"
then obtain x where "(x, Cs cs) \<in> RAG2 s" using tranclD2 by metis
- with a show False by (auto simp: RAG2_def RAG_def wq_def waits_def)
+ with wq_empty show False by (auto simp: RAG2_def RAG_def wq_def waits_def)
qed
- with acyclic_insert ac
- have "acyclic (RAG2 s \<union> {(Cs cs, Th th)})" by simp
- then have "acyclic (RAG2 (P th cs # s))" using RAG_p1[OF a]
+ with ac have "acyclic (RAG2 s \<union> {(Cs cs, Th th)})" by simp
+ then have "acyclic (RAG2 (P th cs # s))" using RAG_p1[OF wq_empty]
by (rule acyclic_subset)
}
moreover
- { assume a: "wq s cs \<noteq> []" -- "case waiting queue is not empty"
- from ds have "(Cs cs, Th th) \<notin> (RAG2 s)\<^sup>*" by (metis node.distinct(1) rtranclD)
- with acyclic_insert ac
- have "acyclic (RAG2 s \<union> {(Th th, Cs cs)})" by auto
- then have "acyclic (RAG2 (P th cs # s))" using RAG_p2[OF ds a]
+ { assume wq_not_empty: "wq s cs \<noteq> []" -- "case waiting queue is not empty"
+ from ac ds
+ have "acyclic (RAG2 s \<union> {(Th th, Cs cs)})" by simp
+ then have "acyclic (RAG2 (P th cs # s))" using RAG_p2[OF ds wq_not_empty]
by (rule acyclic_subset)
}
ultimately show "acyclic (RAG2 (P th cs # s))" by metis
next
- case (step_V th s cs)
+ case (step_V th s cs) -- "case for release of a lock"
have vt: "vt s" by fact
have ac: "acyclic (RAG2 s)" by fact
- have rn: "th \<in> runing s" by fact
have hd: "holds2 s th cs" by fact
- from hd have th_in: "th \<in> set (wq s cs)" and
- eq_hd: "th = hd (wq s cs)" unfolding holds2_def holds_def wq_def by auto
- then obtain wts where
- eq_wq: "wq s cs = th # wts" by (cases "wq s cs") (auto)
- { assume "wts = []" -- "case no thread present to take over"
+ from vt have wq_distinct:"distinct (wq s cs)" by (rule wq_distinct)
+ from hd have "th \<in> set (wq s cs)" "th = hd (wq s cs)" unfolding holds2_def holds_def wq_def by auto
+ then obtain wts where eq_wq: "wq s cs = th # wts" by (cases "wq s cs") (auto)
+ -- "case no thread present in the waiting queue to take over"
+ { assume "wts = []"
with eq_wq have "wq s cs = [th]" by simp
then have "RAG2 (V th cs # s) \<subseteq> RAG2 s - {(Cs cs, Th th)}" by (rule RAG_v1)
moreover have "acyclic (RAG2 s - {(Cs cs, Th th)})" using ac by (auto intro: acyclic_subset)
@@ -287,39 +312,39 @@
have "acyclic (RAG2 (V th cs # s))" by (auto intro: acyclic_subset)
}
moreover
+ -- "at least one thread present to take over"
{ def nth \<equiv> "next_to_run wts"
- assume aa: "wts \<noteq> []" -- "at least one thread present to take over"
- with vt eq_wq
- have "RAG2 (V th cs # s) \<subseteq> RAG2 s - {(Cs cs, Th th)} - {(Th nth, Cs cs)} \<union> {(Cs cs, Th nth)}"
- unfolding nth_def by (rule_tac RAG_v2) (auto)
+ assume wq_not_empty: "wts \<noteq> []"
+ have waits2_cs: "waits2 s nth cs"
+ using eq_wq wq_not_empty wq_distinct
+ unfolding nth_def waits2_def waits_def wq_def[symmetric] by auto
+ have "RAG2 (V th cs # s) \<subseteq> RAG2 s - {(Cs cs, Th th), (Th nth, Cs cs)} \<union> {(Cs cs, Th nth)}"
+ unfolding nth_def using vt wq_not_empty eq_wq by (rule_tac RAG_v2) (auto)
moreover
- have "acyclic (insert (Cs cs, Th nth) (RAG2 s - {(Cs cs, Th th)} - {(Th nth, Cs cs)}))"
+ have "acyclic (RAG2 s - {(Cs cs, Th th), (Th nth, Cs cs)} \<union> {(Cs cs, Th nth)})"
proof -
- have "acyclic (RAG2 s - {(Cs cs, Th th)} - {(Th nth, Cs cs)})" using ac by (auto intro: acyclic_subset)
+ have "acyclic (RAG2 s - {(Cs cs, Th th), (Th nth, Cs cs)})" using ac by (auto intro: acyclic_subset)
moreover
- have "(Th nth, Cs cs) \<notin> (RAG2 s - {(Cs cs, Th th)} - {(Th nth, Cs cs)})\<^sup>+"
- proof
- assume "(Th nth, Cs cs) \<in> (RAG2 s - {(Cs cs, Th th)} - {(Th nth, Cs cs)})\<^sup>+"
- then obtain z where a: "(Th nth, z) \<in> (RAG2 s - {(Cs cs, Th th)} - {(Th nth, Cs cs)})"
- by (metis converse_tranclE)
- then have "(Th nth, z) \<in> RAG2 s" by simp
- then obtain cs' where b: "z = Cs cs'" "(Th nth, Cs cs') \<in> RAG2 s"
- unfolding RAG2_def RAG_def by auto
- then have "cs = cs'"
- apply(rule_tac waiting_unique[OF vt])
- using eq_wq aa
- apply(auto simp add: nth_def RAG2_def RAG_def waits2_def waits_def wq_def)
- apply (metis (mono_tags, lifting) `\<And>thesis. (\<And>wts. wq s cs = th # wts \<Longrightarrow> thesis) \<Longrightarrow> thesis` distinct.simps(2) hd_in_set list.inject set_empty2 tfl_some vt wq_def wq_distinct)
- by (metis (mono_tags, lifting) `\<And>thesis. (\<And>wts. wq s cs = th # wts \<Longrightarrow> thesis) \<Longrightarrow> thesis` distinct.simps(2) hd_in_set list.sel(1) set_empty2 tfl_some vt wq_def wq_distinct)
- then show "False" using a b by simp
- qed
- then have "(Th nth, Cs cs) \<notin> (RAG2 s - {(Cs cs, Th th)} - {(Th nth, Cs cs)})\<^sup>*"
- by (metis node.distinct(1) rtranclD)
+ have "(Th nth, Cs cs) \<notin> (RAG2 s - {(Cs cs, Th th), (Th nth, Cs cs)})\<^sup>+"
+ proof (rule notI)
+ assume "(Th nth, Cs cs) \<in> (RAG2 s - {(Cs cs, Th th), (Th nth, Cs cs)})\<^sup>+"
+ then obtain z where a: "(Th nth, z) \<in> (RAG2 s - {(Cs cs, Th th), (Th nth, Cs cs)})"
+ by (metis converse_tranclE)
+ then have "(Th nth, z) \<in> RAG2 s" by simp
+ then obtain cs' where b: "z = Cs cs'" "(Th nth, Cs cs') \<in> RAG2 s"
+ unfolding RAG2_def RAG_def by auto
+ moreover
+ have "waits2 s nth cs'"
+ using b(2) unfolding RAG2_def RAG_def waits2_def by simp
+ ultimately have "cs = cs'"
+ by (rule_tac waiting_unique[OF vt waits2_cs])
+ then show "False" using a b(1) by simp
+ qed
ultimately
- show "acyclic (insert (Cs cs, Th nth) (RAG2 s - {(Cs cs, Th th)} - {(Th nth, Cs cs)}))"
- by (simp add: acyclic_insert)
+ show "acyclic (RAG2 s - {(Cs cs, Th th), (Th nth, Cs cs)} \<union> {(Cs cs, Th nth) })" by simp
qed
- ultimately have "acyclic (RAG2 (V th cs # s))" by (auto intro: acyclic_subset)
+ ultimately have "acyclic (RAG2 (V th cs # s))"
+ by (rule_tac acyclic_subset)
}
ultimately show "acyclic (RAG2 (V th cs # s))" by metis
qed (simp_all)