Theory Gar_Coll

Up to index of Isabelle/HOL/HoareParallel

theory Gar_Coll
imports Graph OG_Syntax
begin

header {* \section{The Single Mutator Case} *}

theory Gar_Coll imports Graph OG_Syntax begin

declare psubsetE [rule del]

text {* Declaration of variables: *}

record gar_coll_state =
  M :: nodes
  E :: edges
  bc :: "nat set"
  obc :: "nat set"
  Ma :: nodes
  ind :: nat 
  k :: nat
  z :: bool

subsection {* The Mutator *}

text {* The mutator first redirects an arbitrary edge @{text "R"} from
an arbitrary accessible node towards an arbitrary accessible node
@{text "T"}.  It then colors the new target @{text "T"} black. 

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

consts R :: nat  T :: nat

text {* \noindent The following predicate states, given a list of
nodes @{text "m"} and a list of edges @{text "e"}, the conditions
under which the selected edge @{text "R"} and node @{text "T"} are
valid: *}

constdefs
  Mut_init :: "gar_coll_state => bool"
  "Mut_init ≡ « T ∈ Reach ´E ∧ R < length ´E ∧ T < length ´M »"

text {* \noindent For the mutator we
consider two modules, one for each action.  An auxiliary variable
@{text "´z"} is set to false if the mutator has already redirected an
edge but has not yet colored the new target.   *}

constdefs
  Redirect_Edge :: "gar_coll_state ann_com"
  "Redirect_Edge ≡ .{´Mut_init ∧ ´z}. ⟨´E:=´E[R:=(fst(´E!R), T)],, ´z:= (¬´z)⟩"

  Color_Target :: "gar_coll_state ann_com"
  "Color_Target ≡ .{´Mut_init ∧ ¬´z}. ⟨´M:=´M[T:=Black],, ´z:= (¬´z)⟩"

  Mutator :: "gar_coll_state ann_com"
  "Mutator ≡
  .{´Mut_init ∧ ´z}. 
  WHILE True INV .{´Mut_init ∧ ´z}. 
  DO  Redirect_Edge ;; Color_Target  OD"

subsubsection {* Correctness of the mutator *}

lemmas mutator_defs = Mut_init_def Redirect_Edge_def Color_Target_def

lemma Redirect_Edge: 
  "\<turnstile> Redirect_Edge pre(Color_Target)"
apply (unfold mutator_defs)
apply annhoare
apply(simp_all)
apply(force elim:Graph2)
done

lemma Color_Target:
  "\<turnstile> Color_Target .{´Mut_init ∧ ´z}."
apply (unfold mutator_defs)
apply annhoare
apply(simp_all)
done

lemma Mutator: 
 "\<turnstile> Mutator .{False}."
apply(unfold Mutator_def)
apply annhoare
apply(simp_all add:Redirect_Edge Color_Target)
apply(simp add:mutator_defs Redirect_Edge_def)
done

subsection {* The Collector *}

text {* \noindent A constant @{text "M_init"} is used to give @{text "´Ma"} a
suitable first value, defined as a list of nodes where only the @{text
"Roots"} are black. *}

consts  M_init :: nodes

constdefs
  Proper_M_init :: "gar_coll_state => bool"
  "Proper_M_init ≡  « Blacks M_init=Roots ∧ length M_init=length ´M »"
 
  Proper :: "gar_coll_state => bool"
  "Proper ≡ « Proper_Roots ´M ∧ Proper_Edges(´M, ´E) ∧ ´Proper_M_init »"

  Safe :: "gar_coll_state => bool"
  "Safe ≡ « Reach ´E ⊆ Blacks ´M »"

lemmas collector_defs = Proper_M_init_def Proper_def Safe_def

subsubsection {* Blackening the roots *}

constdefs
  Blacken_Roots :: " gar_coll_state ann_com"
  "Blacken_Roots ≡ 
  .{´Proper}.
  ´ind:=0;;
  .{´Proper ∧ ´ind=0}.
  WHILE ´ind<length ´M 
   INV .{´Proper ∧ (∀i<´ind. i ∈ Roots --> ´M!i=Black) ∧ ´ind≤length ´M}.
  DO .{´Proper ∧ (∀i<´ind. i ∈ Roots --> ´M!i=Black) ∧ ´ind<length ´M}.
   IF ´ind∈Roots THEN 
   .{´Proper ∧ (∀i<´ind. i ∈ Roots --> ´M!i=Black) ∧ ´ind<length ´M ∧ ´ind∈Roots}. 
    ´M:=´M[´ind:=Black] FI;;
   .{´Proper ∧ (∀i<´ind+1. i ∈ Roots --> ´M!i=Black) ∧ ´ind<length ´M}.
    ´ind:=´ind+1 
  OD"

lemma Blacken_Roots: 
 "\<turnstile> Blacken_Roots .{´Proper ∧ Roots⊆Blacks ´M}."
apply (unfold Blacken_Roots_def)
apply annhoare
apply(simp_all add:collector_defs Graph_defs)
apply safe
apply(simp_all add:nth_list_update)
  apply (erule less_SucE)
   apply simp+
 apply force
apply force
done

subsubsection {* Propagating black *}

constdefs
  PBInv :: "gar_coll_state => nat => bool"
  "PBInv ≡ « λind. ´obc < Blacks ´M ∨ (∀i <ind. ¬BtoW (´E!i, ´M) ∨
   (¬´z ∧ i=R ∧ (snd(´E!R)) = T ∧ (∃r. ind ≤ r ∧ r < length ´E ∧ BtoW(´E!r,´M))))»"

constdefs  
  Propagate_Black_aux :: "gar_coll_state ann_com"
  "Propagate_Black_aux ≡
  .{´Proper ∧ Roots⊆Blacks ´M ∧ ´obc⊆Blacks ´M ∧ ´bc⊆Blacks ´M}.
  ´ind:=0;;
  .{´Proper ∧ Roots⊆Blacks ´M ∧ ´obc⊆Blacks ´M ∧ ´bc⊆Blacks ´M ∧ ´ind=0}. 
  WHILE ´ind<length ´E 
   INV .{´Proper ∧ Roots⊆Blacks ´M ∧ ´obc⊆Blacks ´M ∧ ´bc⊆Blacks ´M 
         ∧ ´PBInv ´ind ∧ ´ind≤length ´E}.
  DO .{´Proper ∧ Roots⊆Blacks ´M ∧ ´obc⊆Blacks ´M ∧ ´bc⊆Blacks ´M 
       ∧ ´PBInv ´ind ∧ ´ind<length ´E}. 
   IF ´M!(fst (´E!´ind)) = Black THEN 
    .{´Proper ∧ Roots⊆Blacks ´M ∧ ´obc⊆Blacks ´M ∧ ´bc⊆Blacks ´M 
       ∧ ´PBInv ´ind ∧ ´ind<length ´E ∧ ´M!fst(´E!´ind)=Black}.
     ´M:=´M[snd(´E!´ind):=Black];;
    .{´Proper ∧ Roots⊆Blacks ´M ∧ ´obc⊆Blacks ´M ∧ ´bc⊆Blacks ´M 
       ∧ ´PBInv (´ind + 1) ∧ ´ind<length ´E}.
     ´ind:=´ind+1
   FI
  OD"

lemma Propagate_Black_aux: 
  "\<turnstile>  Propagate_Black_aux
  .{´Proper ∧ Roots⊆Blacks ´M ∧ ´obc⊆Blacks ´M ∧ ´bc⊆Blacks ´M 
    ∧ ( ´obc < Blacks ´M ∨ ´Safe)}."
apply (unfold Propagate_Black_aux_def  PBInv_def collector_defs)
apply annhoare
apply(simp_all add:Graph6 Graph7 Graph8 Graph12)
      apply force
     apply force
    apply force
--{* 4 subgoals left *}
apply clarify
apply(simp add:Proper_Edges_def Proper_Roots_def Graph6 Graph7 Graph8 Graph12)
apply (erule disjE)
 apply(rule disjI1)
 apply(erule Graph13)
 apply force
apply (case_tac "M x ! snd (E x ! ind x)=Black")
 apply (simp add: Graph10 BtoW_def)
 apply (rule disjI2)
 apply clarify
 apply (erule less_SucE)
  apply (erule_tac x=i in allE , erule (1) notE impE)
  apply simp
  apply clarify
  apply (drule le_imp_less_or_eq)
  apply (erule disjE)
   apply (subgoal_tac "Suc (ind x)≤r")
    apply fast
   apply arith
  apply fast
 apply fast
