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

Rely-Guarantee-Based Simulation for Compositional Verification of Concurrent Program Transformations HONGJIN LIANG,XINYU FENG and MING FU,University of Science and Technology of China 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 sequen- tial 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 transfor. mations. In this paper,we propose a Rely-Guarantee-based Simulation(RGSim)to verify concurrent program transformations.The relation 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 compositional w.r.t.parallel composi- tions as long as the constraints are satisfied.Also,RGSim does not require semantics preservation under all environments,and can incorporate the assumptions about environments made by specific program transfor. mations in the form of rely/guarantee conditions.We use RGSim to reason about optimizations and prove atomicity of concurrent objects.We also propose 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 Engineeringl:Software/Program Verification-Cor- rectness proofs,Formal methods;F.3.1 [Logics and Meanings of Programs):Specifying and Verifying and Reasoning about Programs General Terms:Theory,Verification Additional Key Words and Phrases:Concurrency,Program Transformation,Rely-Guarantee Reasoning, Simulation ACM Reference Format: Liang,H.,Feng,X.,and Fu,M.2014.Rely-Guarantee-Based Simulation for Compositional Verification of Concurrent Program Transformations.ACM Trans.Program.Lang.Syst.V,N,Article A (January YYYY), 53 pages. D0I:http/dx.doi.org10.1145/0000000.0000000 This work is supported in part by grants from National Natural Science Foundation of China(NSFC)under Grant Nos.61379039,61229201,61103023 and 91318301,Program for New Century Excellent Talents in Universities(Grant No.NCET-2010-0984).and the Fundamental Research Funds for the Central Universi- ties(Grant No.WK0110000031). Author's addresses:H.Liang,X.Feng and M.Fu,School of Computer Science and Technology,University of Science and Technology of China,Hefei,Anhui 230026,China;Suzhou Institute for Advanced Study, University of Science and Technology of China,Suzhou,Jiangsu 215123,China. Emails:H.Liang,Ihj1018@mail.ustc.edu.cn;X.Feng (corresponding author),xyfeng@ustc.edu.cn;and M.Fu,fuming@ustc.edu.cn Permission to make digital or hard copies of part or all 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 show this notice on the first page or initial screen of a display along with the full citation.Copyrights for components of this work owned by others than ACM must be honored.Abstracting with credit is per- mitted.To copy otherwise,to republish,to post on servers,to redistribute to lists,or to use any component of this work in other works requires prior specific permission and/or a fee.Permissions may be requested from Publications Dept.,ACM,Inc.,2 Penn Plaza,Suite 701,New York,NY 10121-0701 USA,fax +1(212) 869-0481,or permissions@acm.org YYYY ACM 0164-0925/YYYY/01-ARTA $15.00 D0I:http/dk.doi.org10.1145/0000000.0000000 ACM Transactions on Programming Languages and Systems,Vol.V,No.N,Article A,Publication date:January YYYY

