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}"
abbreviation
"next_to_run ths \<equiv> hd (SOME q::thread list. distinct q \<and> set q = set ths)"
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) \<subseteq> RAG2 s \<union> {(Cs cs, Th th)}"
using assms
unfolding RAG2_def RAG_def wq_def Let_def waits_def holds_def
by (auto simp add: Let_def)
lemma RAG_p2:
assumes "(Cs cs, Th th) \<notin> (RAG2 s)\<^sup>+" "wq s cs \<noteq> []"
shows "RAG2 (P th cs # s) \<subseteq> RAG2 s \<union> {(Th th, Cs cs)}"
using assms
unfolding RAG2_def RAG_def wq_def Let_def waits_def holds_def
by (auto simp add: Let_def)
lemma [simp]: "(SOME q. distinct q \<and> q = []) = []"
by auto
lemma [simp]: "(x \<in> set (SOME q. distinct q \<and> set q = set p)) = (x \<in> set p)"
apply auto
apply (metis (mono_tags, lifting) List.finite_set finite_distinct_list some_eq_ex)
by (metis (mono_tags, lifting) List.finite_set finite_distinct_list some_eq_ex)
lemma RAG_v1:
assumes vt: "wq s cs = [th]"
shows "RAG2 (V th cs # s) \<subseteq> RAG2 s - {(Cs cs, Th th)}"
using assms
unfolding RAG2_def RAG_def waits_def holds_def wq_def
by (auto simp add: Let_def)
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))}"
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)
lemma waiting_unique:
assumes "vt s"
and "waits2 s th cs1"
and "waits2 s th cs2"
shows "cs1 = cs2"
sorry
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 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)
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 (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]
by (rule acyclic_subset)
}
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 wts where
eq_wq: "wq s cs = th # wts" by (cases "wq s cs") (auto)
{ assume "wts = []" -- "case no thread present to take over"
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)
ultimately
have "acyclic (RAG2 (V th cs # s))" by (auto intro: acyclic_subset)
}
moreover
{ 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)
moreover
have "acyclic (insert (Cs cs, Th nth) (RAG2 s - {(Cs cs, Th th)} - {(Th nth, Cs cs)}))"
proof -
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)
ultimately
show "acyclic (insert (Cs cs, Th nth) (RAG2 s - {(Cs cs, Th th)} - {(Th nth, Cs cs)}))"
by (simp add: acyclic_insert)
qed
ultimately have "acyclic (RAG2 (V th cs # s))" by (auto intro: acyclic_subset)
}
ultimately show "acyclic (RAG2 (V th cs # s))" by metis
qed (simp_all)