We could verify the GC system by using a Hoare-style logic to Its relies should include all the possible guarantees made by other prove that the GC thread and the barriers satisfy their specifications. threads,and the GC's abstract and concrete behaviors respectively: However,we say this is an indirect approach because it is unclear R(t) if the specified correct behaviors would indeed make the mutators ≌AbsGCStep UU=G(t); (7.2) happy and generate the abstract view for high-level programmers. R(t)Ggc UvzG(t'). Usually this part is examined by experts and then trusted. The Re used to verify the GC code can now be defined below: Here we propose a more direct approach.We view a concurrent Rc≌U,G(t) (7.3) garbage collecting system as a transformation T from a high-level garbage-collected language to a low-level language.A standard The refinement proof also needs definitions of binary a,C and atomic memory operation at the source level is transformed into the y relations.The invariant a relates the low-level and the high-level corresponding barrier code at the target level.In the source level, states and needs to be preserved by each low-level step.In general we assume there is an abstract GC thread that magically turns a high-level state can be mapped to a low-level state o by giving unreachable objects into reusable memory.The abstract collector a concrete local store for the GC thread,adding additional struc- AbsGC is transformed into the concrete GC code Ce running tures in the heap (to record information for collection),renaming concurrently with the target mutators.That is, heap cells (for copying GCs),etc..For each mutator thread t,the T(tseAbsGClt1.C...tn.Cn) relations s(t)and (t)need to hold at the beginning and the end of tge.Cge llti.T(C)Il...Itn.T(Cn) each basic transformation unit (every high-level primitive instruc- tion in this case)respectively.We let (t)be the same as s(t)to where T(C)simply translates some memory access instructions in support sequential compositions.We require InitRelr((t))(see C into the corresponding barriers,and leaves the rest unchanged. Figure 6),i.e.,(t)holds over the initial states.In addition,the tar- Then we reduce the correctness of the concurrent garbage col- get and the source boolean expressions should be evaluated to the lecting system to Correct(T),saying that any mutator program will same value under related states,as required in the IF and WHILE not have unexpected behaviors when executed using this system. rules in Figure 7. 7.2 A General Framework GoodT(C(t))InitRelr(C(t))AVB.C(t)C (T(B)B)(7.4) The compositionality of RGSim allows us to develop a general Theorem 8(Verifying Concurrent Garbage Collecting Systems). framework to prove Correct(T),which cannot be done by mono- If there exist Rge,Gge,pge.R(t).R(t).C(t)and a such that (7.1). lithic proof methods.By the parallel compositionality of RGSim (7.2),(7.3),(7.4)and the following hold: (the PAR rule in Figure 7),we can decompose the refinement proofs 1.(Verification of the GC code) into proofs for the GC thread and each mutator thread. Rge;Gge F [pge }Cgeffalse}: Verifying the GC.The semantics of the abstract GC thread can 2.(Correctness of T on mutator instructions) be defined by a binary state predicate AbsGCStep: Vc.(t.T(c),R(t),G(t)):c()()(t.c,R(t),G(t)): (∑，∑)∈AbsGCStep 3.(Side conditions) (tgeAbsGC,)→(tge.AbsGC,D） Gge(AbsGCStep)": That is,the abstract GC thread always makes AbsGCStep to change Va,∑.g=T(∑)=→pge0; the high-level state.We can choose different AbsGCStep for differ- then Correct(T) ent GCs,but usually AbsGCStep guarantees not modifying reach- able objects in the heap. That is,to verify a concurrent garbage collecting system,we need to do the following: Thus for the GC thread,we need to show that Cae is simulated by AbsGC when executed in their environments.This can be re- .Define the a and (t)relations,and prove the correctness of T duced to unary Rely-Guarantee reasoning about Cge by proving on high-level primitive instructions.Since T preserves the syn- R;Gge[pge}Cge{}in a standard Rely-Guarantee logic with tax on most instructions,it's often immediate to prove the target proper Rge.ge,Pge and qge,as long as Gge is a concrete repre- instructions are simulated by their sources.But for instructions sentation of AbsGCStep.The judgment says given an initial state that are transformed to barriers,we need to verify the barriers satisfying the precondition pge.if the environment's behaviors sat- that they implement both the source instructions (by RGSim) isfy Rge,then each step of Cse satisfies Gse,and the postcondition and the interaction mechanism(shown in their guarantees). s holds at the end if Cge terminates.In general,the collector never Find some proper Gse and pge,and verify the GC code by R-G terminates,thus we can let gse be false.Ge and pa should be pro- reasoning.We require the GC's guarantee Gge should not con- vided by the verifier.where pge needs to be general enough that can tain more behaviors than AbsGCStep(the first side condition). be satisfied by any possible low-level initial state.R encodes the and Cge can start its execution from any state o transformed possible behaviors of mutators,which can be derived,as we will from a high-level one (the second side condition). show below. 7.3 Application:Boehm et al.Concurrent GC Algorithm Verifying mutators.For the mutator thread,since T is syntax- directed on C,we can reduce the refinement problem for arbitrary We illustrate the applications of the framework (Theorem 8) mutators to the refinement on each primitive instruction only,by the by proving the correctness of a mostly-concurrent mark-sweep compositionality of RGSim.The proof needs proper rely/guarantee garbage collector proposed by Boehm et al.[7].Variants of the conditions.Let G(t.c)and C(t.T(c))denote the guarantees of the algorithm have been used in practice (e.g.,by IBM [2]).Due to source instruction c and the target code T(c)respectively.Then we the space limit,we only describe the proof sketch here.Details are can define the general guarantees for a mutator thread t: presented in the technical report [20]. G(t)≌U.G(t.c); g(t)U.G(t.T(c)). (7.1) Overview of the GC algorithm.The top-level code of the GC thread is shown in Figure 10.In each collection cycle,after an 465We could verify the GC system by using a Hoare-style logic to prove that the GC thread and the barriers satisfy their specifications. However, we say this is an indirect approach because it is unclear if the specified correct behaviors would indeed make the mutators happy and generate the abstract view for high-level programmers. Usually this part is examined by experts and then trusted. Here we propose a more direct approach. We view a concurrent garbage collecting system as a transformation T from a high-level garbage-collected language to a low-level language. A standard atomic memory operation at the source level is transformed into the corresponding barrier code at the target level. In the source level, we assume there is an abstract GC thread that magically turns unreachable objects into reusable memory. The abstract collector AbsGC is transformed into the concrete GC code Cgc running concurrently with the target mutators. That is, T(tgc.AbsGCt1.C1...tn.Cn) tgc.Cgc t1.T(C1)...tn.T(Cn), where T(C) simply translates some memory access instructions in C into the corresponding barriers, and leaves the rest unchanged. Then we reduce the correctness of the concurrent garbage col￾lecting system to Correct(T), saying that any mutator program will not have unexpected behaviors when executed using this system. 7.2 A General Framework The compositionality of RGSim allows us to develop a general framework to prove Correct(T), which cannot be done by mono￾lithic proof methods. By the parallel compositionality of RGSim (the PAR rule in Figure 7), we can decompose the refinement proofs into proofs for the GC thread and each mutator thread. Verifying the GC. The semantics of the abstract GC thread can be defined by a binary state predicate AbsGCStep: (Σ, Σ ) ∈ AbsGCStep (tgc.AbsGC, Σ) −→ (tgc.AbsGC, Σ ) That is, the abstract GC thread always makes AbsGCStep to change the high-level state. We can choose different AbsGCStep for differ￾ent GCs, but usually AbsGCStep guarantees not modifying reach￾able objects in the heap. Thus for the GC thread, we need to show that Cgc is simulated by AbsGC when executed in their environments. This can be re￾duced to unary Rely-Guarantee reasoning about Cgc by proving Rgc; Ggc  {pgc}Cgc{qgc} in a standard Rely-Guarantee logic with proper Rgc, Ggc, pgc and qgc, as long as Ggc is a concrete repre￾sentation of AbsGCStep. The judgment says given an initial state satisfying the precondition pgc, if the environment’s behaviors sat￾isfy Rgc, then each step of Cgc satisfies Ggc, and the postcondition qgc holds at the end if Cgc terminates. In general, the collector never terminates, thus we can let qgc be false. Ggc and pgc should be pro￾vided by the verifier, where pgc needs to be general enough that can be satisfied by any possible low-level initial state. Rgc encodes the possible behaviors of mutators, which can be derived, as we will show below. Verifying mutators. For the mutator thread, since T is syntax￾directed on C, we can reduce the refinement problem for arbitrary mutators to the refinement on each primitive instruction only, by the compositionality of RGSim. The proof needs proper rely/guarantee conditions. Let G(t.c) and G(t.T(c)) denote the guarantees of the source instruction c and the target code T(c) respectively. Then we can define the general guarantees for a mutator thread t: G(t) c G(t.c) ; G(t) c G(t.T(c)). (7.1) Its relies should include all the possible guarantees made by other threads, and the GC’s abstract and concrete behaviors respectively: R(t) AbsGCStep ∪ t=t G(t ) ; R(t) Ggc ∪ t=t G(t ). (7.2) The Rgc used to verify the GC code can now be defined below: Rgc t G(t). (7.3) The refinement proof also needs definitions of binary α, ζ and γ relations. The invariant α relates the low-level and the high-level states and needs to be preserved by each low-level step. In general, a high-level state Σ can be mapped to a low-level state σ by giving a concrete local store for the GC thread, adding additional struc￾tures in the heap (to record information for collection), renaming heap cells (for copying GCs), etc.. For each mutator thread t, the relations ζ(t) and γ(t) need to hold at the beginning and the end of each basic transformation unit (every high-level primitive instruc￾tion in this case) respectively. We let γ(t) be the same as ζ(t) to support sequential compositions. We require InitRelT(ζ(t)) (see Figure 6), i.e., ζ(t) holds over the initial states. In addition, the tar￾get and the source boolean expressions should be evaluated to the same value under related states, as required in the IF and WHILE rules in Figure 7. GoodT(ζ(t)) InitRelT(ζ(t))∧∀B. ζ(t) ⊆ (T(B)⇔⇔B) (7.4) Theorem 8 (Verifying Concurrent Garbage Collecting Systems). If there exist Rgc, Ggc, pgc, R(t), R(t), ζ(t) and α such that (7.1), (7.2), (7.3), (7.4) and the following hold: 1. (Verification of the GC code) Rgc; Ggc  {pgc}Cgc{false}; 2. (Correctness of T on mutator instructions) ∀c. (t.T(c), R(t), G(t)) α;ζ(t)ζ(t) (t.c, R(t), G(t)); 3. (Side conditions) Ggc ◦ α−1 ⊆ α−1 ◦ (AbsGCStep) ∗; ∀σ, Σ. σ = T(Σ) =⇒ pgc σ; then Correct(T). That is, to verify a concurrent garbage collecting system, we need to do the following: • Define the α and ζ(t) relations, and prove the correctness of T on high-level primitive instructions. Since T preserves the syn￾tax on most instructions, it’s often immediate to prove the target instructions are simulated by their sources. But for instructions that are transformed to barriers, we need to verify the barriers that they implement both the source instructions (by RGSim) and the interaction mechanism (shown in their guarantees). • Find some proper Ggc and pgc, and verify the GC code by R-G reasoning. We require the GC’s guarantee Ggc should not con￾tain more behaviors than AbsGCStep (the first side condition), and Cgc can start its execution from any state σ transformed from a high-level one (the second side condition). 7.3 Application: Boehm et al. Concurrent GC Algorithm We illustrate the applications of the framework (Theorem 8) by proving the correctness of a mostly-concurrent mark-sweep garbage collector proposed by Boehm et al. [7]. Variants of the algorithm have been used in practice (e.g., by IBM [2]). Due to the space limit, we only describe the proof sketch here. Details are presented in the technical report [20]. Overview of the GC algorithm. The top-level code of the GC thread is shown in Figure 10. In each collection cycle, after an 465