A Rely-Guarantee-Based Simulation for Compositional Verification of Concurrent Program Transformations HONGJIN LIANG, XINYU FENG and MING FU, University of Science and Technology of China 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 sequen￾tial 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 transfor￾mations. In this paper, we propose a Rely-Guarantee-based Simulation (RGSim) to verify concurrent program transformations. The relation 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 compositional w.r.t. parallel composi￾tions as long as the constraints are satisfied. Also, RGSim does not require semantics preservation under all environments, and can incorporate the assumptions about environments made by specific program transfor￾mations in the form of rely/guarantee conditions. We use RGSim to reason about optimizations and prove atomicity of concurrent objects. We also propose 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 Engineering]: Software/Program Verification – Cor￾rectness proofs, Formal methods; F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs General Terms: Theory, Verification Additional Key Words and Phrases: Concurrency, Program Transformation, Rely-Guarantee Reasoning, Simulation ACM Reference Format: Liang, H., Feng, X., and Fu, M. 2014. Rely-Guarantee-Based Simulation for Compositional Verification of Concurrent Program Transformations. ACM Trans. Program. Lang. Syst. V, N, Article A (January YYYY), 53 pages. DOI:http://dx.doi.org/10.1145/0000000.0000000 This work is supported in part by grants from National Natural Science Foundation of China (NSFC) under Grant Nos. 61379039, 61229201, 61103023 and 91318301, Program for New Century Excellent Talents in Universities (Grant No. NCET-2010-0984), and the Fundamental Research Funds for the Central Universi￾ties (Grant No. WK0110000031). Author’s addresses: H. Liang, X. Feng and M. Fu, School of Computer Science and Technology, University of Science and Technology of China, Hefei, Anhui 230026, China; Suzhou Institute for Advanced Study, University of Science and Technology of China, Suzhou, Jiangsu 215123, China. Emails: H. Liang, lhj1018@mail.ustc.edu.cn; X. Feng (corresponding author), xyfeng@ustc.edu.cn; and M. Fu, fuming@ustc.edu.cn. Permission to make digital or hard copies of part or all 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 show this notice on the first page or initial screen of a display along with the full citation. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is per￾mitted. To copy otherwise, to republish, to post on servers, to redistribute to lists, or to use any component of this work in other works requires prior specific permission and/or a fee. Permissions may be requested from Publications Dept., ACM, Inc., 2 Penn Plaza, Suite 701, New York, NY 10121-0701 USA, fax +1 (212) 869-0481, or permissions@acm.org. ⃝c YYYY ACM 0164-0925/YYYY/01-ARTA $15.00 DOI:http://dx.doi.org/10.1145/0000000.0000000 ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Article A, Publication date: January YYYY

A:2 Hongjin Liang et al. 1.INTRODUCTION Many verification problems can be reduced to verifying program transformations,i.e., proving the target program of the transformation has no more observable behaviors than the source.Below we give some typical examples in concurrent settings: -Correctness of compilation and optimizations of concurrent programs.In this most natural program transformation verification problem,every compilation phase does a program transformation T,which needs to preserve the semantics of the inputs. Atomicity of concurrent objects.A concurrent object or library provides a set of meth- ods that allow clients to manipulate the shared data structure with abstract atomic behaviors [Herlihy and Shavit 20081.Their correctness can be reduced to the cor- rectness of the transformation from abstract atomic operations to concrete and exe- cutable 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 implemented using some STM protocol (e.g.,TL2 [Dice et al.2006])that allows very fine-grained inter- leavings.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 lan- guages (e.g.,Java)allow programmers to work at an abstract level without knowledge of the underlying GC algorithm.However,the concrete and executable low-level pro- gram involves interactions between the mutators and the collector.If we view the GC implementation as a transformation 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 ap- proach [Leroy 2009]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)→CgC. (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 parallel compositions,i.e., T(CC)=T(C)T(C)),a compositional refinement is of particular importance for modular verification of T. However,existing refinement (or equivalence)relations cannot satisfy all these re- quirements at the same time.Contextual equivalence,the canonical notion for com- paring 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 [Leroy 2009;Benton and Hur 2009;Lochbihler 2010; Hur and Dreyer 2011],but they are usually designed for sequential programs (ex- cept [Lochbihler 2010;Sevcik et al.2011],which we will discuss in Section 8).Since the ACM Transactions on Programming Languages and Systems,Vol.V,No.N,Article A,Publication date:January YYYY

