A:6 Hongjin Liang et al. 2.5.Our Approach In this paper we propose a Rely-Guarantee-based Simulation(RGSim)<between the target and the source programs.It establishes a weak simulation,ensuring that for every externally observable 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 implementation 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 [Jones 1983],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 possible 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 other.Then we can verify their parallel composition by separately verifying 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 intersection 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 environment 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 environment R,and the state transi- tions 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 parallel com- positionality lemma is in the following form.If we know (C1,R1,91)(C1,R1,G1) and(C2,R2,92)(C2,R2,G2),and also the interference constraints are satisfied,i.e., g2≤R1,g1≤R2,G2∈R1 and GICR2,we could get (C1‖C2,R1nR2,G1Ug2)≤(C1‖C2,R1∩R2,G1UG2) The compositionality of RGSim gives us a proof theory for concurrent program trans- formations. Also different from fully abstract semantics for threads,which assumes arbitrary be- haviors of environments,RGSim allows us to instantiate the interference R,C,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. Example.Below we give an example of loop invariant hoisting to illustrate how RGSim works.The formal proofs are shown in Section 5.2.1. Target Code(C1) Source Code(C) local t; local t; t:=x+1; while(i<n){ while(i n){ t:=x+1; i:=i t; i :i +t; 2 ACM Transactions on Programming Languages and Systems,Vol.V,No.N,Article A,Publication date:January YYYY.A:6 Hongjin Liang et al. 2.5. Our Approach In this paper we propose a Rely-Guarantee-based Simulation (RGSim) ≼ between the target and the source programs. It establishes a weak simulation, ensuring that for every externally observable 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 implementation 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 [Jones 1983], 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 possible 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 other. Then we can verify their parallel composition by separately verifying 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 intersection 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 environment 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 environment R, and the state transi￾tions 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 parallel com￾positionality 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 concurrent program trans￾formations. Also different from fully abstract semantics for threads, which assumes arbitrary be￾haviors 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. Example. Below we give an example of loop invariant hoisting to illustrate how RGSim works. The formal proofs are shown in Section 5.2.1. Target Code (C1) local t; t := x + 1; while(i < n) { i := i + t; } ⇐ Source Code (C) local t; while(i < n) { t := x + 1; i := i + t; } ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Article A, Publication date: January YYYY