--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Test.thy Fri May 23 15:19:32 2014 +0100
@@ -0,0 +1,370 @@
+theory Test
+imports Precedence_ord
+begin
+
+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). *}
+
+datatype event =
+ Create thread priority
+| Exit thread
+| P thread cs
+| V thread cs
+| Set thread priority
+
+type_synonym state = "event list"
+
+fun threads :: "state \<Rightarrow> thread set"
+ where
+ "threads [] = {}"
+| "threads (Create th prio#s) = {th} \<union> threads s"
+| "threads (Exit th # s) = (threads s) - {th}"
+| "threads (_#s) = threads s"
+
+fun priority :: "thread \<Rightarrow> state \<Rightarrow> priority"
+ where
+ "priority th [] = 0"
+| "priority th (Create th' prio#s) = (if th' = th then prio else priority th s)"
+| "priority th (Set th' prio#s) = (if th' = th then prio else priority th s)"
+| "priority th (_#s) = priority th s"
+
+fun last_set :: "thread \<Rightarrow> state \<Rightarrow> nat"
+ where
+ "last_set th [] = 0"
+| "last_set th ((Create th' prio)#s) = (if (th = th') then length s else last_set th s)"
+| "last_set th ((Set th' prio)#s) = (if (th = th') then length s else last_set th s)"
+| "last_set th (_#s) = last_set th s"
+
+definition preced :: "thread \<Rightarrow> state \<Rightarrow> precedence"
+ where "preced th s \<equiv> Prc (priority th s) (last_set th s)"
+
+definition
+ "holds wq th cs \<equiv> th \<in> set (wq cs) \<and> th = hd (wq cs)"
+
+definition
+ "waits wq th cs \<equiv> th \<in> set (wq cs) \<and> th \<noteq> hd (wq cs)"
+
+datatype node =
+ Th "thread"
+| Cs "cs"
+
+definition
+ "RAG wq \<equiv> {(Th th, Cs cs) | th cs. waits wq th cs} \<union> {(Cs cs, Th th) | cs th. holds wq th cs}"
+
+definition
+ "dependants wq th \<equiv> {th' . (Th th', Th th) \<in> (RAG wq)^+}"
+
+record schedule_state =
+ wq_fun :: "cs \<Rightarrow> thread list"
+ cprec_fun :: "thread \<Rightarrow> precedence"
+
+definition cpreced :: "(cs \<Rightarrow> thread list) \<Rightarrow> state \<Rightarrow> thread \<Rightarrow> precedence"
+ where
+ "cpreced wq s th \<equiv> Max ({preced th s} \<union> {preced th' s | th'. th' \<in> dependants wq th})"
+
+abbreviation
+ "all_unlocked \<equiv> \<lambda>_::cs. ([]::thread list)"
+
+abbreviation
+ "initial_cprec \<equiv> \<lambda>_::thread. Prc 0 0"
+
+abbreviation
+ "release qs \<equiv> case qs of
+ [] => []
+ | (_#qs) => (SOME q. distinct q \<and> set q = set qs)"
+
+fun schs :: "state \<Rightarrow> schedule_state"
+ where
+ "schs [] = (| wq_fun = \<lambda> cs. [], cprec_fun = (\<lambda>_. Prc 0 0) |)"
+| "schs (Create th prio # s) =
+ (let wq = wq_fun (schs s) in
+ (|wq_fun = wq, cprec_fun = cpreced wq (Create th prio # s)|))"
+| "schs (Exit th # s) =
+ (let wq = wq_fun (schs s) in
+ (|wq_fun = wq, cprec_fun = cpreced wq (Exit th # s)|))"
+| "schs (Set th prio # s) =
+ (let wq = wq_fun (schs s) in
+ (|wq_fun = wq, cprec_fun = cpreced wq (Set th prio # s)|))"
+| "schs (P th cs # s) =
+ (let wq = wq_fun (schs s) in
+ let new_wq = wq(cs := (wq cs @ [th])) in
+ (|wq_fun = new_wq, cprec_fun = cpreced new_wq (P th cs # s)|))"
+| "schs (V th cs # s) =
+ (let wq = wq_fun (schs s) in
+ let new_wq = wq(cs := release (wq cs)) in
+ (|wq_fun = new_wq, cprec_fun = cpreced new_wq (V th cs # s)|))"
+
+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
+ "holds2 s \<equiv> holds (wq_fun (schs s))"
+
+definition
+ "waits2 s \<equiv> waits (wq_fun (schs s))"
+
+definition
+ "RAG2 s \<equiv> RAG (wq_fun (schs s))"
+
+definition
+ "dependants2 s \<equiv> dependants (wq_fun (schs s))"
+
+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))}"
+
+definition holding :: "state \<Rightarrow> thread \<Rightarrow> cs set"
+ where "holding s th \<equiv> {cs . holds2 s th cs}"
+
+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
+by auto
+
+inductive step :: "state \<Rightarrow> event \<Rightarrow> bool"
+ where
+ step_Create: "\<lbrakk>th \<notin> threads s\<rbrakk> \<Longrightarrow> step s (Create th prio)"
+| step_Exit: "\<lbrakk>th \<in> runing s; holding s th = {}\<rbrakk> \<Longrightarrow> step s (Exit th)"
+| step_P: "\<lbrakk>th \<in> runing s; (Cs cs, Th th) \<notin> (RAG2 s)^+\<rbrakk> \<Longrightarrow> step s (P th cs)"
+| 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)"
+
+inductive vt :: "state \<Rightarrow> bool"
+ where
+ vt_nil[intro]: "vt []"
+| vt_cons[intro]: "\<lbrakk>vt s; step s e\<rbrakk> \<Longrightarrow> vt (e#s)"
+
+lemma runing_ready:
+ shows "runing s \<subseteq> readys s"
+ unfolding runing_def readys_def
+ by auto
+
+lemma readys_threads:
+ shows "readys s \<subseteq> threads s"
+ unfolding readys_def
+ by auto
+
+lemma wq_distinct_step:
+ assumes "step s e" "distinct (wq s cs)"
+ shows "distinct (wq (e # s) cs)"
+using assms
+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 split: list.split)
+apply(rule someI2)
+apply(auto)
+done
+
+lemma wq_distinct:
+ assumes "vt s"
+ shows "distinct (wq s cs)"
+using assms
+apply(induct)
+apply(simp add: wq_def)
+apply(simp add: wq_distinct_step)
+done
+
+lemma RAG_set_unchanged[simp]:
+ shows "RAG2 (Set th prio # s) = RAG2 s"
+unfolding RAG2_def
+by (simp add: Let_def)
+
+lemma RAG_create_unchanged[simp]:
+ "RAG2 (Create th prio # s) = RAG2 s"
+unfolding RAG2_def
+by (simp add: Let_def)
+
+lemma RAG_exit_unchanged[simp]:
+ shows "RAG2 (Exit th # s) = RAG2 s"
+unfolding RAG2_def
+by (simp add: Let_def)
+
+lemma RAG_p1:
+ assumes "wq s cs = []"
+ shows "RAG2 (P th cs # s) = RAG2 s \<union> {(Cs cs, Th th)}"
+ using assms
+ apply(auto simp add: RAG2_def RAG_def wq_def Let_def waits_def holds_def)
+ apply (metis in_set_insert insert_Nil list.distinct(1))
+ done
+
+lemma RAG_p2:
+ assumes "vt (P th cs#s)" "wq s cs \<noteq> []"
+ shows "RAG2 (P th cs # s) = RAG2 s \<union> {(Th th, Cs cs)}"
+ using assms
+ apply(simp add: RAG2_def Let_def)
+ apply(erule_tac vt.cases)
+ apply(simp)
+ apply(clarify)
+ apply(simp)
+ apply(erule_tac step.cases)
+ apply(simp_all)
+ apply(simp add: wq_def RAG_def RAG2_def)
+ apply(simp add: waits_def holds_def)
+ apply(auto)
+ done
+
+definition next_th:: "state \<Rightarrow> thread \<Rightarrow> cs \<Rightarrow> thread \<Rightarrow> bool"
+ where "next_th s th cs t =
+ (\<exists> rest. wq s cs = th#rest \<and> rest \<noteq> [] \<and> t = hd (SOME q. distinct q \<and> set q = set rest))"
+
+lemma RAG_v:
+assumes vt:"vt (V th cs#s)"
+shows "
+ RAG2 (V th cs # s) =
+ RAG2 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'}"
+ apply (insert vt, unfold RAG2_def RAG_def)
+ sorry
+
+lemma waiting_unique:
+ assumes "vt s"
+ and "waits2 s th cs1"
+ and "waits2 s th cs2"
+ shows "cs1 = cs2"
+sorry
+
+lemma singleton_Un:
+ shows "A \<union> {x} = insert x A"
+by simp
+
+
+lemma acyclic_RAG_step:
+ assumes vt: "vt s"
+ and stp: "step s e"
+ and ac: "acyclic (RAG2 s)"
+ shows "acyclic (RAG2 (e # s))"
+using stp vt ac
+proof (induct)
+ case (step_P th s cs)
+ have vt: "vt s" by fact
+ have ac: "acyclic (RAG2 s)" by fact
+ have rn: "th \<in> runing s" by fact
+ have ds: "(Cs cs, Th th) \<notin> (RAG2 s)\<^sup>+" by fact
+ have vtt: "vt (P th cs#s)" using vt rn ds by (metis step.step_P vt_cons)
+ { 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)
+ 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)
+ 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] by simp
+ }
+ 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 vtt a] by simp
+ }
+ ultimately show "acyclic (RAG2 (P th cs # s))" by metis
+next
+ case (step_V th s cs)
+ 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 rest where
+ eq_wq: "wq s cs = th # rest" by (cases "wq s cs") (auto)
+ show ?case
+ apply(subst RAG_v)
+ apply(rule vt_cons)
+ apply(rule vt)
+ apply(rule step.step_V)
+ apply(rule rn)
+ apply(rule hd)
+ using eq_wq
+ apply(cases "rest = []")
+ apply(subgoal_tac "{(Cs cs, Th th') |th'. next_th s th cs th'} = {}")
+ apply(simp)
+ apply(rule acyclic_subset)
+ apply(rule ac)
+ apply(auto)[1]
+ apply(auto simp add: next_th_def)[1]
+ -- "case wq more than a singleton"
+ apply(subgoal_tac "{(Cs cs, Th (hd (SOME q. distinct q \<and> set q = set rest)))} =
+ {(Cs cs, Th th') |th'. next_th s th cs th'}")
+ apply(rotate_tac 2)
+ apply(drule sym)
+ apply(simp only: singleton_Un)
+ apply(simp only: acyclic_insert)
+ apply(rule conjI)
+ apply(rule acyclic_subset)
+ apply(rule ac)
+ apply(auto)[1]
+ apply(rotate_tac 2)
+ apply(thin_tac "?X")
+ defer
+ apply(simp add: next_th_def)
+ apply(clarify)
+ apply(simp add: rtrancl_eq_or_trancl)
+ apply(drule tranclD)
+ apply(erule exE)
+ apply(drule conjunct1)
+ apply(subgoal_tac "(Th (hd (SOME q. distinct q \<and> set q = set rest)), z) \<in> RAG2 s")
+ prefer 2
+ apply(simp)
+ apply(case_tac z)
+ apply(simp add: RAG2_def RAG_def)
+ apply(clarify)
+ apply(simp)
+ apply(simp add: next_th_def)
+ apply(rule waiting_unique)
+ apply(rule vt)
+ apply(simp add: RAG2_def RAG_def waits2_def waits_def wq_def)
+ apply(rotate_tac 2)
+ apply(thin_tac "?X")
+ apply(subgoal_tac "distinct (wq s cs)")
+ prefer 2
+ apply(rule wq_distinct)
+ apply(rule vt)
+ apply (unfold waits2_def waits_def wq_def, auto)
+ apply(subgoal_tac "(SOME q. distinct q \<and> set q = set rest) \<noteq> []")
+ prefer 2
+ apply (metis (mono_tags) set_empty tfl_some)
+ apply(subgoal_tac "hd (SOME q. distinct q \<and> set q = set rest) \<in>
+ set (SOME q. distinct q \<and> set q = set rest)")
+ prefer 2
+ apply(auto)[1]
+ apply(subgoal_tac "set (SOME q. distinct q \<and> set q = set rest) = set rest")
+ prefer 2
+ apply(rule someI2)
+ apply(auto)[2]
+ apply(auto)[1]
+ apply(subgoal_tac "(SOME q. distinct q \<and> set q = set rest) \<noteq> []")
+ prefer 2
+ apply (metis (mono_tags) set_empty tfl_some)
+ apply(subgoal_tac "hd (SOME q. distinct q \<and> set q = set rest) \<in>
+ set (SOME q. distinct q \<and> set q = set rest)")
+ prefer 2
+ apply(auto)[1]
+ apply(subgoal_tac "set (SOME q. distinct q \<and> set q = set rest) = set rest")
+ prefer 2
+ apply(rule someI2)
+ apply(auto)[2]
+ apply(auto)[1]
+ done
+qed (simp_all)
+
+
+
+
+
+