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: 456positional 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