apply(rule disjI1)
apply(erule subset_psubset_trans)
apply(erule Graph11)
apply fast
--{* 3 subgoals left *}
apply force
apply force
--{* last *}
apply clarify
apply simp
apply(subgoal_tac "ind x = length (E x)")
 apply (rotate_tac -1)
 apply (simp (asm_lr))
 apply(drule Graph1)
   apply simp
  apply clarify  
 apply(erule allE, erule impE, assumption)
  apply force
 apply force
apply arith
done

subsubsection {* Refining propagating black *}

constdefs
  Auxk :: "gar_coll_state => bool"
  "Auxk ≡ «´k<length ´M ∧ (´M!´k≠Black ∨ ¬BtoW(´E!´ind, ´M) ∨ 
          ´obc<Blacks ´M ∨ (¬´z ∧ ´ind=R ∧ snd(´E!R)=T  
          ∧ (∃r. ´ind<r ∧ r<length ´E ∧ BtoW(´E!r, ´M))))»"

constdefs  
  Propagate_Black :: " gar_coll_state ann_com"
  "Propagate_Black ≡
  .{´Proper ∧ Roots⊆Blacks ´M ∧ ´obc⊆Blacks ´M ∧ ´bc⊆Blacks ´M}.
  ´ind:=0;;
  .{´Proper ∧ Roots⊆Blacks ´M ∧ ´obc⊆Blacks ´M ∧ ´bc⊆Blacks ´M ∧ ´ind=0}.
  WHILE ´ind<length ´E 
   INV .{´Proper ∧ Roots⊆Blacks ´M ∧ ´obc⊆Blacks ´M ∧ ´bc⊆Blacks ´M 
         ∧ ´PBInv ´ind ∧ ´ind≤length ´E}.
  DO .{´Proper ∧ Roots⊆Blacks ´M ∧ ´obc⊆Blacks ´M ∧ ´bc⊆Blacks ´M 
       ∧ ´PBInv ´ind ∧ ´ind<length ´E}. 
   IF (´M!(fst (´E!´ind)))=Black THEN 
    .{´Proper ∧ Roots⊆Blacks ´M ∧ ´obc⊆Blacks ´M ∧ ´bc⊆Blacks ´M 
      ∧ ´PBInv ´ind ∧ ´ind<length ´E ∧ (´M!fst(´E!´ind))=Black}.
     ´k:=(snd(´E!´ind));;
    .{´Proper ∧ Roots⊆Blacks ´M ∧ ´obc⊆Blacks ´M ∧ ´bc⊆Blacks ´M 
      ∧ ´PBInv ´ind ∧ ´ind<length ´E ∧ (´M!fst(´E!´ind))=Black 
      ∧ ´Auxk}.
     ⟨´M:=´M[´k:=Black],, ´ind:=´ind+1⟩
   ELSE .{´Proper ∧ Roots⊆Blacks ´M ∧ ´obc⊆Blacks ´M ∧ ´bc⊆Blacks ´M 
          ∧ ´PBInv ´ind ∧ ´ind<length ´E}. 
         ⟨IF (´M!(fst (´E!´ind)))≠Black THEN ´ind:=´ind+1 FI⟩ 
   FI
  OD"

lemma Propagate_Black: 
  "\<turnstile>  Propagate_Black
  .{´Proper ∧ Roots⊆Blacks ´M ∧ ´obc⊆Blacks ´M ∧ ´bc⊆Blacks ´M 
    ∧ ( ´obc < Blacks ´M ∨ ´Safe)}."
apply (unfold Propagate_Black_def  PBInv_def Auxk_def collector_defs)
apply annhoare
apply(simp_all add:Graph6 Graph7 Graph8 Graph12)
       apply force
      apply force
     apply force
--{* 5 subgoals left *}
apply clarify
apply(simp add:BtoW_def Proper_Edges_def)
--{* 4 subgoals left *}
apply clarify
apply(simp add:Proper_Edges_def Graph6 Graph7 Graph8 Graph12)
apply (erule disjE)
 apply (rule disjI1)
 apply (erule psubset_subset_trans)
 apply (erule Graph9)
apply (case_tac "M x!k x=Black")
 apply (case_tac "M x ! snd (E x ! ind x)=Black")
  apply (simp add: Graph10 BtoW_def)
  apply (rule disjI2)
  apply clarify
  apply (erule less_SucE)
   apply (erule_tac x=i in allE , erule (1) notE impE)
   apply simp
   apply clarify
   apply (drule le_imp_less_or_eq)
   apply (erule disjE)
    apply (subgoal_tac "Suc (ind x)≤r")
     apply fast
    apply arith
   apply fast
  apply fast
 apply (simp add: Graph10 BtoW_def)
 apply (erule disjE)
  apply (erule disjI1)
 apply clarify
 apply (erule less_SucE)
  apply force
 apply simp
 apply (subgoal_tac "Suc R≤r")
  apply fast
 apply arith
apply(rule disjI1)
apply(erule subset_psubset_trans)
apply(erule Graph11)
apply fast
--{* 3 subgoals left *}
apply force
--{* 2 subgoals left *}
apply clarify
apply(simp add:Proper_Edges_def Graph6 Graph7 Graph8 Graph12)
apply (erule disjE)
 apply fast
apply clarify
apply (erule less_SucE)
 apply (erule_tac x=i in allE , erule (1) notE impE)
 apply simp
 apply clarify
 apply (drule le_imp_less_or_eq)
 apply (erule disjE)
  apply (subgoal_tac "Suc (ind x)≤r")
   apply fast
  apply arith
 apply (simp add: BtoW_def)
apply (simp add: BtoW_def)
--{* last *}
apply clarify
apply simp
apply(subgoal_tac "ind x = length (E x)")
 apply (rotate_tac -1)
 apply (simp (asm_lr))
 apply(drule Graph1)
   apply simp
  apply clarify  
 apply(erule allE, erule impE, assumption)
  apply force
 apply force
apply arith
done

subsubsection {* Counting black nodes *}

constdefs
  CountInv :: "gar_coll_state => nat => bool"
  "CountInv ≡ « λind. {i. i<ind ∧ ´Ma!i=Black}⊆´bc »"

constdefs
  Count :: " gar_coll_state ann_com"
  "Count ≡
  .{´Proper ∧ Roots⊆Blacks ´M 
    ∧ ´obc⊆Blacks ´Ma ∧ Blacks ´Ma⊆Blacks ´M ∧ ´bc⊆Blacks ´M 
    ∧ length ´Ma=length ´M ∧ (´obc < Blacks ´Ma ∨ ´Safe) ∧ ´bc={}}.
  ´ind:=0;;
  .{´Proper ∧ Roots⊆Blacks ´M 
    ∧ ´obc⊆Blacks ´Ma ∧ Blacks ´Ma⊆Blacks ´M ∧ ´bc⊆Blacks ´M 
   ∧ length ´Ma=length ´M ∧ (´obc < Blacks ´Ma ∨ ´Safe) ∧ ´bc={} 
   ∧ ´ind=0}.
   WHILE ´ind<length ´M 
     INV .{´Proper ∧ Roots⊆Blacks ´M 
           ∧ ´obc⊆Blacks ´Ma ∧ Blacks ´Ma⊆Blacks ´M ∧ ´bc⊆Blacks ´M 
           ∧ length ´Ma=length ´M ∧ ´CountInv ´ind
           ∧ ( ´obc < Blacks ´Ma ∨ ´Safe) ∧ ´ind≤length ´M}.
   DO .{´Proper ∧ Roots⊆Blacks ´M 
         ∧ ´obc⊆Blacks ´Ma ∧ Blacks ´Ma⊆Blacks ´M ∧ ´bc⊆Blacks ´M 
         ∧ length ´Ma=length ´M ∧ ´CountInv ´ind 
         ∧ ( ´obc < Blacks ´Ma ∨ ´Safe) ∧ ´ind<length ´M}. 
       IF ´M!´ind=Black 
          THEN .{´Proper ∧ Roots⊆Blacks ´M 
                 ∧ ´obc⊆Blacks ´Ma ∧ Blacks ´Ma⊆Blacks ´M ∧ ´bc⊆Blacks ´M 
                 ∧ length ´Ma=length ´M ∧ ´CountInv ´ind
                 ∧ ( ´obc < Blacks ´Ma ∨ ´Safe) ∧ ´ind<length ´M ∧ ´M!´ind=Black}.
          ´bc:=insert ´ind ´bc
       FI;;
      .{´Proper ∧ Roots⊆Blacks ´M 
        ∧ ´obc⊆Blacks ´Ma ∧ Blacks ´Ma⊆Blacks ´M ∧ ´bc⊆Blacks ´M 
        ∧ length ´Ma=length ´M ∧ ´CountInv (´ind+1)
        ∧ ( ´obc < Blacks ´Ma ∨ ´Safe) ∧ ´ind<length ´M}.
      ´ind:=´ind+1
   OD"

