(Events）e:= level languages are atomic in the interleaving semantics.Below we 444 (Labels)o::=er use --for zero or multiple-step transitions with no events (a)Events and Transition Labels generated,and*_for multiple-step transitions with only one event e generated. (LState) (LEpr）E.∈LState-→lntn 3.2 The Event Trace Refinement (LBExp)B∈LState→{true,fase}L Now we can formally define the refinement relation that relates (LInstr）c ∈LState一P(Labels×LState)U{abort)) the set of externally observable event traces generated by the target and the source programs.A trace is a sequence of events e,and may (LStmt)C ::skip c C1;C2 if (B)C1 else C2 end with a termination marker done or a fault marker abort. while (B)C CiC2 (LStep)-→L∈P(LStu/{skip}x LState)x Labels (EvrTrace)::=e done abort e:: x((LStmt x LState)Ufabort)) Definition 1(Event Trace Set).ETrSet,(C,o)represents a set of (b)The Low-Level Language external event traces produced by C inn steps from the state: 。ETrSeto(C,a)e{e}: (HState）∑：=. (HExpr）E ∈HState→ntL ·ETrSetn+-i(C,o)e (HBEp)B∈HState→{true,false} {E|(C,o)-→(C',o)AE∈ETrSetn(C',a') V(C,a)e(C',a）AE∈ETrSet(C',a)AE=e:E (HInstr）c∈HState一P(Labels x HState)U{abort})】 V(C.o)abort A&=abort (HSmmt)C::=skip c C1::C2 if B then C1 else C2 VC=skip A&=done. while B do C C1C2 (HSep)-→L∈P(HSm/八skp}×HState)x Labels We define ETrSet(C,)asU ETrSetn(C,a). x((HSmt x HState)U{abort)) We overload the notation and use ETrSet(C.>for the high-level language.Then we define an event trace refinement as the subset (c)The High-Level Language relation between event trace sets,which is similar to Leroy's re- finement property [19]. Figure 2.Generic Languages at Target and Source Levels Definition 2(Event Trace Refinement).We say (C,o)is an e- trace refinement of (C,)i.e.,(C,a)(C,).if and only if lead to abort.Note that the semantics of an instruction could be ETrSet(C,o)C ETrSet(C,>) non-deterministic.Moreover,it might be undefined on some states making it possible to model blocking operations such as acquiring The refinement is defined for program configurations instead of a lock. for code only because the initial states may affect the behaviors of programs.In this case,the transformation T should translate Statements are either primitive instructions or compositions of states as well as code.We overload the notation and use T()to them.skip is a special statement used as a flag to show the end of represent the state transformation,and use CC for executions.A single-step execution of statements is modeled as a labeled transitionwhich is a triple of an initial program o,∑.o=T()=→(C,σ)E(C,), configuration (a pair of statement and state).a label and a resulting then Correct(T)defined in formula (1.1)can be reformulated as configuration.It is undefined when the initial statement is skip.The step aborts if an unsafe instruction is executed. Correct(T)会∀C,C.C=T(C)=→C二rC.(3.1) The high-level language (source language)is defined similarly 4. The RGSim Relation in Figure 2(c),but it is important to note that its states and primitive instructions may be different from those in the low-level language. The e-trace refinement is defined directly over the externally ob- The compound statements are almost the same as their low-level servable behaviors of programs.It is intuitive,and also abstract in counterparts.C;C2 and CC2 are sequential and parallel com- that it is independent of language details.However,as we explained positions of C and C2 respectively.Note that we choose to use the before,it is not compositional w.rt.parallel compositions.In this same set of compound statements in the two languages for simplic- section we propose RGSim.which can be viewed as a composi- ity only.This is not required by our simulation relation,although tional proof technique that allows us to derive the simple e-trace the analogous program constructs of the two languages (e.g.,paral- refinement and then verify the corresponding transformation T. lel compositions ClC2 and CC2)make it convenient for us to 4.1 The Definition discuss the compositionality later. Figure 3 shows part of the definition of_which gives Our co-inductively defined RGSim relation is in the form of the high-level operational semantics of statements.We often omit (C,a,R,G),≤a7,(C,∑，R,G),which is a simulation between the subscript H (or L)in_>H(or_)and the label on program configurations (C,o)and (C.>)It is parametrized with top of the arrow when it is T.The semantics is mostly standard the rely and guarantee conditions at the low level and the high level, We only show the rules for primitive instructions and parallel com- which are binary relations over states: positions here.Note that when a primitive instruction c is blocked R,g∈P(LState×LState),R,G∈P(HState×HState). at state >(i.e.,dom(c)),we let the program configuration reduce to itself.For example,the instruction lock(1)would be The simulation also takes two additional parameters:the step in- variant o and the postcondition y.which are both relations between blocked when 1 is not 0,making it be repeated until 1 becomes the low-level and the high-level states. 0:whereas unlock(1)simply sets 1 to 0 at any time and would never be blocked.Primitive instructions in the high-level and low- a,Y,S∈P(LState×HState). 458(Events) e ::= ... (Labels) o ::= e | τ (a) Events and Transition Labels (LState) σ ::= ... (LExpr) E ∈ LState → Int⊥ (LBExp) B ∈ LState → {true, false}⊥ (LInstr) c ∈ LState  P((Labels × LState) ∪ {abort}) (LStmt) C ::= skip | c | C1; C2 | if (B) C1 else C2 | while (B) C | C1 C2 (LStep) −→L ∈ P((LStmt/{skip} × LState) × Labels ×((LStmt × LState) ∪ {abort})) (b) The Low-Level Language (HState) Σ ::= ... (HExpr) E ∈ HState → Int⊥ (HBExp) B ∈ HState → {true, false}⊥ (HInstr) c ∈ HState  P((Labels × HState) ∪ {abort}) (HStmt) C ::= skip | c | C1; ; C2 | if B then C1 else C2 | while B do C | C1C2 (HStep) −→L ∈ P((HStmt/{skip} × HState) × Labels ×((HStmt × HState) ∪ {abort})) (c) The High-Level Language Figure 2. Generic Languages at Target and Source Levels lead to abort. Note that the semantics of an instruction could be non-deterministic. Moreover, it might be undefined on some states, making it possible to model blocking operations such as acquiring a lock. Statements are either primitive instructions or compositions of them. skip is a special statement used as a flag to show the end of executions. A single-step execution of statements is modeled as a labeled transition −→L , which is a triple of an initial program configuration (a pair of statement and state), a label and a resulting configuration. It is undefined when the initial statement is skip. The step aborts if an unsafe instruction is executed. The high-level language (source language) is defined similarly in Figure 2(c), but it is important to note that its states and primitive instructions may be different from those in the low-level language. The compound statements are almost the same as their low-level counterparts. C1; ; C2 and C1C2 are sequential and parallel com￾positions of C1 and C2 respectively. Note that we choose to use the same set of compound statements in the two languages for simplic￾ity only. This is not required by our simulation relation, although the analogous program constructs of the two languages (e.g., paral￾lel compositions C1 C2 and C1C2) make it convenient for us to discuss the compositionality later. Figure 3 shows part of the definition of −→H , which gives the high-level operational semantics of statements. We often omit the subscript H (or L) in −→H (or −→L ) and the label on top of the arrow when it is τ . The semantics is mostly standard. We only show the rules for primitive instructions and parallel com￾positions here. Note that when a primitive instruction c is blocked at state Σ (i.e., Σ ∈ dom(c)), we let the program configuration reduce to itself. For example, the instruction lock(l) would be blocked when l is not 0, making it be repeated until l becomes 0; whereas unlock(l) simply sets l to 0 at any time and would never be blocked. Primitive instructions in the high-level and low￾level languages are atomic in the interleaving semantics. Below we use −→ ∗ for zero or multiple-step transitions with no events generated, and e −→∗ for multiple-step transitions with only one event e generated. 3.2 The Event Trace Refinement Now we can formally define the refinement relation that relates the set of externally observable event traces generated by the target and the source programs. A trace is a sequence of events e, and may end with a termination marker done or a fault marker abort. (EvtTrace) E ::= | done | abort | e::E Definition 1 (Event Trace Set). ETrSetn(C, σ) represents a set of external event traces produced by C in n steps from the state σ: • ETrSet0(C, σ) {} ; • ETrSetn+1(C, σ) {E | (C, σ) −→ (C , σ ) ∧E∈ETrSetn(C , σ ) ∨ (C, σ) e −→ (C , σ ) ∧ E ∈ETrSetn(C , σ ) ∧ E =e::E ∨ (C, σ) −→ abort ∧ E =abort ∨ C =skip ∧ E =done} . We define ETrSet(C, σ) as n ETrSetn(C, σ). We overload the notation and use ETrSet(C, Σ) for the high-level language. Then we define an event trace refinement as the subset relation between event trace sets, which is similar to Leroy’s re- finement property [19]. Definition 2 (Event Trace Refinement). We say (C, σ) is an e￾trace refinement of (C, Σ), i.e., (C, σ) (C, Σ), if and only if ETrSet(C, σ) ⊆ ETrSet(C, Σ). The refinement is defined for program configurations instead of for code only because the initial states may affect the behaviors of programs. In this case, the transformation T should translate states as well as code. We overload the notation and use T(Σ) to represent the state transformation, and use C T C for ∀σ, Σ. σ = T(Σ) =⇒ (C, σ) (C, Σ), then Correct(T) defined in formula (1.1) can be reformulated as Correct(T) ∀C, C. C = T(C) =⇒ C T C . (3.1) 4. The RGSim Relation The e-trace refinement is defined directly over the externally ob￾servable behaviors of programs. It is intuitive, and also abstract in that it is independent of language details. However, as we explained before, it is not compositional w.r.t. parallel compositions. In this section we propose RGSim, which can be viewed as a composi￾tional proof technique that allows us to derive the simple e-trace refinement and then verify the corresponding transformation T. 4.1 The Definition Our co-inductively defined RGSim relation is in the form of (C, σ, R, G) α;γ (C, Σ, R, G), which is a simulation between program configurations (C, σ) and (C, Σ). It is parametrized with the rely and guarantee conditions at the low level and the high level, which are binary relations over states: R, G∈P(LState × LState), R, G ∈ P(HState × HState). The simulation also takes two additional parameters: the step in￾variant α and the postcondition γ, which are both relations between the low-level and the high-level states. α, γ, ζ ∈ P(LState × HState). 458