Rely-Guarantee-Based Simulation A:11 (C,)a (c,) (C.o)- 一(C,) ge Gle (C,)-3-(C,) (C)-3-(Cs) (a)Program Steps (b)Environment Steps Fig.5.Simulation Diagrams of RGSim -Starting from a-related states,each step of C corresponds to zero or multiple steps of C,and the resulting states are a-related too.If an external event is produced in the step of C,the same event should be produced by C.We show the simulation diagram with events generated by the program steps in Figure 5(a),where solid lines denote hypotheses and dashed lines denote conclusions,following Leroy's notations [Leroy 2009]. -The a relation reflects the abstractions from the low-level machine model to the high-level one,and is preserved by the related transitions at the two levels (so it is an invariant).For instance,when verifying a fine-grained implementation of sets, the a relation may relate a concrete representation in memory (e.g,a linked-list)at the low level to the corresponding abstract mathematical set at the high level. -The corresponding transitions of C and C need to be in (g,G*).That is,for each step of C,its state transition should satisfy the guarantee g,and the corresponding transition made by the multiple steps of C should be in the transitive closure of G. The guarantees are abstractions of the programs'behaviors.As we will show later in the PAR rule in Figure 7,they will serve as the rely conditions of the sibling threads at the time of parallel compositions.Note that we do not need each step of C to be in G,although we could do so.This is because we only care about the coarse-grained behaviors (with mumbling)of the source that are used to simulate the target.We will explain more by the example (4.1)in Section 4.2. If C terminates,then C terminates as well,and the final states should be related by the postcondition y.We require y a,i.e.,the final state relation is not weaker than the step invariant. C is not safe only if C is not safe either.This means the transformation should not make a safe high-level program unsafe at the low level. Whatever the low-level environment R and the high-level one R do,as long as the state transitions are a-related,they should not affect the simulation between C and C,as shown in Figure 5(b).Here a step in R may correspond to zero or multiple steps of R.Note that different from the program steps,some steps of R may not correspond to steps of R.On the other hand,only requiring that R be simulated by R(see (4.2)in Section 4.2)is not sufficient for parallel compositionality,which we will explain later in Section 4.2. Then based on the simulation,we hide the states by the precondition and de- fine the RGSim relation between programs only.By the definition we know a if (C,R,g)(C,R,G),i.e.,the precondition needs to be no weaker than the step invariant.Usually in practice a is very weak and naturally implied by the pre-and post-conditions and y,e.g.,and y are the same as a in examples in Section 6. RGSim is sound w.r:t.the e-trace refinement (Definition 3.2).That is,(C.,RG) (C,E,R,G)ensures that (C,o)does not have more observable behaviors than(C,E). ACM Transactions on Programming Languages and Systems,Vol.V,No.N,Article A,Publication date:January YYYY
Rely-Guarantee-Based Simulation A:11 (C, σ) (C ′ , σ′ ) (C, Σ) (C ′ , Σ ′ ) α ≼ G ❄ e α ≼ ❄ G ∗ e (C, σ) (C, σ′ ) (C, Σ) (C, Σ ′ ) α ≼ ❄ R α ≼ ❄ R ∗ (a) Program Steps (b) Environment Steps Fig. 5. Simulation Diagrams of RGSim — Starting from α-related states, each step of C corresponds to zero or multiple steps of C, and the resulting states are α-related too. If an external event is produced in the step of C, the same event should be produced by C. We show the simulation diagram with events generated by the program steps in Figure 5(a), where solid lines denote hypotheses and dashed lines denote conclusions, following Leroy’s notations [Leroy 2009]. — The α relation reflects the abstractions from the low-level machine model to the high-level one, and is preserved by the related transitions at the two levels (so it is an invariant). For instance, when verifying a fine-grained implementation of sets, the α relation may relate a concrete representation in memory (e.g., a linked-list) at the low level to the corresponding abstract mathematical set at the high level. — The corresponding transitions of C and C need to be in ⟨G, G∗ ⟩α. That is, for each step of C, its state transition should satisfy the guarantee G, and the corresponding transition made by the multiple steps of C should be in the transitive closure of G. The guarantees are abstractions of the programs’ behaviors. As we will show later in the PAR rule in Figure 7, they will serve as the rely conditions of the sibling threads at the time of parallel compositions. Note that we do not need each step of C to be in G, although we could do so. This is because we only care about the coarse-grained behaviors (with mumbling) of the source that are used to simulate the target. We will explain more by the example (4.1) in Section 4.2. — If C terminates, then C terminates as well, and the final states should be related by the postcondition γ. We require γ ⊆ α, i.e., the final state relation is not weaker than the step invariant. — C is not safe only if C is not safe either. This means the transformation should not make a safe high-level program unsafe at the low level. — Whatever the low-level environment R and the high-level one R do, as long as the state transitions are α-related, they should not affect the simulation between C and C, as shown in Figure 5(b). Here a step in R may correspond to zero or multiple steps of R. Note that different from the program steps, some steps of R may not correspond to steps of R. On the other hand, only requiring that R be simulated by R (see (4.2) in Section 4.2) is not sufficient for parallel compositionality, which we will explain later in Section 4.2. Then based on the simulation, we hide the states by the precondition ζ and de- fine the RGSim relation between programs only. By the definition we know ζ ⊆ α if (C, R, G) ≼α;ζnγ (C, R, G), i.e., the precondition needs to be no weaker than the step invariant. Usually in practice α is very weak and naturally implied by the pre- and post-conditions ζ and γ, e.g., ζ and γ are the same as α in examples in Section 6. RGSim is sound w.r.t. the e-trace refinement (Definition 3.2). That is, (C, σ, R, G) ≼α;γ (C, Σ, R, G) ensures that (C, σ) does not have more observable behaviors than (C, Σ). ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Article A, Publication date: January YYYY
A:12 Hongjin Liang et al. InitRelr()≌o,Σ.o=T()=→(o,)∈S BB(a,)|Bo=B}BAB(a,>)|BaAB} Intuit(a)eo,∑，a','.(a,)∈aAo≤a'A∑≤'=→(a',)∈a a出B≌{(o1出o2,21出2)|(o1,)∈aA(o2,∑2)∈B}n#a兰(mna)C()出a) Boa{(a,)|30.(a,)∈aA(0,)∈B} a-1≌{(E,o)|(a,)∈a} lda{(o,a)lo∈LState} True (a,a')|a,o'E LState} RM isMidOf(a,B:R,R)a,a',∑，.(a,o),(②，)∈(R,R）aoa =→∀0.(a,0)∈aA(0,)∈B =→30.(o,o),(0,0)∈(R,Rr)aA(0,8),(②，)∈(RM,R)8 Fig.6.Auxiliary Definitions for RGSim THEOREM 4.3 (SOUNDNESS/ADEQUACY).If there exist R,g,R,G,a and y such that (C,R,g)(C.,R,G),then (C,)(C,). The soundness theorem shows that RGSim is a proof technique for the simple and natural refinement which is what we ultimately care about.The theorem can be proved by first strengthening the relies to the identity transitions and weakening the guarantees to the universal relations.Then we prove that the resulting simulation under identity environments implies the e-trace refinement.The mechanized proof in the Coq proof assistant [2010]is available online. For program transformations,since the initial state for the target program is trans- formed from the initial state for the source,we use InitRelr(C)(defined in Figure 6)to say the transformation T over states ensures the binary precondition COROLLARY 4.4.If there exist R,g,R,G,a,and y such that InitRelr(C)and (C,R,g)(C,R,G),then C ET C. 4.2.Compositionality Rules RGSim is compositional w.r.t.various program constructs,including parallel composi- tions.We present the compositionality rules in Figure 7,which gives us a relational proof method for concurrent program transformations. As in the R-G logic [Jones 1983],we require that the pre-and post-conditions be stable under the interference from the environments.Here we introduce the concept of stability of a relation w.r.t.a set of transition pairs A P((LState x LState)x (HState x HState)). Definition 4.5 (Stability).Sta(C,A)holds iff for all o,o',and,f(o,)∈(and(o,o),(E,)∈A,then(a',)∈( Usually we need Sta(C,(R,R)),which says whenever holds initially and R and R* perform related actions,the resulting states still satisfy By unfolding(R,R*)a,we could see that a itself is stable w.r.t.any a-related transitions,i.e.,Sta(a,(R,R*)). Another simple example is given below,where both environments could increment x and the unary stable assertion x >0 is lifted to the relation C: (兰{(a,)|σ(x)=(x)Ao(x)≥0} a{(a,)|σ(x)=(x)} R{(o,a)|σ'=o{xσ(x)+1} R会{（公，'）|'={x,(x)+1} We can prove Sta(,(R,R*)).Stability of the pre-and post-conditions under the en- vironments'interference is assumed as an implicit side condition at every proof rule ACM Transactions on Programming Languages and Systems,Vol.V,No.N,Article A,Publication date:January YYYY
A:12 Hongjin Liang et al. InitRelT(ζ) , ∀σ, Σ. σ = T(Σ) =⇒ (σ, Σ) ∈ ζ B⇔⇔B , {(σ, Σ) | B σ = B Σ} B∧∧B , {(σ, Σ) | B σ ∧ B Σ} Intuit(α) , ∀σ, Σ, σ′ , Σ ′ . (σ, Σ) ∈ α ∧ σ ⊆ σ ′ ∧ Σ ⊆ Σ ′ =⇒ (σ ′ , Σ ′ ) ∈ α α ⊎ β , {(σ1 ⊎ σ2, Σ1 ⊎ Σ2) | (σ1, Σ1) ∈ α ∧ (σ2, Σ2) ∈ β} η # α , (η ∩ α) ⊆ (η ⊎ α) β ◦ α , {(σ, Σ) | ∃θ. (σ, θ) ∈ α ∧ (θ, Σ) ∈ β} α −1 , {(Σ, σ) | (σ, Σ) ∈ α} Id , {(σ, σ) | σ ∈ LState} True , {(σ, σ′ ) | σ, σ′ ∈ LState} RM isMidOf (α, β; R, R) , ∀σ, σ′ , Σ, Σ ′ . ((σ, σ′ ),(Σ, Σ ′ )) ∈ ⟨R, R⟩β◦α =⇒ ∀θ. (σ, θ) ∈ α ∧ (θ, Σ) ∈ β =⇒ ∃θ ′ .((σ,σ′ ),(θ,θ′ ))∈ ⟨R, RM⟩α ∧ ((θ,θ′ ),(Σ,Σ ′ ))∈ ⟨RM, R⟩β Fig. 6. Auxiliary Definitions for RGSim THEOREM 4.3 (SOUNDNESS/ADEQUACY). If there exist R, G, R, G, α and γ such that (C, σ, R, G) ≼α;γ (C, Σ, R, G), then (C, σ) ⊑ (C, Σ). The soundness theorem shows that RGSim is a proof technique for the simple and natural refinement ⊑, which is what we ultimately care about. The theorem can be proved by first strengthening the relies to the identity transitions and weakening the guarantees to the universal relations. Then we prove that the resulting simulation under identity environments implies the e-trace refinement. The mechanized proof in the Coq proof assistant [2010] is available online. For program transformations, since the initial state for the target program is transformed from the initial state for the source, we use InitRelT(ζ) (defined in Figure 6) to say the transformation T over states ensures the binary precondition ζ. COROLLARY 4.4. If there exist R, G, R, G, α, ζ and γ such that InitRelT(ζ) and (C, R, G) ≼α;ζnγ (C, R, G), then C ⊑T C. 4.2. Compositionality Rules RGSim is compositional w.r.t. various program constructs, including parallel compositions. We present the compositionality rules in Figure 7, which gives us a relational proof method for concurrent program transformations. As in the R-G logic [Jones 1983], we require that the pre- and post-conditions be stable under the interference from the environments. Here we introduce the concept of stability of a relation ζ w.r.t. a set of transition pairs Λ ∈ P((LState × LState) × (HState × HState)). Definition 4.5 (Stability). Sta(ζ,Λ) holds iff for all σ, σ ′ , Σ and Σ ′ , if (σ, Σ) ∈ ζ and ((σ, σ′ ),(Σ, Σ ′ )) ∈ Λ, then (σ ′ , Σ ′ ) ∈ ζ. Usually we need Sta(ζ,⟨R, R ∗ ⟩α), which says whenever ζ holds initially and R and R ∗ perform related actions, the resulting states still satisfy ζ. By unfolding ⟨R, R ∗ ⟩α, we could see that α itself is stable w.r.t. any α-related transitions, i.e., Sta(α,⟨R, R ∗ ⟩α). Another simple example is given below, where both environments could increment x and the unary stable assertion x ≥ 0 is lifted to the relation ζ: ζ , {(σ, Σ) | σ(x) = Σ(x) ∧ σ(x) ≥ 0} α , {(σ, Σ) | σ(x) = Σ(x)} R , {(σ, σ′ ) | σ ′ = σ{x ❀ σ(x) + 1}} R , {(Σ, Σ ′ ) | Σ ′ = Σ{x ❀ Σ(x) + 1}} We can prove Sta(ζ,⟨R, R ∗ ⟩α). Stability of the pre- and post-conditions under the environments’ interference is assumed as an implicit side condition at every proof rule ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Article A, Publication date: January YYYY
Rely-Guarantee-Based Simulation A:13 SCQ (skip,R,ld)(skip,B,ld)(SKIP) (C1,R,g)3a:cx(C1,R,G)(C2,R,g)3ai7xn(C2,R,G (C1:C2,R,g)a:cxn(C1;;C2,R,G) _(SEQ) (C,R,9)61x(C,R,G)、(C2,R,9)a2x(C2,R,G) S≤(B台B)Gi=(Gn(BmB)》G2=(n(Bm)≤ (if (B)C1 else C2,R,g):(if B then Ci else C2,R,G) _(IF) (C,R,9)1(C,R,G) 7S(BB)7=(n(BAB))((-B-B)) (WHILE) (while (B)C,R.g):(while B do C,R,G) (C,R1,91)≤=x1(C1,R1.G)(C,2,92)a:xg(C2,R2,G2) g1SR292CR1G1≤R2G2R1 (PAR) (C1lIC2,RinR2,91 UG2)0:6(TO)(CC2,R1nR2,G1 UG2) (C,R,9)≤xy(C,R,)(GUy)≤a'ca Sta(a',(g,G*）a -(STREN-a) (C,R,g)≤acx1(C,R,G) (C,R,g)3a:x(C,R,G)aCa'Sta(a,(R,R")) (WEAKEN-Q) (C,R,G)(C,R,G) (C,R,9)5a:x(C,R,G) S'S YCYCa R'CR R'CR GCG GCG (CONSEQ) (C,R',g')a:cx (C,R',G) (C,R,g):(C,R,G) nCB n#,7,a} Intuit(fa,,,B,n,,R,R1,R}) Sta(n,[(G,G")a,(R1,Ri)a}) (FRAME) (C,R出R1,9出G1)≤aw8:(cwnx(wn)(C,R出R1,G出G1) (C,R,G)≤ :K7(M,RM,GM) (M,RM,GM)8:6x(C,R,G)RM isMidOf(a,B;R,R*) (TRANS) (C,R,g)B0a:(605)x (no7)(C,R,G) Fig.7.Compositionality Rules for RGSim.At each proof rule,we implicitly assume that the pre-and post- conditions are stable under the environments'interference (Definition 4.5),and the relies and guarantees are closed over identity transitions. in Figure 7,e.g.,we assume Sta(s,(R,R*))in the SKIP rule.We also require implic- itly that the relies and guarantees are closed over identity transitions,since stuttering steps will not affect observable event traces. In Figure 7,the rules SKIP,SEQ,IF and WHILE reveal a high degree of similarity to the corresponding inference rules in Hoare logic.In the SEQ rule,y serves as the postcondition of Ci and Ci and the precondition of C2 and C2 at the same time.The IF rule requires the boolean conditions of both sides to be evaluated to the same value under the precondition The definitions of the sets BB and BAB are given in Figure 6.The rule also requires the precondition to imply the step invariant a.In the WHILE rule,the y relation is viewed as a loop invariant preserved at the loop entry point,and needs to ensure BB. ACM Transactions on Programming Languages and Systems,Vol.V,No.N,Article A,Publication date:January YYYY
Rely-Guarantee-Based Simulation A:13 ζ ⊆ α (skip, R, Id) ≼α;ζnζ (skip, R, Id) (SKIP) (C1, R, G) ≼α;ζnγ (C1, R, G) (C2, R, G) ≼α;γnη (C2, R, G) (C1; C2, R, G) ≼α;ζnη (C1; ; C2, R, G) (SEQ) (C1, R, G) ≼α;ζ1nγ (C1, R, G) (C2, R, G) ≼α;ζ2nγ (C2, R, G) ζ ⊆ (B⇔⇔B) ζ1 = (ζ ∩ (B∧∧B)) ζ2 = (ζ ∩ (¬B∧∧¬B)) ζ ⊆ α (if (B) C1 else C2, R, G) ≼α;ζnγ (if B then C1 else C2, R, G) (IF) (C, R, G) ≼α;γ1nγ (C, R, G) γ ⊆ (B⇔⇔B) γ1 = (γ ∩ (B∧∧B)) γ2 = (γ ∩ (¬B∧∧¬B)) (while (B) C, R, G) ≼α;γnγ2 (while B do C, R, G) (WHILE) (C1, R1, G1) ≼α;ζnγ1 (C1, R1, G1) (C2, R2, G2) ≼α;ζnγ2 (C2, R2, G2) G1 ⊆ R2 G2 ⊆ R1 G1 ⊆ R2 G2 ⊆ R1 (C1 ∥C2, R1 ∩ R2, G1 ∪ G2) ≼α;ζn(γ1∩γ2) (C19C2, R1 ∩ R2, G1 ∪ G2) (PAR) (C, R, G) ≼α;ζnγ (C, R, G) (ζ ∪ γ) ⊆ α ′ ⊆ α Sta(α ′ ,⟨G, G ∗ ⟩α) (C, R, G) ≼α′ ;ζnγ (C, R, G) (STREN-α) (C, R, G) ≼α;ζnγ (C, R, G) α ⊆ α ′ Sta(α,⟨R, R ∗ ⟩α′ ) (C, R, G) ≼α′ ;ζnγ (C, R, G) (WEAKEN-α) (C, R, G) ≼α;ζnγ (C, R, G) ζ ′ ⊆ ζ γ ⊆ γ ′ ⊆ α R′ ⊆ R R ′ ⊆ R G ⊆ G′ G ⊆ G ′ (C, R′ , G ′ ) ≼α;ζ ′nγ′ (C, R ′ , G ′ ) (CONSEQ) (C, R, G) ≼α;ζnγ (C, R, G) η ⊆ β η # {ζ, γ, α} Intuit({α, ζ, γ, β, η, R, R, R1, R1}) Sta(η, {⟨G, G ∗ ⟩α,⟨R1, R ∗ 1⟩β}) (C, R ⊎ R1, G ⊎ G1) ≼α⊎β;(ζ⊎η)n(γ⊎η) (C, R ⊎ R1, G ⊎ G1) (FRAME) (C, R, G) ≼α;ζnγ (M, RM, GM) (M, RM, GM) ≼β;δnη (C, R, G) RM isMidOf (α, β; R, R ∗ ) (C, R, G) ≼β◦α;(δ◦ζ)n(η◦γ) (C, R, G) (TRANS) Fig. 7. Compositionality Rules for RGSim. At each proof rule, we implicitly assume that the pre- and postconditions are stable under the environments’ interference (Definition 4.5), and the relies and guarantees are closed over identity transitions. in Figure 7, e.g., we assume Sta(ζ,⟨R, R ∗ ⟩α) in the SKIP rule. We also require implicitly that the relies and guarantees are closed over identity transitions, since stuttering steps will not affect observable event traces. In Figure 7, the rules SKIP, SEQ, IF and WHILE reveal a high degree of similarity to the corresponding inference rules in Hoare logic. In the SEQ rule, γ serves as the postcondition of C1 and C1 and the precondition of C2 and C2 at the same time. The IF rule requires the boolean conditions of both sides to be evaluated to the same value under the precondition ζ. The definitions of the sets B ⇔⇔ B and B ∧∧B are given in Figure 6. The rule also requires the precondition ζ to imply the step invariant α. In the WHILE rule, the γ relation is viewed as a loop invariant preserved at the loop entry point, and needs to ensure B⇔⇔B. ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Article A, Publication date: January YYYY
A:14 Hongjin Liang et al. Parallel compositionality.The PAR rule shows parallel compositionality of RGSim. The interference constraints say that two threads can be composed in parallel if one thread's guarantee implies the rely of the other.After parallel composition,they are expected to run in the common environment and their guaranteed behaviors contain each single thread's behaviors. Note that,although RGSim does not require every step of the high-level program to be in its guarantee (see the first two conditions in Definition 4.2),this relaxation does not affect the parallel compositionality.This is because the target could have less behaviors than the source.To let CIC2 simulate Cill C2,we only need a subset of the interleavings of Ci and C2 to simulate those of Ci and C2.Thus the high-level relies and guarantees need to ensure the existence of those interleavings only.Below we give a simple example to explain this subtle issue.We can prove (x:=x+2,R,9)5ax1(区：=x+1;x:=x+1,R,G), (4.1) where the relies and the guarantees say x can be increased by 2 and a,and y relate x of the two sides: r=g会{(a,）|a'=Va=a{x(x)+2}: R=G会{(E,')|=∑V={x(x)+2}: a=(=y{(a,)|o(x)=(x}. Note that the high-level program is actually finer-grained than its guarantee,but to prove (4.1)we only need the execution in which it goes two steps to the end with- out interference from its environment.Also we can prove (print(x),R,G) (print(x),R,G).Here we use the instruction print(E)to observe the value of x,which will produce an external event out(n)if E evaluates to n.Then by the PAR rule,we get (x:=x+2lprint(x),R,G):c ((x:=x+1;x:=x+1)print(x),R,G), which does not violate the natural meaning of refinements.That is,all the possible external events produced by the low-level side can also be produced by the high-level side,although the latter could have more external behaviors due to its finer granular- ity. Another subtlety in the RGSim definition is with the fifth condition over the envi- ronments,which is crucial for parallel compositionality.One may think a more natural alternative to this condition is to require that R be simulated by R: If(o,')E R,then there exists such that (②，)∈R*and(C,o',R,g)ay(C,',R,G). (4.2) We refer to this modified simulation definition as<'.Unfortunately,<'does not have parallel compositionality.As a counter-example,if the invariant a says the left-side x is not greater than the right-side x,i.e., a≌{(o,)|o(x)≤(x}, we could prove the following: (x:=x+1,Id,True):axa (x:=x+2,ld,True); (4.3) (x:=0;print(x),True,Id):axa (x:=0;print(x),True,Id). (4.4) Here we use ld and True(defined in Figure 6)for the sets of identity transitions and arbitrary transitions respectively,and overload the notations at the low level to the high level.However,the following refinement does not hold after parallel composition: (x:=x+1l(x:=0;print(x)),Id,True):ax(x:=x+2(x:=0;print(x)),Id,True). ACM Transactions on Programming Languages and Systems,Vol.V,No.N,Article A,Publication date:January YYYY
A:14 Hongjin Liang et al. Parallel compositionality. The PAR rule shows parallel compositionality of RGSim. The interference constraints say that two threads can be composed in parallel if one thread’s guarantee implies the rely of the other. After parallel composition, they are expected to run in the common environment and their guaranteed behaviors contain each single thread’s behaviors. Note that, although RGSim does not require every step of the high-level program to be in its guarantee (see the first two conditions in Definition 4.2), this relaxation does not affect the parallel compositionality. This is because the target could have less behaviors than the source. To let C19C2 simulate C1 ∥C2, we only need a subset of the interleavings of C1 and C2 to simulate those of C1 and C2. Thus the high-level relies and guarantees need to ensure the existence of those interleavings only. Below we give a simple example to explain this subtle issue. We can prove (x:=x+2, R, G) ≼α;ζnγ (x:=x+1;x:=x+1, R, G), (4.1) where the relies and the guarantees say x can be increased by 2 and α, ζ and γ relate x of the two sides: R = G , {(σ, σ′ ) | σ ′ = σ ∨ σ ′ = σ{x ❀ σ(x) + 2}} ; R = G , {(Σ, Σ ′ ) | Σ ′ = Σ ∨ Σ ′ = Σ{x ❀ Σ(x) + 2}} ; α = ζ = γ , {(σ, Σ) | σ(x) = Σ(x)} . Note that the high-level program is actually finer-grained than its guarantee, but to prove (4.1) we only need the execution in which it goes two steps to the end without interference from its environment. Also we can prove (print(x), R, G) ≼α;ζnγ (print(x), R, G). Here we use the instruction print(E) to observe the value of x, which will produce an external event out(n) if E evaluates to n. Then by the PAR rule, we get (x:=x+2∥print(x), R, G) ≼α;ζnγ ((x:=x+1;x:=x+1)9print(x), R, G), which does not violate the natural meaning of refinements. That is, all the possible external events produced by the low-level side can also be produced by the high-level side, although the latter could have more external behaviors due to its finer granularity. Another subtlety in the RGSim definition is with the fifth condition over the environments, which is crucial for parallel compositionality. One may think a more natural alternative to this condition is to require that R be simulated by R: If (σ, σ′ ) ∈ R,then there exists Σ ′ such that (Σ, Σ ′ ) ∈ R ∗ and (C, σ′ , R, G) ≼′ α;γ (C, Σ ′ , R, G). (4.2) We refer to this modified simulation definition as ≼′ . Unfortunately, ≼′ does not have parallel compositionality. As a counter-example, if the invariant α says the left-side x is not greater than the right-side x, i.e., α , {(σ, Σ) | σ(x) ≤ Σ(x)} , we could prove the following: (x:=x+1, Id, True) ≼ ′ α;αnα (x:=x+2, Id, True) ; (4.3) (x:=0;print(x), True, Id) ≼ ′ α;αnα (x:=0;print(x), True, Id). (4.4) Here we use Id and True (defined in Figure 6) for the sets of identity transitions and arbitrary transitions respectively, and overload the notations at the low level to the high level. However, the following refinement does not hold after parallel composition: (x:=x+1∥(x:=0;print(x)), Id, True) ≼ ′ α;αnα (x:=x+29(x:=0;print(x)), Id, True). ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Article A, Publication date: January YYYY
Rely-Guarantee-Based Simulation A:15 This is because the rely R(or R)is an abstraction of all the permitted behaviors in the environment of a thread t.Any thread t'whose behaviors are allowed in R(or R)can run in parallel with t.Thus to obtain parallel compositionality,we have to ensure that the simulation is preserved with any possible sibling thread t'.With our definition 3,the refinement (4.4)is not provable,because after some a-related transitions of environments,the target may print a value smaller than the one printed by the source. Other rules.We also develop some other useful rules about RGSim.For example,the STREN-a rule allows us to replace the invariant a by a stronger invariant a'.We need to check that a'is indeed an invariant preserved by the related program steps,i.e., Sta(a',(g,G*))holds.Symmetrically,the WEAKEN-a rule requires a to be preserved by environment steps related by the weaker invariant a'.As usual,the pre-and post- conditions,the relies and the guarantees can be strengthened or weakened by the CONSEQ rule. The FRAME rule allows us to use local specifications [Reynolds 2002].When veri- fying the simulation between C and C.we need to only talk about the locally-used resource in a,and y,and the local relies and guarantees R,g,R and G.Then the proof can be reused in contexts where some extra resource n is used,and the accesses of it respect the invariant B and R1,G,Ri and G1.We give the auxiliary definitions in Figure 6.The disjoint union w between states is lifted to state pairs.A state re- lation a is intuitionistic,denoted by Intuit(@),if it is monotone w.r.t.the extension of states.The disjointness n#a says that any state pair satisfying both n and a can be split into two disjoint state pairs satisfying n and a respectively.For example,let n≌{(o,)|o(y)=(y)}anda≌{(a,)|σ(x)=∑(x)}where x and y are two distinct variables,then both n and a are intuitionistic and n a holds.We also require n to be stable under interference from the programs(i.e.,the programs do not change the extra resource)and the extra environments.We use n#{a}as a shorthand for (#)A(#)A (n#a).Similar representations are used in this rule. Finally,the transitivity rule TRANS allows us to verify a transformation by using an intermediate level as a bridge.The intermediate environment Ry should be chosen with caution so that the (Bo a)-related transitions can be decomposed into B-related and a-related transitions,as illustrated in Figure 4(b).Here o defines the composition of two relations and isMidOf defines the side condition over the environments,as shown in Figure 6.We use 6 for a middle-level state. Soundness.All the rules in Figure 7 are sound,i.e.,for each rule the premises im- ply the conclusion.We prove their soundness by co-induction,directly following the definition of RGSim.The proofs are checked in the Cog proof assistant [2010]. Instantiations of relies and guarantees.We can derive the sequential refinement and the fully-abstract-semantics-based refinement by instantiating the rely conditions in RGSim.For example,the refinement(4.5)over closed programs assumes identity en- vironments,making the interference constraints in the PAR rule unsatisfiable.This confirms the observation in Section 2.1 that the sequential refinement loses parallel compositionality. (C,ld,True)(C,Id,True) (4.5) The refinement (4.6)assumes arbitrary environments,which makes the interference constraints in the PAR rule trivially true.But this assumption is too strong:usually (4.6)cannot be satisfied in practice. (C,True,True):(C,True,True) (4.6) ACM Transactions on Programming Languages and Systems,Vol.V,No.N,Article A,Publication date:January YYYY
Rely-Guarantee-Based Simulation A:15 This is because the rely R (or R) is an abstraction of all the permitted behaviors in the environment of a thread t. Any thread t ′ whose behaviors are allowed in R (or R) can run in parallel with t. Thus to obtain parallel compositionality, we have to ensure that the simulation is preserved with any possible sibling thread t ′ . With our definition ≼, the refinement (4.4) is not provable, because after some α-related transitions of environments, the target may print a value smaller than the one printed by the source. Other rules. We also develop some other useful rules about RGSim. For example, the STREN-α rule allows us to replace the invariant α by a stronger invariant α ′ . We need to check that α ′ is indeed an invariant preserved by the related program steps, i.e., Sta(α ′ ,⟨G, G∗ ⟩α) holds. Symmetrically, the WEAKEN-α rule requires α to be preserved by environment steps related by the weaker invariant α ′ . As usual, the pre- and postconditions, the relies and the guarantees can be strengthened or weakened by the CONSEQ rule. The FRAME rule allows us to use local specifications [Reynolds 2002]. When verifying the simulation between C and C, we need to only talk about the locally-used resource in α, ζ and γ, and the local relies and guarantees R, G, R and G. Then the proof can be reused in contexts where some extra resource η is used, and the accesses of it respect the invariant β and R1, G1, R1 and G1. We give the auxiliary definitions in Figure 6. The disjoint union ⊎ between states is lifted to state pairs. A state relation α is intuitionistic, denoted by Intuit(α), if it is monotone w.r.t. the extension of states. The disjointness η # α says that any state pair satisfying both η and α can be split into two disjoint state pairs satisfying η and α respectively. For example, let η , {(σ, Σ) | σ(y) = Σ(y)} and α , {(σ, Σ) | σ(x) = Σ(x)} where x and y are two distinct variables, then both η and α are intuitionistic and η # α holds. We also require η to be stable under interference from the programs (i.e., the programs do not change the extra resource) and the extra environments. We use η # {ζ, γ, α} as a shorthand for (η # ζ) ∧ (η # γ) ∧ (η # α). Similar representations are used in this rule. Finally, the transitivity rule TRANS allows us to verify a transformation by using an intermediate level as a bridge. The intermediate environment RM should be chosen with caution so that the (β ◦ α)-related transitions can be decomposed into β-related and α-related transitions, as illustrated in Figure 4(b). Here ◦ defines the composition of two relations and isMidOf defines the side condition over the environments, as shown in Figure 6. We use θ for a middle-level state. Soundness. All the rules in Figure 7 are sound, i.e., for each rule the premises imply the conclusion. We prove their soundness by co-induction, directly following the definition of RGSim. The proofs are checked in the Coq proof assistant [2010]. Instantiations of relies and guarantees. We can derive the sequential refinement and the fully-abstract-semantics-based refinement by instantiating the rely conditions in RGSim. For example, the refinement (4.5) over closed programs assumes identity environments, making the interference constraints in the PAR rule unsatisfiable. This confirms the observation in Section 2.1 that the sequential refinement loses parallel compositionality. (C, Id, True) ≼α;ζnγ (C, Id, True) (4.5) The refinement (4.6) assumes arbitrary environments, which makes the interference constraints in the PAR rule trivially true. But this assumption is too strong: usually (4.6) cannot be satisfied in practice. (C, True, True) ≼α;ζnγ (C, True, True) (4.6) ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Article A, Publication date: January YYYY