Since the transformation of other high-level instructions is identity, simulations.They focus on correctness of a particular compiler,and the corresponding refinement proofs are simple. there are two phases in their compiler whose proofs are not compo Rely-Guarantee reasoning about the GC code.The unary pro- sitional.Here we provide a general,compiler-independent,compo sitional proof technique to verify concurrent transformations. gram logic we use to verify the GC thread is a standard Rely- Guarantee logic adapted to the target language.We describe states We apply RGSim to justify concurrent optimizations.following using separation logic assertions,as shown below: Benton [3]who presents a declarative set of rules for sequential p,q::=B I t.ownp(x)t.ownap(x)I E1.id E2 Ip*gl... optimizations.Also the proof rules of RGSim for sequential com- positions,conditional statements and loops coincide with those in Following Parkinson et al.[23],we treat program variables as re- relational Hoare logic [3]and relational separation logic [321. source and use t.ownp()and t.ownp()for the thread t's owner- Proving linearizability or atomicity of concurrent objects.Fil- ships of pointers and non-pointers respectively.We omit the thread identifiers if these predicates hold for the current thread. ipovic et al.[13]show linearizability can be characterized in terms of an observational refinement,where the latter is defined similarly We first give the precondition and the guarantee of the GC.The to our Correct(T).There is no proof method given to verify the GC starts its executions from a low-level well-formed state,i.e. linearizability of fine-grained object implementations. Pwfstate.Just corresponding to the high-level wfstate defi- nition,the low-level wfstate predicate says none of the reachable Turon and Wand [27]propose a refinement-based proof method objects are BLUE.We define Gae as follows: to verify concurrent objects.They first propose a simple refinement based on Brookes'fully abstract trace semantics [8],which is com- 9ge兰{(（π世{tgcs},h,(红{tg一s,h') positional but cannot handle complex algorithms (as discussed in Vn.reachable(n)(,h) Section 2.2).Their fenced refinement then uses rely conditions to →h(n)=lh'(n)l filter out illegal environment transitions.The basic idea is similar to ∧h(n).color≠BLUE A h'(n).color≠BLUE}. ours,and the refinement can also be used to verify Treiber's stack The GC guarantees not modifying the mutator stores.For any algorithm.However,it is "not a congruence for parallel composi- mutator-reachable object,the GC does not update its fields coming tion".In their settings,both the concrete (fine-grained)and the ab from the high-level mutator,nor does it reclaim the object.Here- stract (atomic)versions of object operations need to be expressed lifts a low-level object to a new one that contains mutator data only. in the same language.They also require that the fine-grained im plementation should have only one update action over the shared The proof sketch is given in Figure 10.One of the key invariants state to correspond to the high-level atomic operation.These re- used in the proof is reach_inv,which says any WHITE reachable quirements and the lack of parallel compositionality limit the ap- object can either be traced from a root object in a path on which plicability of their method.It is unclear if the method can be used every object is WHITE,or be reachable from a BLACK object whose for general verification of transformations,such as concurrent GCs pointer field was updated and dirty bit was set to 1.Since the proof is done in the unary logic,the details here are orthogonal Elmas et al.[12]prove linearizability by incrementally rewrit- to our simulation-based proof (but it is RGSim that allows us to ing the fine-grained implementation to the atomic abstract speci- derive Theorem 8,which then links proofs in the unary logic with fication.Their behavioral simulation used to characterize lineariz- relational proofs).We give the complete proofs in the technical ability is an event-trace subset relation with requirements on the report [20]. orders of method invocations and returns.Their rules heavily rely on movers (i.e.,operations that can commute over any operation of 8. Related Work and Conclusion other threads)and always rewrite programs to instructions,thus are designed specifically for atomicity verification. There is a large body of work on refinements and verification of program transformations.Here we only focus on the work most In his thesis [28].Vafeiadis proves linearizability of concurrent closely related to the typical applications discussed in this paper. objects in RGSep logic by introducing abstract objects and abstract atomic operations as auxiliary variables and code.The refinement Verifying compilation and optimizations of concurrent programs. between the concrete implementation and the abstract operation is Compiler verification for concurrent programming languages can implicitly embodied in the unary verification process,but is not date back to work by Wand [31]and Gladstein et al.[14].which spelled out formally in the meta-theory (e.g.,the soundness). is about functional languages using message-passing mechanisms Recently,Lochbihler [21]presents a verified compiler for Java Verifying concurrent GCs.Vechev et al.[30]define transforma- threads and prove semantics preservation by a weak bisimulation. tions to generate concurrent GCs from an abstract collector.After- He views every heap update as an observable move,thus does not wards,Pavlovic et al.[24]present refinements to derive concrete allow the target and the source to have different granularities of concurrent GCs from specifications.These methods focus on de- scribing the behaviors of variants (or instantiations)of a correct ab- atomic updates.To achieve parallel compositionality,he requires stract collector (or a specification)in a single framework,assuming the relation to be preserved by any transitions of shared states i.e.,the environments are assumed arbitrary.As we explained in all the mutator operations are atomic.By comparison,we provide Section 2.2,this is a too strong requirement in general for many a general correctness notion and a proof method for verifying con- transformations,including the examples in this paper. current GCs and the interactions with mutators (where the barriers could be fine-grained).Furthermore,the correctness of their trans- Burckhardt et al.[9]present a proof method for verifying con- formations or refinements is expressed in a GC-oriented way (e.g., current program transformations on relaxed memory models.The the target GC should mark no less objects than the source),which method relies on a compositional trace-based denotational seman- cannot be used to justify other transformations. tics,where the values of shared variables are always considered arbitrary at any program point.In other words,they also assume Kapoor et al.[18]verify Dijkstra's GC using concurrent sepa- arbitrary environments. ration logic.To validate the GC specifications,they also verify a representative mutator in the same system.In contrast,we reduce Following Leroy's CompCert project [19].Seveik et al.[25] the problem of verifying a concurrent GC to verifying a transfor- verify compilation from a C-like concurrent language to x86 by mation,ensuring semantics preservation for all mutators.Our GC 467Since the transformation of other high-level instructions is identity, the corresponding refinement proofs are simple. Rely-Guarantee reasoning about the GC code. The unary pro￾gram logic we use to verify the GC thread is a standard Rely￾Guarantee logic adapted to the target language. We describe states using separation logic assertions, as shown below: p, q ::= B | t.ownp(x) | t.ownnp(x) | E1.id → E2 | p ∗ q | ... Following Parkinson et al. [23], we treat program variables as re￾source and use t.ownp(x) and t.ownnp(x) for the thread t’s owner￾ships of pointers and non-pointers respectively. We omit the thread identifiers if these predicates hold for the current thread. We first give the precondition and the guarantee of the GC. The GC starts its executions from a low-level well-formed state, i.e., pgc wfstate. Just corresponding to the high-level wfstate defi- nition, the low-level wfstate predicate says none of the reachable objects are BLUE. We define Ggc as follows: Ggc {((π  {tgc s}, h), (π  {tgc s }, h )) | ∀n. reachable(n)(π, h) =⇒ h(n) = h (n) ∧ h(n).color = BLUE ∧ h (n).color = BLUE} . The GC guarantees not modifying the mutator stores. For any mutator-reachable object, the GC does not update its fields coming from the high-level mutator, nor does it reclaim the object. Here   lifts a low-level object to a new one that contains mutator data only. The proof sketch is given in Figure 10. One of the key invariants used in the proof is reach inv, which says any WHITE reachable object can either be traced from a root object in a path on which every object is WHITE, or be reachable from a BLACK object whose pointer field was updated and dirty bit was set to 1. Since the proof is done in the unary logic, the details here are orthogonal to our simulation-based proof (but it is RGSim that allows us to derive Theorem 8, which then links proofs in the unary logic with relational proofs). We give the complete proofs in the technical report [20]. 8. Related Work and Conclusion There is a large body of work on refinements and verification of program transformations. Here we only focus on the work most closely related to the typical applications discussed in this paper. Verifying compilation and optimizations of concurrent programs. Compiler verification for concurrent programming languages can date back to work by Wand [31] and Gladstein et al. [14], which is about functional languages using message-passing mechanisms. Recently, Lochbihler [21] presents a verified compiler for Java threads and prove semantics preservation by a weak bisimulation. He views every heap update as an observable move, thus does not allow the target and the source to have different granularities of atomic updates. To achieve parallel compositionality, he requires the relation to be preserved by any transitions of shared states, i.e., the environments are assumed arbitrary. As we explained in Section 2.2, this is a too strong requirement in general for many transformations, including the examples in this paper. Burckhardt et al. [9] present a proof method for verifying con￾current program transformations on relaxed memory models. The method relies on a compositional trace-based denotational seman￾tics, where the values of shared variables are always considered arbitrary at any program point. In other words, they also assume arbitrary environments. Following Leroy’s CompCert project [19], Sev ˇ cˇ´ık et al. [25] verify compilation from a C-like concurrent language to x86 by simulations. They focus on correctness of a particular compiler, and there are two phases in their compiler whose proofs are not compo￾sitional. Here we provide a general, compiler-independent, compo￾sitional proof technique to verify concurrent transformations. We apply RGSim to justify concurrent optimizations, following Benton [3] who presents a declarative set of rules for sequential optimizations. Also the proof rules of RGSim for sequential com￾positions, conditional statements and loops coincide with those in relational Hoare logic [3] and relational separation logic [32]. Proving linearizability or atomicity of concurrent objects. Fil￾ipovic´ et al. [13] show linearizability can be characterized in terms of an observational refinement, where the latter is defined similarly to our Correct(T). There is no proof method given to verify the linearizability of fine-grained object implementations. Turon and Wand [27] propose a refinement-based proof method to verify concurrent objects. They first propose a simple refinement based on Brookes’ fully abstract trace semantics [8], which is com￾positional but cannot handle complex algorithms (as discussed in Section 2.2). Their fenced refinement then uses rely conditions to filter out illegal environment transitions. The basic idea is similar to ours, and the refinement can also be used to verify Treiber’s stack algorithm. However, it is “not a congruence for parallel composi￾tion”. In their settings, both the concrete (fine-grained) and the ab￾stract (atomic) versions of object operations need to be expressed in the same language. They also require that the fine-grained im￾plementation should have only one update action over the shared state to correspond to the high-level atomic operation. These re￾quirements and the lack of parallel compositionality limit the ap￾plicability of their method. It is unclear if the method can be used for general verification of transformations, such as concurrent GCs. Elmas et al. [12] prove linearizability by incrementally rewrit￾ing the fine-grained implementation to the atomic abstract speci- fication. Their behavioral simulation used to characterize lineariz￾ability is an event-trace subset relation with requirements on the orders of method invocations and returns. Their rules heavily rely on movers (i.e., operations that can commute over any operation of other threads) and always rewrite programs to instructions, thus are designed specifically for atomicity verification. In his thesis [28], Vafeiadis proves linearizability of concurrent objects in RGSep logic by introducing abstract objects and abstract atomic operations as auxiliary variables and code. The refinement between the concrete implementation and the abstract operation is implicitly embodied in the unary verification process, but is not spelled out formally in the meta-theory (e.g., the soundness). Verifying concurrent GCs. Vechev et al. [30] define transforma￾tions to generate concurrent GCs from an abstract collector. After￾wards, Pavlovic et al. [24] present refinements to derive concrete concurrent GCs from specifications. These methods focus on de￾scribing the behaviors of variants (or instantiations) of a correct ab￾stract collector (or a specification) in a single framework, assuming all the mutator operations are atomic. By comparison, we provide a general correctness notion and a proof method for verifying con￾current GCs and the interactions with mutators (where the barriers could be fine-grained). Furthermore, the correctness of their trans￾formations or refinements is expressed in a GC-oriented way (e.g., the target GC should mark no less objects than the source), which cannot be used to justify other transformations. Kapoor et al. [18] verify Dijkstra’s GC using concurrent sepa￾ration logic. To validate the GC specifications, they also verify a representative mutator in the same system. In contrast, we reduce the problem of verifying a concurrent GC to verifying a transfor￾mation, ensuring semantics preservation for all mutators. Our GC 467