lemma Count: 
  "\<turnstile> Count 
  .{´Proper ∧ Roots⊆Blacks ´M 
   ∧ ´obc⊆Blacks ´Ma ∧ Blacks ´Ma⊆´bc ∧ ´bc⊆Blacks ´M ∧ length ´Ma=length ´M
   ∧ (´obc < Blacks ´Ma ∨ ´Safe)}."
apply(unfold Count_def)
apply annhoare
apply(simp_all add:CountInv_def Graph6 Graph7 Graph8 Graph12 Blacks_def collector_defs)
      apply force
     apply force
    apply force
   apply clarify
   apply simp
   apply(fast elim:less_SucE)
  apply clarify
  apply simp
  apply(fast elim:less_SucE)
 apply force
apply force
done

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

consts Append_to_free :: "nat × edges => edges"

axioms
  Append_to_free0: "length (Append_to_free (i, e)) = length e"
  Append_to_free1: "Proper_Edges (m, e) 
                   ==> Proper_Edges (m, Append_to_free(i, e))"
  Append_to_free2: "i ∉ Reach e 
     ==> n ∈ Reach (Append_to_free(i, e)) = ( n = i ∨ n ∈ Reach e)"

constdefs
  AppendInv :: "gar_coll_state => nat => bool"
  "AppendInv ≡ «λind. ∀i<length ´M. ind≤i --> i∈Reach ´E --> ´M!i=Black»"

constdefs
  Append :: " gar_coll_state ann_com"
   "Append ≡
  .{´Proper ∧ Roots⊆Blacks ´M ∧ ´Safe}.
  ´ind:=0;;
  .{´Proper ∧ Roots⊆Blacks ´M ∧ ´Safe ∧ ´ind=0}.
    WHILE ´ind<length ´M 
      INV .{´Proper ∧ ´AppendInv ´ind ∧ ´ind≤length ´M}.
    DO .{´Proper ∧ ´AppendInv ´ind ∧ ´ind<length ´M}.
       IF ´M!´ind=Black THEN 
          .{´Proper ∧ ´AppendInv ´ind ∧ ´ind<length ´M ∧ ´M!´ind=Black}. 
          ´M:=´M[´ind:=White] 
       ELSE .{´Proper ∧ ´AppendInv ´ind ∧ ´ind<length ´M ∧ ´ind∉Reach ´E}.
              ´E:=Append_to_free(´ind,´E)
       FI;;
     .{´Proper ∧ ´AppendInv (´ind+1) ∧ ´ind<length ´M}. 
       ´ind:=´ind+1
    OD"

lemma Append: 
  "\<turnstile> Append .{´Proper}."