A:2 Hongjin Liang et al. 1. INTRODUCTION Many verification problems can be reduced to verifying program transformations, i.e., proving the target program of the transformation has no more observable behaviors than the source. Below we give some typical examples in concurrent settings: — Correctness of compilation and optimizations of concurrent programs. In this most natural program transformation verification problem, every compilation phase does a program transformation T, which needs to preserve the semantics of the inputs. — Atomicity of concurrent objects. A concurrent object or library provides a set of meth￾ods that allow clients to manipulate the shared data structure with abstract atomic behaviors [Herlihy and Shavit 2008]. Their correctness can be reduced to the cor￾rectness of the transformation from abstract atomic operations to concrete and exe￾cutable 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 implemented using some STM protocol (e.g., TL2 [Dice et al. 2006]) that allows very fine-grained inter￾leavings. 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 lan￾guages (e.g., Java) allow programmers to work at an abstract level without knowledge of the underlying GC algorithm. However, the concrete and executable low-level pro￾gram involves interactions between the mutators and the collector. If we view the GC implementation as a transformation 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 ap￾proach [Leroy 2009] 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 parallel compositions, i.e., T(C∥C ′ ) = T(C)∥T(C ′ )), a compositional refinement is of particular importance for modular verification of T. However, existing refinement (or equivalence) relations cannot satisfy all these re￾quirements at the same time. Contextual equivalence, the canonical notion for com￾paring 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 [Leroy 2009; Benton and Hur 2009; Lochbihler 2010; Hur and Dreyer 2011], but they are usually designed for sequential programs (ex￾cept [Lochbihler 2010; Sev ˇ cˇ´ık et al. 2011], which we will discuss in Section 8). Since the ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Article A, Publication date: January YYYY

Rely-Guarantee-Based Simulation A:3 refinement or equivalence relation between sequential threads cannot be preserved in general with parallel compositions,we cannot simply adapt existing work on sequen- tial programs to verify transformations of concurrent programs.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 composi- tional verification of concurrent transformations.By addressing the above problems. we make the following contributions: -RGSim parametrizes the simulation between concurrent programs with rely/guarantee conditions [Jones 1983],which specify the interactions between the programs and their environments.This makes the corresponding refinement relation compositional w.rt.parallel compositions,allowing us to decompose refine- ment proofs for multi-threaded programs into proofs for individual threads.On the other hand,the rely/guarantee conditions 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 comparing externally observ- able behaviors (e.g.,I/O events)only,which gives us considerable leeway in the imple- mentations of related programs.The relation is mostly independent of the language 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 possible in parallel contexts. We present a set of relational reasoning rules to characterize and justify common optimizations in a concurrent setting,including hoisting loop invariants,strength reduction and induction variable elimination,dead code elimination,redundancy in- troduction,etc. RGSim gives us a refinement-based proof method to verify fine-grained implemen- tations of abstract algorithms and concurrent objects.We successfully apply RGSim to verify concurrent counters,the concurrent GCD algorithm,Treiber's non-blocking stack and the lock-coupling list. We reduce the problem of verifying concurrent garbage collectors to verifying trans- formations,and present a general GC verification framework,which combines unary Rely-Guarantee-based verification [Jones 1983]with relational proofs based on RGSim. We verify the Boehm et al.concurrent garbage collection algorithm [Boehm et al. 1991]using our framework.As far as we know,it is the first time to formally prove the correctness of this algorithm. We give a mechanized formulation of RGSim,and prove its soundness and composi- tionality in the Coq proof assistant [2010].Both the manual and mechanized proofs are available online' This paper extends the conference paper in POPL 2012 [Liang et al.2012].First,we add more examples,including strength reduction and induction variable elimination, the non-blocking concurrent counter,Treiber's stack algorithm,and the concurrent GCD algorithm.Second,we significantly expand the details for the concurrent GC verification,demonstrating that RGSim is a powerful proof technique for verifying program transformations which involve concurrent run-time systems. In the rest of this paper,we first analyze the challenges for compositional verifica- tion of concurrent program transformations,and explain our approach informally in ihttp://kyhcs.ustcsz.edu.cn/relconcur/rgsim ACM Transactions on Programming Languages and Systems,Vol.V,No.N,Article A,Publication date:January YYYY

