Compositional Verification of Termination-Preserving Refinement of Concurrent Programs Hongjin Liangt Xinyu Fengt Zhong Shaot University of Science and Technology of China +Yale University lhj1018@mail.ustc.edu.cn xyfeng@ustc.edu.cn zhong.shao@yale.edu Abstract should termination of the source be preserved too by the target?If Many verification problems can be reduced to refinement verifica- yes,how to verify such refinement? Preservation of termination is an indispensable requirement tion.However,existing work on verifying refinement of concurrent programs either fails to prove the preservation of termination.al- in many refinement applications.For instance,compilation and lowing a diverging program to trivially refine any programs,or is optimizations are not allowed to transform a terminating source difficult to apply in compositional thread-local reasoning.In this program to a diverging (non-terminating)target.Also,implemen- paper,we first propose a new simulation technique,which estab- tations of concurrent data structures are often expected to have lishes termination-preserving refinement and is a congruence with progress guarantees (e.g.,lock-freedom and wait-freedom)in ad- respect to parallel composition.We then give a proof theory for the dition to linearizability.The requirements are equivalent to some simulation,which is the first Hoare-style concurrent program logic contextual refinements that preserve the termination of client pro- supporting termination-preserving refinement proofs.We show two grams [12]. key applications of our logic,i.e.,verifying linearizability and lock- Most existing approaches for verifying concurrent program freedom together for fine-grained concurrent objects,and verifying refinement,including simulations (e.g.,[11]),logical relations full correctness of optimizations of concurrent algorithms. (e.g..[221),and refinement logics (e.g.,[211).do not reason about the preservation of termination.As a result,a program that Categories and Subject Descriptors D.2.4 [Software Engineer- does an infinite loop without generating any external events,e.g ing]:Software/Program Verification-Correctness proofs,Formal while true do skip,would trivially refine any source program methods;F.3.1 [Logics and Meanings of Programs]:Specifying (just like that it trivially satisfies partial correctness in Hoare logic). and Verifying and Reasoning about Programs Certainly this kind of refinement is not acceptable in the applica- General Terms Theory,Verification tions mentioned above. CompCert [9]addresses the problem by introducing a well- Keywords Concurrency,Refinement,Termination Preservation, founded order in the simulation,but it works only for sequential Rely-Guarantee Reasoning.Simulation programs.It is difficult to apply this idea to do thread-local ver- ification of concurrent program refinement,which enables us to 1.Introduction know Ti Il T2 S1 ll S2 by proving T1 S1 and T2E S2 Verifying refinement between programs is the crux of many ver- In practice,the termination preservation in the refinement proofs of ification problems.For instance.reasoning about compilation or individual threads could be easily broken by the interference from their environments (i.e.,other threads running in parallel).For in- program transformations requires proving that every target pro- gram is a refinement of its source [9].In concurrent settings,re- stance,a method call of a lock-free data structure (e.g.,Treiber cent work [4.12]shows that the correctness of concurrent data stack)may never terminate when other threads call the methods structures and libraries can be characterized via some forms of con- and update the shared memory infinitely often.As we will explain in Sec.2,the key challenge here is to effectively specify the en textual refinements,i.e.,every client that calls the concrete library vironments'effects on the termination preservation of individual methods should refine the client with some abstract atomic oper- ations.Verification of concurrent garbage collectors [11]and OS threads.As far as we know,no previous work can use "composi- kernels [18]can also be reduced to refinement verification. tional"thread-local reasoning to verify termination-preserving re- finement between(whole)concurrent programs. Refinement from the source program S to the target T,written as T S,requires that T have no more observable behaviors In this paper,we first propose novel rely/guarantee conditions than S.Usually observable behaviors include the traces of external which can effectively specify the interference over the termina- tion properties between a thread and its environment.Traditional events such as 1/O operations and runtime errors.The question is rely/guarantee conditions [8]are binary relations of program states and they specify the state updates.We extend them with a boolean tag indicating whether a state update may let the thread or its envi- 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 ronment make more moves for profit or commercial advantage and that copies bear this notice and the full citation With the help of our new rely/guarantee conditions,we then on the first page.Copyrights for components of this work owned by others than ACM propose a new simulation RGSim-T,and a new Hoare-style pro- must be honored.Abstracting with credit is permitted.To copy otherwise.or republish gram logic,both of which support compositional verification to post on servers or to redistribute to lists,requires prior specific permission and/or a of termination-preserving refinement of concurrent programs fee.Request permissions from permissions@acm.org. Our work is based on our previous compositional simulation RGSim [11](which unfortunately cannot preserve termination), http:/ldk.doi.org/10.1145/2603088.2603123 and is inspired by Hoffmann et al.'s program logic for lock-
Compositional Verification of Termination-Preserving Refinement of Concurrent Programs Hongjin Liang† Xinyu Feng† Zhong Shao‡ †University of Science and Technology of China ‡Yale University lhj1018@mail.ustc.edu.cn xyfeng@ustc.edu.cn zhong.shao@yale.edu Abstract Many verification problems can be reduced to refinement verification. However, existing work on verifying refinement of concurrent programs either fails to prove the preservation of termination, allowing a diverging program to trivially refine any programs, or is difficult to apply in compositional thread-local reasoning. In this paper, we first propose a new simulation technique, which establishes termination-preserving refinement and is a congruence with respect to parallel composition. We then give a proof theory for the simulation, which is the first Hoare-style concurrent program logic supporting termination-preserving refinement proofs. We show two key applications of our logic, i.e., verifying linearizability and lockfreedom together for fine-grained concurrent objects, and verifying full correctness of optimizations of concurrent algorithms. Categories and Subject Descriptors D.2.4 [Software Engineering]: 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, Refinement, Termination Preservation, Rely-Guarantee Reasoning, Simulation 1. Introduction Verifying refinement between programs is the crux of many verification problems. For instance, reasoning about compilation or program transformations requires proving that every target program is a refinement of its source [9]. In concurrent settings, recent work [4, 12] shows that the correctness of concurrent data structures and libraries can be characterized via some forms of contextual refinements, i.e., every client that calls the concrete library methods should refine the client with some abstract atomic operations. Verification of concurrent garbage collectors [11] and OS kernels [18] can also be reduced to refinement verification. Refinement from the source program S to the target T , written as T ⊑ S, requires that T have no more observable behaviors than S. Usually observable behaviors include the traces of external events such as I/O operations and runtime errors. The question is, 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. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from permissions@acm.org. CSL-LICS 2014, July 14–18, 2014, Vienna, Austria. Copyright c 2014 ACM 978-1-4503-2886-9. . . $15.00. http://dx.doi.org/10.1145/2603088.2603123 should termination of the source be preserved too by the target? If yes, how to verify such refinement? Preservation of termination is an indispensable requirement in many refinement applications. For instance, compilation and optimizations are not allowed to transform a terminating source program to a diverging (non-terminating) target. Also, implementations of concurrent data structures are often expected to have progress guarantees (e.g., lock-freedom and wait-freedom) in addition to linearizability. The requirements are equivalent to some contextual refinements that preserve the termination of client programs [12]. Most existing approaches for verifying concurrent program refinement, including simulations (e.g., [11]), logical relations (e.g., [22]), and refinement logics (e.g., [21]), do not reason about the preservation of termination. As a result, a program that does an infinite loop without generating any external events, e.g. while true do skip, would trivially refine any source program (just like that it trivially satisfies partial correctness in Hoare logic). Certainly this kind of refinement is not acceptable in the applications mentioned above. CompCert [9] addresses the problem by introducing a wellfounded order in the simulation, but it works only for sequential programs. It is difficult to apply this idea to do thread-local verification of concurrent program refinement, which enables us to know T1 k T2 ⊑ S1 k S2 by proving T1 ⊑ S1 and T2 ⊑ S2. In practice, the termination preservation in the refinement proofs of individual threads could be easily broken by the interference from their environments (i.e., other threads running in parallel). For instance, a method call of a lock-free data structure (e.g., Treiber stack) may never terminate when other threads call the methods and update the shared memory infinitely often. As we will explain in Sec. 2, the key challenge here is to effectively specify the environments’ effects on the termination preservation of individual threads. As far as we know, no previous work can use “compositional” thread-local reasoning to verify termination-preserving re- finement between (whole) concurrent programs. In this paper, we first propose novel rely/guarantee conditions which can effectively specify the interference over the termination properties between a thread and its environment. Traditional rely/guarantee conditions [8] are binary relations of program states and they specify the state updates. We extend them with a boolean tag indicating whether a state update may let the thread or its environment make more moves. With the help of our new rely/guarantee conditions, we then propose a new simulation RGSim-T, and a new Hoare-style program logic, both of which support compositional verification of termination-preserving refinement of concurrent programs. Our work is based on our previous compositional simulation RGSim [11] (which unfortunately cannot preserve termination), and is inspired by Hoffmann et al.’s program logic for lock-
(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 terminationpreserving refinement of concurrent programs. As an extension of RGSim, it considers the interference between threads and the environments by taking our novel rely/guarantee conditions 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 individual 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 reasoning) rules, we also provide a set of unary rules (built upon the unary program logic LRG [3]) that can reason about conditional 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 supports 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 finegrained concurrent objects, or to verify the full correctness of optimizations of concurrent programs, i.e., the optimized program 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 correctness + 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 reS 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 between the source and the target (note S and T here are whole program 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 correspond 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 terminationpreserving 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 wellfounded 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 impossible 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 compositionality, 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
Then,to prove termination-preserving concurrent refinement,it source level.Our new simulation RGSim-T extends RGSim by in seems natural to combine the two ideas and have a simulation pa corporating the idea of metrics to achieve termination preservation rameterized with environment interference and a metric decreasing It is parameterized with the new rely (and guarantee)conditions so for target steps that correspond to no steps at the source.Therefore that we know how an environment step could affect the metric.The we require T2<T1 and T4<T3 in the case of Fig.2(b).But formal definition of RGSim-T is given in Sec.4. how would the environment steps change the metric? Relationships to lock-freedom,obstruction-freedom and wait- First attempt.Our first attempt to answer this question is to allow freedom.If the source program is just a single atomic opera- environment steps to arbitrarily change the metrics associated with tion (e.g.x++),our new simulation RGSim-T can be viewed as a the target program configurations.Therefore it is possible to have proof technique for lock-freedom of the target,which ensures that T2<Ts in Fig.2(b). there always exists some thread that will complete an operation at The resulting simulation,however,is still not compositional the source level in a finite number of steps.That is,the failure of w.r.t.parallel compositions.For instance,for the following two a thread to finish its operation must be caused by the successful threads in the target program: completion of source operations by its environment. In fact,the simulations of our first and second attempts can whi1e(i==0)i-；‖wh11e(i=0)1+; be viewed as proof techniques for obstruction-freedom and wait- we can prove that this simulation holds between each of them and freedom respectively of concurrent objects.Obstruction-freedom the source program skip,if we view i as local data used only ensures that every thread will complete its operation whenever it is at the target level.We could define the metric as 1 if i=0 executed in isolation (i.e..without interference from other threads). and 0 otherwise.For the left thread.it decreases the metric if it In the simulation of our first attempt,though a thread is allowed to executes the loop body.The increment of i by its environment not make progress under environment interference,it has to com- (the right thread)may change i back to 0,increasing the metric. plete some source operations when its environments do not inter- This is allowed in our simulation.The case for the right thread is fere.Wait-freedom ensures the completion of the operation of any symmetric.However,if we view the parallel composition of the two thread.Correspondingly in the simulation of our second attempt,a threads as a whole program,it may not terminate,thus cannot be a thread has to make progress no matter what the environment does termination-preserving refinement of skipskip 2.2 Program Logic Second attempt.The first attempt is too permissive to have par- The compositionality of our new simulation RGSim-T allows us allel compositionality,because we allow a thread to make more to decompose the refinement for large programs to refinements moves whenever its environment interferes with it.Thus our sec- ond attempt enforces the metric of a thread to decrease or stay un- for small program units,therefore we could derive a set of syn- tactic Hoare-style rules for refinement verification,as we did for changed under environment interference.For the case of Fig.2(b) we require T3<Tl on environment steps. RGSim [11].For instance,a sequential composition rule may be in This simulation is compositional,but it is too strong and can- the following form: not be satisfied by many useful refinements.For instance.T.in RH(P)T3S1(P}RH(P)T3S2{Q} Fig.I(c)uses a compare-and-swap (cas)instruction to atomically RF{P}T1;T2≤S1;S2{Q} update x.It is a correct lock-free implementation of S in concur- rent settings,but the new simulation of our second attempt does Here we use RHPIT<SO}to represent the corresponding not hold between T and S.If an environment step between lines 3 syntactic judgment of RGSim-T.R denotes the environment inter and 4 of T increments x,the cas at line 4 will return false and T ference.P,and P'are relational assertions that relate the pro- needs to execute another round of loop.Therefore such an environ- gram states at the target and the source levels.The rule says if we ment step increases the number of silent steps of Te that correspond could establish refinements (in fact,RGSim-Ts)between T and to no moves of S.However,our new simulation does not allow an S1,and between T2 and S2,we know T1:T2 refines S1:S2.We environment step to increase the metric,so the simulation cannot could give similar rules for parallel composition and other compo- be established. sitional commands However,in many cases the correspondence between program Our solution.Our solution lies in the middle ground of the two units at the target and the source levels cannot be determined failed attempts.We specify explicitly in the parameter R which statically.That is,just by looking at T;T2 and S1;S2,we may environment steps may make the current thread move more (i.e. not know statically that T refines S and T2 refines S2 and then allow the thread's metric to increase in the simulation).Here we apply the above sequential composition rule.To see the problem. distinguish in R the steps that correspond to source level moves we unfold the while-loop of Te in Fig.I and get the following T from those that do not.We allow the metric to be increased by the former (as in our first attempt),but not by the latter (which must local t,done; 4 while (!done){ 2 decrease or preserve the metric,as in our second attempt). t:=x; 5 t:=X; 3 done :cas(&x,t,t+1);6 done :cas(&x,t,t+1); This approach is based on the observation that the failure of 7] cas in Te of Fig.I(c)must be caused by an environment step that successfully increments x,which corresponds to a step at the Clearly T refines S too.However,whether the cas instruction at source level.Although the termination of the current thread Te is line 3 fulfils the operation in S or not depends on whether the com- delayed,the whole system consisting of both the current thread and parison succeeds in runtime.Thus we cannot apply the composi- the environment progresses by making a corresponding step at the tionality rules for RGSim-T to decompose the refinement about T source level.Therefore,the delay of the termination of the current We have to refer to the semantics of the simulation definition to thread should be acceptable,and we should allow such environment prove the refinement,which would be rather ineffective for large steps to increase the metric of the current thread scale programs.Similar issues also show up in our earlier work on In this paper,we follow the idea of rely/guarantee reasoning [8 RGSim [11],and in relational Hoare logic [1]and relational sepa- and use the rely condition to specify environment steps.However ration logic [25]if they are applied to concurrent settings we extend the traditional rely conditions with an extra boolean tag To address this problem,we extend the assertion language to indicating whether an environment step corresponds to a step at the specify as auxiliary state the source code remaining to be refined
Then, to prove termination-preserving concurrent refinement, it seems natural to combine the two ideas and have a simulation parameterized with environment interference and a metric decreasing for target steps that correspond to no steps at the source. Therefore we require |T2| < |T1| and |T4| < |T3| in the case of Fig. 2(b). But how would the environment steps change the metric? First attempt. Our first attempt to answer this question is to allow environment steps to arbitrarily change the metrics associated with the target program configurations. Therefore it is possible to have |T2| < |T3| in Fig. 2(b). The resulting simulation, however, is still not compositional w.r.t. parallel compositions. For instance, for the following two threads in the target program: while(i==0) i--; k while(i==0) i++; we can prove that this simulation holds between each of them and the source program skip, if we view i as local data used only at the target level. We could define the metric as 1 if i = 0 and 0 otherwise. For the left thread, it decreases the metric if it executes the loop body. The increment of i by its environment (the right thread) may change i back to 0, increasing the metric. This is allowed in our simulation. The case for the right thread is symmetric. However, if we view the parallel composition of the two threads as a whole program, it may not terminate, thus cannot be a termination-preserving refinement of skipkskip. Second attempt. The first attempt is too permissive to have parallel compositionality, because we allow a thread to make more moves whenever its environment interferes with it. Thus our second attempt enforces the metric of a thread to decrease or stay unchanged under environment interference. For the case of Fig. 2(b), we require |T3| ≤ |T2| on environment steps. This simulation is compositional, but it is too strong and cannot be satisfied by many useful refinements. For instance, Tc in Fig. 1(c) uses a compare-and-swap (cas) instruction to atomically update x. It is a correct lock-free implementation of S in concurrent settings, but the new simulation of our second attempt does not hold between Tc and S. If an environment step between lines 3 and 4 of Tc increments x, the cas at line 4 will return false and Tc needs to execute another round of loop. Therefore such an environment step increases the number of silent steps of Tc that correspond to no moves of S. However, our new simulation does not allow an environment step to increase the metric, so the simulation cannot be established. Our solution. Our solution lies in the middle ground of the two failed attempts. We specify explicitly in the parameter R which environment steps may make the current thread move more (i.e., allow the thread’s metric to increase in the simulation). Here we distinguish in R the steps that correspond to source level moves from those that do not. We allow the metric to be increased by the former (as in our first attempt), but not by the latter (which must decrease or preserve the metric, as in our second attempt). This approach is based on the observation that the failure of cas in Tc of Fig. 1(c) must be caused by an environment step that successfully increments x, which corresponds to a step at the source level. Although the termination of the current thread Tc is delayed, the whole system consisting of both the current thread and the environment progresses by making a corresponding step at the source level. Therefore, the delay of the termination of the current thread should be acceptable, and we should allow such environment steps to increase the metric of the current thread. In this paper, we follow the idea of rely/guarantee reasoning [8] and use the rely condition to specify environment steps. However, we extend the traditional rely conditions with an extra boolean tag indicating whether an environment step corresponds to a step at the source level. Our new simulation RGSim-T extends RGSim by incorporating the idea of metrics to achieve termination preservation. It is parameterized with the new rely (and guarantee) conditions so that we know how an environment step could affect the metric. The formal definition of RGSim-T is given in Sec. 4. Relationships to lock-freedom, obstruction-freedom and waitfreedom. If the source program is just a single atomic operation (e.g. x++), our new simulation RGSim-T can be viewed as a proof technique for lock-freedom of the target, which ensures that there always exists some thread that will complete an operation at the source level in a finite number of steps. That is, the failure of a thread to finish its operation must be caused by the successful completion of source operations by its environment. In fact, the simulations of our first and second attempts can be viewed as proof techniques for obstruction-freedom and waitfreedom respectively of concurrent objects. Obstruction-freedom ensures that every thread will complete its operation whenever it is executed in isolation (i.e., without interference from other threads). In the simulation of our first attempt, though a thread is allowed to not make progress under environment interference, it has to complete some source operations when its environments do not interfere. Wait-freedom ensures the completion of the operation of any thread. Correspondingly in the simulation of our second attempt, a thread has to make progress no matter what the environment does. 2.2 Program Logic The compositionality of our new simulation RGSim-T allows us to decompose the refinement for large programs to refinements for small program units, therefore we could derive a set of syntactic Hoare-style rules for refinement verification, as we did for RGSim [11]. For instance, a sequential composition rule may be in the following form: R ⊢ {P}T1 S1{P ′} R ⊢ {P ′}T2 S2{Q} R ⊢ {P}T1; T2 S1; S2{Q} Here we use R ⊢ {P}T S{Q} to represent the corresponding syntactic judgment of RGSim-T. R denotes the environment interference. P, Q and P ′ are relational assertions that relate the program states at the target and the source levels. The rule says if we could establish refinements (in fact, RGSim-Ts) between T1 and S1, and between T2 and S2, we know T1; T2 refines S1; S2. We could give similar rules for parallel composition and other compositional commands. However, in many cases the correspondence between program units at the target and the source levels cannot be determined statically. That is, just by looking at T1; T2 and S1; S2, we may not know statically that T1 refines S1 and T2 refines S2 and then apply the above sequential composition rule. To see the problem, we unfold the while-loop of Tc in Fig. 1 and get the following T ′ c: 1 local t, done; 4 while (!done) { 2 t := x; 5 t := x; 3 done := cas(&x,t,t+1); 6 done := cas(&x,t,t+1); 7 } Clearly T ′ c refines S too. However, whether the cas instruction at line 3 fulfils the operation in S or not depends on whether the comparison succeeds in runtime. Thus we cannot apply the compositionality rules for RGSim-T to decompose the refinement about T ′ c . We have to refer to the semantics of the simulation definition to prove the refinement, which would be rather ineffective for large scale programs. Similar issues also show up in our earlier work on RGSim [11], and in relational Hoare logic [1] and relational separation logic [25] if they are applied to concurrent settings. To address this problem, we extend the assertion language to specify as auxiliary state the source code remaining to be refined
In addition to the binary judgment R[P)T<S{Q).we intro- (Evenr)e:=... (Label)::=eT duce a unary judgment in the form of R[P A arem(S))T[QA arem(S)for refinements that cannot be decomposed.Here (Store)s,s∈Par一al(Heap)h,h∈Addr一al arem(S)means S is the remaining source to be refined by the (Sae)o,∑：=(s,h) (mstr）c,e=.. target.Then R,GF IP A arem(S)ITQ A arem(skip)says (Expr)E,E:=x n E+E... that T refines S,since the postcondition shows at the end of the (BExp)B,B ::true false E=E !B .. target T there are no remaining operations from S to be refined. We provide the following rule to derive the binary judgment from (Srmr)C,C::=skip c(C)I C1;C2 I if (B)C1 else C2 while (B)C CC2 the unary one: RH[P A arem(S))T{Q A arem(skip)) Figure 3.Generic language at target and source levels. RF{P}T≤S{Q} On the other hand,if the final remaining source is the same as To prove that T shown above preserves the termination of S'. the initial one,we know the execution steps of the target correspond we set the initial number of tokens to 1.We use up the token at to zero source steps.Then for the T above,we can give pre-and the first iteration,but could gain another token during the iteration post-conditions for line 3 as follows: (either by self moves or by environment steps)to pay for the next {...A arem(S) iteration.We can see that the above reasoning with tokens coincides done :cas(&x,t,t+1) with the direct refinement proof in our simulation RGSim-T.In fact, {...A (done A arem(skip)V-done A arem(S))} RGSim-T can serve as the meta-theory of our logic. The use of tokens as an explicit metric for termination reason- As the postcondition shows,whether the cas instruction refines S or not is now conditional upon the value of done.Thanks to the ing poses another challenge,which is to handle infinite nondeter- minism.Consider the following target C. new assertions arem(S),we can reduce the relational and semantic refinement proofs to unary and syntactic Hoare-style reasoning. C: x:=0;whi1e(1>0)1--; The key to verifying the preservation of termination is the rule Assume the environment R may arbitrarily update i when x is not for while loops.One may first think of the total correctness rule for 0,but does not change anything when x is 0.We hope to verify C while loops in Hoare-style logics (e.g.,[19]).However,preserving refines skip.We can see that the loop in C must terminate (thus the the termination does not necessarily mean that the code must termi- refinement holds).and the number n of tokens must be no less than nate,and the total correctness rule would not be applicable in many the value of i at the beginning of the loop.But we cannot decide cases.For example,the following T and S'never terminate: the value of n before executing x :=0.This example cannot be T": S': verified if we have to predetermine and specify the metric for the local t; while loops at the very beginning of the whole program. while (true){ To address this issue,we introduce the following hiding rule: while (true) t:=x; x++; RHip)Cig cas(&x,t,t+1); RHIplw}Cilglw) Here pw discards all the knowledge about tokens in p.For the but T<S'holds for our RGSim-T-Every iteration of T above example,we can hide the number of tokens after we verify either corresponds to a step of S',or is interfered by environment the while loop.Then we do not need to specify the number of steps corresponding to source moves. tokens in the precondition of the whole program.We formally Inspired by Hoffmann et al.'s logic for lock-freedom [7],we present the set of logic rules in Sec.5. introduce a counter n(i.e.the number of tokens assigned to the current thread)as a while-specific metric,which means the thread 3. can only run the loop for no more than n rounds before it or its Formal Settings and Termination-Preserving environment fulfils one or more source-level moves.The counter Refinement is treated as an auxiliary state,and decreases at the beginning of In this section,we define the termination-preserving refinement C, every round of loop (i.e..we pay one token for each iteration). which is the proof goal of our RGSim-T and logic. If we reach a step in the loop body that corresponds to source moves,we could reset the counter to increase the number of tokens. 3.1 The Language Tokens could also increase under environment interference if the environment step corresponds to source moves.Correspondingly Fig.3 shows the programming language for both the source and our WHILE rule is in the following form (we give a simplified the target levels.We model the program semantics as a labeled version to demonstrate the idea here.The actual rule is given in transition system.A label t that will be associated with a state Sec.5): transition is either an event e or T.The latter marks a silent step generating no events. PAB P'*wf(1)RH(P)CIP) A state o is a pair of a store and a heap.The store s is a fi- RHP)while (B)CIPA-B) nite partial mapping from program variables to values (e.g.,inte- gers and memory addresses)and a heap h maps memory addresses We use wf(1)to represent one token,and"+"for normal sepa to values.Statements C are either primitive instructions or compo- rating conjunction in separation logic.To verify the loop body C sitions of them.A single-step execution of statements is modeled we use the precondition P',which has one less token than P,show- as a labeled transition:(C,)(C,').We abstract away the ing that one token has been consumed to start this new round of form of an instruction c.It may generate an external event (e.g., loop.During the execution of C,the number of token could be in- print(E)generates an output event).It may be non-deterministic creased if C itself or its environment steps correspond to source (e.g.,x :nondet assigns a random value to x).It may also be moves.As usual,the loop invariant P needs to be re-established at blocked at some states (e.g.,requesting a lock).We assume prim- the end of C. itive instructions are atomic in the semantics.We also provide an
In addition to the binary judgment R ⊢ {P}T S{Q}, we introduce a unary judgment in the form of R ⊢ {P ∧ arem(S)}T {Q ∧ arem(S ′ )} for refinements that cannot be decomposed. Here arem(S) means S is the remaining source to be refined by the target. Then R, G ⊢ {P ∧ arem(S)}T {Q ∧ arem(skip)} says that T refines S, since the postcondition shows at the end of the target T there are no remaining operations from S to be refined. We provide the following rule to derive the binary judgment from the unary one: R ⊢ {P ∧ arem(S)}T{Q ∧ arem(skip)} R ⊢ {P}T S{Q} On the other hand, if the final remaining source is the same as the initial one, we know the execution steps of the target correspond to zero source steps. Then for the T ′ c above, we can give pre- and post-conditions for line 3 as follows: {· · · ∧ arem(S)} done := cas(&x, t, t+1) {· · · ∧ (done ∧ arem(skip) ∨ ¬done ∧ arem(S))} As the postcondition shows, whether the cas instruction refines S or not is now conditional upon the value of done. Thanks to the new assertions arem(S), we can reduce the relational and semantic refinement proofs to unary and syntactic Hoare-style reasoning. The key to verifying the preservation of termination is the rule for while loops. One may first think of the total correctness rule for while loops in Hoare-style logics (e.g., [19]). However, preserving the termination does not necessarily mean that the code must terminate, and the total correctness rule would not be applicable in many cases. For example, the following T ′′ c and S ′ never terminate: T ′′ c : S ′ : local t; while (true){ while (true) t := x; x++; cas(&x, t, t+1); } but T ′′ c S ′ holds for our RGSim-T () — Every iteration of T ′′ c either corresponds to a step of S ′ , or is interfered by environment steps corresponding to source moves. Inspired by Hoffmann et al.’s logic for lock-freedom [7], we introduce a counter n (i.e. the number of tokens assigned to the current thread) as a while-specific metric, which means the thread can only run the loop for no more than n rounds before it or its environment fulfils one or more source-level moves. The counter is treated as an auxiliary state, and decreases at the beginning of every round of loop (i.e., we pay one token for each iteration). If we reach a step in the loop body that corresponds to source moves, we could reset the counter to increase the number of tokens. Tokens could also increase under environment interference if the environment step corresponds to source moves. Correspondingly our WHILE rule is in the following form (we give a simplified version to demonstrate the idea here. The actual rule is given in Sec. 5): P ∧ B ⇒ P ′ ∗ wf(1) R ⊢ {P ′}C{P} R ⊢ {P}while (B) C{P ∧ ¬B} We use wf(1) to represent one token, and “∗” for normal separating conjunction in separation logic. To verify the loop body C, we use the precondition P ′ , which has one less token than P, showing that one token has been consumed to start this new round of loop. During the execution of C, the number of token could be increased if C itself or its environment steps correspond to source moves. As usual, the loop invariant P needs to be re-established at the end of C. (Event) e ::= . . . (Label) ι ::= e | τ (Store) s, s ∈ PVar ⇀ Val (Heap) h, h ∈ Addr ⇀ Val (State) σ, Σ ::= (s, h) (Instr) c, ::= . . . (Expr) E,E ::= x | n | E + E | . . . (BExp) B, B ::= true | false | E = E | !B | . . . (Stmt) C, C ::= skip | c | hCi | C1; C2 | if (B) C1 else C2 | while (B) C | C1 kC2 Figure 3. Generic language at target and source levels. To prove that T ′′ c shown above preserves the termination of S ′ , we set the initial number of tokens to 1. We use up the token at the first iteration, but could gain another token during the iteration (either by self moves or by environment steps) to pay for the next iteration. We can see that the above reasoning with tokens coincides with the direct refinement proof in our simulation RGSim-T. In fact, RGSim-T can serve as the meta-theory of our logic. The use of tokens as an explicit metric for termination reasoning poses another challenge, which is to handle infinite nondeterminism. Consider the following target C. C: x := 0; while(i > 0) i--; Assume the environment R may arbitrarily update i when x is not 0, but does not change anything when x is 0. We hope to verify C refines skip. We can see that the loop in C must terminate (thus the refinement holds), and the number n of tokens must be no less than the value of i at the beginning of the loop. But we cannot decide the value of n before executing x := 0. This example cannot be verified if we have to predetermine and specify the metric for the while loops at the very beginning of the whole program. To address this issue, we introduce the following hiding rule: R ⊢ {p}C{q} R ⊢ {⌊p⌋w}C{⌊q⌋w} Here ⌊p⌋w discards all the knowledge about tokens in p. For the above example, we can hide the number of tokens after we verify the while loop. Then we do not need to specify the number of tokens in the precondition of the whole program. We formally present the set of logic rules in Sec. 5. 3. Formal Settings and Termination-Preserving Refinement In this section, we define the termination-preserving refinement ⊑, which is the proof goal of our RGSim-T and logic. 3.1 The Language Fig. 3 shows the programming language for both the source and the target levels. We model the program semantics as a labeled transition system. A label ι that will be associated with a state transition is either an event e or τ . The latter marks a silent step generating no events. A state σ is a pair of a store and a heap. The store s is a fi- nite partial mapping from program variables to values (e.g., integers and memory addresses) and a heap h maps memory addresses to values. Statements C are either primitive instructions or compositions of them. A single-step execution of statements is modeled as a labeled transition: (C, σ) ι −→ (C ′ , σ′ ). We abstract away the form of an instruction c. It may generate an external event (e.g., print(E) generates an output event). It may be non-deterministic (e.g., x := nondet assigns a random value to x). It may also be blocked at some states (e.g., requesting a lock). We assume primitive instructions are atomic in the semantics. We also provide an
(C,a)-→+abort (C,a)+(C',d）ET(C,d,) (RelAssn)P,Q,I:=B I own(x)I emp IE→E|E片E P*QI PVQp... ETr(C,o,) ETr(C.o,e::E) (FullAssn)p.q :=P I arem(C)I wf(E)p]a Lp]w (C,a)→*(skip,) (C,a)→+(C,a) ETr(C,o',8) p*9 pV q... ETr(C,o,) ETr(C,o,E) (RelAct)R,G ::[P]I PxQ I P&QI R+R I R+.. Figure 4.Co-inductive definition of ETr(C,o,E). Figure 5.Assertion language. atomic block (C)to execute a piece of code C atomically.Then the source levels from which the simulation holds,and Q is about the generic language in Fig.3 is expressive enough for the source the pair of final states when the target and the source terminate.So and the target programs which may have different granularities of before we give our definition of RGSim-T,we first introduce our state accesses.Due to the space limit,the operational semantics and assertion language more details about the language are formally presented in TR [13] 4.1 Conventions.We usually write blackboard bold or capital letters Assertions and New Rely/Guarantee Conditions (s,h,C,E,B and C)for the notations at the source level to We show the syntax of the basic assertion language in Fig.5. distinguish from the target-level ones (s,h,o,c,E,B and C). including the state assertions P and Q,and our new rely/guarantee Below we use_->-for zero or multiple-step transitions with conditions R and G (let's first ignore the assertions p and g,which no events generated,+-for multiple-step transitions without will be explained in Sec.5). events,and+for multiple-step transitions with only one The state assertions P and Q relate the program states o and event e generated. at the target and source levels.They are separation logic assertions over a pair of states.We show their semantics in the top part of 3.2 Termination-Preserving Event Trace Refinement Fig.6.For simplicity,we assume the program variables used in Now we formally define the refinement relation that relates the target code are different from the ones in the source (e.g.,we the observable event traces generated by the source and the target use and X for target and source level variables respectively).B programs.A trace is a finite or infinite sequence of external events holds if it evaluates to true at the disjoint union of the target and the e,and may end with a termination marker or an abortion marker source stores s and s.We treat program variables as resources [15] It is co-inductively defined as follows. and use own()for the ownership of the program variable x. The assertion E E2 specifies a singleton heap of the targer (EvrTrace)::=Ie::&(co-inductive) level with E2 stored at the address E and requires that the stores We use ETr(C,o,E)to say that the trace is produced by contain variables used to evaluate E and E2.Its counterpart for executing C from the state o.It is co-inductively defined in Fig.4 source level heaps is represented as EE2,whose semantics is Here skip plays the role of a flag showing the end of execution (the defined similarly.emp describes empty stores and heaps at both normal termination).Unsafe executions lead to abort.We know levels.Semantics of separating conjunction P+Q is similar as if C diverges at o,then its trace is either of infinite length or in separation logic,except that it is now lifted to assertions over finite but does not end with or For instance,while(true)skip relational states (o,)The union of two disjoint relational states only produces an empty trace e,and while (true)[print(1)only (1,1)and (2,2)is defined in the middle part of Fig.6.We produces an infinite trace of output events. will define the assertion lpl in Sec.5(see Fig.8),which ignores Then we define a refinement (C,o)(C,)saying that ev- the additional information other than the relational states about p. ery event trace generated by (C,o)at the target level can be repro- Our new rely/guarantee assertions R and G specify the transi- duced by (C,>at the source.Since we could distinguish traces of tions over the relational states (o.)and also the effects on termi- diverging executions from those of terminating executions,the re- nation preservation.Their semantics is defined in the bottom part finement definition ensures that if(C,)diverges,so does (C,) of Fig.6.Here we use S for the relational states.A model con- Thus we know the target preserves the termination of the source. sists of the initial relational state S,the resulting state S',and an effect bit b to record whether the target transitions correspond to Definition 1 (Termination-Preserving Refinement). some source steps and can affect the termination preservation of (C,o)g(C,∑)iffE.ETr(C,o,E)=→ET(C,∑，E) the current thread (for R)or other threads(for G). We use [P]for identity transitions with the relational states RGSim-T:A Compositional Simulation with satisfying P.The action Px Q says that the initial relational states satisfy P and the resulting states satisfy Q.For these two kinds Termination Preservation of actions,we do not care whether there is any source step in the Below we propose RGSim-T,a new simulation as a compositional transition satisfying them(the effect bit b in their interpretations proof technique for the above termination-preserving refinement. could either be true or false).We also introduce a new action As we explained in Sec.2,the key to compositionality is to param- P O asserting that one or more steps are made at the source level eterize the simulation with the interferences between the programs (the effect bit b must be true).Following LRG [3],we introduce and their environments.In this paper,we specify the interferences separating conjunction over actions to locally reason about shared using rely/guarantee conditions [8],but extend them to also specify state updates.RI*R2 means that the actions Ri and R2 start from the effects on the termination preservation of individual threads. disjoint relational states and the resulting states are also disjoint Our simulation relation between C and C is in the form of But here we also require consistency over the effect bits for the two R,G,I (P)C3 C(Q).It takes R.G.I,P and Q as pa- disjoint state transitions.We use R for the transitive closure of rameters.R and G are rely and guarantee conditions specifying the R,where the effect bits in consecutive transitions are accumulated interference between the current thread and its environment.The The syntactic sugars ld,Emp and True represent arbitrary identity assertion I specifies the consistency relation between states at the transitions,empty transitions and arbitrary transitions respectively target and the source levels,which needs to be preserved during Since we logically split states into local and shared parts as in the execution.P specifies the pair of initial states at the target and LRG [3],we need a precise invariant I to fence actions over shared
(C, σ) −→+ abort ETr(C, σ, ) (C, σ) e −→+ (C′ , σ′ ) ETr(C′ , σ′ , E) ETr(C, σ, e ::E) (C, σ) −→∗ (skip, σ′ ) ETr(C, σ, ⇓) (C, σ) −→+ (C′ , σ′ ) ETr(C′ , σ′ , E) ETr(C, σ, E) Figure 4. Co-inductive definition of ETr(C, σ, E). atomic block hCi to execute a piece of code C atomically. Then the generic language in Fig. 3 is expressive enough for the source and the target programs which may have different granularities of state accesses. Due to the space limit, the operational semantics and more details about the language are formally presented in TR [13]. Conventions. We usually write blackboard bold or capital letters (s, h, Σ, , E, B and C) for the notations at the source level to distinguish from the target-level ones (s, h, σ, c, E, B and C). Below we use −→∗ for zero or multiple-step transitions with no events generated, −→+ for multiple-step transitions without events, and e −→ + for multiple-step transitions with only one event e generated. 3.2 Termination-Preserving Event Trace Refinement Now we formally define the refinement relation ⊑ that relates the observable event traces generated by the source and the target programs. A trace E is a finite or infinite sequence of external events e, and may end with a termination marker ⇓ or an abortion marker . It is co-inductively defined as follows. (EvtTrace) E ::= ⇓ | | ǫ | e ::E (co-inductive) We use ETr(C, σ, E) to say that the trace E is produced by executing C from the state σ. It is co-inductively defined in Fig. 4. Here skip plays the role of a flag showing the end of execution (the normal termination). Unsafe executions lead to abort. We know if C diverges at σ, then its trace E is either of infinite length or finite but does not end with ⇓ or . For instance, while (true) skip only produces an empty trace ǫ, and while (true) {print(1)} only produces an infinite trace of output events. Then we define a refinement (C, σ) ⊑ (C, Σ), saying that every event trace generated by (C, σ) at the target level can be reproduced by (C, Σ) at the source. Since we could distinguish traces of diverging executions from those of terminating executions, the re- finement definition ensures that if (C, σ) diverges, so does (C, Σ). Thus we know the target preserves the termination of the source. Definition 1 (Termination-Preserving Refinement). (C, σ) ⊑ (C, Σ) iff ∀E. ETr(C, σ, E) =⇒ ETr(C, Σ, E). 4. RGSim-T: A Compositional Simulation with Termination Preservation Below we propose RGSim-T, a new simulation as a compositional proof technique for the above termination-preserving refinement. As we explained in Sec. 2, the key to compositionality is to parameterize the simulation with the interferences between the programs and their environments. In this paper, we specify the interferences using rely/guarantee conditions [8], but extend them to also specify the effects on the termination preservation of individual threads. Our simulation relation between C and C is in the form of R, G, I |= {P}C C{Q}. It takes R, G, I, P and Q as parameters. R and G are rely and guarantee conditions specifying the interference between the current thread and its environment. The assertion I specifies the consistency relation between states at the target and the source levels, which needs to be preserved during the execution. P specifies the pair of initial states at the target and (RelAssn) P, Q, I ::= B | own(x) | emp | E 7→ E | E Z⇒ E | P ∗ Q | P ∨ Q | TpU | . . . (FullAssn) p, q ::= P | arem(C) | wf(E) | ⌊p⌋a | ⌊p⌋w | p ∗ q | p ∨ q | . . . (RelAct) R, G ::= [P] | P ⋉Q | P ∝ Q | R∗R | R+ | . . . Figure 5. Assertion language. the source levels from which the simulation holds, and Q is about the pair of final states when the target and the source terminate. So before we give our definition of RGSim-T, we first introduce our assertion language. 4.1 Assertions and New Rely/Guarantee Conditions We show the syntax of the basic assertion language in Fig. 5, including the state assertions P and Q, and our new rely/guarantee conditions R and G (let’s first ignore the assertions p and q, which will be explained in Sec. 5). The state assertions P and Q relate the program states σ and Σ at the target and source levels. They are separation logic assertions over a pair of states. We show their semantics in the top part of Fig. 6. For simplicity, we assume the program variables used in the target code are different from the ones in the source (e.g., we use x and X for target and source level variables respectively). B holds if it evaluates to true at the disjoint union of the target and the source stores s and s. We treat program variables as resources [15] and use own(x) for the ownership of the program variable x. The assertion E1 7→ E2 specifies a singleton heap of the target level with E2 stored at the address E1 and requires that the stores contain variables used to evaluate E1 and E2. Its counterpart for source level heaps is represented as E1 Z⇒ E2, whose semantics is defined similarly. emp describes empty stores and heaps at both levels. Semantics of separating conjunction P ∗ Q is similar as in separation logic, except that it is now lifted to assertions over relational states (σ, Σ). The union of two disjoint relational states (σ1, Σ1) and (σ2, Σ2) is defined in the middle part of Fig. 6. We will define the assertion TpU in Sec. 5 (see Fig. 8), which ignores the additional information other than the relational states about p. Our new rely/guarantee assertions R and G specify the transitions over the relational states (σ, Σ) and also the effects on termination preservation. Their semantics is defined in the bottom part of Fig. 6. Here we use S for the relational states. A model consists of the initial relational state S, the resulting state S ′ , and an effect bit b to record whether the target transitions correspond to some source steps and can affect the termination preservation of the current thread (for R) or other threads (for G). We use [P] for identity transitions with the relational states satisfying P. The action P ⋉ Q says that the initial relational states satisfy P and the resulting states satisfy Q. For these two kinds of actions, we do not care whether there is any source step in the transition satisfying them (the effect bit b in their interpretations could either be true or false). We also introduce a new action P ∝ Q asserting that one or more steps are made at the source level (the effect bit b must be true). Following LRG [3], we introduce separating conjunction over actions to locally reason about shared state updates. R1 ∗R2 means that the actions R1 and R2 start from disjoint relational states and the resulting states are also disjoint. But here we also require consistency over the effect bits for the two disjoint state transitions. We use R + for the transitive closure of R, where the effect bits in consecutive transitions are accumulated. The syntactic sugars Id, Emp and True represent arbitrary identity transitions, empty transitions and arbitrary transitions respectively. Since we logically split states into local and shared parts as in LRG [3], we need a precise invariant I to fence actions over shared