apply(unfold Append_def AppendInv_def)
apply annhoare
apply(simp_all add:collector_defs Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
       apply(force simp:Blacks_def nth_list_update)
      apply force
     apply force
    apply(force simp add:Graph_defs)
   apply force
  apply clarify
  apply simp
  apply(rule conjI)
   apply (erule Append_to_free1)
  apply clarify
  apply (drule_tac n = "i" in Append_to_free2)
  apply force
 apply force
apply force
done

subsubsection {* Correctness of the Collector *}

constdefs 
  Collector :: " gar_coll_state ann_com"
  "Collector ≡
.{´Proper}.  
 WHILE True INV .{´Proper}. 
 DO  
  Blacken_Roots;; 
  .{´Proper ∧ Roots⊆Blacks ´M}.  
   ´obc:={};; 
  .{´Proper ∧ Roots⊆Blacks ´M ∧ ´obc={}}. 
   ´bc:=Roots;; 
  .{´Proper ∧ Roots⊆Blacks ´M ∧ ´obc={} ∧ ´bc=Roots}. 
   ´Ma:=M_init;;  
  .{´Proper ∧ Roots⊆Blacks ´M ∧ ´obc={} ∧ ´bc=Roots ∧ ´Ma=M_init}. 
   WHILE ´obc≠´bc  
     INV .{´Proper ∧ Roots⊆Blacks ´M 
           ∧ ´obc⊆Blacks ´Ma ∧ Blacks ´Ma⊆´bc ∧ ´bc⊆Blacks ´M 
           ∧ length ´Ma=length ´M ∧ (´obc < Blacks ´Ma ∨ ´Safe)}. 
   DO .{´Proper ∧ Roots⊆Blacks ´M ∧ ´bc⊆Blacks ´M}.
       ´obc:=´bc;;
       Propagate_Black;; 
      .{´Proper ∧ Roots⊆Blacks ´M ∧ ´obc⊆Blacks ´M ∧ ´bc⊆Blacks ´M 
        ∧ (´obc < Blacks ´M ∨ ´Safe)}. 
       ´Ma:=´M;;
      .{´Proper ∧ Roots⊆Blacks ´M ∧ ´obc⊆Blacks ´Ma 
        ∧ Blacks ´Ma⊆Blacks ´M ∧ ´bc⊆Blacks ´M ∧ length ´Ma=length ´M 
        ∧ ( ´obc < Blacks ´Ma ∨ ´Safe)}.
       ´bc:={};;
       Count 
   OD;; 
  Append  
 OD"

lemma Collector: 
  "\<turnstile> Collector .{False}."
apply(unfold Collector_def)
apply annhoare
apply(simp_all add: Blacken_Roots Propagate_Black Count Append)
apply(simp_all add:Blacken_Roots_def Propagate_Black_def Count_def Append_def collector_defs)
   apply (force simp add: Proper_Roots_def)
  apply force
 apply force
apply clarify
apply (erule disjE)
apply(simp add:psubsetI)
 apply(force dest:subset_antisym)
done

subsection {* Interference Freedom *}

lemmas modules = Redirect_Edge_def Color_Target_def Blacken_Roots_def 
                 Propagate_Black_def Count_def Append_def
lemmas Invariants = PBInv_def Auxk_def CountInv_def AppendInv_def
lemmas abbrev = collector_defs mutator_defs Invariants

lemma interfree_Blacken_Roots_Redirect_Edge: 
 "interfree_aux (Some Blacken_Roots, {}, Some Redirect_Edge)"
apply (unfold modules)
apply interfree_aux
apply safe
apply (simp_all add:Graph6 Graph12 abbrev)
done

lemma interfree_Redirect_Edge_Blacken_Roots: 
  "interfree_aux (Some Redirect_Edge, {}, Some Blacken_Roots)"
apply (unfold modules)
apply interfree_aux
apply safe
apply(simp add:abbrev)+
done

lemma interfree_Blacken_Roots_Color_Target: 
  "interfree_aux (Some Blacken_Roots, {}, Some Color_Target)"
apply (unfold modules)
apply interfree_aux
apply safe
apply(simp_all add:Graph7 Graph8 nth_list_update abbrev)
done

lemma interfree_Color_Target_Blacken_Roots: 
  "interfree_aux (Some Color_Target, {}, Some Blacken_Roots)"
apply (unfold modules )
apply interfree_aux
apply safe
apply(simp add:abbrev)+
done

lemma interfree_Propagate_Black_Redirect_Edge: 
  "interfree_aux (Some Propagate_Black, {}, Some Redirect_Edge)"
apply (unfold modules )
apply interfree_aux
--{* 11 subgoals left *}
apply(clarify, simp add:abbrev Graph6 Graph12)
apply(clarify, simp add:abbrev Graph6 Graph12)
apply(clarify, simp add:abbrev Graph6 Graph12)
apply(clarify, simp add:abbrev Graph6 Graph12)
apply(erule conjE)+
apply(erule disjE, erule disjI1, rule disjI2, rule allI, (rule impI)+, case_tac "R=i", rule conjI, erule sym)
 apply(erule Graph4) 
   apply(simp)+
  apply (simp add:BtoW_def)
 apply (simp add:BtoW_def)
apply(rule conjI)
 apply (force simp add:BtoW_def)
apply(erule Graph4)
   apply simp+
--{* 7 subgoals left *}
apply(clarify, simp add:abbrev Graph6 Graph12)
apply(erule conjE)+
apply(erule disjE, erule disjI1, rule disjI2, rule allI, (rule impI)+, case_tac "R=i", rule conjI, erule sym)
 apply(erule Graph4) 
   apply(simp)+
  apply (simp add:BtoW_def)
 apply (simp add:BtoW_def)
apply(rule conjI)
 apply (force simp add:BtoW_def)
apply(erule Graph4)
   apply simp+
--{* 6 subgoals left *}
apply(clarify, simp add:abbrev Graph6 Graph12)
apply(erule conjE)+
apply(rule conjI)
 apply(erule disjE, erule disjI1, rule disjI2, rule allI, (rule impI)+, case_tac "R=i", rule conjI, erule sym)
  apply(erule Graph4) 
    apply(simp)+
   apply (simp add:BtoW_def)
  apply (simp add:BtoW_def)
 apply(rule conjI)
  apply (force simp add:BtoW_def)
 apply(erule Graph4)
    apply simp+
apply(simp add:BtoW_def nth_list_update) 
apply force
--{* 5 subgoals left *}
apply(clarify, simp add:abbrev Graph6 Graph12)
--{* 4 subgoals left *}
apply(clarify, simp add:abbrev Graph6 Graph12)
apply(rule conjI)
 apply(erule disjE, erule disjI1, rule disjI2, rule allI, (rule impI)+, case_tac "R=i", rule conjI, erule sym)
  apply(erule Graph4) 
    apply(simp)+
   apply (simp add:BtoW_def)
  apply (simp add:BtoW_def)
 apply(rule conjI)
  apply (force simp add:BtoW_def)
 apply(erule Graph4)
    apply simp+
apply(rule conjI)
 apply(simp add:nth_list_update)
 apply force
apply(rule impI, rule impI, erule disjE, erule disjI1, case_tac "R = (ind x)" ,case_tac "M x ! T = Black")
  apply(force simp add:BtoW_def)
 apply(case_tac "M x !snd (E x ! ind x)=Black")
  apply(rule disjI2)
  apply simp
  apply (erule Graph5)
  apply simp+
 apply(force simp add:BtoW_def)
apply(force simp add:BtoW_def)
--{* 3 subgoals left *}
apply(clarify, simp add:abbrev Graph6 Graph12)
--{* 2 subgoals left *}
apply(clarify, simp add:abbrev Graph6 Graph12)
apply(erule disjE, erule disjI1, rule disjI2, rule allI, (rule impI)+, case_tac "R=i", rule conjI, erule sym)
 apply clarify
 apply(erule Graph4) 
   apply(simp)+
  apply (simp add:BtoW_def)
 apply (simp add:BtoW_def)
apply(rule conjI)
 apply (force simp add:BtoW_def)
apply(erule Graph4)
   apply simp+
done

lemma interfree_Redirect_Edge_Propagate_Black: 
  "interfree_aux (Some Redirect_Edge, {}, Some Propagate_Black)"
apply (unfold modules )
apply interfree_aux
apply(clarify, simp add:abbrev)+
done

lemma interfree_Propagate_Black_Color_Target: 
  "interfree_aux (Some Propagate_Black, {}, Some Color_Target)"
apply (unfold modules )
apply interfree_aux
--{* 11 subgoals left *}
apply(clarify, simp add:abbrev Graph7 Graph8 Graph12)+
apply(erule conjE)+
apply(erule disjE,rule disjI1,erule psubset_subset_trans,erule Graph9, 
      case_tac "M x!T=Black", rule disjI2,rotate_tac -1, simp add: Graph10, clarify,
      erule allE, erule impE, assumption, erule impE, assumption, 
      simp add:BtoW_def, rule disjI1, erule subset_psubset_trans, erule Graph11, force) 
--{* 7 subgoals left *}
apply(clarify, simp add:abbrev Graph7 Graph8 Graph12)
apply(erule conjE)+
apply(erule disjE,rule disjI1,erule psubset_subset_trans,erule Graph9, 
      case_tac "M x!T=Black", rule disjI2,rotate_tac -1, simp add: Graph10, clarify,
      erule allE, erule impE, assumption, erule impE, assumption, 
      simp add:BtoW_def, rule disjI1, erule subset_psubset_trans, erule Graph11, force) 
--{* 6 subgoals left *}
apply(clarify, simp add:abbrev Graph7 Graph8 Graph12)
apply clarify
apply (rule conjI)
 apply(erule disjE,rule disjI1,erule psubset_subset_trans,erule Graph9, 
      case_tac "M x!T=Black", rule disjI2,rotate_tac -1, simp add: Graph10, clarify,
      erule allE, erule impE, assumption, erule impE, assumption, 
      simp add:BtoW_def, rule disjI1, erule subset_psubset_trans, erule Graph11, force) 
apply(simp add:nth_list_update)
--{* 5 subgoals left *}
apply(clarify, simp add:abbrev Graph7 Graph8 Graph12)
--{* 4 subgoals left *}
apply(clarify, simp add:abbrev Graph7 Graph8 Graph12)
apply (rule conjI)
 apply(erule disjE,rule disjI1,erule psubset_subset_trans,erule Graph9, 
      case_tac "M x!T=Black", rule disjI2,rotate_tac -1, simp add: Graph10, clarify,
      erule allE, erule impE, assumption, erule impE, assumption, 
      simp add:BtoW_def, rule disjI1, erule subset_psubset_trans, erule Graph11, force) 
apply(rule conjI)
apply(simp add:nth_list_update)
apply(rule impI,rule impI, case_tac "M x!T=Black",rotate_tac -1, force simp add: BtoW_def Graph10, 
      erule subset_psubset_trans, erule Graph11, force)
--{* 3 subgoals left *}
apply(clarify, simp add:abbrev Graph7 Graph8 Graph12)
--{* 2 subgoals left *}
apply(clarify, simp add:abbrev Graph7 Graph8 Graph12)
apply(erule disjE,rule disjI1,erule psubset_subset_trans,erule Graph9, 
      case_tac "M x!T=Black", rule disjI2,rotate_tac -1, simp add: Graph10, clarify,
      erule allE, erule impE, assumption, erule impE, assumption, 
      simp add:BtoW_def, rule disjI1, erule subset_psubset_trans, erule Graph11, force) 
--{* 3 subgoals left *}
apply(simp add:abbrev)
done

lemma interfree_Color_Target_Propagate_Black: 
  "interfree_aux (Some Color_Target, {}, Some Propagate_Black)"
apply (unfold modules )
apply interfree_aux
apply(clarify, simp add:abbrev)+
done

lemma interfree_Count_Redirect_Edge: 
  "interfree_aux (Some Count, {}, Some Redirect_Edge)"
apply (unfold modules)
apply interfree_aux
--{* 9 subgoals left *}
apply(simp_all add:abbrev Graph6 Graph12)
--{* 6 subgoals left *}
apply(clarify, simp add:abbrev Graph6 Graph12,
      erule disjE,erule disjI1,rule disjI2,rule subset_trans, erule Graph3,force,force)+
done

lemma interfree_Redirect_Edge_Count: 
  "interfree_aux (Some Redirect_Edge, {}, Some Count)"
apply (unfold modules )
apply interfree_aux
apply(clarify,simp add:abbrev)+
apply(simp add:abbrev)
done

lemma interfree_Count_Color_Target: 
  "interfree_aux (Some Count, {}, Some Color_Target)"
apply (unfold modules )
apply interfree_aux
--{* 9 subgoals left *}
apply(simp_all add:abbrev Graph7 Graph8 Graph12)
--{* 6 subgoals left *}
apply(clarify,simp add:abbrev Graph7 Graph8 Graph12,
      erule disjE, erule disjI1, rule disjI2,erule subset_trans, erule Graph9)+
--{* 2 subgoals left *}
apply(clarify, simp add:abbrev Graph7 Graph8 Graph12)
apply(rule conjI)
 apply(erule disjE, erule disjI1, rule disjI2,erule subset_trans, erule Graph9) 
apply(simp add:nth_list_update)
--{* 1 subgoal left *}
apply(clarify, simp add:abbrev Graph7 Graph8 Graph12,
      erule disjE, erule disjI1, rule disjI2,erule subset_trans, erule Graph9)
done

lemma interfree_Color_Target_Count: 
  "interfree_aux (Some Color_Target, {}, Some Count)"
apply (unfold modules )
apply interfree_aux
apply(clarify, simp add:abbrev)+
apply(simp add:abbrev)
done

lemma interfree_Append_Redirect_Edge: 
  "interfree_aux (Some Append, {}, Some Redirect_Edge)"
apply (unfold modules )
apply interfree_aux
apply( simp_all add:abbrev Graph6 Append_to_free0 Append_to_free1 Graph12)
apply(clarify, simp add:abbrev Graph6 Append_to_free0 Append_to_free1 Graph12, force dest:Graph3)+
done

lemma interfree_Redirect_Edge_Append: 
  "interfree_aux (Some Redirect_Edge, {}, Some Append)"
apply (unfold modules )
apply interfree_aux
apply(clarify, simp add:abbrev Append_to_free0)+
apply (force simp add: Append_to_free2)
apply(clarify, simp add:abbrev Append_to_free0)+
done

lemma interfree_Append_Color_Target: 
  "interfree_aux (Some Append, {}, Some Color_Target)"
apply (unfold modules )
apply interfree_aux
apply(clarify, simp add:abbrev Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12 nth_list_update)+
apply(simp add:abbrev Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12 nth_list_update)
done

lemma interfree_Color_Target_Append: 
  "interfree_aux (Some Color_Target, {}, Some Append)"
apply (unfold modules )
apply interfree_aux
apply(clarify, simp add:abbrev Append_to_free0)+
apply (force simp add: Append_to_free2)
apply(clarify,simp add:abbrev Append_to_free0)+
done

lemmas collector_mutator_interfree = 
 interfree_Blacken_Roots_Redirect_Edge interfree_Blacken_Roots_Color_Target 
 interfree_Propagate_Black_Redirect_Edge interfree_Propagate_Black_Color_Target  
 interfree_Count_Redirect_Edge interfree_Count_Color_Target 
 interfree_Append_Redirect_Edge interfree_Append_Color_Target 
 interfree_Redirect_Edge_Blacken_Roots interfree_Color_Target_Blacken_Roots 
 interfree_Redirect_Edge_Propagate_Black interfree_Color_Target_Propagate_Black  
 interfree_Redirect_Edge_Count interfree_Color_Target_Count 
 interfree_Redirect_Edge_Append interfree_Color_Target_Append

subsubsection {* Interference freedom Collector-Mutator *}

lemma interfree_Collector_Mutator:
 "interfree_aux (Some Collector, {}, Some Mutator)"
apply(unfold Collector_def Mutator_def)
apply interfree_aux
apply(simp_all add:collector_mutator_interfree)
apply(unfold modules collector_defs mutator_defs)
apply(tactic  {* TRYALL (interfree_aux_tac) *})
--{* 32 subgoals left *}
apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
--{* 20 subgoals left *}
apply(tactic{* TRYALL Clarify_tac *})
apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
apply(tactic {* TRYALL (etac disjE) *})
apply simp_all
apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac subset_trans,etac (thm "Graph3"),Force_tac, assume_tac]) *})
apply(tactic {* TRYALL(EVERY'[rtac disjI2,etac subset_trans,rtac (thm "Graph9"),Force_tac]) *})
apply(tactic {* TRYALL(EVERY'[rtac disjI1,etac psubset_subset_trans,rtac (thm "Graph9"),Force_tac]) *})
done

subsubsection {* Interference freedom Mutator-Collector *}

lemma interfree_Mutator_Collector:
 "interfree_aux (Some Mutator, {}, Some Collector)"
apply(unfold Collector_def Mutator_def)
apply interfree_aux
apply(simp_all add:collector_mutator_interfree)
apply(unfold modules collector_defs mutator_defs)
apply(tactic  {* TRYALL (interfree_aux_tac) *})
--{* 64 subgoals left *}
apply(simp_all add:nth_list_update Invariants Append_to_free0)+
apply(tactic{* TRYALL Clarify_tac *})
--{* 4 subgoals left *}
apply force
apply(simp add:Append_to_free2)
apply force
apply(simp add:Append_to_free2)
done

subsubsection {* The Garbage Collection algorithm *}

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

lemma Gar_Coll: 
  "\<parallel>- .{´Proper ∧ ´Mut_init ∧ ´z}.  
  COBEGIN  
   Collector
  .{False}.
 \<parallel>  
   Mutator
  .{False}. 
 COEND 
  .{False}."
apply oghoare
apply(force simp add: Mutator_def Collector_def modules)
apply(rule Collector)
apply(rule Mutator)
apply(simp add:interfree_Collector_Mutator)
apply(simp add:interfree_Mutator_Collector)
apply force
done

end

The Mutator

Correctness of the mutator

lemmas mutator_defs:

  Mut_init == %s. T ∈ Reach (E s) ∧ R < length (E s) ∧ T < length (M s)
  Redirect_Edge == .{´Mut_init ∧ ´z}.
  ⟨´E := ´E[R := (fst (´E ! R), T)],, ´z := (¬ ´z)⟩
  Color_Target == .{´Mut_init ∧ ¬ ´z}.
  ⟨´M := ´M[T := Black],, ´z := (¬ ´z)⟩

lemmas mutator_defs:

  Mut_init == %s. T ∈ Reach (E s) ∧ R < length (E s) ∧ T < length (M s)
  Redirect_Edge == .{´Mut_init ∧ ´z}.
  ⟨´E := ´E[R := (fst (´E ! R), T)],, ´z := (¬ ´z)⟩
  Color_Target == .{´Mut_init ∧ ¬ ´z}.
  ⟨´M := ´M[T := Black],, ´z := (¬ ´z)⟩

lemma Redirect_Edge:

  \<turnstile> Redirect_Edge
     pre Color_Target

lemma Color_Target:

  \<turnstile> Color_Target
     .{´Mut_init ∧ ´z}.

lemma Mutator:

  \<turnstile> Mutator
     .{False}.

The Collector

lemmas collector_defs:

  Proper_M_init == %s. Blacks M_init = Roots ∧ length M_init = length (M s)
  Proper == %s. Proper_Roots (M s) ∧ Proper_Edges (M s, E s) ∧ Proper_M_init s
  Safe == %s. Reach (E s) ⊆ Blacks (M s)

lemmas collector_defs:

  Proper_M_init == %s. Blacks M_init = Roots ∧ length M_init = length (M s)
  Proper == %s. Proper_Roots (M s) ∧ Proper_Edges (M s, E s) ∧ Proper_M_init s
  Safe == %s. Reach (E s) ⊆ Blacks (M s)

Blackening the roots

lemma Blacken_Roots:

  \<turnstile> Blacken_Roots
     .{´Proper ∧ Roots ⊆ Blacks ´M}.

Propagating black

lemma Propagate_Black_aux:

  \<turnstile> Propagate_Black_aux
     .{´Proper ∧
       Roots ⊆ Blacks ´M ∧
       ´obc ⊆ Blacks ´M ∧ ´bc ⊆ Blacks ´M ∧ (´obc ⊂ Blacks ´M ∨ ´Safe)}.

Refining propagating black

lemma Propagate_Black:

  \<turnstile> Propagate_Black
     .{´Proper ∧
       Roots ⊆ Blacks ´M ∧
       ´obc ⊆ Blacks ´M ∧ ´bc ⊆ Blacks ´M ∧ (´obc ⊂ Blacks ´M ∨ ´Safe)}.

Counting black nodes

lemma Count:

  \<turnstile> Count
     .{´Proper ∧
       Roots ⊆ Blacks ´M ∧
       ´obc ⊆ Blacks ´Ma ∧
       Blacks ´Ma ⊆ ´bc ∧
       ´bc ⊆ Blacks ´M ∧ length ´Ma = length ´M ∧ (´obc ⊂ Blacks ´Ma ∨ ´Safe)}.

Appending garbage nodes to the free list

lemma Append:

  \<turnstile> Append
     .{´Proper}.

Correctness of the Collector

lemma Collector:

  \<turnstile> Collector
     .{False}.

Interference Freedom

lemmas modules:

  Redirect_Edge == .{´Mut_init ∧ ´z}.
  ⟨´E := ´E[R := (fst (´E ! R), T)],, ´z := (¬ ´z)⟩
  Color_Target == .{´Mut_init ∧ ¬ ´z}.
  ⟨´M := ´M[T := Black],, ´z := (¬ ´z)⟩
  Blacken_Roots == .{´Proper}. ´ind := 0;; .{´Proper ∧ ´ind = 0}. 
  WHILE ´ind < length ´M 
  INV .{´Proper ∧ (∀i<´ind. i ∈ Roots --> ´M ! i = Black) ∧ ´ind ≤ length ´M}. 
  DO .{´Proper ∧ (∀i<´ind. i ∈ Roots --> ´M ! i = Black) ∧ ´ind < length ´M}. 
  IF ´ind ∈ Roots 
  THEN .{´Proper ∧
         (∀i<´ind. i ∈ Roots --> ´M ! i = Black) ∧
         ´ind < length ´M ∧ ´ind ∈ Roots}. ´M :=
       ´M[´ind := Black] 
  FI;;
  .{´Proper ∧
    (∀i<´ind + 1. i ∈ Roots --> ´M ! i = Black) ∧ ´ind < length ´M}. ´ind :=
  ´ind + 1
  OD
  Propagate_Black ==
  .{´Proper ∧ Roots ⊆ Blacks ´M ∧ ´obc ⊆ Blacks ´M ∧ ´bc ⊆ Blacks ´M}. ´ind := 0;;
  .{´Proper ∧ Roots ⊆ Blacks ´M ∧ ´obc ⊆ Blacks ´M ∧ ´bc ⊆ Blacks ´M ∧ ´ind = 0}. 
  WHILE ´ind < length ´E 
  INV .{´Proper ∧
        Roots ⊆ Blacks ´M ∧
        ´obc ⊆ Blacks ´M ∧ ´bc ⊆ Blacks ´M ∧ ´PBInv ´ind ∧ ´ind ≤ length ´E}. 
  DO .{´Proper ∧
       Roots ⊆ Blacks ´M ∧
       ´obc ⊆ Blacks ´M ∧ ´bc ⊆ Blacks ´M ∧ ´PBInv ´ind ∧ ´ind < length ´E}. 
  IF ´M ! fst (´E ! ´ind) = Black 
  THEN .{´Proper ∧
         Roots ⊆ Blacks ´M ∧
         ´obc ⊆ Blacks ´M ∧
         ´bc ⊆ Blacks ´M ∧
         ´PBInv ´ind ∧ ´ind < length ´E ∧ ´M ! fst (´E ! ´ind) = Black}. ´k :=
       snd (´E ! ´ind);;
  .{´Proper ∧
    Roots ⊆ Blacks ´M ∧
    ´obc ⊆ Blacks ´M ∧
    ´bc ⊆ Blacks ´M ∧
    ´PBInv ´ind ∧ ´ind < length ´E ∧ ´M ! fst (´E ! ´ind) = Black ∧ ´Auxk}.
  ⟨´M := ´M[´k := Black],, ´ind := ´ind + 1⟩ 
  ELSE .{´Proper ∧
         Roots ⊆ Blacks ´M ∧
         ´obc ⊆ Blacks ´M ∧ ´bc ⊆ Blacks ´M ∧ ´PBInv ´ind ∧ ´ind < length ´E}.
  ⟨IF ´M ! fst (´E ! ´ind) ≠ Black THEN ´ind := ´ind + 1 FI⟩ FI
  OD
  Count ==
  .{´Proper ∧
    Roots ⊆ Blacks ´M ∧
    ´obc ⊆ Blacks ´Ma ∧
    Blacks ´Ma ⊆ Blacks ´M ∧
    ´bc ⊆ Blacks ´M ∧
    length ´Ma = length ´M ∧ (´obc ⊂ Blacks ´Ma ∨ ´Safe) ∧ ´bc = {}}. ´ind :=
  0;;
  .{´Proper ∧
    Roots ⊆ Blacks ´M ∧
    ´obc ⊆ Blacks ´Ma ∧
    Blacks ´Ma ⊆ Blacks ´M ∧
    ´bc ⊆ Blacks ´M ∧
    length ´Ma = length ´M ∧ (´obc ⊂ Blacks ´Ma ∨ ´Safe) ∧ ´bc = {} ∧ ´ind = 0}. 
  WHILE ´ind < length ´M 
  INV .{´Proper ∧
        Roots ⊆ Blacks ´M ∧
        ´obc ⊆ Blacks ´Ma ∧
        Blacks ´Ma ⊆ Blacks ´M ∧
        ´bc ⊆ Blacks ´M ∧
        length ´Ma = length ´M ∧
        ´CountInv ´ind ∧ (´obc ⊂ Blacks ´Ma ∨ ´Safe) ∧ ´ind ≤ length ´M}. 
  DO .{´Proper ∧
       Roots ⊆ Blacks ´M ∧
       ´obc ⊆ Blacks ´Ma ∧
       Blacks ´Ma ⊆ Blacks ´M ∧
       ´bc ⊆ Blacks ´M ∧
       length ´Ma = length ´M ∧
       ´CountInv ´ind ∧ (´obc ⊂ Blacks ´Ma ∨ ´Safe) ∧ ´ind < length ´M}. 
  IF ´M ! ´ind = Black 
  THEN .{´Proper ∧
         Roots ⊆ Blacks ´M ∧
         ´obc ⊆ Blacks ´Ma ∧
         Blacks ´Ma ⊆ Blacks ´M ∧
         ´bc ⊆ Blacks ´M ∧
         length ´Ma = length ´M ∧
         ´CountInv ´ind ∧
         (´obc ⊂ Blacks ´Ma ∨ ´Safe) ∧
         ´ind < length ´M ∧ ´M ! ´ind = Black}. ´bc :=
       insert ´ind ´bc 
  FI;;
  .{´Proper ∧
    Roots ⊆ Blacks ´M ∧
    ´obc ⊆ Blacks ´Ma ∧
    Blacks ´Ma ⊆ Blacks ´M ∧
    ´bc ⊆ Blacks ´M ∧
    length ´Ma = length ´M ∧
    ´CountInv (´ind + 1) ∧
    (´obc ⊂ Blacks ´Ma ∨ ´Safe) ∧ ´ind < length ´M}. ´ind :=
  ´ind + 1
  OD
  Append == .{´Proper ∧ Roots ⊆ Blacks ´M ∧ ´Safe}. ´ind := 0;;
  .{´Proper ∧ Roots ⊆ Blacks ´M ∧ ´Safe ∧ ´ind = 0}. 
  WHILE ´ind < length ´M INV .{´Proper ∧ ´AppendInv ´ind ∧ ´ind ≤ length ´M}. 
  DO .{´Proper ∧ ´AppendInv ´ind ∧ ´ind < length ´M}. 
  IF ´M ! ´ind = Black 
  THEN .{´Proper ∧ ´AppendInv ´ind ∧ ´ind < length ´M ∧ ´M ! ´ind = Black}. ´M :=
       ´M[´ind := White] 
  ELSE .{´Proper ∧ ´AppendInv ´ind ∧ ´ind < length ´M ∧ ´ind ∉ Reach ´E}. ´E :=
       Append_to_free (´ind, ´E) 
  FI;; .{´Proper ∧ ´AppendInv (´ind + 1) ∧ ´ind < length ´M}. ´ind := ´ind + 1
  OD

lemmas modules:

  Redirect_Edge == .{´Mut_init ∧ ´z}.
  ⟨´E := ´E[R := (fst (´E ! R), T)],, ´z := (¬ ´z)⟩
  Color_Target == .{´Mut_init ∧ ¬ ´z}.
  ⟨´M := ´M[T := Black],, ´z := (¬ ´z)⟩
  Blacken_Roots == .{´Proper}. ´ind := 0;; .{´Proper ∧ ´ind = 0}. 
  WHILE ´ind < length ´M 
  INV .{´Proper ∧ (∀i<´ind. i ∈ Roots --> ´M ! i = Black) ∧ ´ind ≤ length ´M}. 
  DO .{´Proper ∧ (∀i<´ind. i ∈ Roots --> ´M ! i = Black) ∧ ´ind < length ´M}. 
  IF ´ind ∈ Roots 
  THEN .{´Proper ∧
         (∀i<´ind. i ∈ Roots --> ´M ! i = Black) ∧
         ´ind < length ´M ∧ ´ind ∈ Roots}. ´M :=
       ´M[´ind := Black] 
  FI;;
  .{´Proper ∧
    (∀i<´ind + 1. i ∈ Roots --> ´M ! i = Black) ∧ ´ind < length ´M}. ´ind :=
  ´ind + 1
  OD
  Propagate_Black ==
  .{´Proper ∧ Roots ⊆ Blacks ´M ∧ ´obc ⊆ Blacks ´M ∧ ´bc ⊆ Blacks ´M}. ´ind := 0;;
  .{´Proper ∧ Roots ⊆ Blacks ´M ∧ ´obc ⊆ Blacks ´M ∧ ´bc ⊆ Blacks ´M ∧ ´ind = 0}. 
  WHILE ´ind < length ´E 
  INV .{´Proper ∧
        Roots ⊆ Blacks ´M ∧
        ´obc ⊆ Blacks ´M ∧ ´bc ⊆ Blacks ´M ∧ ´PBInv ´ind ∧ ´ind ≤ length ´E}. 
  DO .{´Proper ∧
       Roots ⊆ Blacks ´M ∧
       ´obc ⊆ Blacks ´M ∧ ´bc ⊆ Blacks ´M ∧ ´PBInv ´ind ∧ ´ind < length ´E}. 
  IF ´M ! fst (´E ! ´ind) = Black 
  THEN .{´Proper ∧
         Roots ⊆ Blacks ´M ∧
         ´obc ⊆ Blacks ´M ∧
         ´bc ⊆ Blacks ´M ∧
         ´PBInv ´ind ∧ ´ind < length ´E ∧ ´M ! fst (´E ! ´ind) = Black}. ´k :=
       snd (´E ! ´ind);;
  .{´Proper ∧
    Roots ⊆ Blacks ´M ∧
    ´obc ⊆ Blacks ´M ∧
    ´bc ⊆ Blacks ´M ∧
    ´PBInv ´ind ∧ ´ind < length ´E ∧ ´M ! fst (´E ! ´ind) = Black ∧ ´Auxk}.
  ⟨´M := ´M[´k := Black],, ´ind := ´ind + 1⟩ 
  ELSE .{´Proper ∧
         Roots ⊆ Blacks ´M ∧
         ´obc ⊆ Blacks ´M ∧ ´bc ⊆ Blacks ´M ∧ ´PBInv ´ind ∧ ´ind < length ´E}.
  ⟨IF ´M ! fst (´E ! ´ind) ≠ Black THEN ´ind := ´ind + 1 FI⟩ FI
  OD
  Count ==
  .{´Proper ∧
    Roots ⊆ Blacks ´M ∧
    ´obc ⊆ Blacks ´Ma ∧
    Blacks ´Ma ⊆ Blacks ´M ∧
    ´bc ⊆ Blacks ´M ∧
    length ´Ma = length ´M ∧ (´obc ⊂ Blacks ´Ma ∨ ´Safe) ∧ ´bc = {}}. ´ind :=
  0;;
  .{´Proper ∧
    Roots ⊆ Blacks ´M ∧
    ´obc ⊆ Blacks ´Ma ∧
    Blacks ´Ma ⊆ Blacks ´M ∧
    ´bc ⊆ Blacks ´M ∧
    length ´Ma = length ´M ∧ (´obc ⊂ Blacks ´Ma ∨ ´Safe) ∧ ´bc = {} ∧ ´ind = 0}. 
  WHILE ´ind < length ´M 
  INV .{´Proper ∧
        Roots ⊆ Blacks ´M ∧
        ´obc ⊆ Blacks ´Ma ∧
        Blacks ´Ma ⊆ Blacks ´M ∧
        ´bc ⊆ Blacks ´M ∧
        length ´Ma = length ´M ∧
        ´CountInv ´ind ∧ (´obc ⊂ Blacks ´Ma ∨ ´Safe) ∧ ´ind ≤ length ´M}. 
  DO .{´Proper ∧
       Roots ⊆ Blacks ´M ∧
       ´obc ⊆ Blacks ´Ma ∧
       Blacks ´Ma ⊆ Blacks ´M ∧
       ´bc ⊆ Blacks ´M ∧
       length ´Ma = length ´M ∧
       ´CountInv ´ind ∧ (´obc ⊂ Blacks ´Ma ∨ ´Safe) ∧ ´ind < length ´M}. 
  IF ´M ! ´ind = Black 
  THEN .{´Proper ∧
         Roots ⊆ Blacks ´M ∧
         ´obc ⊆ Blacks ´Ma ∧
         Blacks ´Ma ⊆ Blacks ´M ∧
         ´bc ⊆ Blacks ´M ∧
         length ´Ma = length ´M ∧
         ´CountInv ´ind ∧
         (´obc ⊂ Blacks ´Ma ∨ ´Safe) ∧
         ´ind < length ´M ∧ ´M ! ´ind = Black}. ´bc :=
       insert ´ind ´bc 
  FI;;
  .{´Proper ∧
    Roots ⊆ Blacks ´M ∧
    ´obc ⊆ Blacks ´Ma ∧
    Blacks ´Ma ⊆ Blacks ´M ∧
    ´bc ⊆ Blacks ´M ∧
    length ´Ma = length ´M ∧
    ´CountInv (´ind + 1) ∧
    (´obc ⊂ Blacks ´Ma ∨ ´Safe) ∧ ´ind < length ´M}. ´ind :=
  ´ind + 1
  OD
  Append == .{´Proper ∧ Roots ⊆ Blacks ´M ∧ ´Safe}. ´ind := 0;;
  .{´Proper ∧ Roots ⊆ Blacks ´M ∧ ´Safe ∧ ´ind = 0}. 
  WHILE ´ind < length ´M INV .{´Proper ∧ ´AppendInv ´ind ∧ ´ind ≤ length ´M}. 
  DO .{´Proper ∧ ´AppendInv ´ind ∧ ´ind < length ´M}. 
  IF ´M ! ´ind = Black 
  THEN .{´Proper ∧ ´AppendInv ´ind ∧ ´ind < length ´M ∧ ´M ! ´ind = Black}. ´M :=
       ´M[´ind := White] 
  ELSE .{´Proper ∧ ´AppendInv ´ind ∧ ´ind < length ´M ∧ ´ind ∉ Reach ´E}. ´E :=
       Append_to_free (´ind, ´E) 
  FI;; .{´Proper ∧ ´AppendInv (´ind + 1) ∧ ´ind < length ´M}. ´ind := ´ind + 1
  OD

lemmas Invariants:

  PBInv ==
  %s ind.
     obc s ⊂ Blacks (M s) ∨
     (∀i<ind.
         ¬ BtoW (E s ! i, M s) ∨
         ¬ z si = R ∧
         snd (E s ! R) = T ∧
         (∃r. indrr < length (E s) ∧ BtoW (E s ! r, M s)))
  Auxk ==
  %s. k s < length (M s) ∧
      (M s ! k s ≠ Black ∨
       ¬ BtoW (E s ! ind s, M s) ∨
       obc s ⊂ Blacks (M s) ∨
       ¬ z s ∧
       ind s = R ∧
       snd (E s ! R) = T ∧ (∃r>ind s. r < length (E s) ∧ BtoW (E s ! r, M s)))
  CountInv == %s ind. .{´op < ind ∧ ´(op ! (Ma s)) = Black}. ⊆ bc s
  AppendInv ==
  %s ind. ∀i<length (M s). indi --> i ∈ Reach (E s) --> M s ! i = Black

lemmas Invariants:

  PBInv ==
  %s ind.
     obc s ⊂ Blacks (M s) ∨
     (∀i<ind.
         ¬ BtoW (E s ! i, M s) ∨
         ¬ z si = R ∧
         snd (E s ! R) = T ∧
         (∃r. indrr < length (E s) ∧ BtoW (E s ! r, M s)))
  Auxk ==
  %s. k s < length (M s) ∧
      (M s ! k s ≠ Black ∨
       ¬ BtoW (E s ! ind s, M s) ∨
       obc s ⊂ Blacks (M s) ∨
       ¬ z s ∧
       ind s = R ∧
       snd (E s ! R) = T ∧ (∃r>ind s. r < length (E s) ∧ BtoW (E s ! r, M s)))
  CountInv == %s ind. .{´op < ind ∧ ´(op ! (Ma s)) = Black}. ⊆ bc s
  AppendInv ==
  %s ind. ∀i<length (M s). indi --> i ∈ Reach (E s) --> M s ! i = Black

lemmas abbrev:

  Proper_M_init == %s. Blacks M_init = Roots ∧ length M_init = length (M s)
  Proper == %s. Proper_Roots (M s) ∧ Proper_Edges (M s, E s) ∧ Proper_M_init s
  Safe == %s. Reach (E s) ⊆ Blacks (M s)
  Mut_init == %s. T ∈ Reach (E s) ∧ R < length (E s) ∧ T < length (M s)
  Redirect_Edge == .{´Mut_init ∧ ´z}.
  ⟨´E := ´E[R := (fst (´E ! R), T)],, ´z := (¬ ´z)⟩
  Color_Target == .{´Mut_init ∧ ¬ ´z}.
  ⟨´M := ´M[T := Black],, ´z := (¬ ´z)⟩
  PBInv ==
  %s ind.
     obc s ⊂ Blacks (M s) ∨
     (∀i<ind.
         ¬ BtoW (E s ! i, M s) ∨
         ¬ z si = R ∧
         snd (E s ! R) = T ∧
         (∃r. indrr < length (E s) ∧ BtoW (E s ! r, M s)))
  Auxk ==
  %s. k s < length (M s) ∧
      (M s ! k s ≠ Black ∨
       ¬ BtoW (E s ! ind s, M s) ∨
       obc s ⊂ Blacks (M s) ∨
       ¬ z s ∧
       ind s = R ∧
       snd (E s ! R) = T ∧ (∃r>ind s. r < length (E s) ∧ BtoW (E s ! r, M s)))
  CountInv == %s ind. .{´op < ind ∧ ´(op ! (Ma s)) = Black}. ⊆ bc s
  AppendInv ==
  %s ind. ∀i<length (M s). indi --> i ∈ Reach (E s) --> M s ! i = Black

lemmas abbrev:

  Proper_M_init == %s. Blacks M_init = Roots ∧ length M_init = length (M s)
  Proper == %s. Proper_Roots (M s) ∧ Proper_Edges (M s, E s) ∧ Proper_M_init s
  Safe == %s. Reach (E s) ⊆ Blacks (M s)
  Mut_init == %s. T ∈ Reach (E s) ∧ R < length (E s) ∧ T < length (M s)
  Redirect_Edge == .{´Mut_init ∧ ´z}.
  ⟨´E := ´E[R := (fst (´E ! R), T)],, ´z := (¬ ´z)⟩
  Color_Target == .{´Mut_init ∧ ¬ ´z}.
  ⟨´M := ´M[T := Black],, ´z := (¬ ´z)⟩
  PBInv ==
  %s ind.
     obc s ⊂ Blacks (M s) ∨
     (∀i<ind.
         ¬ BtoW (E s ! i, M s) ∨
         ¬ z si = R ∧
         snd (E s ! R) = T ∧
         (∃r. indrr < length (E s) ∧ BtoW (E s ! r, M s)))
  Auxk ==
  %s. k s < length (M s) ∧
      (M s ! k s ≠ Black ∨
       ¬ BtoW (E s ! ind s, M s) ∨
       obc s ⊂ Blacks (M s) ∨
       ¬ z s ∧
       ind s = R ∧
       snd (E s ! R) = T ∧ (∃r>ind s. r < length (E s) ∧ BtoW (E s ! r, M s)))
  CountInv == %s ind. .{´op < ind ∧ ´(op ! (Ma s)) = Black}. ⊆ bc s
  AppendInv ==
  %s ind. ∀i<length (M s). indi --> i ∈ Reach (E s) --> M s ! i = Black

lemma interfree_Blacken_Roots_Redirect_Edge:

  interfree_aux (Some Blacken_Roots, {}, Some Redirect_Edge)

lemma interfree_Redirect_Edge_Blacken_Roots:

  interfree_aux (Some Redirect_Edge, {}, Some Blacken_Roots)

lemma interfree_Blacken_Roots_Color_Target:

  interfree_aux (Some Blacken_Roots, {}, Some Color_Target)

lemma interfree_Color_Target_Blacken_Roots:

  interfree_aux (Some Color_Target, {}, Some Blacken_Roots)

lemma interfree_Propagate_Black_Redirect_Edge:

  interfree_aux (Some Propagate_Black, {}, Some Redirect_Edge)

lemma interfree_Redirect_Edge_Propagate_Black:

  interfree_aux (Some Redirect_Edge, {}, Some Propagate_Black)

lemma interfree_Propagate_Black_Color_Target:

  interfree_aux (Some Propagate_Black, {}, Some Color_Target)

lemma interfree_Color_Target_Propagate_Black:

  interfree_aux (Some Color_Target, {}, Some Propagate_Black)

lemma interfree_Count_Redirect_Edge:

  interfree_aux (Some Count, {}, Some Redirect_Edge)

lemma interfree_Redirect_Edge_Count:

  interfree_aux (Some Redirect_Edge, {}, Some Count)

lemma interfree_Count_Color_Target:

  interfree_aux (Some Count, {}, Some Color_Target)

lemma interfree_Color_Target_Count:

  interfree_aux (Some Color_Target, {}, Some Count)

lemma interfree_Append_Redirect_Edge:

  interfree_aux (Some Append, {}, Some Redirect_Edge)

lemma interfree_Redirect_Edge_Append:

  interfree_aux (Some Redirect_Edge, {}, Some Append)

lemma interfree_Append_Color_Target:

  interfree_aux (Some Append, {}, Some Color_Target)

lemma interfree_Color_Target_Append:

  interfree_aux (Some Color_Target, {}, Some Append)

lemmas collector_mutator_interfree:

  interfree_aux (Some Blacken_Roots, {}, Some Redirect_Edge)
  interfree_aux (Some Blacken_Roots, {}, Some Color_Target)
  interfree_aux (Some Propagate_Black, {}, Some Redirect_Edge)
  interfree_aux (Some Propagate_Black, {}, Some Color_Target)
  interfree_aux (Some Count, {}, Some Redirect_Edge)
  interfree_aux (Some Count, {}, Some Color_Target)
  interfree_aux (Some Append, {}, Some Redirect_Edge)
  interfree_aux (Some Append, {}, Some Color_Target)
  interfree_aux (Some Redirect_Edge, {}, Some Blacken_Roots)
  interfree_aux (Some Color_Target, {}, Some Blacken_Roots)
  interfree_aux (Some Redirect_Edge, {}, Some Propagate_Black)
  interfree_aux (Some Color_Target, {}, Some Propagate_Black)
  interfree_aux (Some Redirect_Edge, {}, Some Count)
  interfree_aux (Some Color_Target, {}, Some Count)
  interfree_aux (Some Redirect_Edge, {}, Some Append)
  interfree_aux (Some Color_Target, {}, Some Append)

lemmas collector_mutator_interfree:

  interfree_aux (Some Blacken_Roots, {}, Some Redirect_Edge)
  interfree_aux (Some Blacken_Roots, {}, Some Color_Target)
  interfree_aux (Some Propagate_Black, {}, Some Redirect_Edge)
  interfree_aux (Some Propagate_Black, {}, Some Color_Target)
  interfree_aux (Some Count, {}, Some Redirect_Edge)
  interfree_aux (Some Count, {}, Some Color_Target)
  interfree_aux (Some Append, {}, Some Redirect_Edge)
  interfree_aux (Some Append, {}, Some Color_Target)
  interfree_aux (Some Redirect_Edge, {}, Some Blacken_Roots)
  interfree_aux (Some Color_Target, {}, Some Blacken_Roots)
  interfree_aux (Some Redirect_Edge, {}, Some Propagate_Black)
  interfree_aux (Some Color_Target, {}, Some Propagate_Black)
  interfree_aux (Some Redirect_Edge, {}, Some Count)
  interfree_aux (Some Color_Target, {}, Some Count)
  interfree_aux (Some Redirect_Edge, {}, Some Append)
  interfree_aux (Some Color_Target, {}, Some Append)

Interference freedom Collector-Mutator

lemma interfree_Collector_Mutator:

  interfree_aux (Some Collector, {}, Some Mutator)

Interference freedom Mutator-Collector

lemma interfree_Mutator_Collector:

  interfree_aux (Some Mutator, {}, Some Collector)

The Garbage Collection algorithm

lemma Gar_Coll:

  \<parallel>- .{´Proper ∧ ´Mut_init ∧ ´z}.
     COBEGIN
     Collector
     .{False}.
     \<parallel>
     Mutator
     .{False}.
     COEND
     .{False}.