(a)source code S: X++; 1 local t,done :false; s--4s S1- →S2 2 while(！done)C 1 local t; 3 t:=x; or 2 done :cas(&x,t,t+1); TI T1→T2→T3→T4 3x:=t+1; 5] (b)target code T (c)target code Te (with T<T) (with T2<Ti|and |Tal T3|) (a)T<S b)R上T<'S Figure 1.Counters. Figure 2.Simulation diagrams freedom [7](which does not support refinement verification and has limitations on local reasoning,as we will explain in Sec.7),but finement and then discuss its problems in termination-preserving makes the following new contributions: concurrent refinement verification. Fig.1(a)shows the source code S that increments x.In a We design a simulation,RGSim-T,to verify termination- sequential setting,it can be implemented as T in Fig.1(b).To preserving refinement of concurrent programs.As an exten- show that T refines S,a natural way is to prove that they satisfy sion of RGSim,it considers the interference between threads the (weak)simulation in Fig.2(a). and the environments by taking our novel rely/guarantee condi- The simulation first establishes some consistency relation be- tions as parameters.RGSim-T is compositional.It allows us to tween the source and the target (note S and T here are whole pro- thread-locally reason about the preservation of whole-program gram configurations consisting of both code and states).Then it termination,but without enforcing the preservation of individ- requires that there is some correspondence between the execution ual threads'termination,thus can be applied to many practical of the target and the source so that the relation is always preserved refinement applications. Every execution step of the target must either correspond to one We propose the first program logic that supports compositional or more steps of the source (the left part of Fig.2(a)),or corre verification of termination-preserving refinement of concurrent spond to zero steps(the right part;Let's ignore the requirement of programs.In addition to a set of compositionality (binary rea- IT<T]for now).! soning)rules,we also provide a set of unary rules (built upon For our example in Fig.1,the simulation requires that x at the the unary program logic LRG [3])that can reason about con- target level have the same value with x in the source.We let line 2 ditional correspondence between the target and the source,a at T correspond to zero steps of S,and line 3 correspond to the usual situation in concurrent refinement (see Sec.2).The logic single step of S. enables compositional verification of nested loops and sup- Such a simulation,however,has two problems for termination- ports programs with infinite nondeterminism.The soundness of preserving concurrent refinement verification.First,it does not the logic ensures RGSim-T between the target and the source, require the target to preserve the termination of the source.Since which implies the termination-preserving refinement. a silent step at the target level may correspond to zero steps at the source (the right part of Fig.2(a)),the target may execute such Our simulation and logic are general.They can be applied steps infinitely many times and never correspond to a step at the to verify linearizability and lock-freedom together for fine- source.For instance,if we insert while true do skip before grained concurrent objects,or to verify the full correctness of line 2 in T.the simulation still holds,but T diverges now.To optimizations of concurrent programs,i.e.,the optimized pro- address this problem.CompCert [9]introduces a metric T over gram preserves behaviors on both functionality and termination the target program configurations,which is equipped with a well- of the original one.We demonstrate the effectiveness of our founded order <If a target step corresponds to no moves of the logic by verifying linearizability and lock-freedom of Treiber source.the metric over the target programs should strictly decrease stack [20],Michael-Scott queue [14]and DGLM queue [2],the (i.e.,the condition T<T in Fig.2(a)).Since the well-founded full correctness of synchronous queue [16]and the equivalence order ensures that there are no infinite decreasing chains,execution between TTAS lock and TAS lock implementations [6]. of the target will finally correspond to at least one step at the source It is important to note that our simulation and logic ensure that Second,it is not compositional w.r.t.parallel compositions. the target preserves the termination/divergence behaviors of the Though T S holds,(T ll T):print()(Sll S);print() source.The target could diverge if the source diverges.Therefore does not hold since the left side may print out 1,which is im- our logic is not for verifying total correctness (i.e.,partial correct- possible for the source on the right.The problem is that when we ness termination).It is actually more powerful and general.We prove TS.T and S are viewed as closed programs and the give more discussions on this point in Secs.2.2 and 5.2. interference from environments is ignored.To get the parallel com- In the rest of this paper,we first analyze the challenges and positionality,we follow the ideas in our previous work RGSim [11] explain our approach informally in Sec.2.Then we formulate and parameterize the simulation with the interference between the termination-preserving refinement in Sec.3.We present our new programs and their environments. simulation RGSim-T in Sec.4 and our new program logic in Sec.5 As shown in Fig.2(b),the new simulation <is parameterized We summarize examples that we verified in Sec.6,and discuss the with the environment interference R,i.e.the set of all possible related work and conclude in Sec.7. transitions of the environments at the target and source levels.Here we use thin arrows for the transitions of the current thread at the source and the target levels (e.g.,from T to T2 and from T3 to T4 2.Informal Development in Fig.2(b)),and thick arrows for the possible environment steps Below we informally explain the challenges and our solutions in (e.g.,from T2 to T3 and from S1 to S2 in the figure).We require our design of the simulation and the logic respectively. the simulation to be preserved by R. 2.1 Simulation INote here we only discuss silent steps (a.k.a.T-steps)which produce no external events.The simulation also requires that every step with an extemal Simulation is a standard technique for refinement verification.We event at the target level must correspond to one step at the source with the start by showing a simple simulation for verifying sequential re- same event plus zero or multiple T-steps.(a) source code S: x++; 1 local t; 2 t := x; 3 x := t + 1; (b) target code Tb 1 local t, done := false; 2 while (! done) { 3 t := x; 4 done := cas(&x, t, t+1); 5 } (c) target code Tc Figure 1. Counters. freedom [7] (which does not support refinement verification and has limitations on local reasoning, as we will explain in Sec. 7), but makes the following new contributions: • We design a simulation, RGSim-T, to verify termination￾preserving refinement of concurrent programs. As an exten￾sion of RGSim, it considers the interference between threads and the environments by taking our novel rely/guarantee condi￾tions as parameters. RGSim-T is compositional. It allows us to thread-locally reason about the preservation of whole-program termination, but without enforcing the preservation of individ￾ual threads’ termination, thus can be applied to many practical refinement applications. • We propose the first program logic that supports compositional verification of termination-preserving refinement of concurrent programs. In addition to a set of compositionality (binary rea￾soning) rules, we also provide a set of unary rules (built upon the unary program logic LRG [3]) that can reason about con￾ditional correspondence between the target and the source, a usual situation in concurrent refinement (see Sec. 2). The logic enables compositional verification of nested loops and sup￾ports programs with infinite nondeterminism. The soundness of the logic ensures RGSim-T between the target and the source, which implies the termination-preserving refinement. • Our simulation and logic are general. They can be applied to verify linearizability and lock-freedom together for fine￾grained concurrent objects, or to verify the full correctness of optimizations of concurrent programs, i.e., the optimized pro￾gram preserves behaviors on both functionality and termination of the original one. We demonstrate the effectiveness of our logic by verifying linearizability and lock-freedom of Treiber stack [20], Michael-Scott queue [14] and DGLM queue [2], the full correctness of synchronous queue [16] and the equivalence between TTAS lock and TAS lock implementations [6]. It is important to note that our simulation and logic ensure that the target preserves the termination/divergence behaviors of the source. The target could diverge if the source diverges. Therefore our logic is not for verifying total correctness (i.e., partial correct￾ness + termination). It is actually more powerful and general. We give more discussions on this point in Secs. 2.2 and 5.2. In the rest of this paper, we first analyze the challenges and explain our approach informally in Sec. 2. Then we formulate termination-preserving refinement in Sec. 3. We present our new simulation RGSim-T in Sec. 4 and our new program logic in Sec. 5. We summarize examples that we verified in Sec. 6, and discuss the related work and conclude in Sec. 7. 2. Informal Development Below we informally explain the challenges and our solutions in our design of the simulation and the logic respectively. 2.1 Simulation Simulation is a standard technique for refinement verification. We start by showing a simple simulation for verifying sequential re￾S S ′ T T ′ +   or S T T ′   (with |T ′ | < |T|) (a) T  S S1 T1 T2 S2 T3 T4 ′ ′ R ′ ′ (with |T2| < |T1| and |T4| < |T3|) (b) R ⊢ T ′ S Figure 2. Simulation diagrams. finement and then discuss its problems in termination-preserving concurrent refinement verification. Fig. 1(a) shows the source code S that increments x. In a sequential setting, it can be implemented as Tb in Fig. 1(b). To show that Tb refines S, a natural way is to prove that they satisfy the (weak) simulation  in Fig. 2(a). The simulation first establishes some consistency relation be￾tween the source and the target (note S and T here are whole pro￾gram configurations consisting of both code and states). Then it requires that there is some correspondence between the execution of the target and the source so that the relation is always preserved. Every execution step of the target must either correspond to one or more steps of the source (the left part of Fig. 2(a)), or corre￾spond to zero steps (the right part; Let’s ignore the requirement of |T ′ | < |T | for now).1 For our example in Fig. 1, the simulation requires that x at the target level have the same value with x in the source. We let line 2 at Tb correspond to zero steps of S, and line 3 correspond to the single step of S. Such a simulation, however, has two problems for termination￾preserving concurrent refinement verification. First, it does not require the target to preserve the termination of the source. Since a silent step at the target level may correspond to zero steps at the source (the right part of Fig. 2(a)), the target may execute such steps infinitely many times and never correspond to a step at the source. For instance, if we insert while true do skip before line 2 in Tb, the simulation still holds, but Tb diverges now. To address this problem, CompCert [9] introduces a metric |T | over the target program configurations, which is equipped with a well￾founded order <. If a target step corresponds to no moves of the source, the metric over the target programs should strictly decrease (i.e., the condition |T ′ | < |T | in Fig. 2(a)). Since the well-founded order ensures that there are no infinite decreasing chains, execution of the target will finally correspond to at least one step at the source. Second, it is not compositional w.r.t. parallel compositions. Though Tb  S holds, (Tb k Tb); print(x)  (S k S); print(x) does not hold since the left side may print out 1, which is im￾possible for the source on the right. The problem is that when we prove Tb  S, Tb and S are viewed as closed programs and the interference from environments is ignored. To get the parallel com￾positionality, we follow the ideas in our previous work RGSim [11] and parameterize the simulation with the interference between the programs and their environments. As shown in Fig. 2(b), the new simulation  ′ is parameterized with the environment interference R, i.e. the set of all possible transitions of the environments at the target and source levels. Here we use thin arrows for the transitions of the current thread at the source and the target levels (e.g., from T1 to T2 and from T3 to T4 in Fig. 2(b)), and thick arrows for the possible environment steps (e.g., from T2 to T3 and from S1 to S2 in the figure). We require the simulation  ′ to be preserved by R. 1 Note here we only discuss silent steps (a.k.a. τ-steps) which produce no external events. The simulation also requires that every step with an external event at the target level must correspond to one step at the source with the same event plus zero or multiple τ-steps