CCa (C1R):K(C1 R,G)(C2,R,G)a:n(C2,R,G) (SKIP) ·(sEQ) (skip,R,ld)(skip,R,ld) (C1:C2,R,9)a:(C1;C2,R,G) (C,R,G)。61xy(C1,R,G)(C2,R,9)5a2x7(2,R,G) (≤(B台B)S=(n(BmB)2=(Gn(BAB)SCa (F) (if (B)C1 else C2 R,g)if B then C1 else C2.R,G) (C,R,g)30:7K7(C,R,G)7(BB)1=(n(BAB))72=(n(BA-B)) (WHILE) (while (B)C,R,G):(while B do C,R,G) (C1,R1.G1)3a (C1,R1,G1) (C2,R2,S2）ax3 (C2,R2,G2 G1 C R2 g2 CR1 G1 C R2 G2 CR1 GC,inR2,Su9g)≤KK(a)(Ge,RnR2,GuG(eR） (C.,R.G)(C,RG) (C.R,G) (CU)acaSta(d,(G.G")a)(STREN-a) (C,R,G)3a:5x7 a≤a'Sta(a,(R,R")a） (WEAKEN-Q) (C,R,9)≤a:xy(C,R,G) (C,R,9)≤a'K1(C,R,G) (C,R,9)≤：x1(C,R,G)S'C5y≤YSa R'CR R'CR GCG G二G (CONSEQ)】 (C,R',G')ax (C,R',) sBC2a是E》 (C.R,g)(M,RM,GM) (M,RM,GM≤8：6xn(C,R,G) n#{,Y,a}Sta(n,{(G,G*)a,(R1,Ri)a}) RM isMidOf (a,B;R,R*) (FRAME) (C,RwR1,9wGi)≤awa:(ux(w(C,R出R1,G出G1) (C,R,9)≤goal6ocxo)(C,R,G(TRANS） Figure 7.Compositionality Rules for RGSim we could prove the following: respect the invariant B and R1.G1.Ri and G1.We give the auxil- 国之CT. (x:=x+1.ld,True) iary definitions in Figure 6.The disjoint union between states is lifted to state pairs.An intuitionistic state relation is monotone w.r.t. the extension of states.The disjointness n a says that any state Here we use ld and True(defined in Figure 6)for the sets of identity pair satisfying both n and o can be split into two disjoint state pairs transitions and arbitrary transitions respectively,and overload the satisfying n and a respectively.For example.let n{(, notations at the low level to the high level.However,the following a(y)=(y)}and a(a,>I a(x)=(x)},then both n refinement does not hold after parallel composition: and a are intuitionistic and n#o holds.We also require n to be (x:=x+1llprint(x),Id,True):xa stable under interference from the programs (i.e.,the programs do (x:=x+2print (x),Id,True). not change the extra resource)and the extra environments.We use This is because the rely R(or R)is an abstraction of all the per- n#{S,,a}as a shorthand for(忉#)A(忉#y）A(m#a)- Similar representations are used in this rule. mitted behaviors in the environment of a thread.But a concrete sibling thread that runs in parallel may produce less transitions Finally,the transitivity rule TRANS allows us to verify a trans- than R(or R).To obtain parallel compositionality,we need to en- formation by using an intermediate level as a bridge.The interme- sure that the simulation holds for all concrete sibling threads.With diate environment RM should be chosen with caution so that the our definition≤，the refinement(print(x),True,ld≤a:xa (B o a)-related transitions can be decomposed into B-related and (print(x),True,ld)is not provable because,after the environ- a-related transitions,as illustrated in Figure 4(b).Here o defines ments'o-related transitions,the target may print a value smaller the composition of two relations and isMidOf defines the side con- than the one printed by the source. dition over the environments,as shown in Figure 6.We use 0 for a middle-level state. Other rules.We also develop some other useful rules about RGSim.For example,the STREN-o rule allows us to replace the Soundness of all the rules in Figure 7 is proved in the techni- invariant a by a stronger invariant a'.We need to check that a' cal report [20],showing that for each rule the premises imply the is indeed an invariant preserved by the related program steps,i.e.. conclusion.The proofs are also mechanized in the Coq proof assis- Sta(a',(9,G)holds.Symmetrically,the WEAKEN-o rule re- tant [10]. quires a to be preserved by environment steps related by the weaker Instantiations of relies and guarantees.We can derive the se- invariant a'.As usual,the pre/post conditions,the relies and the quential refinement and the fully-abstract-semantics-based refine- guarantees can be strengthened or weakened by the CoNSEQ rule. ment by instantiating the rely conditions in RGSim.For example, The FRAME rule allows us to use local specifications.When ver- the refinement (4.3)over closed programs assumes identity envi- ifying the simulation between C and C,we need to only talk about ronments,making the interference constraints in the PAR rule un- satisfiable.This confirms the observation in Section 2.1 that the the locally-used resource in o,6 and y,and the local relies and guarantees R,g,R and G.Then the proof can be reused in con- sequential refinement loses parallel compositionality. texts where some extra resource n is used,and the accesses of it (C,Id,True):(C,Id,True) (4.3) 461ζ ⊆ α (skip, R, Id) α;ζζ (skip, R, Id) (SKIP) (C1, R, G) α;ζγ (C1, R, G) (C2, R, G) α;γη (C2, R, G) (C1; C2, R, G) α;ζη (C1; ; C2, R, G) (SEQ) (C1, R, G) α;ζ1γ (C1, R, G) (C2, R, G) α;ζ2γ (C2, R, G) ζ ⊆ (B⇔⇔B) ζ1 = (ζ ∩ (B∧∧B)) ζ2 = (ζ ∩ (¬B∧∧¬B)) ζ ⊆ α (if (B) C1 else C2, R, G) α;ζγ (if B then C1 else C2, R, G) (IF) (C, R, G) α;γ1γ (C, R, G) γ ⊆ (B⇔⇔B) γ1 = (γ ∩ (B∧∧B)) γ2 = (γ ∩ (¬B∧∧¬B)) (while (B) C, R, G) α;γγ2 (while B do C, R, G) (WHILE) (C1, R1, G1) α;ζγ1 (C1, R1, G1) (C2, R2, G2) α;ζγ2 (C2, R2, G2) G1 ⊆ R2 G2 ⊆ R1 G1 ⊆ R2 G2 ⊆ R1 (C1 C2, R1 ∩ R2, G1 ∪ G2) α;ζ(γ1∩γ2) (C1C2, R1 ∩ R2, G1 ∪ G2) (PAR) (C, R, G) α;ζγ (C, R, G) (ζ ∪ γ) ⊆ α ⊆ α Sta(α , G, G∗α) (C, R, G) α;ζγ (C, R, G) (STREN-α) (C, R, G) α;ζγ (C, R, G) α ⊆ α Sta(α, R, R∗α ) (C, R, G) α;ζγ (C, R, G) (WEAKEN-α) (C, R, G) α;ζγ (C, R, G) ζ ⊆ ζ γ ⊆ γ ⊆ α R ⊆ R R ⊆ R G⊆G G ⊆ G (C, R , G ) α;ζγ (C, R , G ) (CONSEQ) (C, R, G) α;ζγ (C, R, G) η ⊆ β Intuit({α, ζ, γ, β, η, R, R, R1, R1}) η # {ζ, γ,α} Sta(η, {G, G∗α, R1, R∗ 1β}) (C, RR1, GG1) αβ;(ζη)(γη) (C, R  R1, G  G1) (FRAME) (C, R, G) α;ζγ (M, RM, GM) (M, RM, GM) β;δη (C, R, G) RM isMidOf (α, β; R, R∗) (C, R, G) β◦α;(δ◦ζ)(η◦γ) (C, R, G) (TRANS) Figure 7. Compositionality Rules for RGSim we could prove the following: (x:=x+1, Id, True)  α;ζα (x:=x+2, Id, True) ; (print(x), True, Id)  α;ζα (print(x), True, Id) . 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+1print(x), Id, True)  α;ζα (x:=x+2print(x), Id, True) . This is because the rely R (or R) is an abstraction of all the per￾mitted behaviors in the environment of a thread. But a concrete sibling thread that runs in parallel may produce less transitions than R (or R). To obtain parallel compositionality, we need to en￾sure that the simulation holds for all concrete sibling threads. With our definition , the refinement (print(x), True, Id) α;ζα (print(x), True, Id) is not provable because, after the environ￾ments’ α-related transitions, 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 re￾quires α to be preserved by environment steps related by the weaker invariant α . As usual, the pre/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. When ver￾ifying 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 con￾texts where some extra resource η is used, and the accesses of it respect the invariant β and R1, G1, R1 and G1. We give the auxil￾iary definitions in Figure 6. The disjoint union  between states is lifted to state pairs. An intuitionistic state relation 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)}, 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 trans￾formation by using an intermediate level as a bridge. The interme￾diate 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 con￾dition over the environments, as shown in Figure 6. We use θ for a middle-level state. Soundness of all the rules in Figure 7 is proved in the techni￾cal report [20], showing that for each rule the premises imply the conclusion. The proofs are also mechanized in the Coq proof assis￾tant [10]. Instantiations of relies and guarantees. We can derive the se￾quential refinement and the fully-abstract-semantics-based refine￾ment by instantiating the rely conditions in RGSim. For example, the refinement (4.3) over closed programs assumes identity envi￾ronments, making the interference constraints in the PAR rule un￾satisfiable. This confirms the observation in Section 2.1 that the sequential refinement loses parallel compositionality. (C, Id, True) α;ζγ (C, Id, True) (4.3) 461