Rely-Guarantee-Based Simulation A:9 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. (EutTrace)&::=e done abort e::8 Definition 3.1 (Event Trace Set).ETrSetn(C,o)represents a set of external event traces produced by C in n steps from the state o: (1)ETrSeto(C,a)e; (2)ETrSetn+1(C,σ）≌ {E|(C,o)-→(C',a）AEEETrSetn(C,a) V(C,a)(C',a')AE'EETrSetn(C',')AE=e::E' V(C,o)-abort A&=abort VC=skip AE=done}. We define ETrSet(C,o)as U ETrSetn(C,o). We overload the notation and use ETrSet(C,>)for the high-level language.Note that we treat abort as a specific behavior instead of undefined arbitrary behaviors.The choices should depend on applications.The ideas in the paper should also apply for the latter setting,though we need to change our refinement and simulation relations defined below. Then we define an event trace refinement as the subset relation between event trace sets,which is similar to Leroy's refinement property [Leroy 2009]. Definition 3.2 (Event Trace Refinement).We say (C,o)is an e-trace refinement of (C,>),i.e.,(C,)(C >)if and only if ETrSet(C,a)C ETrSet(C,E) 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 Cr C for o,∑.o=T()→(C,σ)三(C,), then Correct(T)defined in formula(1.1)can be reformulated as Correct(T)≌VC,C.C=T(C)→CgrC, (3.1) From the above e-trace refinement definition,we can derive an e-trace equivalence relation by requiring both directions hold: (C,σ)≈(C,)(C,o)E(C,)A(C,)E(C,o), and use C≈rC for Vo,∑.o=T()→(C,o)≈(C,). 4.THE RGSIM RELATION The e-trace refinement is defined directly over the externally observable 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 composi- tions.In this section we propose RGSim,which can be viewed as a compositional proof technique that allows us to derive the simple e-trace refinement and then verify the corresponding transformation T. ACM Transactions on Programming Languages and Systems,Vol.V,No.N,Article A,Publication date:January YYYY.Rely-Guarantee-Based Simulation A:9 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 3.1 (Event Trace Set). ETrSetn(C, σ) represents a set of external event traces produced by C in n steps from the state σ: (1) ETrSet0(C, σ) , {ϵ} ; (2) 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. Note that we treat abort as a specific behavior instead of undefined arbitrary behaviors. The choices should depend on applications. The ideas in the paper should also apply for the latter setting, though we need to change our refinement and simulation relations defined below. Then we define an event trace refinement as the subset relation between event trace sets, which is similar to Leroy’s refinement property [Leroy 2009]. Definition 3.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) From the above e-trace refinement definition, we can derive an e-trace equivalence relation by requiring both directions hold: (C, σ) ≈ (C, Σ) , (C, σ) ⊑ (C, Σ) ∧ (C, Σ) ⊑ (C, σ), and use C ≈T C for ∀σ, Σ. σ = T(Σ) =⇒ (C, σ) ≈ (C, Σ). 4. THE RGSIM RELATION The e-trace refinement is defined directly over the externally observable 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 composi￾tions. In this section we propose RGSim, which can be viewed as a compositional proof technique that allows us to derive the simple e-trace refinement and then verify the corresponding transformation T. ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Article A, Publication date: January YYYY