Test.thy
author Christian Urban <christian dot urban at kcl dot ac dot uk>
Sat, 24 May 2014 12:39:12 +0100
changeset 37 c820ac0f3088
parent 36 af38526275f8
child 38 c89013dca1aa
permissions -rw-r--r--
simplified RAG_acyclic proof

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)