{wfstate 0 Collection(){ (HStore)S∈Par⊥Hal (HHeap)H∈Loc-HObj local mstk:Seq(Int); (HThrds)Π∈MutID→HStore (HState)Σ∈HThrds x HHeap Loop Imariant:{wfstate *(ownnp(mstk)A mstk=e) while (true) (LS1ore)s∈Par-Lal×{0,1} (LHeap)h∈[L.M]一LOb Initialize(); LThrds)π∈ThdD→LStore {(wfstate A reach_inv)*(ownap(mstk)Amstk=c)} (LState)a E LThrds x LHeap Trace(); ((wfstate A reach_inv)*(ownap(mstk)Amstk = Figure 12.High-Level and Low-Level State Models CleanCard(); (wfstate A reach_inv)*(ownap(mstk)Amstk =c)} atomic{ The transformation.The transformation T is defined as follows. ScanRoot(); For code,the high-level abstract GC thread is transformed to the X.(wfstate A reach_rtnw stk(X)A stk_black(X)) GC thread shown in Figure 10.Each instruction z.id :=E in *(ownmp(mstk)Amstk=X) mutators is transformed to the write barrier,where id is a pointer CleanCard(); field ofz.Other instructions and the program structures of mutators are unchanged. {(wfstate A reach_black)*(ownnp(mstk)A mstk =e)} Sweep(); The following transformations are made over initial states First we require the high-level initial state to be well-formed: false wfstate(Π，H)兰l.reachable()(L,H=→l∈dom(H) That is,reachable locations cannot be dangling pointers. Figure 10.Outline of the GC Code and Proof Sketch High-level locations are transformed to integers by a bijective function Loc2Int Loc 0..M]satisfying Loc2Int(nil)=0. update(x.id,E){//idE {pt1,...,ptm} Variables are transformed to the low level using an extra bit to atomic{x.id :E;aux :x; preserve the high-level type information(0 for non-pointers and atomic{x.dirty :1;aux :0; 1 for pointers). High-level objects are transformed to the low level by adding Figure 11.The Write Barrier for Boehm et al.GC the color and dirty fields with initial values WHITE and 0 re- spectively.Other addresses in the low-level heap domain [1..M] are filled out using unallocated objects whose colors are BLUE initialization process,the GC enters the concurrent mark-phase and all the other fields are initialized by 0.Here we use BLACK (line 4)and traces the objects reachable from the roots (i.e.,the and WHITE for marked and unmarked objects respectively,and mutators'local pointer variables that may contain references to BLUE for unallocated memory. the heap objects).A mark stack (mstk)is used to do a depth-first The concrete GC thread is given an initial store. tracing.During the tracing,the connectivity between objects might be changed by the mutators,thus a write barrier is required to notify The formal definition of T is included in the technical report [20] the collector of those modified objects by dirtying the objects' To prove Correct(T)in our framework,we apply Theorem 8, tags(called cards).When the tracing is done,the GC suspends all prove the refinement between low-level and high-level mutators. the mutators and re-traces from the dirty objects that have been and verify the GC code using a unary Rely-Guarantee-based logic marked (called card-cleaning,line 6 and 7).The stop-the-world phase is implemented by atomicfC.Finally,all the reachable Refinement proofs for mutator instructions.We first define the objects are ensured marked and the GC performs the concurrent a and s(t)relations. sweep-phase (line 8),in which unmarked objects are reclaimed a会{(x出{ts,h),(Π，H)l Usually in practice,there is also a concurrent card-cleaning phase ∀t∈dom(I).store_map(π(t),Π(t) (line 5)before the stop-the-world card-cleaning to reduce the pause A heap_map(h,H)A wfstate(Π，H)} time.The full GC code Ce is given in the technical report [20]. In o,the relation between low-level and high-level stores and heaps The write barrier is shown in Figure 11.where the dirty field are enforced by store_map and heap_map respectively.Their defi- is set after modifying the object's pointer field.Here we use a nitions reflect the state transformations we describe above,ignoring write-only auxiliary variable aux for each mutator thread to record the values of those high-level-invisible structures.It also requires the current object that the mutator is updating.We add aux only the well-formedness of high-level states. for the purpose of verification,so that we can easily specify the fine-grained property of the write barrier in the guarantees that For each mutator thread t,the (t)relation enforced at the immediately after updating the pointer field,the thread would do beginning and the end of each transformation unit (each high-level nothing else except setting the corresponding dirty field.The GC instruction)is stronger than a.It requires that the value of the does not use read barriers nor allocation barriers. auxiliary variable aux (see Figure 11)be a null pointer (OP): We first present the high-level and low-level program state mod- (t)≌an{(r,h),(L,H)|π(t)(aux)=0} els in Figure 12.The behaviors of the high-level abstract GC thread are defined as follows: The refinement between the write barrier at the low level and AbsGCStep the pointer update instruction at the high level is formulated as: {(Π，H),(Π，H) Il.reachable()(Π，H)=→H()=H(l)}, (t.update(r.id,E),R(t),Gwritehamer):()(t) saying that,the mutator stores and the reachable objects in the (t.(r.id:=E),R(t),Gwrite.pt), heap are remained unmodified.Here reachable()(II,H)means the where and G are the guarantees of the two-step object at the location l is reachable in H from the roots in II. write barrier and the high-level atomic write operation respectively 466{wfstate} 0 Collection() { 1 local mstk: Seq(Int); Loop Invariant: {wfstate ∗ (ownnp(mstk) ∧ mstk = )} 2 while (true) { 3 Initialize(); {(wfstate ∧ reach inv) ∗ (ownnp(mstk) ∧ mstk = )} 4 Trace(); {(wfstate ∧ reach inv) ∗ (ownnp(mstk) ∧ mstk = )} 5 CleanCard(); {(wfstate ∧ reach inv) ∗ (ownnp(mstk) ∧ mstk = )} atomic{ 6 ScanRoot(); {∃X.(wfstate ∧ reach rtnw stk(X) ∧ stk black(X)) ∗(ownnp(mstk) ∧ mstk = X)} 7 CleanCard(); } {(wfstate ∧ reach black) ∗ (ownnp(mstk) ∧ mstk = )} 8 Sweep(); } } {false} Figure 10. Outline of the GC Code and Proof Sketch update(x.id, E) { // id ∈ {pt1, ..., ptm} atomic{ x.id := E; aux := x; } atomic{ x.dirty := 1; aux := 0; } } Figure 11. The Write Barrier for Boehm et al. GC initialization process, the GC enters the concurrent mark-phase (line 4) and traces the objects reachable from the roots (i.e., the mutators’ local pointer variables that may contain references to the heap objects). A mark stack (mstk) is used to do a depth-first tracing. During the tracing, the connectivity between objects might be changed by the mutators, thus a write barrier is required to notify the collector of those modified objects by dirtying the objects’ tags (called cards). When the tracing is done, the GC suspends all the mutators and re-traces from the dirty objects that have been marked (called card-cleaning, line 6 and 7). The stop-the-world phase is implemented by atomic{C}. Finally, all the reachable objects are ensured marked and the GC performs the concurrent sweep-phase (line 8), in which unmarked objects are reclaimed. Usually in practice, there is also a concurrent card-cleaning phase (line 5) before the stop-the-world card-cleaning to reduce the pause time. The full GC code Cgc is given in the technical report [20]. The write barrier is shown in Figure 11, where the dirty field is set after modifying the object’s pointer field. Here we use a write-only auxiliary variable aux for each mutator thread to record the current object that the mutator is updating. We add aux only for the purpose of verification, so that we can easily specify the fine-grained property of the write barrier in the guarantees that immediately after updating the pointer field, the thread would do nothing else except setting the corresponding dirty field. The GC does not use read barriers nor allocation barriers. We first present the high-level and low-level program state mod￾els in Figure 12. The behaviors of the high-level abstract GC thread are defined as follows: AbsGCStep {((Π, H), (Π, H )) | ∀l. reachable(l)(Π, H) =⇒ H(l) = H (l)} , saying that, the mutator stores and the reachable objects in the heap are remained unmodified. Here reachable(l)(Π, H) means the object at the location l is reachable in H from the roots in Π. (HStore) S ∈ PVar  HVal (HHeap) H ∈ Loc  HObj (HThrds) Π ∈ MutID → HStore (HState) Σ ∈ HThrds × HHeap (LStore) s ∈ PVar  LVal×{0, 1} (LHeap) h ∈ [1..M]  LObj (LThrds) π ∈ ThrdID → LStore (LState) σ ∈ LThrds × LHeap Figure 12. High-Level and Low-Level State Models The transformation. The transformation T is defined as follows. For code, the high-level abstract GC thread is transformed to the GC thread shown in Figure 10. Each instruction x.id := E in mutators is transformed to the write barrier, where id is a pointer field of x. Other instructions and the program structures of mutators are unchanged. The following transformations are made over initial states. • First we require the high-level initial state to be well-formed: wfstate(Π, H) ∀l. reachable(l)(Π, H) =⇒ l ∈ dom(H) . That is, reachable locations cannot be dangling pointers. • High-level locations are transformed to integers by a bijective function Loc2Int : Loc ↔ [0..M] satisfying Loc2Int(nil)=0. • Variables are transformed to the low level using an extra bit to preserve the high-level type information (0 for non-pointers and 1 for pointers). • High-level objects are transformed to the low level by adding the color and dirty fields with initial values WHITE and 0 re￾spectively. Other addresses in the low-level heap domain [1..M] are filled out using unallocated objects whose colors are BLUE and all the other fields are initialized by 0. Here we use BLACK and WHITE for marked and unmarked objects respectively, and BLUE for unallocated memory. • The concrete GC thread is given an initial store. The formal definition of T is included in the technical report [20]. To prove Correct(T) in our framework, we apply Theorem 8, prove the refinement between low-level and high-level mutators, and verify the GC code using a unary Rely-Guarantee-based logic. Refinement proofs for mutator instructions. We first define the α and ζ(t) relations. α {((π  {tgc }, h),(Π, H)) | ∀t ∈ dom(Π). store map(π(t), Π(t)) ∧ heap map(h, H) ∧ wfstate(Π, H)} . In α, the relation between low-level and high-level stores and heaps are enforced by store map and heap map respectively. Their defi- nitions reflect the state transformations we describe above, ignoring the values of those high-level-invisible structures. It also requires the well-formedness of high-level states. For each mutator thread t, the ζ(t) relation enforced at the beginning and the end of each transformation unit (each high-level instruction) is stronger than α. It requires that the value of the auxiliary variable aux (see Figure 11) be a null pointer (0p ): ζ(t) α ∩ {((π, h),(Π, H)) | π(t)(aux)=0p } . The refinement between the write barrier at the low level and the pointer update instruction at the high level is formulated as: (t.update(x.id, E), R(t), Gt write barrier) α;ζ(t)ζ(t) (t.(x.id := E), R(t), Gt write pt), where Gt write barrier and Gt write pt are the guarantees of the two-step write barrier and the high-level atomic write operation respectively. 466