1 theory Test 

     2 imports Precedence_ord

     3 begin

     4 

     5 type_synonym thread = nat -- {* Type for thread identifiers. *}

     6 type_synonym priority = nat  -- {* Type for priorities. *}

     7 type_synonym cs = nat -- {* Type for critical sections (or critical resources). *}

     8 

     9 datatype event = 

    10   Create thread priority 

    11 | Exit thread 

    12 | P thread cs 

    13 | V thread cs 

    14 | Set thread priority 

    15 

    16 type_synonym state = "event list"

    17 

    18 fun threads :: "state \<Rightarrow> thread set"

    19   where 

    20   "threads [] = {}" 

    21 | "threads (Create th prio#s) = {th} \<union> threads s" 

    22 | "threads (Exit th # s) = (threads s) - {th}" 

    23 | "threads (_#s) = threads s" 

    24 

    25 fun priority :: "thread \<Rightarrow> state \<Rightarrow> priority"

    26   where

    27   "priority th [] = 0" 

    28 | "priority th (Create th' prio#s) = (if th' = th then prio else priority th s)" 

    29 | "priority th (Set th' prio#s) = (if th' = th then prio else priority th s)" 

    30 | "priority th (_#s) = priority th s"

    31 

    32 fun last_set :: "thread \<Rightarrow> state \<Rightarrow> nat"

    33   where

    34   "last_set th [] = 0" 

    35 | "last_set th ((Create th' prio)#s) = (if (th = th') then length s else last_set th s)" 

    36 | "last_set th ((Set th' prio)#s) = (if (th = th') then length s else last_set th s)" 

    37 | "last_set th (_#s) = last_set th s"

    38 

    39 definition preced :: "thread \<Rightarrow> state \<Rightarrow> precedence"

    40   where "preced th s \<equiv> Prc (priority th s) (last_set th s)"

    41 

    42 definition

    43   "holds wq th cs \<equiv> th \<in> set (wq cs) \<and> th = hd (wq cs)"

    44 

    45 definition

    46   "waits wq th cs \<equiv> th \<in> set (wq cs) \<and> th \<noteq> hd (wq cs)"

    47 

    48 datatype node = 

    49   Th "thread" 

    50 | Cs "cs" 

    51 

    52 definition

    53   "RAG wq \<equiv> {(Th th, Cs cs) | th cs. waits wq th cs} \<union> {(Cs cs, Th th) | cs th. holds wq th cs}"

    54 

    55 definition

    56   "dependants wq th \<equiv> {th' . (Th th', Th th) \<in> (RAG wq)^+}"

    57 

    58 record schedule_state = 

    59   wq_fun :: "cs \<Rightarrow> thread list" 

    60   cprec_fun :: "thread \<Rightarrow> precedence" 

    61 

    62 definition cpreced :: "(cs \<Rightarrow> thread list) \<Rightarrow> state \<Rightarrow> thread \<Rightarrow> precedence"

    63   where 

    64   "cpreced wq s th \<equiv> Max ({preced th s} \<union> {preced th' s | th'. th' \<in> dependants wq th})"

    65 

    66 abbreviation

    67   "all_unlocked \<equiv> \<lambda>_::cs. ([]::thread list)"

    68 

    69 abbreviation 

    70   "initial_cprec \<equiv> \<lambda>_::thread. Prc 0 0"

    71  

    72 abbreviation

    73   "release qs \<equiv> case qs of

    74              [] => [] 

    75           |  (_#qs) => (SOME q. distinct q \<and> set q = set qs)"

    76 

    77 fun schs :: "state \<Rightarrow> schedule_state"

    78   where 

    79   "schs [] = (| wq_fun = \<lambda> cs. [],  cprec_fun = (\<lambda>_. Prc 0 0) |)" 

    80 | "schs (Create th prio # s) = 

    81        (let wq = wq_fun (schs s) in

    82           (|wq_fun = wq, cprec_fun = cpreced wq (Create th prio # s)|))"

    83 |  "schs (Exit th # s) = 

    84        (let wq = wq_fun (schs s) in

    85           (|wq_fun = wq, cprec_fun = cpreced wq (Exit th # s)|))"

    86 |  "schs (Set th prio # s) = 

    87        (let wq = wq_fun (schs s) in

    88           (|wq_fun = wq, cprec_fun = cpreced wq (Set th prio # s)|))"

    89 |  "schs (P th cs # s) = 

    90        (let wq = wq_fun (schs s) in

    91         let new_wq = wq(cs := (wq cs @ [th])) in

    92           (|wq_fun = new_wq, cprec_fun = cpreced new_wq (P th cs # s)|))"

    93 |  "schs (V th cs # s) = 

    94        (let wq = wq_fun (schs s) in

    95         let new_wq = wq(cs := release (wq cs)) in

    96           (|wq_fun = new_wq, cprec_fun = cpreced new_wq (V th cs # s)|))"

    97 

    98 definition wq :: "state \<Rightarrow> cs \<Rightarrow> thread list" 

    99   where "wq s = wq_fun (schs s)"

   100 

   101 definition cp :: "state \<Rightarrow> thread \<Rightarrow> precedence"

   102   where "cp s \<equiv> cprec_fun (schs s)"

   103 

   104 definition

   105   "holds2 s \<equiv> holds (wq_fun (schs s))"

   106 

   107 definition

   108   "waits2 s \<equiv> waits (wq_fun (schs s))"

   109 

   110 definition

   111   "RAG2 s \<equiv> RAG (wq_fun (schs s))"

   112   

   113 definition

   114   "dependants2 s \<equiv> dependants (wq_fun (schs s))"

   115 

   116 definition readys :: "state \<Rightarrow> thread set"

   117   where "readys s \<equiv> {th . th \<in> threads s \<and> (\<forall> cs. \<not> waits2 s th cs)}"

   118 

   119 definition runing :: "state \<Rightarrow> thread set"

   120   where "runing s \<equiv> {th . th \<in> readys s \<and> cp s th = Max ((cp s) ` (readys s))}"

   121 

   122 definition holding :: "state \<Rightarrow> thread \<Rightarrow> cs set"

   123   where "holding s th \<equiv> {cs . holds2 s th cs}"

   124 

   125 lemma holding_RAG: 

   126   "holding s th = {cs . (Cs cs, Th th) \<in> RAG2 s}"

   127 unfolding holding_def

   128 unfolding holds2_def

   129 unfolding RAG2_def RAG_def

   130 unfolding holds_def waits_def

   131 by auto

   132 

   133 inductive step :: "state \<Rightarrow> event \<Rightarrow> bool"

   134   where

   135   step_Create: "\<lbrakk>th \<notin> threads s\<rbrakk> \<Longrightarrow> step s (Create th prio)" 

   136 | step_Exit: "\<lbrakk>th \<in> runing s; holding s th = {}\<rbrakk> \<Longrightarrow> step s (Exit th)" 

   137 | step_P: "\<lbrakk>th \<in> runing s;  (Cs cs, Th th)  \<notin> (RAG2 s)^+\<rbrakk> \<Longrightarrow> step s (P th cs)" 

   138 | step_V: "\<lbrakk>th \<in> runing s;  holds2 s th cs\<rbrakk> \<Longrightarrow> step s (V th cs)" 

   139 | step_Set: "\<lbrakk>th \<in> runing s\<rbrakk> \<Longrightarrow> step s (Set th prio)"

   140 

   141 inductive vt :: "state \<Rightarrow> bool"

   142   where

   143   vt_nil[intro]: "vt []" 

   144 | vt_cons[intro]: "\<lbrakk>vt s; step s e\<rbrakk> \<Longrightarrow> vt (e#s)"

   145 

   146 lemma runing_ready: 

   147   shows "runing s \<subseteq> readys s"

   148   unfolding runing_def readys_def

   149   by auto 

   150 

   151 lemma readys_threads:

   152   shows "readys s \<subseteq> threads s"

   153   unfolding readys_def

   154   by auto

   155 

   156 lemma wq_distinct_step: 

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

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

   159 using assms

   160 apply(induct)

   161 apply(auto simp add: wq_def Let_def)

   162 apply(auto simp add: wq_def Let_def RAG2_def RAG_def holds_def runing_def waits2_def waits_def readys_def)[1]

   163 apply(auto split: list.split)

   164 apply(rule someI2)

   165 apply(auto)

   166 done

   167 

   168 lemma wq_distinct: 

   169   assumes "vt s" 

   170   shows "distinct (wq s cs)"

   171 using assms

   172 apply(induct)

   173 apply(simp add: wq_def)

   174 apply(simp add: wq_distinct_step)

   175 done

   176 

   177 lemma RAG_set_unchanged[simp]: 

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

   179 unfolding RAG2_def

   180 by (simp add: Let_def)

   181 

   182 lemma RAG_create_unchanged[simp]: 

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

   184 unfolding RAG2_def

   185 by (simp add: Let_def)

   186 

   187 lemma RAG_exit_unchanged[simp]: 

   188   shows "RAG2 (Exit th # s) = RAG2 s"

   189 unfolding RAG2_def

   190 by (simp add: Let_def)

   191 

   192 lemma RAG_p1:

   193   assumes "wq s cs = []"

   194   shows "RAG2 (P th cs # s) = RAG2 s \<union> {(Cs cs, Th th)}"

   195   using assms

   196   apply(auto simp add: RAG2_def RAG_def wq_def Let_def waits_def holds_def)

   197   apply (metis in_set_insert insert_Nil list.distinct(1))

   198   done

   199 

   200 lemma RAG_p2:

   201   assumes "vt (P th cs#s)" "wq s cs \<noteq> []"

   202   shows "RAG2 (P th cs # s) = RAG2 s \<union> {(Th th, Cs cs)}"

   203   using assms

   204   apply(simp add: RAG2_def Let_def)

   205   apply(erule_tac vt.cases)

   206   apply(simp)

   207   apply(clarify)

   208   apply(simp)

   209   apply(erule_tac step.cases)

   210   apply(simp_all)

   211   apply(simp add: wq_def RAG_def RAG2_def)

   212   apply(simp add: waits_def holds_def)

   213   apply(auto)

   214   done

   215 

   216 definition next_th:: "state \<Rightarrow> thread \<Rightarrow> cs \<Rightarrow> thread \<Rightarrow> bool"

   217   where "next_th s th cs t = 

   218     (\<exists> rest. wq s cs = th#rest \<and> rest \<noteq> [] \<and> t = hd (SOME q. distinct q \<and> set q = set rest))"

   219 

   220 lemma RAG_v:

   221 assumes vt:"vt (V th cs#s)"

   222 shows "

   223   RAG2 (V th cs # s) =

   224   RAG2 s - {(Cs cs, Th th)} -

   225   {(Th th', Cs cs) |th'. next_th s th cs th'} \<union>

   226   {(Cs cs, Th th') |th'.  next_th s th cs th'}"

   227   apply (insert vt, unfold RAG2_def RAG_def)

   228   sorry

   229 

   230 lemma waiting_unique:

   231   assumes "vt s"

   232   and "waits2 s th cs1"

   233   and "waits2 s th cs2"

   234   shows "cs1 = cs2"

   235 sorry

   236 

   237 lemma singleton_Un:

   238   shows "A \<union> {x} = insert x A"

   239 by simp

   240 

   241 

   242 lemma acyclic_RAG_step: 

   243   assumes vt: "vt s"

   244   and     stp: "step s e"

   245   and     ac: "acyclic (RAG2 s)"

   246   shows "acyclic (RAG2 (e # s))"

   247 using stp vt ac

   248 proof (induct)

   249   case (step_P th s cs)

   250   have vt: "vt s" by fact

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

   252   have rn: "th \<in> runing s" by fact

   253   have ds: "(Cs cs, Th th) \<notin> (RAG2 s)\<^sup>+" by fact

   254   have vtt: "vt (P th cs#s)" using vt rn ds by (metis step.step_P vt_cons)

   255   { assume a: "wq s cs = []" -- "case waiting queue is empty"

   256     have "(Th th, Cs cs) \<notin> (RAG2 s)\<^sup>*"  

   257     proof

   258       assume "(Th th, Cs cs) \<in> (RAG2 s)\<^sup>*"

   259       then have "(Th th, Cs cs) \<in> (RAG2 s)\<^sup>+" by (simp add: rtrancl_eq_or_trancl)

   260       then obtain x where "(x, Cs cs) \<in> RAG2 s" using tranclD2 by metis 

   261       with a show False by (auto simp: RAG2_def RAG_def wq_def waits_def)

   262     qed

   263     with acyclic_insert ac

   264     have "acyclic (RAG2 s \<union> {(Cs cs, Th th)})" by simp

   265     then have "acyclic (RAG2 (P th cs # s))" using RAG_p1[OF a] by simp

   266   }

   267   moreover

   268   { assume a: "wq s cs \<noteq> []" -- "case waiting queue is not empty"

   269     from ds have "(Cs cs, Th th) \<notin> (RAG2 s)\<^sup>*" by (metis node.distinct(1) rtranclD)

   270     with acyclic_insert ac 

   271     have "acyclic (RAG2 s \<union> {(Th th, Cs cs)})" by auto

   272     then have "acyclic (RAG2 (P th cs # s))" using RAG_p2[OF vtt a] by simp

   273   }

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

   275 next    

   276   case (step_V th s cs) 

   277   have vt: "vt s" by fact

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

   279   have rn: "th \<in> runing s" by fact

   280   have hd: "holds2 s th cs" by fact

   281   from hd 

   282   have th_in: "th \<in> set (wq s cs)" and

   283        eq_hd: "th = hd (wq s cs)" unfolding holds2_def holds_def wq_def by auto

   284   then obtain rest where

   285     eq_wq: "wq s cs = th # rest" by (cases "wq s cs") (auto)

   286   show ?case

   287     apply(subst RAG_v)

   288     apply(rule vt_cons)

   289     apply(rule vt)

   290     apply(rule step.step_V)

   291     apply(rule rn)

   292     apply(rule hd)

   293     using eq_wq

   294     apply(cases "rest = []")

   295     apply(subgoal_tac "{(Cs cs, Th th') |th'. next_th s th cs th'} = {}")

   296     apply(simp)

   297     apply(rule acyclic_subset)

   298     apply(rule ac)

   299     apply(auto)[1]

   300     apply(auto simp add: next_th_def)[1]

   301     -- "case wq more than a singleton"

   302     apply(subgoal_tac "{(Cs cs, Th (hd (SOME q. distinct q \<and> set q = set rest)))} = 

   303       {(Cs cs, Th th') |th'. next_th s th cs th'}")

   304     apply(rotate_tac 2)

   305     apply(drule sym)

   306     apply(simp only: singleton_Un)

   307     apply(simp only: acyclic_insert)

   308     apply(rule conjI)

   309     apply(rule acyclic_subset)

   310     apply(rule ac)

   311     apply(auto)[1]

   312     apply(rotate_tac 2)

   313     apply(thin_tac "?X")

   314     defer 

   315     apply(simp add: next_th_def)

   316     apply(clarify)

   317     apply(simp add: rtrancl_eq_or_trancl)

   318     apply(drule tranclD)

   319     apply(erule exE)

   320     apply(drule conjunct1)

   321     apply(subgoal_tac "(Th (hd (SOME q. distinct q \<and> set q = set rest)), z) \<in> RAG2 s")

   322     prefer 2

   323     apply(simp)

   324     apply(case_tac z)

   325     apply(simp add: RAG2_def RAG_def)

   326     apply(clarify)

   327     apply(simp)

   328     apply(simp add: next_th_def)

   329     apply(rule waiting_unique)

   330     apply(rule vt)

   331     apply(simp add: RAG2_def RAG_def waits2_def waits_def wq_def)

   332     apply(rotate_tac 2)

   333     apply(thin_tac "?X")

   334     apply(subgoal_tac "distinct (wq s cs)")

   335     prefer 2

   336     apply(rule wq_distinct)

   337     apply(rule vt)

   338     apply (unfold waits2_def waits_def wq_def, auto)

   339     apply(subgoal_tac "(SOME q. distinct q \<and> set q = set rest) \<noteq> []")

   340     prefer 2

   341     apply (metis (mono_tags) set_empty tfl_some)

   342     apply(subgoal_tac "hd (SOME q. distinct q \<and> set q = set rest) \<in> 

   343                 set (SOME q. distinct q \<and> set q = set rest)") 

   344     prefer 2

   345     apply(auto)[1]

   346     apply(subgoal_tac "set (SOME q. distinct q \<and> set q = set rest) = set rest") 

   347     prefer 2

   348     apply(rule someI2)

   349     apply(auto)[2]

   350     apply(auto)[1]

   351     apply(subgoal_tac "(SOME q. distinct q \<and> set q = set rest) \<noteq> []")

   352     prefer 2

   353     apply (metis (mono_tags) set_empty tfl_some)

   354     apply(subgoal_tac "hd (SOME q. distinct q \<and> set q = set rest) \<in> 

   355                 set (SOME q. distinct q \<and> set q = set rest)") 

   356     prefer 2

   357     apply(auto)[1]

   358     apply(subgoal_tac "set (SOME q. distinct q \<and> set q = set rest) = set rest") 

   359     prefer 2

   360     apply(rule someI2)

   361     apply(auto)[2]

   362     apply(auto)[1]

   363     done

   364 qed (simp_all)

   365 

   366 

   367 

   368 

   369 

   370