《计算机科学》相关教学资源（参考文献）A Rely-Guarantee-Based Simulation for Verifying Concurrent Program Transformations

A Rely-Guarantee-Based Simulation for Verifying Concurrent Program Transformations Hongjin Liang Xinyu Feng Ming Fu School of Computer Science and Technology,University of Science and Technology of China Hefei.Anhui 230026.China Ihj1018@mail.ustc.edu.cn xyfeng@ustc.edu.cn fumingOustc.edu.cn Abstract Correctness of compilation and optimizations of concurrent Verifying program transformations usually requires proving that programs.In this most natural program transformation verifica- the resulting program(the target)refines or is equivalent to the tion problem,every compilation phase does a program transfor- original one (the source).However,the refinement relation between mation T,which needs to preserve the semantics of the inputs individual sequential threads cannot be preserved in general with Atomicity of concurrent objects.A concurrent object or library the presence of parallel compositions,due to instruction reordering provides a set of methods that allow clients to manipulate the and the different granularities of atomic operations at the source shared data structure with abstract atomic behaviors [15].Their and the target.On the other hand,the refinement relation defined correctness can be reduced to the correctness of the transforma- based on fully abstract semantics of concurrent programs assumes tion from abstract atomic operations to concrete and executable arbitrary parallel environments,which is too strong and cannot be programs in a concurrent context. satisfied by many well-known transformations. Verifying implementations of software transactional memory In this paper,we propose a Rely-Guarantee-based Simulation (STM).Many languages supporting STM provide a high-level (RGSim)to verify concurrent program transformations.The rela- atomic block atomicC,so that programmers can assume the tion is parametrized with constraints of the environments that the atomicity of the execution of C.Atomic blocks are imple- source and the target programs may compose with.It considers the mented using some STM protocol (e.g.,TL2 [111)that allows interference between threads and their environments,thus is less very fine-grained interleavings.Verifying that the fine-grained permissive than relations over sequential programs.It is composi- program respects the semantics of atomic blocks gives us the tional w.rt.parallel compositions as long as the constraints are sat- correctness of the STM implementation. isfied.Also,RGSim does not require semantics preservation under Correctness of concurrent garbage collectors (GCs).High- all environments,and can incorporate the assumptions about en- level garbage-collected languages (e.g.,Java)allow program- vironments made by specific program transformations in the form mers to work at an abstract level without knowledge of the un- of rely/guarantee conditions.We use RGSim to reason about opti- derlying GC algorithm.However,the concrete and executable mizations and prove atomicity of concurrent objects.We also pro- low-level program involves interactions between the mutators pose a general garbage collector verification framework based on and the collector.If we view the GC implementation as a trans- RGSim,and verify the Boehm et al.concurrent mark-sweep GC. formation from high-level mutators to low-level ones with a Categories and Subject Descriptors D.2.4 [Software Engineer- concrete GC thread,the GC safety can be reduced naturally to ing]:Software/Program Verification-Correctness proofs,Formal the semantics preservation of the transformation. methods;F.3.1 [Logics and Meanings of Programs]:Specifying To verify the correctness of a program transformation T,we and Verifying and Reasoning about Programs follow Leroy's approach [19]and define a refinement relation General Terms Theory,Verification between the target and the source programs,which says the target has no more observable behaviors than the source.Then we can Keywords Concurrency,Program Transformation,Rely-Guarantee formalize the correctness of the transformation as follows: Reasoning.Simulation Correct(T)≌C,C.C=T(C)=→CgC. (1.1) 1. Introduction That is,for any source program C acceptable by T.T(C)is Many verification problems can be reduced to verifying program a refinement of C.When the source and the target are shared- transformations,i.e.,proving the target program of the transforma- state concurrent programs,the refinement needs to satisfy the tion has no more observable behaviors than the source.Below we following requirements to support effective proof of Correct(T): give some typical examples in concurrent settings: Since the target T(C)may be in a different language from the source,the refinement should be general and independent of the language details. Permission to make digital or hard copies of all or part of this work for personal or To verify fine-grained implementations of abstract operations classroom use is granted without fee provided that copies are not made or distributed the refinement should support different views of program states for profit or commercial advantage and that copies bear this notice and the full citation and different granularities of state accesses at the source and the on the first page.To copy otherwisc.to republish,to post toredistribute to lists,requires prior specific permission and/or a fee. target levels. POPL'12.January 25-27.2012.Philadelphia,PA,USA. When T is syntax-directed (and it is usually the case for par- Copyright©2012ACM978-1-4503-1083-3/1201..s10.00 allel compositions,i.e.,T(CC)=T(C)T(C)).a com 455

A Rely-Guarantee-Based Simulation for Verifying Concurrent Program Transformations Hongjin Liang Xinyu Feng Ming Fu School of Computer Science and Technology, University of Science and Technology of China Hefei, Anhui 230026, China lhj1018@mail.ustc.edu.cn xyfeng@ustc.edu.cn fuming@ustc.edu.cn Abstract Verifying program transformations usually requires proving that the resulting program (the target) refines or is equivalent to the original one (the source). However, the refinement relation between individual sequential threads cannot be preserved in general with the presence of parallel compositions, due to instruction reordering and the different granularities of atomic operations at the source and the target. On the other hand, the refinement relation defined based on fully abstract semantics of concurrent programs assumes arbitrary parallel environments, which is too strong and cannot be satisfied by many well-known transformations. In this paper, we propose a Rely-Guarantee-based Simulation (RGSim) to verify concurrent program transformations. The rela￾tion is parametrized with constraints of the environments that the source and the target programs may compose with. It considers the interference between threads and their environments, thus is less permissive than relations over sequential programs. It is composi￾tional w.r.t. parallel compositions as long as the constraints are sat￾isfied. Also, RGSim does not require semantics preservation under all environments, and can incorporate the assumptions about en￾vironments made by specific program transformations in the form of rely/guarantee conditions. We use RGSim to reason about opti￾mizations and prove atomicity of concurrent objects. We also pro￾pose a general garbage collector verification framework based on RGSim, and verify the Boehm et al. concurrent mark-sweep GC. Categories and Subject Descriptors D.2.4 [Software Engineer￾ing]: Software/Program Verification – Correctness proofs, Formal methods; F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs General Terms Theory, Verification Keywords Concurrency, Program Transformation, Rely-Guarantee Reasoning, Simulation 1. Introduction Many verification problems can be reduced to verifying program transformations, i.e., proving the target program of the transforma￾tion has no more observable behaviors than the source. Below we give some typical examples in concurrent settings: Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. To copy otherwise, to republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. POPL’12, January 25–27, 2012, Philadelphia, PA, USA. Copyright c 2012 ACM 978-1-4503-1083-3/12/01. . . $10.00 • Correctness of compilation and optimizations of concurrent programs. In this most natural program transformation verifica￾tion problem, every compilation phase does a program transfor￾mation T, which needs to preserve the semantics of the inputs. • Atomicity of concurrent objects. A concurrent object or library provides a set of methods that allow clients to manipulate the shared data structure with abstract atomic behaviors [15]. Their correctness can be reduced to the correctness of the transforma￾tion from abstract atomic operations to concrete and executable programs in a concurrent context. • Verifying implementations of software transactional memory (STM). Many languages supporting STM provide a high-level atomic block atomic{C}, so that programmers can assume the atomicity of the execution of C. Atomic blocks are imple￾mented using some STM protocol (e.g., TL2 [11]) that allows very fine-grained interleavings. Verifying that the fine-grained program respects the semantics of atomic blocks gives us the correctness of the STM implementation. • Correctness of concurrent garbage collectors (GCs). High￾level garbage-collected languages (e.g., Java) allow program￾mers to work at an abstract level without knowledge of the un￾derlying GC algorithm. However, the concrete and executable low-level program involves interactions between the mutators and the collector. If we view the GC implementation as a trans￾formation from high-level mutators to low-level ones with a concrete GC thread, the GC safety can be reduced naturally to the semantics preservation of the transformation. To verify the correctness of a program transformation T, we follow Leroy’s approach [19] and define a refinement relation between the target and the source programs, which says the target has no more observable behaviors than the source. Then we can formalize the correctness of the transformation as follows: Correct(T) ∀C, C. C = T(C) =⇒ C C . (1.1) That is, for any source program C acceptable by T, T(C) is a refinement of C. When the source and the target are shared￾state concurrent programs, the refinement needs to satisfy the following requirements to support effective proof of Correct(T): • Since the target T(C) may be in a different language from the source, the refinement should be general and independent of the language details. • To verify fine-grained implementations of abstract operations, the refinement should support different views of program states and different granularities of state accesses at the source and the target levels. • When T is syntax-directed (and it is usually the case for par￾allel compositions, i.e., T(C C ) = T(C) T(C )), a com- 455

positional refinement is of particular importance for modular local r1; local r2; verification of T. x:=1; y:=1; 1。y r2:=X However,existing refinement(or equivalence)relations cannot sat- if (r1=0)then if (r2 =0)then isfy all these requirements at the same time.Contextual equiva- critical region critical region lence,the canonical notion for comparing program behaviors.fails to handle different languages since the contexts of the source and (a)Dekker's Mutual Exclusion Algorithm the target will be different.Simulations and logical relations have been used to verify compilation [4,16,19,21].but they are usu- x:=x+1;‖X:=x+1; ally designed for sequential programs (except [21,25],which we Vs. will discuss in Section 8).Since the refinement or equivalence re- local r1; local r2; lation between sequential threads cannot be preserved in general r1=X; ‖r2:=x; with parallel compositions,we cannot simply adapt existing work x=r1+1; x:=r2+1; on sequential programs to verify transformations of concurrent pro- grams.Refinement relations based on fully abstract semantics of (b)Different Granularities of Atomic Operations concurrent programs are compositional,but they assume arbitrary program contexts,which is too strong for many practical transfor- Figure 1.Equivalence Lost after Parallel Composition mations.We will explain the challenges in detail in Section 2. In this paper,we propose a Rely-Guarantee-based Simulation (RGSim)for compositional verification of concurrent transforma- optimizations in Section 5,verify atomicity of concurrent objects tions.By addressing the above problems,we make the following in Section 6,and prove the correctness of concurrent GCs in Sec- tion 7.Finally we discuss related work and conclude in Section 8. contributions RGSim parametrizes the simulation between concurrent pro- 2. grams with rely/guarantee conditions [17],which specify the Challenges and Our Approach interactions between the programs and their environments. The major challenge we face is to have a compositional refinement This makes the corresponding refinement relation composi- relation between concurrent programs.i.e..we should be able to tional w.r.t.parallel compositions,allowing us to decompose know T(C1)T(C2)Cil C2 if we have T(C1)C1 and refinement proofs for multi-threaded programs into proofs for T(C2)C2. individual threads.On the other hand,the rely/guarantee con- ditions can incorporate the assumptions about environments 2.1 Sequential Refinement Loses Parallel Compositionality made by specific program transformations,so RGSim can be applied to verify many practical transformations. Observable behaviors of sequential imperative programs usually re- fer to their control effects (e.g.,termination and exceptions)and Based on the simulation technique.RGSim focuses on com- final program states.However,refinement relations defined cor- paring externally observable behaviors (e.g.,I/O events)only, respondingly cannot be preserved after parallel compositions.It which gives us considerable leeway in the implementations of has been a well-known fact in the compiler community that sound related programs.The relation is mostly independent of the lan- optimizations for sequential programs may change the behaviors guage details.It can be used to relate programs in different of multi-threaded programs [5].The Dekker's algorithm shown in languages with different views of program states and different Figure 1(a)has been widely used to demonstrate the problem.Re- granularities of atomic state accesses. ordering the first two statements of the thread on the left preserves RGSim makes relational reasoning about optimizations possi- its sequential behaviors,but the whole program can no longer en- ble in parallel contexts.We present a set of relational reason- sure exclusive access to the critical region. ing rules to characterize and justify common optimizations in a In addition to instruction reordering,the different granularities concurrent setting,including hoisting loop invariants,strength of atomic operations between the source and the target programs reduction and induction variable elimination,dead code elimi- can also break the compositionality of program equivalence in a nation,redundancy introduction,efc.. concurrent setting.In Figure 1(b),the target program at the bottom RGSim gives us a refinement-based proof method to verify behaves differently from the source at the top (assuming each fine-grained implementations of abstract algorithms and con- statement is executed atomically),although the individual threads current objects.We successfully apply RGSim to verify con- at the target and the source have the same behaviors current counters,the concurrent GCD algorithm,Treiber's non- blocking stack and the lock-coupling list. 2.2 Assuming Arbitrary Environments is Too Strong We reduce the problem of verifying concurrent garbage collec- The problem with the refinement for sequential programs is that it tors to verifying transformations,and present a general GC ver- does not consider the effects of threads'intermediate state accesses ification framework,which combines unary Rely-Guarantee- on their parallel environments.People have given fully abstract se- based verification [17]with relational proofs based on RGSim. mantics to concurrent programs (e.g.,[1,8)).The semantics of a We verify the Boehm et al.concurrent garbage collection algo- program is modeled as a set of execution traces.Each trace is an rithm [7]using our framework.As far as we know,it is the first interleaving of state transitions made by the program itself and ar- time to formally prove the correctness of this algorithm. bitrary transitions made by the environment.Then the refinement between programs can be defined as the subset relation between In the rest of this paper,we first analyze the challenges for com- the corresponding trace sets.Since it considers all possible envi- positional verification of concurrent program transformations,and ronments,the refinement relation has very nice compositionality, explain our approach informally in Section 2.Then we give the ba- but unfortunately is too strong to formulate the correctness of many sic technical settings in Section 3 and present the formal definition well-known transformations,including the four classes of transfor- of RGSim in Section 4.We show the use of RGSim to reason about mations mentioned before: 456

positional refinement is of particular importance for modular verification of T. However, existing refinement (or equivalence) relations cannot sat￾isfy all these requirements at the same time. Contextual equiva￾lence, the canonical notion for comparing program behaviors, fails to handle different languages since the contexts of the source and the target will be different. Simulations and logical relations have been used to verify compilation [4, 16, 19, 21], but they are usu￾ally designed for sequential programs (except [21, 25], which we will discuss in Section 8). Since the refinement or equivalence re￾lation between sequential threads cannot be preserved in general with parallel compositions, we cannot simply adapt existing work on sequential programs to verify transformations of concurrent pro￾grams. Refinement relations based on fully abstract semantics of concurrent programs are compositional, but they assume arbitrary program contexts, which is too strong for many practical transfor￾mations. We will explain the challenges in detail in Section 2. In this paper, we propose a Rely-Guarantee-based Simulation (RGSim) for compositional verification of concurrent transforma￾tions. By addressing the above problems, we make the following contributions: • RGSim parametrizes the simulation between concurrent pro￾grams with rely/guarantee conditions [17], which specify the interactions between the programs and their environments. This makes the corresponding refinement relation composi￾tional w.r.t. parallel compositions, allowing us to decompose refinement proofs for multi-threaded programs into proofs for individual threads. On the other hand, the rely/guarantee con￾ditions can incorporate the assumptions about environments made by specific program transformations, so RGSim can be applied to verify many practical transformations. • Based on the simulation technique, RGSim focuses on com￾paring externally observable behaviors (e.g., I/O events) only, which gives us considerable leeway in the implementations of related programs. The relation is mostly independent of the lan￾guage details. It can be used to relate programs in different languages with different views of program states and different granularities of atomic state accesses. • RGSim makes relational reasoning about optimizations possi￾ble in parallel contexts. We present a set of relational reason￾ing rules to characterize and justify common optimizations in a concurrent setting, including hoisting loop invariants, strength reduction and induction variable elimination, dead code elimi￾nation, redundancy introduction, etc.. • RGSim gives us a refinement-based proof method to verify fine-grained implementations of abstract algorithms and con￾current objects. We successfully apply RGSim to verify con￾current counters, the concurrent GCD algorithm, Treiber’s non￾blocking stack and the lock-coupling list. • We reduce the problem of verifying concurrent garbage collec￾tors to verifying transformations, and present a general GC ver￾ification framework, which combines unary Rely-Guarantee￾based verification [17] with relational proofs based on RGSim. • We verify the Boehm et al. concurrent garbage collection algo￾rithm [7] using our framework. As far as we know, it is the first time to formally prove the correctness of this algorithm. In the rest of this paper, we first analyze the challenges for com￾positional verification of concurrent program transformations, and explain our approach informally in Section 2. Then we give the ba￾sic technical settings in Section 3 and present the formal definition of RGSim in Section 4. We show the use of RGSim to reason about local r1; x := 1; r1 := y; if (r1 = 0) then critical region local r2; y := 1; r2 := x; if (r2 = 0) then critical region (a) Dekker’s Mutual Exclusion Algorithm x := x+1; x := x+1; vs. local r1; r1 := x; x := r1 + 1; local r2; r2 := x; x := r2 + 1; (b) Different Granularities of Atomic Operations Figure 1. Equivalence Lost after Parallel Composition optimizations in Section 5, verify atomicity of concurrent objects in Section 6, and prove the correctness of concurrent GCs in Sec￾tion 7. Finally we discuss related work and conclude in Section 8. 2. Challenges and Our Approach The major challenge we face is to have a compositional refinement relation between concurrent programs, i.e., we should be able to know T(C1) T(C2) C1 C2 if we have T(C1) C1 and T(C2) C2. 2.1 Sequential Refinement Loses Parallel Compositionality Observable behaviors of sequential imperative programs usually re￾fer to their control effects (e.g., termination and exceptions) and final program states. However, refinement relations defined cor￾respondingly cannot be preserved after parallel compositions. It has been a well-known fact in the compiler community that sound optimizations for sequential programs may change the behaviors of multi-threaded programs [5]. The Dekker’s algorithm shown in Figure 1(a) has been widely used to demonstrate the problem. Re￾ordering the first two statements of the thread on the left preserves its sequential behaviors, but the whole program can no longer en￾sure exclusive access to the critical region. In addition to instruction reordering, the different granularities of atomic operations between the source and the target programs can also break the compositionality of program equivalence in a concurrent setting. In Figure 1(b), the target program at the bottom behaves differently from the source at the top (assuming each statement is executed atomically), although the individual threads at the target and the source have the same behaviors. 2.2 Assuming Arbitrary Environments is Too Strong The problem with the refinement for sequential programs is that it does not consider the effects of threads’ intermediate state accesses on their parallel environments. People have given fully abstract se￾mantics to concurrent programs (e.g., [1, 8]). The semantics of a program is modeled as a set of execution traces. Each trace is an interleaving of state transitions made by the program itself and ar￾bitrary transitions made by the environment. Then the refinement between programs can be defined as the subset relation between the corresponding trace sets. Since it considers all possible envi￾ronments, the refinement relation has very nice compositionality, but unfortunately is too strong to formulate the correctness of many well-known transformations, including the four classes of transfor￾mations mentioned before: 456

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

(Events）e:= level languages are atomic in the interleaving semantics.Below we 444 (Labels)o::=er use --for zero or multiple-step transitions with no events (a)Events and Transition Labels generated,and*_for multiple-step transitions with only one event e generated. (LState) (LEpr）E.∈LState-→lntn 3.2 The Event Trace Refinement (LBExp)B∈LState→{true,fase}L Now we can formally define the refinement relation that relates (LInstr）c ∈LState一P(Labels×LState)U{abort)) the set of externally observable event traces generated by the target and the source programs.A trace is a sequence of events e,and may (LStmt)C ::skip c C1;C2 if (B)C1 else C2 end with a termination marker done or a fault marker abort. while (B)C CiC2 (LStep)-→L∈P(LStu/{skip}x LState)x Labels (EvrTrace)::=e done abort e:: x((LStmt x LState)Ufabort)) Definition 1(Event Trace Set).ETrSet,(C,o)represents a set of (b)The Low-Level Language external event traces produced by C inn steps from the state: 。ETrSeto(C,a)e{e}: (HState）∑：=. (HExpr）E ∈HState→ntL ·ETrSetn+-i(C,o)e (HBEp)B∈HState→{true,false} {E|(C,o)-→(C',o)AE∈ETrSetn(C',a') V(C,a)e(C',a）AE∈ETrSet(C',a)AE=e:E (HInstr）c∈HState一P(Labels x HState)U{abort})】 V(C.o)abort A&=abort (HSmmt)C::=skip c C1::C2 if B then C1 else C2 VC=skip A&=done. while B do C C1C2 (HSep)-→L∈P(HSm/八skp}×HState)x Labels We define ETrSet(C,)asU ETrSetn(C,a). x((HSmt x HState)U{abort)) We overload the notation and use ETrSet(C.>for the high-level language.Then we define an event trace refinement as the subset (c)The High-Level Language relation between event trace sets,which is similar to Leroy's re- finement property [19]. Figure 2.Generic Languages at Target and Source Levels Definition 2(Event Trace Refinement).We say (C,o)is an e- trace refinement of (C,)i.e.,(C,a)(C,).if and only if lead to abort.Note that the semantics of an instruction could be ETrSet(C,o)C ETrSet(C,>) non-deterministic.Moreover,it might be undefined on some states making it possible to model blocking operations such as acquiring The refinement is defined for program configurations instead of a lock. for code only because the initial states may affect the behaviors of programs.In this case,the transformation T should translate Statements are either primitive instructions or compositions of states as well as code.We overload the notation and use T()to them.skip is a special statement used as a flag to show the end of represent the state transformation,and use CC for executions.A single-step execution of statements is modeled as a labeled transitionwhich is a triple of an initial program o,∑.o=T()=→(C,σ)E(C,), configuration (a pair of statement and state).a label and a resulting then Correct(T)defined in formula (1.1)can be reformulated as configuration.It is undefined when the initial statement is skip.The step aborts if an unsafe instruction is executed. Correct(T)会∀C,C.C=T(C)=→C二rC.(3.1) The high-level language (source language)is defined similarly 4. The RGSim Relation in Figure 2(c),but it is important to note that its states and primitive instructions may be different from those in the low-level language. The e-trace refinement is defined directly over the externally ob- The compound statements are almost the same as their low-level servable behaviors of programs.It is intuitive,and also abstract in counterparts.C;C2 and CC2 are sequential and parallel com- that it is independent of language details.However,as we explained positions of C and C2 respectively.Note that we choose to use the before,it is not compositional w.rt.parallel compositions.In this same set of compound statements in the two languages for simplic- section we propose RGSim.which can be viewed as a composi- ity only.This is not required by our simulation relation,although tional proof technique that allows us to derive the simple e-trace the analogous program constructs of the two languages (e.g.,paral- refinement and then verify the corresponding transformation T. lel compositions ClC2 and CC2)make it convenient for us to 4.1 The Definition discuss the compositionality later. Figure 3 shows part of the definition of_which gives Our co-inductively defined RGSim relation is in the form of the high-level operational semantics of statements.We often omit (C,a,R,G),≤a7,(C,∑，R,G),which is a simulation between the subscript H (or L)in_>H(or_)and the label on program configurations (C,o)and (C.>)It is parametrized with top of the arrow when it is T.The semantics is mostly standard the rely and guarantee conditions at the low level and the high level, We only show the rules for primitive instructions and parallel com- which are binary relations over states: positions here.Note that when a primitive instruction c is blocked R,g∈P(LState×LState),R,G∈P(HState×HState). at state >(i.e.,dom(c)),we let the program configuration reduce to itself.For example,the instruction lock(1)would be The simulation also takes two additional parameters:the step in- variant o and the postcondition y.which are both relations between blocked when 1 is not 0,making it be repeated until 1 becomes the low-level and the high-level states. 0:whereas unlock(1)simply sets 1 to 0 at any time and would never be blocked.Primitive instructions in the high-level and low- a,Y,S∈P(LState×HState). 458

(Events) e ::= ... (Labels) o ::= e | τ (a) Events and Transition Labels (LState) σ ::= ... (LExpr) E ∈ LState → Int⊥ (LBExp) B ∈ LState → {true, false}⊥ (LInstr) c ∈ LState  P((Labels × LState) ∪ {abort}) (LStmt) C ::= skip | c | C1; C2 | if (B) C1 else C2 | while (B) C | C1 C2 (LStep) −→L ∈ P((LStmt/{skip} × LState) × Labels ×((LStmt × LState) ∪ {abort})) (b) The Low-Level Language (HState) Σ ::= ... (HExpr) E ∈ HState → Int⊥ (HBExp) B ∈ HState → {true, false}⊥ (HInstr) c ∈ HState  P((Labels × HState) ∪ {abort}) (HStmt) C ::= skip | c | C1; ; C2 | if B then C1 else C2 | while B do C | C1C2 (HStep) −→L ∈ P((HStmt/{skip} × HState) × Labels ×((HStmt × HState) ∪ {abort})) (c) The High-Level Language Figure 2. Generic Languages at Target and Source Levels lead to abort. Note that the semantics of an instruction could be non-deterministic. Moreover, it might be undefined on some states, making it possible to model blocking operations such as acquiring a lock. Statements are either primitive instructions or compositions of them. skip is a special statement used as a flag to show the end of executions. A single-step execution of statements is modeled as a labeled transition −→L , which is a triple of an initial program configuration (a pair of statement and state), a label and a resulting configuration. It is undefined when the initial statement is skip. The step aborts if an unsafe instruction is executed. The high-level language (source language) is defined similarly in Figure 2(c), but it is important to note that its states and primitive instructions may be different from those in the low-level language. The compound statements are almost the same as their low-level counterparts. C1; ; C2 and C1C2 are sequential and parallel com￾positions of C1 and C2 respectively. Note that we choose to use the same set of compound statements in the two languages for simplic￾ity only. This is not required by our simulation relation, although the analogous program constructs of the two languages (e.g., paral￾lel compositions C1 C2 and C1C2) make it convenient for us to discuss the compositionality later. Figure 3 shows part of the definition of −→H , which gives the high-level operational semantics of statements. We often omit the subscript H (or L) in −→H (or −→L ) and the label on top of the arrow when it is τ . The semantics is mostly standard. We only show the rules for primitive instructions and parallel com￾positions here. Note that when a primitive instruction c is blocked at state Σ (i.e., Σ ∈ dom(c)), we let the program configuration reduce to itself. For example, the instruction lock(l) would be blocked when l is not 0, making it be repeated until l becomes 0; whereas unlock(l) simply sets l to 0 at any time and would never be blocked. Primitive instructions in the high-level and low￾level languages are atomic in the interleaving semantics. Below we use −→ ∗ for zero or multiple-step transitions with no events generated, and e −→∗ for multiple-step transitions with only one event e generated. 3.2 The Event Trace Refinement Now we can formally define the refinement relation that relates the set of externally observable event traces generated by the target and the source programs. A trace is a sequence of events e, and may end with a termination marker done or a fault marker abort. (EvtTrace) E ::= | done | abort | e::E Definition 1 (Event Trace Set). ETrSetn(C, σ) represents a set of external event traces produced by C in n steps from the state σ: • ETrSet0(C, σ) {} ; • ETrSetn+1(C, σ) {E | (C, σ) −→ (C , σ ) ∧E∈ETrSetn(C , σ ) ∨ (C, σ) e −→ (C , σ ) ∧ E ∈ETrSetn(C , σ ) ∧ E =e::E ∨ (C, σ) −→ abort ∧ E =abort ∨ C =skip ∧ E =done} . We define ETrSet(C, σ) as n ETrSetn(C, σ). We overload the notation and use ETrSet(C, Σ) for the high-level language. Then we define an event trace refinement as the subset relation between event trace sets, which is similar to Leroy’s re- finement property [19]. Definition 2 (Event Trace Refinement). We say (C, σ) is an e￾trace refinement of (C, Σ), i.e., (C, σ) (C, Σ), if and only if ETrSet(C, σ) ⊆ ETrSet(C, Σ). The refinement is defined for program configurations instead of for code only because the initial states may affect the behaviors of programs. In this case, the transformation T should translate states as well as code. We overload the notation and use T(Σ) to represent the state transformation, and use C T C for ∀σ, Σ. σ = T(Σ) =⇒ (C, σ) (C, Σ), then Correct(T) defined in formula (1.1) can be reformulated as Correct(T) ∀C, C. C = T(C) =⇒ C T C . (3.1) 4. The RGSim Relation The e-trace refinement is defined directly over the externally ob￾servable behaviors of programs. It is intuitive, and also abstract in that it is independent of language details. However, as we explained before, it is not compositional w.r.t. parallel compositions. In this section we propose RGSim, which can be viewed as a composi￾tional proof technique that allows us to derive the simple e-trace refinement and then verify the corresponding transformation T. 4.1 The Definition Our co-inductively defined RGSim relation is in the form of (C, σ, R, G) α;γ (C, Σ, R, G), which is a simulation between program configurations (C, σ) and (C, Σ). It is parametrized with the rely and guarantee conditions at the low level and the high level, which are binary relations over states: R, G∈P(LState × LState), R, G ∈ P(HState × HState). The simulation also takes two additional parameters: the step in￾variant α and the postcondition γ, which are both relations between the low-level and the high-level states. α, γ, ζ ∈ P(LState × HState). 458

(r,)∈c (e,)∈c abort∈c∑ ∑tdom(c) (c,)→(skp,) (c )(skip,) (c,)-→abort c,)→(c,) (C1,)→(C,) (C2,)-→(C2,) (skp川sk,)→(skp习】 (ClC2,)-→+(CⅢC2,) (C1lC2,)-→(C1ⅢC,) (C1,)(C1,) (C2,)(C%,) (C1,)-→abort or(C2,)-→abort (C1lC2,)e(C1ⅢC2,) (CC,)(C,) (C1lC2,)-→abort Figure 3.Operational Semantics of the High-Level Language a a (C.a)a (C,)a R R R RMI R Gle ↓* a o_ C,）-3-(c,2y Co)-3-(C) (a)o-Related Transitions (b)The Side Condition of TRANS (a)Program Steps (b)Environment Steps Figure 4.Related Transitions Figure 5.Simulation Diagrams of RGSim Before we formally define RGSim in Definition 4,we first introduce the a-related transitions as follows. C.the same event should be produced by C.We show the Definition 3(o-Related Transitions). simulation diagram with events generated by the program steps (R,R)a≌{(a,o),(②，∑)|(o,o)∈RA(②，)∈R in Figure 5(a),where solid lines denote hypotheses and dashed ∧(o,)∈aA(σ'，D)∈a} lines denote conclusions,following Leroy's notations [19]. The a relation reflects the abstractions from the low-level ma- (R.R)represents a set of the a-related transitions in R and R chine model to the high-level one,and is preserved by the re- putting together the corresponding transitions in R and R that can lated transitions at the two levels (so it is an invariant).For be related by o,as illustrated in Figure 4(a).(9,G)is defined in instance,when verifying a fine-grained implementation of sets, the same way. the a relation may relate a concrete representation in memory Definition 4(RGSim).Whenever (C,a,R,g)(C,S,R,G). (e.g.,a linked-list)at the low level to the corresponding abstract mathematical set at the high level. then (o,)Eo and the following are true: 1.if (C,)(C,),then there exist C'and such that The corresponding transitions of C and C need to be in (C,)-→*(C,),(o,o),(②，)∈(g,G)aand (G,G*)That is,for each step of C,its state transition should (C,',R,g)(C',E',R,G): satisfy the guarantee g,and the corresponding transition made by the multiple steps of C should be in the transitive closure of 2.if (C,)(C,'),then there exist C'and 'such that G.The guarantees are abstractions of the programs'behaviors. (C,)e→*(C','),(a,a),(②，')∈(g,G)aand As we will show later in the PAR rule in Figure 7,they will serve as the rely conditions of the sibling threads at the time of (C',o',R,g):(C,E,R,G): parallel compositions.Note that we do not need each step of C 3.if C=skip,then there exists'such that to be in G,although we could do so.This is because we only (C,)→*(skp,),(a,o),(②，)∈(G,G*)a care about the coarse-grained behaviors(with mumbling)of the (a,∑)∈y and yCo: source that are used to simulate the target.We will explain more by the example (4.1)in Section 4.2. 4.if(C,o)→abort,then(C,)→*abort; If C terminates,then C terminates as well,and the final states 5.if(o,o),(∑，∑))∈(R,R*)a,then should be related by the postcondition y.We require c a, (Co,R,9)≤a7(C,,R,G). i.e.,the final state relation is not weaker than the step invariant. Then.(C,R,g):(C,R,G)iff .C is not safe only if C is not safe either.This means the trans- for allo and∑，if(a,)∈(，then(C,o,R,g)≤a(C,∑，R,G) formation should not make a safe high-level program unsafe at Here the precondition is used to relate the initial states and the low level. Informally,CG)(CR G)says the low-level Whatever the low-level environment R and the high-level one R do,as long as the state transitions are o-related,they should configuration (C,o)is simulated by the high-level configuration (C,)with behaviors g and G respectively,no matter how their not affect the simulation between C and C,as shown in Fig- environments R and R interfere with them.It requires the follow- ure 5(b).Here a step in R may correspond to zero or multiple ing hold for every execution of C: steps of R.Note that different from the program steps,for the environment steps we do not require each step of R to corre- .Starting from a-related states,each step of C corresponds to spond to zero or multiple steps of R.On the other hand,only zero or multiple steps of C,and the resulting states are o- requiring that R be simulated by R is not sufficient for parallel related too.If an external event is produced in the step of compositionality,which we will explain later in Section 4.2. 459

(τ, Σ ) ∈ c Σ (c, Σ) −→ (skip, Σ ) (e, Σ ) ∈ c Σ (c, Σ) e −→ (skip, Σ ) abort ∈ c Σ (c, Σ) −→ abort Σ ∈ dom(c) (c, Σ) −→ (c, Σ) (skipskip, Σ) −→ (skip, Σ) (C1, Σ) −→ (C 1, Σ ) (C1C2, Σ) −→ (C 1C2, Σ ) (C2, Σ) −→ (C 2, Σ ) (C1C2, Σ) −→ (C1C 2, Σ ) (C1, Σ) e −→ (C 1, Σ ) (C1C2, Σ) e −→ (C 1C2, Σ ) (C2, Σ) e −→ (C 2, Σ ) (C1C2, Σ) e −→ (C1C 2, Σ ) (C1, Σ) −→ abort or (C2, Σ) −→ abort (C1C2, Σ) −→ abort Figure 3. Operational Semantics of the High-Level Language σ σ Σ Σ α ❄ R α ❄ R σ σ θ θ Σ Σ α β ❄ R ❄ RM ❄ R ∗ α β (a) α-Related Transitions (b) The Side Condition of TRANS Figure 4. Related Transitions Before we formally define RGSim in Definition 4, we first introduce the α-related transitions as follows. Definition 3 (α-Related Transitions). R, Rα {((σ, σ ),(Σ, Σ )) | (σ, σ ) ∈R∧ (Σ, Σ ) ∈ R ∧ (σ, Σ) ∈ α ∧ (σ , Σ ) ∈ α} . R, Rα represents a set of the α-related transitions in R and R, putting together the corresponding transitions in R and R that can be related by α, as illustrated in Figure 4(a). G, Gα is defined in the same way. Definition 4 (RGSim). Whenever(C, σ, R, G) α;γ (C, Σ, R, G), then (σ, Σ)∈α and the following are true: 1. if (C, σ) −→ (C , σ ), then there exist C and Σ such that (C, Σ) −→∗ (C , Σ ), ((σ, σ ),(Σ, Σ )) ∈ G, G∗α and (C , σ , R, G) α;γ (C , Σ , R, G); 2. if (C, σ) e −→ (C , σ ), then there exist C and Σ such that (C, Σ) e −→∗ (C , Σ ), ((σ, σ ),(Σ, Σ )) ∈ G, G∗α and (C , σ , R, G) α;γ (C , Σ , R, G); 3. if C = skip, then there exists Σ such that (C, Σ) −→∗ (skip, Σ ), ((σ, σ),(Σ, Σ )) ∈ G, G∗α, (σ, Σ ) ∈ γ and γ ⊆ α; 4. if (C, σ) −→ abort, then (C, Σ) −→∗ abort; 5. if ((σ, σ ),(Σ, Σ )) ∈ R, R∗α, then (C, σ , R, G) α;γ (C, Σ , R, G). Then, (C, R, G) α;ζγ (C, R, G) iff for all σ and Σ, if(σ, Σ) ∈ ζ, then (C, σ, R, G) α;γ (C, Σ, R, G). Here the precondition ζ is used to relate the initial states σ and Σ. Informally, (C, σ, R, G) α;γ (C, Σ, R, G) says the low-level configuration (C, σ) is simulated by the high-level configuration (C, Σ) with behaviors G and G respectively, no matter how their environments R and R interfere with them. It requires the follow￾ing hold for every execution of C: • Starting from α-related states, each step of C corresponds to zero or multiple steps of C, and the resulting states are α- related too. If an external event is produced in the step of (C, σ) (C , σ ) (C, Σ) (C , Σ ) α  G ❄ e α  ❄ G ∗ e (C, σ) (C, σ ) (C, Σ) (C, Σ ) α  ❄ R α  ❄ R ∗ (a) Program Steps (b) Environment Steps Figure 5. Simulation Diagrams of RGSim C, the same event should be produced by C. We show the simulation diagram with events generated by the program steps in Figure 5(a), where solid lines denote hypotheses and dashed lines denote conclusions, following Leroy’s notations [19]. • The α relation reflects the abstractions from the low-level ma￾chine model to the high-level one, and is preserved by the re￾lated transitions at the two levels (so it is an invariant). For instance, when verifying a fine-grained implementation of sets, the α relation may relate a concrete representation in memory (e.g., a linked-list) at the low level to the corresponding abstract mathematical set at the high level. • The corresponding transitions of C and C need to be in G, G∗α. That is, for each step of C, its state transition should satisfy the guarantee G, and the corresponding transition made by the multiple steps of C should be in the transitive closure of G. The guarantees are abstractions of the programs’ behaviors. As we will show later in the PAR rule in Figure 7, they will serve as the rely conditions of the sibling threads at the time of parallel compositions. Note that we do not need each step of C to be in G, although we could do so. This is because we only care about the coarse-grained behaviors (with mumbling) of the source that are used to simulate the target. We will explain more by the example (4.1) in Section 4.2. • If C terminates, then C terminates as well, and the final states should be related by the postcondition γ. We require γ ⊆ α, i.e., the final state relation is not weaker than the step invariant. • C is not safe only if C is not safe either. This means the trans￾formation should not make a safe high-level program unsafe at the low level. • Whatever the low-level environment R and the high-level one R do, as long as the state transitions are α-related, they should not affect the simulation between C and C, as shown in Fig￾ure 5(b). Here a step in R may correspond to zero or multiple steps of R. Note that different from the program steps, for the environment steps we do not require each step of R to corre￾spond to zero or multiple steps of R. On the other hand, only requiring that R be simulated by R is not sufficient for parallel compositionality, which we will explain later in Section 4.2. 459