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 anIn addition to the binary judgment R ⊢ {P}T  S{Q}, we intro￾duce 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 termi￾nate, 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 sepa￾rating conjunction in separation logic. To verify the loop body C, we use the precondition P ′ , which has one less token than P, show￾ing that one token has been consumed to start this new round of loop. During the execution of C, the number of token could be in￾creased 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 reason￾ing poses another challenge, which is to handle infinite nondeter￾minism. 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., inte￾gers and memory addresses) and a heap h maps memory addresses to values. Statements C are either primitive instructions or compo￾sitions 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 prim￾itive instructions are atomic in the semantics. We also provide an