theory Test 

imports Precedence_ord Graphs

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 resources). *}

-- {* Schedulling Events *}

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)"

abbreviation 

  "preceds s ths \<equiv> {preced th s | th. th \<in> ths}"

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)"

--{* Nodes in Resource Graph *}

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"

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(rule iffI)

apply (metis (mono_tags, lifting) List.finite_set finite_distinct_list some_eq_ex)+

done

abbreviation

  "next_to_run ths \<equiv> hd (SOME q::thread list. distinct q \<and> set q = set ths)"

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 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))"

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))"

(* 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> 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}"

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 RAG2_def RAG_def

unfolding holds2_def 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)"

(* valid states *)

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_threads: 

  assumes vt: "vt s"

  and h: "th \<in> set (wq s cs)"

  shows "th \<in> threads s"

using assms

apply(induct)

apply(simp add: wq_def)

apply(erule step.cases)

apply(auto simp add: wq_def Let_def holding_def holds2_def holds_def waits2_def runing_def readys_def)

apply(simp add: waits_def)

apply(auto simp add: waits_def split: if_splits)[1]

apply(auto split: if_splits)

apply(simp only: waits_def)

by (metis insert_iff set_simps(2))

lemma Domain_RAG_threads:

  assumes vt: "vt s"

  and in_dom: "(Th th) \<in> Domain (RAG2 s)"

  shows "th \<in> threads s"

proof -

  from in_dom obtain n where "(Th th, n) \<in> RAG2 s" by auto

  then obtain cs where "n = Cs cs" "(Th th, Cs cs) \<in> RAG2 s"  

    unfolding RAG2_def RAG_def by auto

  then have "th \<in> set (wq s cs)"

    unfolding wq_def RAG_def RAG2_def waits_def by auto

  with wq_threads [OF vt] show ?thesis .

qed

lemma dependants_threads:

  assumes vt: "vt s"

  shows "dependants2 s th \<subseteq> threads s"

proof

  fix th1 

  assume "th1 \<in> dependants2 s th"

  then have h: "(Th th1, Th th) \<in> (RAG2 s)\<^sup>+"

    unfolding dependants2_def dependants_def RAG2_def by simp

  then have "Th th1 \<in> Domain ((RAG2 s)\<^sup>+)" unfolding Domain_def by auto

  then have "Th th1 \<in> Domain (RAG2 s)" using trancl_domain by simp

  then show "th1 \<in> threads s" using vt by (rule_tac Domain_RAG_threads)

qed

lemma finite_threads:

  assumes vt: "vt s"

  shows "finite (threads s)"

using vt by (induct) (auto elim: step.cases)

section {* Distinctness of @{const wq} *}

lemma wq_distinct_step: 

  assumes "step s e" "distinct (wq s cs)" 

  shows "distinct (wq (e # s) cs)"

using assms

unfolding wq_def

apply(erule_tac step.cases)

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)

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

section {* Single_Valuedness of @{const waits2}, @{const holds2}, @{const RAG2} *}

lemma waits2_unique:

  assumes "vt s"

  and "waits2 s th cs1"

  and "waits2 s th cs2"

  shows "cs1 = cs2"

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 single_valued_waits2:

  assumes "vt s"

  shows "single_valuedP (waits2 s)"

using assms

unfolding single_valued_def

by (metis Collect_splitD fst_eqD sndI waits2_unique)

lemma single_valued_holds2:

  assumes "vt s"

  shows "single_valuedP (\<lambda>cs th. holds2 s th cs)"

unfolding single_valued_def holds2_def holds_def by simp

lemma single_valued_RAG2:

  assumes "vt s"

  shows "single_valued (RAG2 s)"

using single_valued_waits2[OF assms] single_valued_holds2[OF assms] 

unfolding RAG2_def RAG_def

apply(rule_tac single_valued_union)

unfolding holds2_def[symmetric] waits2_def[symmetric]

apply(rule single_valued_Collect)

apply(simp)

apply(simp add: inj_on_def)

