src/HOL/Hoare_Parallel/Gar_Coll.thy
 author wenzelm Thu May 24 17:25:53 2012 +0200 (2012-05-24) changeset 47988 e4b69e10b990 parent 45827 66c68453455c child 51717 9e7d1c139569 permissions -rw-r--r--
tuned proofs;
     1 header {* \section{The Single Mutator Case} *}

     2

     3 theory Gar_Coll imports Graph OG_Syntax begin

     4

     5 declare psubsetE [rule del]

     6

     7 text {* Declaration of variables: *}

     8

     9 record gar_coll_state =

    10   M :: nodes

    11   E :: edges

    12   bc :: "nat set"

    13   obc :: "nat set"

    14   Ma :: nodes

    15   ind :: nat

    16   k :: nat

    17   z :: bool

    18

    19 subsection {* The Mutator *}

    20

    21 text {* The mutator first redirects an arbitrary edge @{text "R"} from

    22 an arbitrary accessible node towards an arbitrary accessible node

    23 @{text "T"}.  It then colors the new target @{text "T"} black.

    24

    25 We declare the arbitrarily selected node and edge as constants:*}

    26

    27 consts R :: nat  T :: nat

    28

    29 text {* \noindent The following predicate states, given a list of

    30 nodes @{text "m"} and a list of edges @{text "e"}, the conditions

    31 under which the selected edge @{text "R"} and node @{text "T"} are

    32 valid: *}

    33

    34 definition Mut_init :: "gar_coll_state \<Rightarrow> bool" where

    35   "Mut_init \<equiv> \<guillemotleft> T \<in> Reach \<acute>E \<and> R < length \<acute>E \<and> T < length \<acute>M \<guillemotright>"

    36

    37 text {* \noindent For the mutator we

    38 consider two modules, one for each action.  An auxiliary variable

    39 @{text "\<acute>z"} is set to false if the mutator has already redirected an

    40 edge but has not yet colored the new target.   *}

    41

    42 definition Redirect_Edge :: "gar_coll_state ann_com" where

    43   "Redirect_Edge \<equiv> .{\<acute>Mut_init \<and> \<acute>z}. \<langle>\<acute>E:=\<acute>E[R:=(fst(\<acute>E!R), T)],, \<acute>z:= (\<not>\<acute>z)\<rangle>"

    44

    45 definition Color_Target :: "gar_coll_state ann_com" where

    46   "Color_Target \<equiv> .{\<acute>Mut_init \<and> \<not>\<acute>z}. \<langle>\<acute>M:=\<acute>M[T:=Black],, \<acute>z:= (\<not>\<acute>z)\<rangle>"

    47

    48 definition Mutator :: "gar_coll_state ann_com" where

    49   "Mutator \<equiv>

    50   .{\<acute>Mut_init \<and> \<acute>z}.

    51   WHILE True INV .{\<acute>Mut_init \<and> \<acute>z}.

    52   DO  Redirect_Edge ;; Color_Target  OD"

    53

    54 subsubsection {* Correctness of the mutator *}

    55

    56 lemmas mutator_defs = Mut_init_def Redirect_Edge_def Color_Target_def

    57

    58 lemma Redirect_Edge:

    59   "\<turnstile> Redirect_Edge pre(Color_Target)"

    60 apply (unfold mutator_defs)

    61 apply annhoare

    62 apply(simp_all)

    63 apply(force elim:Graph2)

    64 done

    65

    66 lemma Color_Target:

    67   "\<turnstile> Color_Target .{\<acute>Mut_init \<and> \<acute>z}."

    68 apply (unfold mutator_defs)

    69 apply annhoare

    70 apply(simp_all)

    71 done

    72

    73 lemma Mutator:

    74  "\<turnstile> Mutator .{False}."

    75 apply(unfold Mutator_def)

    76 apply annhoare

    77 apply(simp_all add:Redirect_Edge Color_Target)

    78 apply(simp add:mutator_defs Redirect_Edge_def)

    79 done

    80

    81 subsection {* The Collector *}

    82

    83 text {* \noindent A constant @{text "M_init"} is used to give @{text "\<acute>Ma"} a

    84 suitable first value, defined as a list of nodes where only the @{text

    85 "Roots"} are black. *}

    86

    87 consts  M_init :: nodes

    88

    89 definition Proper_M_init :: "gar_coll_state \<Rightarrow> bool" where

    90   "Proper_M_init \<equiv>  \<guillemotleft> Blacks M_init=Roots \<and> length M_init=length \<acute>M \<guillemotright>"

    91

    92 definition Proper :: "gar_coll_state \<Rightarrow> bool" where

    93   "Proper \<equiv> \<guillemotleft> Proper_Roots \<acute>M \<and> Proper_Edges(\<acute>M, \<acute>E) \<and> \<acute>Proper_M_init \<guillemotright>"

    94

    95 definition Safe :: "gar_coll_state \<Rightarrow> bool" where

    96   "Safe \<equiv> \<guillemotleft> Reach \<acute>E \<subseteq> Blacks \<acute>M \<guillemotright>"

    97

    98 lemmas collector_defs = Proper_M_init_def Proper_def Safe_def

    99

   100 subsubsection {* Blackening the roots *}

   101

   102 definition Blacken_Roots :: " gar_coll_state ann_com" where

   103   "Blacken_Roots \<equiv>

   104   .{\<acute>Proper}.

   105   \<acute>ind:=0;;

   106   .{\<acute>Proper \<and> \<acute>ind=0}.

   107   WHILE \<acute>ind<length \<acute>M

   108    INV .{\<acute>Proper \<and> (\<forall>i<\<acute>ind. i \<in> Roots \<longrightarrow> \<acute>M!i=Black) \<and> \<acute>ind\<le>length \<acute>M}.

   109   DO .{\<acute>Proper \<and> (\<forall>i<\<acute>ind. i \<in> Roots \<longrightarrow> \<acute>M!i=Black) \<and> \<acute>ind<length \<acute>M}.

   110    IF \<acute>ind\<in>Roots THEN

   111    .{\<acute>Proper \<and> (\<forall>i<\<acute>ind. i \<in> Roots \<longrightarrow> \<acute>M!i=Black) \<and> \<acute>ind<length \<acute>M \<and> \<acute>ind\<in>Roots}.

   112     \<acute>M:=\<acute>M[\<acute>ind:=Black] FI;;

   113    .{\<acute>Proper \<and> (\<forall>i<\<acute>ind+1. i \<in> Roots \<longrightarrow> \<acute>M!i=Black) \<and> \<acute>ind<length \<acute>M}.

   114     \<acute>ind:=\<acute>ind+1

   115   OD"

   116

   117 lemma Blacken_Roots:

   118  "\<turnstile> Blacken_Roots .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M}."

   119 apply (unfold Blacken_Roots_def)

   120 apply annhoare

   121 apply(simp_all add:collector_defs Graph_defs)

   122 apply safe

   123 apply(simp_all add:nth_list_update)

   124   apply (erule less_SucE)

   125    apply simp+

   126  apply force

   127 apply force

   128 done

   129

   130 subsubsection {* Propagating black *}

   131

   132 definition PBInv :: "gar_coll_state \<Rightarrow> nat \<Rightarrow> bool" where

   133   "PBInv \<equiv> \<guillemotleft> \<lambda>ind. \<acute>obc < Blacks \<acute>M \<or> (\<forall>i <ind. \<not>BtoW (\<acute>E!i, \<acute>M) \<or>

   134    (\<not>\<acute>z \<and> i=R \<and> (snd(\<acute>E!R)) = T \<and> (\<exists>r. ind \<le> r \<and> r < length \<acute>E \<and> BtoW(\<acute>E!r,\<acute>M))))\<guillemotright>"

   135

   136 definition Propagate_Black_aux :: "gar_coll_state ann_com" where

   137   "Propagate_Black_aux \<equiv>

   138   .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M}.

   139   \<acute>ind:=0;;

   140   .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M \<and> \<acute>ind=0}.

   141   WHILE \<acute>ind<length \<acute>E

   142    INV .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M

   143          \<and> \<acute>PBInv \<acute>ind \<and> \<acute>ind\<le>length \<acute>E}.

   144   DO .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M

   145        \<and> \<acute>PBInv \<acute>ind \<and> \<acute>ind<length \<acute>E}.

   146    IF \<acute>M!(fst (\<acute>E!\<acute>ind)) = Black THEN

   147     .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M

   148        \<and> \<acute>PBInv \<acute>ind \<and> \<acute>ind<length \<acute>E \<and> \<acute>M!fst(\<acute>E!\<acute>ind)=Black}.

   149      \<acute>M:=\<acute>M[snd(\<acute>E!\<acute>ind):=Black];;

   150     .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M

   151        \<and> \<acute>PBInv (\<acute>ind + 1) \<and> \<acute>ind<length \<acute>E}.

   152      \<acute>ind:=\<acute>ind+1

   153    FI

   154   OD"

   155

   156 lemma Propagate_Black_aux:

   157   "\<turnstile>  Propagate_Black_aux

   158   .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M

   159     \<and> ( \<acute>obc < Blacks \<acute>M \<or> \<acute>Safe)}."

   160 apply (unfold Propagate_Black_aux_def  PBInv_def collector_defs)

   161 apply annhoare

   162 apply(simp_all add:Graph6 Graph7 Graph8 Graph12)

   163       apply force

   164      apply force

   165     apply force

   166 --{* 4 subgoals left *}

   167 apply clarify

   168 apply(simp add:Proper_Edges_def Proper_Roots_def Graph6 Graph7 Graph8 Graph12)

   169 apply (erule disjE)

   170  apply(rule disjI1)

   171  apply(erule Graph13)

   172  apply force

   173 apply (case_tac "M x ! snd (E x ! ind x)=Black")

   174  apply (simp add: Graph10 BtoW_def)

   175  apply (rule disjI2)

   176  apply clarify

   177  apply (erule less_SucE)

   178   apply (erule_tac x=i in allE , erule (1) notE impE)

   179   apply simp

   180   apply clarify

   181   apply (drule_tac y = r in le_imp_less_or_eq)

   182   apply (erule disjE)

   183    apply (subgoal_tac "Suc (ind x)\<le>r")

   184     apply fast

   185    apply arith

   186   apply fast

   187  apply fast

   188 apply(rule disjI1)

   189 apply(erule subset_psubset_trans)

   190 apply(erule Graph11)

   191 apply fast

   192 --{* 3 subgoals left *}

   193 apply force

   194 apply force

   195 --{* last *}

   196 apply clarify

   197 apply simp

   198 apply(subgoal_tac "ind x = length (E x)")

   199  apply (simp)

   200  apply(drule Graph1)

   201    apply simp

   202   apply clarify

   203   apply(erule allE, erule impE, assumption)

   204   apply force

   205  apply force

   206 apply arith

   207 done

   208

   209 subsubsection {* Refining propagating black *}

   210

   211 definition Auxk :: "gar_coll_state \<Rightarrow> bool" where

   212   "Auxk \<equiv> \<guillemotleft>\<acute>k<length \<acute>M \<and> (\<acute>M!\<acute>k\<noteq>Black \<or> \<not>BtoW(\<acute>E!\<acute>ind, \<acute>M) \<or>

   213           \<acute>obc<Blacks \<acute>M \<or> (\<not>\<acute>z \<and> \<acute>ind=R \<and> snd(\<acute>E!R)=T

   214           \<and> (\<exists>r. \<acute>ind<r \<and> r<length \<acute>E \<and> BtoW(\<acute>E!r, \<acute>M))))\<guillemotright>"

   215

   216 definition Propagate_Black :: " gar_coll_state ann_com" where

   217   "Propagate_Black \<equiv>

   218   .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M}.

   219   \<acute>ind:=0;;

   220   .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M \<and> \<acute>ind=0}.

   221   WHILE \<acute>ind<length \<acute>E

   222    INV .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M

   223          \<and> \<acute>PBInv \<acute>ind \<and> \<acute>ind\<le>length \<acute>E}.

   224   DO .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M

   225        \<and> \<acute>PBInv \<acute>ind \<and> \<acute>ind<length \<acute>E}.

   226    IF (\<acute>M!(fst (\<acute>E!\<acute>ind)))=Black THEN

   227     .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M

   228       \<and> \<acute>PBInv \<acute>ind \<and> \<acute>ind<length \<acute>E \<and> (\<acute>M!fst(\<acute>E!\<acute>ind))=Black}.

   229      \<acute>k:=(snd(\<acute>E!\<acute>ind));;

   230     .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M

   231       \<and> \<acute>PBInv \<acute>ind \<and> \<acute>ind<length \<acute>E \<and> (\<acute>M!fst(\<acute>E!\<acute>ind))=Black

   232       \<and> \<acute>Auxk}.

   233      \<langle>\<acute>M:=\<acute>M[\<acute>k:=Black],, \<acute>ind:=\<acute>ind+1\<rangle>

   234    ELSE .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M

   235           \<and> \<acute>PBInv \<acute>ind \<and> \<acute>ind<length \<acute>E}.

   236          \<langle>IF (\<acute>M!(fst (\<acute>E!\<acute>ind)))\<noteq>Black THEN \<acute>ind:=\<acute>ind+1 FI\<rangle>

   237    FI

   238   OD"

   239

   240 lemma Propagate_Black:

   241   "\<turnstile>  Propagate_Black

   242   .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M

   243     \<and> ( \<acute>obc < Blacks \<acute>M \<or> \<acute>Safe)}."

   244 apply (unfold Propagate_Black_def  PBInv_def Auxk_def collector_defs)

   245 apply annhoare

   246 apply(simp_all add: Graph6 Graph7 Graph8 Graph12)

   247        apply force

   248       apply force

   249      apply force

   250 --{* 5 subgoals left *}

   251 apply clarify

   252 apply(simp add:BtoW_def Proper_Edges_def)

   253 --{* 4 subgoals left *}

   254 apply clarify

   255 apply(simp add:Proper_Edges_def Graph6 Graph7 Graph8 Graph12)

   256 apply (erule disjE)

   257  apply (rule disjI1)

   258  apply (erule psubset_subset_trans)

   259  apply (erule Graph9)

   260 apply (case_tac "M x!k x=Black")

   261  apply (case_tac "M x ! snd (E x ! ind x)=Black")

   262   apply (simp add: Graph10 BtoW_def)

   263   apply (rule disjI2)

   264   apply clarify

   265   apply (erule less_SucE)

   266    apply (erule_tac x=i in allE , erule (1) notE impE)

   267    apply simp

   268    apply clarify

   269    apply (drule_tac y = r in le_imp_less_or_eq)

   270    apply (erule disjE)

   271     apply (subgoal_tac "Suc (ind x)\<le>r")

   272      apply fast

   273     apply arith

   274    apply fast

   275   apply fast

   276  apply (simp add: Graph10 BtoW_def)

   277  apply (erule disjE)

   278   apply (erule disjI1)

   279  apply clarify

   280  apply (erule less_SucE)

   281   apply force

   282  apply simp

   283  apply (subgoal_tac "Suc R\<le>r")

   284   apply fast

   285  apply arith

   286 apply(rule disjI1)

   287 apply(erule subset_psubset_trans)

   288 apply(erule Graph11)

   289 apply fast

   290 --{* 2 subgoals left *}

   291 apply clarify

   292 apply(simp add:Proper_Edges_def Graph6 Graph7 Graph8 Graph12)

   293 apply (erule disjE)

   294  apply fast

   295 apply clarify

   296 apply (erule less_SucE)

   297  apply (erule_tac x=i in allE , erule (1) notE impE)

   298  apply simp

   299  apply clarify

   300  apply (drule_tac y = r in le_imp_less_or_eq)

   301  apply (erule disjE)

   302   apply (subgoal_tac "Suc (ind x)\<le>r")

   303    apply fast

   304   apply arith

   305  apply (simp add: BtoW_def)

   306 apply (simp add: BtoW_def)

   307 --{* last *}

   308 apply clarify

   309 apply simp

   310 apply(subgoal_tac "ind x = length (E x)")

   311  apply (simp)

   312  apply(drule Graph1)

   313    apply simp

   314   apply clarify

   315   apply(erule allE, erule impE, assumption)

   316   apply force

   317  apply force

   318 apply arith

   319 done

   320

   321 subsubsection {* Counting black nodes *}

   322

   323 definition CountInv :: "gar_coll_state \<Rightarrow> nat \<Rightarrow> bool" where

   324   "CountInv \<equiv> \<guillemotleft> \<lambda>ind. {i. i<ind \<and> \<acute>Ma!i=Black}\<subseteq>\<acute>bc \<guillemotright>"

   325

   326 definition Count :: " gar_coll_state ann_com" where

   327   "Count \<equiv>

   328   .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M

   329     \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M

   330     \<and> length \<acute>Ma=length \<acute>M \<and> (\<acute>obc < Blacks \<acute>Ma \<or> \<acute>Safe) \<and> \<acute>bc={}}.

   331   \<acute>ind:=0;;

   332   .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M

   333     \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M

   334    \<and> length \<acute>Ma=length \<acute>M \<and> (\<acute>obc < Blacks \<acute>Ma \<or> \<acute>Safe) \<and> \<acute>bc={}

   335    \<and> \<acute>ind=0}.

   336    WHILE \<acute>ind<length \<acute>M

   337      INV .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M

   338            \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M

   339            \<and> length \<acute>Ma=length \<acute>M \<and> \<acute>CountInv \<acute>ind

   340            \<and> ( \<acute>obc < Blacks \<acute>Ma \<or> \<acute>Safe) \<and> \<acute>ind\<le>length \<acute>M}.

   341    DO .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M

   342          \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M

   343          \<and> length \<acute>Ma=length \<acute>M \<and> \<acute>CountInv \<acute>ind

   344          \<and> ( \<acute>obc < Blacks \<acute>Ma \<or> \<acute>Safe) \<and> \<acute>ind<length \<acute>M}.

   345        IF \<acute>M!\<acute>ind=Black

   346           THEN .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M

   347                  \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M

   348                  \<and> length \<acute>Ma=length \<acute>M \<and> \<acute>CountInv \<acute>ind

   349                  \<and> ( \<acute>obc < Blacks \<acute>Ma \<or> \<acute>Safe) \<and> \<acute>ind<length \<acute>M \<and> \<acute>M!\<acute>ind=Black}.

   350           \<acute>bc:=insert \<acute>ind \<acute>bc

   351        FI;;

   352       .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M

   353         \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M

   354         \<and> length \<acute>Ma=length \<acute>M \<and> \<acute>CountInv (\<acute>ind+1)

   355         \<and> ( \<acute>obc < Blacks \<acute>Ma \<or> \<acute>Safe) \<and> \<acute>ind<length \<acute>M}.

   356       \<acute>ind:=\<acute>ind+1

   357    OD"

   358

   359 lemma Count:

   360   "\<turnstile> Count

   361   .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M

   362    \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>\<acute>bc \<and> \<acute>bc\<subseteq>Blacks \<acute>M \<and> length \<acute>Ma=length \<acute>M

   363    \<and> (\<acute>obc < Blacks \<acute>Ma \<or> \<acute>Safe)}."

   364 apply(unfold Count_def)

   365 apply annhoare

   366 apply(simp_all add:CountInv_def Graph6 Graph7 Graph8 Graph12 Blacks_def collector_defs)

   367       apply force

   368      apply force

   369     apply force

   370    apply clarify

   371    apply simp

   372    apply(fast elim:less_SucE)

   373   apply clarify

   374   apply simp

   375   apply(fast elim:less_SucE)

   376  apply force

   377 apply force

   378 done

   379

   380 subsubsection {* Appending garbage nodes to the free list *}

   381

   382 axiomatization Append_to_free :: "nat \<times> edges \<Rightarrow> edges"

   383 where

   384   Append_to_free0: "length (Append_to_free (i, e)) = length e" and

   385   Append_to_free1: "Proper_Edges (m, e)

   386                    \<Longrightarrow> Proper_Edges (m, Append_to_free(i, e))" and

   387   Append_to_free2: "i \<notin> Reach e

   388      \<Longrightarrow> n \<in> Reach (Append_to_free(i, e)) = ( n = i \<or> n \<in> Reach e)"

   389

   390 definition AppendInv :: "gar_coll_state \<Rightarrow> nat \<Rightarrow> bool" where

   391   "AppendInv \<equiv> \<guillemotleft>\<lambda>ind. \<forall>i<length \<acute>M. ind\<le>i \<longrightarrow> i\<in>Reach \<acute>E \<longrightarrow> \<acute>M!i=Black\<guillemotright>"

   392

   393 definition Append :: "gar_coll_state ann_com" where

   394    "Append \<equiv>

   395   .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>Safe}.

   396   \<acute>ind:=0;;

   397   .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>Safe \<and> \<acute>ind=0}.

   398     WHILE \<acute>ind<length \<acute>M

   399       INV .{\<acute>Proper \<and> \<acute>AppendInv \<acute>ind \<and> \<acute>ind\<le>length \<acute>M}.

   400     DO .{\<acute>Proper \<and> \<acute>AppendInv \<acute>ind \<and> \<acute>ind<length \<acute>M}.

   401        IF \<acute>M!\<acute>ind=Black THEN

   402           .{\<acute>Proper \<and> \<acute>AppendInv \<acute>ind \<and> \<acute>ind<length \<acute>M \<and> \<acute>M!\<acute>ind=Black}.

   403           \<acute>M:=\<acute>M[\<acute>ind:=White]

   404        ELSE .{\<acute>Proper \<and> \<acute>AppendInv \<acute>ind \<and> \<acute>ind<length \<acute>M \<and> \<acute>ind\<notin>Reach \<acute>E}.

   405               \<acute>E:=Append_to_free(\<acute>ind,\<acute>E)

   406        FI;;

   407      .{\<acute>Proper \<and> \<acute>AppendInv (\<acute>ind+1) \<and> \<acute>ind<length \<acute>M}.

   408        \<acute>ind:=\<acute>ind+1

   409     OD"

   410

   411 lemma Append:

   412   "\<turnstile> Append .{\<acute>Proper}."

   413 apply(unfold Append_def AppendInv_def)

   414 apply annhoare

   415 apply(simp_all add:collector_defs Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)

   416        apply(force simp:Blacks_def nth_list_update)

   417       apply force

   418      apply force

   419     apply(force simp add:Graph_defs)

   420    apply force

   421   apply clarify

   422   apply simp

   423   apply(rule conjI)

   424    apply (erule Append_to_free1)

   425   apply clarify

   426   apply (drule_tac n = "i" in Append_to_free2)

   427   apply force

   428  apply force

   429 apply force

   430 done

   431

   432 subsubsection {* Correctness of the Collector *}

   433

   434 definition Collector :: " gar_coll_state ann_com" where

   435   "Collector \<equiv>

   436 .{\<acute>Proper}.

   437  WHILE True INV .{\<acute>Proper}.

   438  DO

   439   Blacken_Roots;;

   440   .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M}.

   441    \<acute>obc:={};;

   442   .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc={}}.

   443    \<acute>bc:=Roots;;

   444   .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc={} \<and> \<acute>bc=Roots}.

   445    \<acute>Ma:=M_init;;

   446   .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc={} \<and> \<acute>bc=Roots \<and> \<acute>Ma=M_init}.

   447    WHILE \<acute>obc\<noteq>\<acute>bc

   448      INV .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M

   449            \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>\<acute>bc \<and> \<acute>bc\<subseteq>Blacks \<acute>M

   450            \<and> length \<acute>Ma=length \<acute>M \<and> (\<acute>obc < Blacks \<acute>Ma \<or> \<acute>Safe)}.

   451    DO .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M}.

   452        \<acute>obc:=\<acute>bc;;

   453        Propagate_Black;;

   454       .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M

   455         \<and> (\<acute>obc < Blacks \<acute>M \<or> \<acute>Safe)}.

   456        \<acute>Ma:=\<acute>M;;

   457       .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma

   458         \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M \<and> length \<acute>Ma=length \<acute>M

   459         \<and> ( \<acute>obc < Blacks \<acute>Ma \<or> \<acute>Safe)}.

   460        \<acute>bc:={};;

   461        Count

   462    OD;;

   463   Append

   464  OD"

   465

   466 lemma Collector:

   467   "\<turnstile> Collector .{False}."

   468 apply(unfold Collector_def)

   469 apply annhoare

   470 apply(simp_all add: Blacken_Roots Propagate_Black Count Append)

   471 apply(simp_all add:Blacken_Roots_def Propagate_Black_def Count_def Append_def collector_defs)

   472    apply (force simp add: Proper_Roots_def)

   473   apply force

   474  apply force

   475 apply clarify

   476 apply (erule disjE)

   477 apply(simp add:psubsetI)

   478  apply(force dest:subset_antisym)

   479 done

   480

   481 subsection {* Interference Freedom *}

   482

   483 lemmas modules = Redirect_Edge_def Color_Target_def Blacken_Roots_def

   484                  Propagate_Black_def Count_def Append_def

   485 lemmas Invariants = PBInv_def Auxk_def CountInv_def AppendInv_def

   486 lemmas abbrev = collector_defs mutator_defs Invariants

   487

   488 lemma interfree_Blacken_Roots_Redirect_Edge:

   489  "interfree_aux (Some Blacken_Roots, {}, Some Redirect_Edge)"

   490 apply (unfold modules)

   491 apply interfree_aux

   492 apply safe

   493 apply (simp_all add:Graph6 Graph12 abbrev)

   494 done

   495

   496 lemma interfree_Redirect_Edge_Blacken_Roots:

   497   "interfree_aux (Some Redirect_Edge, {}, Some Blacken_Roots)"

   498 apply (unfold modules)

   499 apply interfree_aux

   500 apply safe

   501 apply(simp add:abbrev)+

   502 done

   503

   504 lemma interfree_Blacken_Roots_Color_Target:

   505   "interfree_aux (Some Blacken_Roots, {}, Some Color_Target)"

   506 apply (unfold modules)

   507 apply interfree_aux

   508 apply safe

   509 apply(simp_all add:Graph7 Graph8 nth_list_update abbrev)

   510 done

   511

   512 lemma interfree_Color_Target_Blacken_Roots:

   513   "interfree_aux (Some Color_Target, {}, Some Blacken_Roots)"

   514 apply (unfold modules )

   515 apply interfree_aux

   516 apply safe

   517 apply(simp add:abbrev)+

   518 done

   519

   520 lemma interfree_Propagate_Black_Redirect_Edge:

   521   "interfree_aux (Some Propagate_Black, {}, Some Redirect_Edge)"

   522 apply (unfold modules )

   523 apply interfree_aux

   524 --{* 11 subgoals left *}

   525 apply(clarify, simp add:abbrev Graph6 Graph12)

   526 apply(clarify, simp add:abbrev Graph6 Graph12)

   527 apply(clarify, simp add:abbrev Graph6 Graph12)

   528 apply(clarify, simp add:abbrev Graph6 Graph12)

   529 apply(erule conjE)+

   530 apply(erule disjE, erule disjI1, rule disjI2, rule allI, (rule impI)+, case_tac "R=i", rule conjI, erule sym)

   531  apply(erule Graph4)

   532    apply(simp)+

   533   apply (simp add:BtoW_def)

   534  apply (simp add:BtoW_def)

   535 apply(rule conjI)

   536  apply (force simp add:BtoW_def)

   537 apply(erule Graph4)

   538    apply simp+

   539 --{* 7 subgoals left *}

   540 apply(clarify, simp add:abbrev Graph6 Graph12)

   541 apply(erule conjE)+

   542 apply(erule disjE, erule disjI1, rule disjI2, rule allI, (rule impI)+, case_tac "R=i", rule conjI, erule sym)

   543  apply(erule Graph4)

   544    apply(simp)+

   545   apply (simp add:BtoW_def)

   546  apply (simp add:BtoW_def)

   547 apply(rule conjI)

   548  apply (force simp add:BtoW_def)

   549 apply(erule Graph4)

   550    apply simp+

   551 --{* 6 subgoals left *}

   552 apply(clarify, simp add:abbrev Graph6 Graph12)

   553 apply(erule conjE)+

   554 apply(rule conjI)

   555  apply(erule disjE, erule disjI1, rule disjI2, rule allI, (rule impI)+, case_tac "R=i", rule conjI, erule sym)

   556   apply(erule Graph4)

   557     apply(simp)+

   558    apply (simp add:BtoW_def)

   559   apply (simp add:BtoW_def)

   560  apply(rule conjI)

   561   apply (force simp add:BtoW_def)

   562  apply(erule Graph4)

   563     apply simp+

   564 apply(simp add:BtoW_def nth_list_update)

   565 apply force

   566 --{* 5 subgoals left *}

   567 apply(clarify, simp add:abbrev Graph6 Graph12)

   568 --{* 4 subgoals left *}

   569 apply(clarify, simp add:abbrev Graph6 Graph12)

   570 apply(rule conjI)

   571  apply(erule disjE, erule disjI1, rule disjI2, rule allI, (rule impI)+, case_tac "R=i", rule conjI, erule sym)

   572   apply(erule Graph4)

   573     apply(simp)+

   574    apply (simp add:BtoW_def)

   575   apply (simp add:BtoW_def)

   576  apply(rule conjI)

   577   apply (force simp add:BtoW_def)

   578  apply(erule Graph4)

   579     apply simp+

   580 apply(rule conjI)

   581  apply(simp add:nth_list_update)

   582  apply force

   583 apply(rule impI, rule impI, erule disjE, erule disjI1, case_tac "R = (ind x)" ,case_tac "M x ! T = Black")

   584   apply(force simp add:BtoW_def)

   585  apply(case_tac "M x !snd (E x ! ind x)=Black")

   586   apply(rule disjI2)

   587   apply simp

   588   apply (erule Graph5)

   589   apply simp+

   590  apply(force simp add:BtoW_def)

   591 apply(force simp add:BtoW_def)

   592 --{* 3 subgoals left *}

   593 apply(clarify, simp add:abbrev Graph6 Graph12)

   594 --{* 2 subgoals left *}

   595 apply(clarify, simp add:abbrev Graph6 Graph12)

   596 apply(erule disjE, erule disjI1, rule disjI2, rule allI, (rule impI)+, case_tac "R=i", rule conjI, erule sym)

   597  apply clarify

   598  apply(erule Graph4)

   599    apply(simp)+

   600   apply (simp add:BtoW_def)

   601  apply (simp add:BtoW_def)

   602 apply(rule conjI)

   603  apply (force simp add:BtoW_def)

   604 apply(erule Graph4)

   605    apply simp+

   606 done

   607

   608 lemma interfree_Redirect_Edge_Propagate_Black:

   609   "interfree_aux (Some Redirect_Edge, {}, Some Propagate_Black)"

   610 apply (unfold modules )

   611 apply interfree_aux

   612 apply(clarify, simp add:abbrev)+

   613 done

   614

   615 lemma interfree_Propagate_Black_Color_Target:

   616   "interfree_aux (Some Propagate_Black, {}, Some Color_Target)"

   617 apply (unfold modules )

   618 apply interfree_aux

   619 --{* 11 subgoals left *}

   620 apply(clarify, simp add:abbrev Graph7 Graph8 Graph12)+

   621 apply(erule conjE)+

   622 apply(erule disjE,rule disjI1,erule psubset_subset_trans,erule Graph9,

   623       case_tac "M x!T=Black", rule disjI2,rotate_tac -1, simp add: Graph10, clarify,

   624       erule allE, erule impE, assumption, erule impE, assumption,

   625       simp add:BtoW_def, rule disjI1, erule subset_psubset_trans, erule Graph11, force)

   626 --{* 7 subgoals left *}

   627 apply(clarify, simp add:abbrev Graph7 Graph8 Graph12)

   628 apply(erule conjE)+

   629 apply(erule disjE,rule disjI1,erule psubset_subset_trans,erule Graph9,

   630       case_tac "M x!T=Black", rule disjI2,rotate_tac -1, simp add: Graph10, clarify,

   631       erule allE, erule impE, assumption, erule impE, assumption,

   632       simp add:BtoW_def, rule disjI1, erule subset_psubset_trans, erule Graph11, force)

   633 --{* 6 subgoals left *}

   634 apply(clarify, simp add:abbrev Graph7 Graph8 Graph12)

   635 apply clarify

   636 apply (rule conjI)

   637  apply(erule disjE,rule disjI1,erule psubset_subset_trans,erule Graph9,

   638       case_tac "M x!T=Black", rule disjI2,rotate_tac -1, simp add: Graph10, clarify,

   639       erule allE, erule impE, assumption, erule impE, assumption,

   640       simp add:BtoW_def, rule disjI1, erule subset_psubset_trans, erule Graph11, force)

   641 apply(simp add:nth_list_update)

   642 --{* 5 subgoals left *}

   643 apply(clarify, simp add:abbrev Graph7 Graph8 Graph12)

   644 --{* 4 subgoals left *}

   645 apply(clarify, simp add:abbrev Graph7 Graph8 Graph12)

   646 apply (rule conjI)

   647  apply(erule disjE,rule disjI1,erule psubset_subset_trans,erule Graph9,

   648       case_tac "M x!T=Black", rule disjI2,rotate_tac -1, simp add: Graph10, clarify,

   649       erule allE, erule impE, assumption, erule impE, assumption,

   650       simp add:BtoW_def, rule disjI1, erule subset_psubset_trans, erule Graph11, force)

   651 apply(rule conjI)

   652 apply(simp add:nth_list_update)

   653 apply(rule impI,rule impI, case_tac "M x!T=Black",rotate_tac -1, force simp add: BtoW_def Graph10,

   654       erule subset_psubset_trans, erule Graph11, force)

   655 --{* 3 subgoals left *}

   656 apply(clarify, simp add:abbrev Graph7 Graph8 Graph12)

   657 --{* 2 subgoals left *}

   658 apply(clarify, simp add:abbrev Graph7 Graph8 Graph12)

   659 apply(erule disjE,rule disjI1,erule psubset_subset_trans,erule Graph9,

   660       case_tac "M x!T=Black", rule disjI2,rotate_tac -1, simp add: Graph10, clarify,

   661       erule allE, erule impE, assumption, erule impE, assumption,

   662       simp add:BtoW_def, rule disjI1, erule subset_psubset_trans, erule Graph11, force)

   663 --{* 3 subgoals left *}

   664 apply(simp add:abbrev)

   665 done

   666

   667 lemma interfree_Color_Target_Propagate_Black:

   668   "interfree_aux (Some Color_Target, {}, Some Propagate_Black)"

   669 apply (unfold modules )

   670 apply interfree_aux

   671 apply(clarify, simp add:abbrev)+

   672 done

   673

   674 lemma interfree_Count_Redirect_Edge:

   675   "interfree_aux (Some Count, {}, Some Redirect_Edge)"

   676 apply (unfold modules)

   677 apply interfree_aux

   678 --{* 9 subgoals left *}

   679 apply(simp_all add:abbrev Graph6 Graph12)

   680 --{* 6 subgoals left *}

   681 apply(clarify, simp add:abbrev Graph6 Graph12,

   682       erule disjE,erule disjI1,rule disjI2,rule subset_trans, erule Graph3,force,force)+

   683 done

   684

   685 lemma interfree_Redirect_Edge_Count:

   686   "interfree_aux (Some Redirect_Edge, {}, Some Count)"

   687 apply (unfold modules )

   688 apply interfree_aux

   689 apply(clarify,simp add:abbrev)+

   690 apply(simp add:abbrev)

   691 done

   692

   693 lemma interfree_Count_Color_Target:

   694   "interfree_aux (Some Count, {}, Some Color_Target)"

   695 apply (unfold modules )

   696 apply interfree_aux

   697 --{* 9 subgoals left *}

   698 apply(simp_all add:abbrev Graph7 Graph8 Graph12)

   699 --{* 6 subgoals left *}

   700 apply(clarify,simp add:abbrev Graph7 Graph8 Graph12,

   701       erule disjE, erule disjI1, rule disjI2,erule subset_trans, erule Graph9)+

   702 --{* 2 subgoals left *}

   703 apply(clarify, simp add:abbrev Graph7 Graph8 Graph12)

   704 apply(rule conjI)

   705  apply(erule disjE, erule disjI1, rule disjI2,erule subset_trans, erule Graph9)

   706 apply(simp add:nth_list_update)

   707 --{* 1 subgoal left *}

   708 apply(clarify, simp add:abbrev Graph7 Graph8 Graph12,

   709       erule disjE, erule disjI1, rule disjI2,erule subset_trans, erule Graph9)

   710 done

   711

   712 lemma interfree_Color_Target_Count:

   713   "interfree_aux (Some Color_Target, {}, Some Count)"

   714 apply (unfold modules )

   715 apply interfree_aux

   716 apply(clarify, simp add:abbrev)+

   717 apply(simp add:abbrev)

   718 done

   719

   720 lemma interfree_Append_Redirect_Edge:

   721   "interfree_aux (Some Append, {}, Some Redirect_Edge)"

   722 apply (unfold modules )

   723 apply interfree_aux

   724 apply( simp_all add:abbrev Graph6 Append_to_free0 Append_to_free1 Graph12)

   725 apply(clarify, simp add:abbrev Graph6 Append_to_free0 Append_to_free1 Graph12, force dest:Graph3)+

   726 done

   727

   728 lemma interfree_Redirect_Edge_Append:

   729   "interfree_aux (Some Redirect_Edge, {}, Some Append)"

   730 apply (unfold modules )

   731 apply interfree_aux

   732 apply(clarify, simp add:abbrev Append_to_free0)+

   733 apply (force simp add: Append_to_free2)

   734 apply(clarify, simp add:abbrev Append_to_free0)+

   735 done

   736

   737 lemma interfree_Append_Color_Target:

   738   "interfree_aux (Some Append, {}, Some Color_Target)"

   739 apply (unfold modules )

   740 apply interfree_aux

   741 apply(clarify, simp add:abbrev Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12 nth_list_update)+

   742 apply(simp add:abbrev Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12 nth_list_update)

   743 done

   744

   745 lemma interfree_Color_Target_Append:

   746   "interfree_aux (Some Color_Target, {}, Some Append)"

   747 apply (unfold modules )

   748 apply interfree_aux

   749 apply(clarify, simp add:abbrev Append_to_free0)+

   750 apply (force simp add: Append_to_free2)

   751 apply(clarify,simp add:abbrev Append_to_free0)+

   752 done

   753

   754 lemmas collector_mutator_interfree =

   755  interfree_Blacken_Roots_Redirect_Edge interfree_Blacken_Roots_Color_Target

   756  interfree_Propagate_Black_Redirect_Edge interfree_Propagate_Black_Color_Target

   757  interfree_Count_Redirect_Edge interfree_Count_Color_Target

   758  interfree_Append_Redirect_Edge interfree_Append_Color_Target

   759  interfree_Redirect_Edge_Blacken_Roots interfree_Color_Target_Blacken_Roots

   760  interfree_Redirect_Edge_Propagate_Black interfree_Color_Target_Propagate_Black

   761  interfree_Redirect_Edge_Count interfree_Color_Target_Count

   762  interfree_Redirect_Edge_Append interfree_Color_Target_Append

   763

   764 subsubsection {* Interference freedom Collector-Mutator *}

   765

   766 lemma interfree_Collector_Mutator:

   767  "interfree_aux (Some Collector, {}, Some Mutator)"

   768 apply(unfold Collector_def Mutator_def)

   769 apply interfree_aux

   770 apply(simp_all add:collector_mutator_interfree)

   771 apply(unfold modules collector_defs mutator_defs)

   772 apply(tactic  {* TRYALL (interfree_aux_tac) *})

   773 --{* 32 subgoals left *}

   774 apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)

   775 --{* 20 subgoals left *}

   776 apply(tactic{* TRYALL (clarify_tac @{context}) *})

   777 apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)

   778 apply(tactic {* TRYALL (etac disjE) *})

   779 apply simp_all

   780 apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac subset_trans,etac @{thm Graph3},force_tac @{context}, assume_tac]) *})

   781 apply(tactic {* TRYALL(EVERY'[rtac disjI2,etac subset_trans,rtac @{thm Graph9},force_tac @{context}]) *})

   782 apply(tactic {* TRYALL(EVERY'[rtac disjI1,etac @{thm psubset_subset_trans},rtac @{thm Graph9},force_tac @{context}]) *})

   783 done

   784

   785 subsubsection {* Interference freedom Mutator-Collector *}

   786

   787 lemma interfree_Mutator_Collector:

   788  "interfree_aux (Some Mutator, {}, Some Collector)"

   789 apply(unfold Collector_def Mutator_def)

   790 apply interfree_aux

   791 apply(simp_all add:collector_mutator_interfree)

   792 apply(unfold modules collector_defs mutator_defs)

   793 apply(tactic  {* TRYALL (interfree_aux_tac) *})

   794 --{* 64 subgoals left *}

   795 apply(simp_all add:nth_list_update Invariants Append_to_free0)+

   796 apply(tactic{* TRYALL (clarify_tac @{context}) *})

   797 --{* 4 subgoals left *}

   798 apply force

   799 apply(simp add:Append_to_free2)

   800 apply force

   801 apply(simp add:Append_to_free2)

   802 done

   803

   804 subsubsection {* The Garbage Collection algorithm *}

   805

   806 text {* In total there are 289 verification conditions.  *}

   807

   808 lemma Gar_Coll:

   809   "\<parallel>- .{\<acute>Proper \<and> \<acute>Mut_init \<and> \<acute>z}.

   810   COBEGIN

   811    Collector

   812   .{False}.

   813  \<parallel>

   814    Mutator

   815   .{False}.

   816  COEND

   817   .{False}."

   818 apply oghoare

   819 apply(force simp add: Mutator_def Collector_def modules)

   820 apply(rule Collector)

   821 apply(rule Mutator)

   822 apply(simp add:interfree_Collector_Mutator)

   823 apply(simp add:interfree_Mutator_Collector)

   824 apply force

   825 done

   826

   827 end