Rely-Guarantee-Based Simulation A:3 refinement or equivalence relation between sequential threads cannot be preserved in general with parallel compositions, we cannot simply adapt existing work on sequen￾tial programs to verify transformations of concurrent programs. 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 composi￾tional verification of concurrent transformations. By addressing the above problems, we make the following contributions: — RGSim parametrizes the simulation between concurrent programs with rely/guarantee conditions [Jones 1983], which specify the interactions between the programs and their environments. This makes the corresponding refinement relation compositional w.r.t. parallel compositions, allowing us to decompose refine￾ment proofs for multi-threaded programs into proofs for individual threads. On the other hand, the rely/guarantee conditions 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 comparing externally observ￾able behaviors (e.g., I/O events) only, which gives us considerable leeway in the imple￾mentations of related programs. The relation is mostly independent of the language 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 possible in parallel contexts. We present a set of relational reasoning rules to characterize and justify common optimizations in a concurrent setting, including hoisting loop invariants, strength reduction and induction variable elimination, dead code elimination, redundancy in￾troduction, etc. — RGSim gives us a refinement-based proof method to verify fine-grained implemen￾tations of abstract algorithms and concurrent objects. We successfully apply RGSim to verify concurrent counters, the concurrent GCD algorithm, Treiber’s non-blocking stack and the lock-coupling list. — We reduce the problem of verifying concurrent garbage collectors to verifying trans￾formations, and present a general GC verification framework, which combines unary Rely-Guarantee-based verification [Jones 1983] with relational proofs based on RGSim. — We verify the Boehm et al. concurrent garbage collection algorithm [Boehm et al. 1991] using our framework. As far as we know, it is the first time to formally prove the correctness of this algorithm. — We give a mechanized formulation of RGSim, and prove its soundness and composi￾tionality in the Coq proof assistant [2010]. Both the manual and mechanized proofs are available online1 . This paper extends the conference paper in POPL 2012 [Liang et al. 2012]. First, we add more examples, including strength reduction and induction variable elimination, the non-blocking concurrent counter, Treiber’s stack algorithm, and the concurrent GCD algorithm. Second, we significantly expand the details for the concurrent GC verification, demonstrating that RGSim is a powerful proof technique for verifying program transformations which involve concurrent run-time systems. In the rest of this paper, we first analyze the challenges for compositional verifica￾tion of concurrent program transformations, and explain our approach informally in 1http://kyhcs.ustcsz.edu.cn/relconcur/rgsim ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Article A, Publication date: January YYYY

A:4 Hongjin Liang et al. local ri; local r2; x:=1; y:=1; r1:=y; ‖r2:=x; if (r1 =0)then if (r2 =0)then critical region critical region (a)Dekker's Mutual Exclusion Algorithm x:=x+1;‖x:=x+1: US. local ri; local r2; r1:=x; ‖2：=x; x:=r1+1; X:=r2+1; (b)Different Granularities of Atomic Operations Fig.1.Equivalence Lost after Parallel Composition Section 2.Then we give the basic technical settings in Section 3 and present the formal definition of RGSim in Section 4.We show the use of RGSim to reason about optimiza- tions in Section 5,verify fine-grained algorithms and atomicity of concurrent objects in Section 6,and prove the correctness of concurrent GCs in Section 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)IT(C2)C1ll 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 refer to their con- trol effects (e.g.,termination and exceptions)and final program states.However,re- finement relations defined correspondingly cannot be preserved after parallel compo- sitions.It has been a well-known fact in the compiler community that sound opti- mizations for sequential programs may change the behaviors of multi-threaded pro- grams [Boehm 2005].The Dekker's algorithm shown in Figure 1(a)has been widely used to demonstrate the problem.Reordering the first two assignment statements of the thread on the left preserves its sequential behaviors,but the whole program can no longer ensure 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.Peo- ple have given fully abstract semantics to concurrent programs (e.g.,[Brookes 1996; Abadi and Plotkin 2009]).The semantics of a program is modeled as a set of execu- ACM Transactions on Programming Languages and Systems,Vol.V,No.N,Article A,Publication date:January YYYY