apply(rule single_valued_Collect)

apply(simp)

apply(simp add: inj_on_def)

apply(auto)

done

section {* Properties of @{const RAG2} under events *}

lemma RAG_Set [simp]: 

  shows "RAG2 (Set th prio # s) = RAG2 s"

unfolding RAG2_def

by (simp add: Let_def)

lemma RAG_Create [simp]: 

  "RAG2 (Create th prio # s) = RAG2 s"

unfolding RAG2_def

by (simp add: Let_def)

lemma RAG_Exit [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 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)

section {* Acyclicity of @{const RAG2} *}

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 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 wq_empty show False by (auto simp: RAG2_def RAG_def wq_def waits_def)

    qed

    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 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 for release of a lock" 

  have vt: "vt s" by fact

  have ac: "acyclic (RAG2 s)" by fact

  have hd: "holds2 s th cs" by fact

  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)

    ultimately 

    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 wq_not_empty: "wts \<noteq> []" 

    have "waits2 s nth cs" 

      using eq_wq wq_not_empty wq_distinct

      unfolding nth_def waits2_def waits_def wq_def[symmetric] by auto

    then have cs_in_RAG: "(Th nth, Cs cs) \<in> RAG2 s" 

      unfolding RAG2_def RAG_def waits2_def 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 (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)

      moreover 

      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 have "z = Cs cs" using cs_in_RAG single_valued_RAG2[OF vt]

          by (simp add: single_valued_def)

        then show "False" using a by simp

      qed

      ultimately 

      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 (rule_tac acyclic_subset)

  }

  ultimately show "acyclic (RAG2 (V th cs # s))" by metis

qed (simp_all)

lemma finite_RAG:

  assumes "vt s"

  shows "finite (RAG2 s)"

using assms

apply(induct)

apply(simp add: RAG2_def RAG_def waits_def holds_def)

apply(erule step.cases)

apply(auto)

apply(case_tac "wq sa cs = []")

apply(rule finite_subset)

apply(rule RAG_P1)

apply(simp)

apply(simp)

apply(rule finite_subset)

apply(rule RAG_P2)

apply(simp)

apply(simp)

apply(simp)

apply(subgoal_tac "\<exists>wts. wq sa cs = th # wts")

apply(erule exE)

apply(case_tac "wts = []")

apply(rule finite_subset)

apply(rule RAG_V1)

apply(simp)

apply(simp)

apply(rule finite_subset)

apply(rule RAG_V2)

apply(simp)

apply(simp)

apply(simp)

apply(subgoal_tac "th \<in> set (wq sa cs) \<and> th = hd (wq sa cs)") 

apply(case_tac "wq sa cs") 

apply(auto)[2]

apply(auto simp add: holds2_def holds_def wq_def)

done

lemma dchain_unique:

  assumes vt: "vt s"

  and th1_d: "(n, Th th1) \<in> (RAG2 s)^+"

  and th1_r: "th1 \<in> readys s"

  and th2_d: "(n, Th th2) \<in> (RAG2 s)^+"

  and th2_r: "th2 \<in> readys s"

  shows "th1 = th2"

proof(rule ccontr)

  assume neq: "th1 \<noteq> th2"

   with single_valued_confluent2 [OF single_valued_RAG2 [OF vt]] th1_d th2_d

  have "(Th th1, Th th2) \<in> (RAG2 s)\<^sup>+ \<or> (Th th2, Th th1) \<in> (RAG2 s)\<^sup>+" by auto

  moreover

  { assume "(Th th1, Th th2) \<in> (RAG2 s)\<^sup>+"      

    then obtain n where dd: "(Th th1, n) \<in> RAG2 s" by (metis converse_tranclE)

    then obtain cs where eq_n: "n = Cs cs"

      unfolding RAG2_def RAG_def by (case_tac n) (auto)

    from dd eq_n have "th1 \<notin> readys s"

      unfolding RAG2_def RAG_def waits2_def readys_def by (auto)

    with th1_r have "False" by auto

  }