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