A:4 Hongjin Liang et al. 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 Fig. 1. Equivalence Lost after Parallel Composition Section 2. Then we give the basic technical settings in Section 3 and present the formal definition of RGSim in Section 4. We show the use of RGSim to reason about optimiza￾tions in Section 5, verify fine-grained algorithms and atomicity of concurrent objects in Section 6, and prove the correctness of concurrent GCs in Section 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 refer to their con￾trol effects (e.g., termination and exceptions) and final program states. However, re- finement relations defined correspondingly cannot be preserved after parallel compo￾sitions. It has been a well-known fact in the compiler community that sound opti￾mizations for sequential programs may change the behaviors of multi-threaded pro￾grams [Boehm 2005]. The Dekker’s algorithm shown in Figure 1(a) has been widely used to demonstrate the problem. Reordering the first two assignment statements of the thread on the left preserves its sequential behaviors, but the whole program can no longer ensure 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. Peo￾ple have given fully abstract semantics to concurrent programs (e.g., [Brookes 1996; Abadi and Plotkin 2009]). The semantics of a program is modeled as a set of execu￾ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Article A, Publication date: January YYYY

Rely-Guarantee-Based Simulation A:5 tion traces.Each trace is an interleaving of state transitions made by the program itself and arbitrary transitions made by the environment.Then the refinement be- tween programs can be defined as the subset relation between the corresponding trace sets.Since it considers all possible environments,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 transformations mentioned before: -Many concurrent languages(e.g.,C++[Boehm and Adve 20081)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 concurrent object is a re- finement of an abstract atomic object,we can assume that all accesses to the object are made through the object's methods only,e.g.,a stack object can only be accessed through push and pop methods,and its internal data cannot be arbitrarily updated. Usually the implementation of STM (e.g.,TL2 [Dice et al.2006])ensures the atom- icity of a transaction atomicfC}only when there are no data races.Therefore,the correctness of the transformation from high-level atomic blocks to fine-grained con- current code assumes data-race-freedom in the source. Many garbage-collected languages are type-safe and prohibit operations such as pointer arithmetic.Therefore the garbage collector could make corresponding as- sumptions about the mutators 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 formu- lation of the transformation correctness more difficult.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 proving 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 contexts.External observers do not care about the implementation details of the source and the target programs.For them, intermediate state accesses(such as memory reads and writes)are silent steps (un- observable),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 explained in Section 2.1.On the other hand,re- lating all state accesses of programs is too strong.Any reordering of state accesses or change of atomicity would fail the refinement. ACM Transactions on Programming Languages and Systems,Vol.V,No.N,Article A,Publication date:January YYYY

Rely-Guarantee-Based Simulation A:5 tion traces. Each trace is an interleaving of state transitions made by the program itself and arbitrary transitions made by the environment. Then the refinement be￾tween programs can be defined as the subset relation between the corresponding trace sets. Since it considers all possible environments, 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 transformations mentioned before: — Many concurrent languages (e.g., C++ [Boehm and Adve 2008]) 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 concurrent object is a re- finement of an abstract atomic object, we can assume that all accesses to the object are made through the object’s methods only, e.g., a stack object can only be accessed through push and pop methods, and its internal data cannot be arbitrarily updated. — Usually the implementation of STM (e.g., TL2 [Dice et al. 2006]) ensures the atom￾icity 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 con￾current code assumes data-race-freedom in the source. — Many garbage-collected languages are type-safe and prohibit operations such as pointer arithmetic. Therefore the garbage collector could make corresponding as￾sumptions about the mutators 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 formu￾lation of the transformation correctness more difficult. 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 proving 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 contexts. External observers do not care about the implementation details of the source and the target programs. For them, intermediate state accesses (such as memory reads and writes) are silent steps (un￾observable), 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 explained in Section 2.1. On the other hand, re￾lating all state accesses of programs is too strong. Any reordering of state accesses or change of atomicity would fail the refinement. ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Article A, Publication date: January YYYY