Many concurrent languages (e.g.,C++[6])do not give seman- condition R of a thread specifies the permitted state transitions that tics to programs with data races (like the examples shown in its environment may have,and its guarantee G specifies the possi- Figure 1).Therefore the compilers only need to guarantee the ble transitions made by the thread itself.To ensure parallel threads semantics preservation of data-race-free programs. can collaborate,we need to check the interference constraint,i.e., When we prove that a fine-grained implementation of a concur- the guarantee of each thread is permitted in the rely of every others. rent object is a refinement of an abstract atomic operation,we Then we can verify their parallel composition by separately veri can assume that all accesses to the object in the context of the fying each thread,showing its behaviors under the rely condition target program use the same set of primitives. indeed satisfy its guarantee.After parallel composition,the threads should be executed under their common environment (i.e.,the in- Usually the implementation of STM (e.g.,TL2 [11])ensures tersection of their relies)and guarantee all the possible transitions the atomicity of a transaction atomicC only when there are made by them (i.e.,the union of their guarantees). no data races.Therefore,the correctness of the transformation from high-level atomic blocks to fine-grained concurrent code Parametrized with rely/guarantee conditions for the two levels. assumes data-race-freedom in the source. our relation (C,R,g)(C,R,G)talks about not only the target C and the source C,but also the interference R and g between C Many garbage-collected languages are type-safe and prohibit and its target-level environment,and R and G between C and its en- operations such as pointer arithmetics.Therefore the garbage vironment at the source level.Informally,(C,R,g)(C,R,G) collector could make corresponding assumptions about the mu- says the executions of C under the environment R do not exhibit tators that run in parallel. more observable behaviors than the executions of C under the en- In all these cases,the transformations of individual threads are vironment R,and the state transitions of C and C satisfy g and G allowed to make various assumptions about the environments.They respectively.RGSim is now compositional,as long as the threads do not have to ensure semantics preservation within all contexts are composed with well-behaved environments only.The paral- lel compositionality lemma is in the following form.If we know 2.3 Languages at Source and Target May Be Different (C1,R1,91)≤(C1,R1,G1)and(C2,R2,92)(C2,R2,G2), The use of different languages at the source and the target levels and also the interference constraints are satisfied,i.e.,92 C Ri, GI C R2.G2C RI and GIC R2,we could get makes the formulation of the transformation correctness more dif- ficult.If the source and the target languages have different views of (C1lC2,R1∩R2,g1Ug2)(C1‖C2,R1nR2,G1UG2). program states and different atomic primitives,we cannot directly compare the state transitions made by the source and the target pro- The compositionality of RGSim gives us a proof theory for concur- rent program transformations. grams.This is another reason that makes the aforementioned subset relation between sets of program traces in fully abstract semantics Also different from fully abstract semantics for threads.which infeasible.For the same reason,many existing techniques for prov- assumes arbitrary behaviors of environments,RGSim allows us to ing refinement or equivalence of programs in the same language instantiate the interference R,C,R and G differently for different cannot be applied either. assumptions about environments,therefore it can be used to verify the aforementioned four classes of transformations.For instance.if 2.4 Different Observers Make Different Observations we want to prove that a transformation preserves the behaviors of Concurrency introduces tensions between two kinds of observers: data-race-free programs,we can specify the data-race-freedom in human beings(as external observers)and the parallel program con- R and G.Then we are no longer concerned with the examples in texts.External observers do not care about the implementation de- Figure 1.both of which have data races. tails of the source and the target programs.For them,intermediate state accesses (such as memory reads and writes)are silent steps 3. Basic Technical Settings (unobservable),and only external events(such as I/O operations) In this section,we present the source and the target programming are observable.On the other hand,state accesses have effects on languages.Then we define a basic refinement C,which naturally the parallel program contexts,and are not silent to them. says the target has no more externally observable event traces than If the refinement relation relates externally observable event the source.We use as an intuitive formulation of the correctness traces only,it cannot have parallel compositionality,as we ex- of transformations. plained in Section 2.1.On the other hand,relating all state ac- cesses of programs is too strong.Any reordering of state accesses 3.1 The Languages or change of atomicity would fail the refinement. Following standard simulation techniques,we model the seman- 2.5 Our Approach tics of target and source programs as labeled transition systems. Before showing the languages,we first define events and labels in In this paper we propose a Rely-Guarantee-based Simulation Figure 2(a).We leave the set of events unspecified here.It can be (RGSim)<between the target and the source programs.It es- instantiated by program verifiers,depending on their interest (e.g., tablishes a weak simulation,ensuring that for every externally ob- input/output events).A label that will be associated with a state servable event made by the target program there is a corresponding transition is either an event or T,which means the corresponding one in the source.We choose to view intermediate state accesses transition does not generate any event (i.e.,a silent step). as silent steps,thus we can relate programs with different imple- mentation details.This also makes our simulation independent of The target language,which we also call the low-level language, language details. is shown in Figure 2(b).We abstract away the forms of states,ex- pressions and primitive instructions in the language.An arithmetic To support parallel compositionality,our relation takes into expression E is modeled as a function from states to integers lifted account explicitly the expected interference between threads and with an undefined value L.Boolean expressions are modeled sim their parallel environments.Inspired by the Rely-Guarantee (R- ilarly.An instruction is a partial function from states to sets of la- G)verification method [17],we specify the interference using bel and state pairs,describing the state transitions and the events it rely/guarantee conditions.In Rely-Guarantee reasoning,the rely generates.We use P(-)to denote the power set.Unsafe executions 457• Many concurrent languages (e.g., C++ [6]) do not give seman￾tics to programs with data races (like the examples shown in Figure 1). Therefore the compilers only need to guarantee the semantics preservation of data-race-free programs. • When we prove that a fine-grained implementation of a concur￾rent object is a refinement of an abstract atomic operation, we can assume that all accesses to the object in the context of the target program use the same set of primitives. • Usually the implementation of STM (e.g., TL2 [11]) ensures the atomicity of a transaction atomic{C} only when there are no data races. Therefore, the correctness of the transformation from high-level atomic blocks to fine-grained concurrent code assumes data-race-freedom in the source. • Many garbage-collected languages are type-safe and prohibit operations such as pointer arithmetics. Therefore the garbage collector could make corresponding assumptions about the mu￾tators that run in parallel. In all these cases, the transformations of individual threads are allowed to make various assumptions about the environments. They do not have to ensure semantics preservation within all contexts. 2.3 Languages at Source and Target May Be Different The use of different languages at the source and the target levels makes the formulation of the transformation correctness more dif- ficult. If the source and the target languages have different views of program states and different atomic primitives, we cannot directly compare the state transitions made by the source and the target pro￾grams. This is another reason that makes the aforementioned subset relation between sets of program traces in fully abstract semantics infeasible. For the same reason, many existing techniques for prov￾ing refinement or equivalence of programs in the same language cannot be applied either. 2.4 Different Observers Make Different Observations Concurrency introduces tensions between two kinds of observers: human beings (as external observers) and the parallel program con￾texts. External observers do not care about the implementation de￾tails of the source and the target programs. For them, intermediate state accesses (such as memory reads and writes) are silent steps (unobservable), and only external events (such as I/O operations) are observable. On the other hand, state accesses have effects on the parallel program contexts, and are not silent to them. If the refinement relation relates externally observable event traces only, it cannot have parallel compositionality, as we ex￾plained in Section 2.1. On the other hand, relating all state ac￾cesses of programs is too strong. Any reordering of state accesses or change of atomicity would fail the refinement. 2.5 Our Approach In this paper we propose a Rely-Guarantee-based Simulation (RGSim)  between the target and the source programs. It es￾tablishes a weak simulation, ensuring that for every externally ob￾servable event made by the target program there is a corresponding one in the source. We choose to view intermediate state accesses as silent steps, thus we can relate programs with different imple￾mentation details. This also makes our simulation independent of language details. To support parallel compositionality, our relation takes into account explicitly the expected interference between threads and their parallel environments. Inspired by the Rely-Guarantee (R￾G) verification method [17], we specify the interference using rely/guarantee conditions. In Rely-Guarantee reasoning, the rely condition R of a thread specifies the permitted state transitions that its environment may have, and its guarantee G specifies the possi￾ble transitions made by the thread itself. To ensure parallel threads can collaborate, we need to check the interference constraint, i.e., the guarantee of each thread is permitted in the rely of every others. Then we can verify their parallel composition by separately veri￾fying each thread, showing its behaviors under the rely condition indeed satisfy its guarantee. After parallel composition, the threads should be executed under their common environment (i.e., the in￾tersection of their relies) and guarantee all the possible transitions made by them (i.e., the union of their guarantees). Parametrized with rely/guarantee conditions for the two levels, our relation (C, R, G)  (C, R, G) talks about not only the target C and the source C, but also the interference R and G between C and its target-level environment, and R and G between C and its en￾vironment at the source level. Informally, (C, R, G)  (C, R, G) says the executions of C under the environment R do not exhibit more observable behaviors than the executions of C under the en￾vironment R, and the state transitions of C and C satisfy G and G respectively. RGSim is now compositional, as long as the threads are composed with well-behaved environments only. The paral￾lel compositionality lemma is in the following form. If we know (C1, R1, G1)  (C1, R1, G1) and (C2, R2, G2)  (C2, R2, G2), and also the interference constraints are satisfied, i.e., G2 ⊆ R1, G1 ⊆ R2, G2 ⊆ R1 and G1 ⊆ R2, we could get (C1 C2, R1 ∩ R2, G1 ∪ G2)  (C1 C2, R1 ∩ R2, G1 ∪ G2). The compositionality of RGSim gives us a proof theory for concur￾rent program transformations. Also different from fully abstract semantics for threads, which assumes arbitrary behaviors of environments, RGSim allows us to instantiate the interference R, G, R and G differently for different assumptions about environments, therefore it can be used to verify the aforementioned four classes of transformations. For instance, if we want to prove that a transformation preserves the behaviors of data-race-free programs, we can specify the data-race-freedom in R and G. Then we are no longer concerned with the examples in Figure 1, both of which have data races. 3. Basic Technical Settings In this section, we present the source and the target programming languages. Then we define a basic refinement , which naturally says the target has no more externally observable event traces than the source. We use as an intuitive formulation of the correctness of transformations. 3.1 The Languages Following standard simulation techniques, we model the seman￾tics of target and source programs as labeled transition systems. Before showing the languages, we first define events and labels in Figure 2(a). We leave the set of events unspecified here. It can be instantiated by program verifiers, depending on their interest (e.g., input/output events). A label that will be associated with a state transition is either an event or τ , which means the corresponding transition does not generate any event (i.e., a silent step). The target language, which we also call the low-level language, is shown in Figure 2(b). We abstract away the forms of states, ex￾pressions and primitive instructions in the language. An arithmetic expression E is modeled as a function from states to integers lifted with an undefined value ⊥. Boolean expressions are modeled sim￾ilarly. An instruction is a partial function from states to sets of la￾bel and state pairs, describing the state transitions and the events it generates. We use P( ) to denote the power set. Unsafe executions 457