(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 ev￾ery event trace generated by (C, σ) at the target level can be repro￾duced 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 param￾eterize 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 pa￾rameters. 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 transi￾tions over the relational states (σ, Σ) and also the effects on termi￾nation preservation. Their semantics is defined in the bottom part of Fig. 6. Here we use S for the relational states. A model con￾sists 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