(s,h),(s,h)=B iff B]sw=true 2.for anye,C',o”,oF and oF,if(Ca世or）e(C',aand ((s,h),(sh))own()iff dom(ss)={} ∑l∑r,hen there exist o',M',Cand'such that (a)o”=σ'出oF, (s,h),(s,h)卡E1→E2ifh={[E1]sw=IE2lsw=} b)(C,Σ出F)S+(C,y'出F). ((s,h),(sh))emp iff s=h===0 (c)R,G,IF (C',o',M')(C,'),and fLf2 iff (dom(f1)ndom(f2)=0)ff2fuf2,if fLf2 (d)((a,)(a',>),true)G*True. 3.for any b.a'and 'if ((a )('),b)R*ld,then (s1,h1)L(s2,h2)iff(s1⊥s2)A(h1⊥h2) there exists M'such that (s1,h1)(s2,h2)(s1Us2,hiUh2),if (s1:h1)L(s2,h2) (a)R,G,IF(C,o',M')Q(C,').and (a1,1)u(a2,∑2)兰(1w2,B1y22),ifa1⊥2and1⊥2 (b)if b false,we need M'=M. 4.ifC=skip,then for any∑such that∑⊥∑F,there exist n S=(a,) and X'such that (S,S',6)[P]iff (S P)A(S=S') (a)(C,世∑r)→"(skip,'世F), (S,S,b)上P×Qif(S上P)A(S上Q) b)(o,∑)=Q, (S,S',b)乍PQiff(SFP)A(S'乍Q)A(b=true) (c)if n >0,then ((,)(a,')true)G++True. 5.for any og and∑F,if(C,oyoF)→abort and∑⊥∑F,then (S,S,b)片R1*R2f3S1,S2,S1,S%·(S=S1出S2)A (C,∑世∑F)→+abort. (S=S1世S%)A(S1,S1,b)=R1)∧(S2,S,b)=R2} (S,S',b)R+iff ((S,S,b)R)v (3s",U.8. (S,S,)=)A(S,S',b)=R+)A(6=HV") The simulation R.G,I=(C,o,M)o (C,>relates the ld兰[true]Emp兰emp x emp True些true xtrue executions of the target configuration (C,)(with its metric M) to the source (C.)under the interferences with the environment I R iff([I]→R)A(R→IKI)A Precise(I) specified by R and G.It first requires that the relational state (o, Sta(P,R)ifS,S,b.(SFP)A(S,S',b)上R)→(S=P) satisfy I*true,I for the shared part and true for the local part, establishing a consistency relation between the states at the two Figure 6.Semantics of assertions (part D) levels.For every silent step of (C,a)(condition 1,let's first ignore the frame states op and which will be discussed later),the source could make n steps (n>0)correspondingly (1(b)),and the states,which is a state assertion like P and Q.We define the fence simulation is preserved afterwards with a new metric M(1(c)). IDR in a similar way as in our previous work [10]and LRG [3] Here we use--"-to represent n-step silent transitions.If which says that I precisely determines the boundaries of the states n=0 in 1(b)(i.e..the source does not move).the metric must of the transitions in R(see Fig.6).The formal definition of the decrease along the associated well-founded order (M'<M in precise requirement Precise()is given in TR [13],which follows I(e)),otherwise we do not have any restrictions over M'.We also its usual meaning as in separation logic but is now interpreted over require that the related steps at the two levels satisfy the guarantee relational states. condition G+*True(1(d)),the transitive closure G+for the shared part and True for the private.If the target step corresponds to no 4.2 Definition of RGSim-T source moves (n=0),we use false as the corresponding effect bit, Our simulation RGSim-T is parameterized over the rely/guarantee otherwise the bit should be true (1(e)). conditions R and G to specify the interferences between threads If a target step produces an event e,the requirements(condition and their environments,and a precise invariant to logically deter- 2)are similar to those in condition 1,except that we know for mine the boundaries of the shared states and fence R and G. sure that target step corresponds to one or more source steps that The simulation also takes a metric M,which was referred to produce the same e. as T in our previous informal explanations in Sec.2.We leave The simulation should be preserved after environment transi- its type unspecified here,which can be instantiated by program tions satisfying R*ld,R for the shared part and ld for the verifiers,as long as it is equipped with a well-founded order<. private (condition 3).If the corresponding effect bit of the envi- The formal definition below follows the intuition explained in ronment transition is true,we know there are one or more source Sec.2.Readers who are interested only in the proof theory could moves,therefore there are no restrictions over the metric M'for the skip this definition,which can be viewed as the meta-theory of our resulting code (which could be larger than M).Otherwise,the met- program logic presented in Sec.4.3 and Sec.5. ric should be unaffected under the environment interference (i.e.. M'=M in 3(b)). Definition 2(RGSim-T).R,G,I(P)C<C[Q}iff If C terminates (condition 4),the corresponding C must also for all o and S.if ()P.then there exists M such that terminate and the resulting states satisfy the postcondition Q.Fi- R,G,IF (C,a,M)(C,) nally.if C is unsafe,then C must be unsafe too (condition 5). Here R,G,I (C,o,M)(C,)is the largest rela- Inspired by Vafeiadis [24],we directly embed the framing as- tion such that whenever R,G,I (C,a,M)(C,)then pect of separation logic in Def.2.At each condition,we introduce (o,)I+true and the following are true: the frame states oF and >F at the target and source levels to repre- 1.for any C,",oF and∑F,if(C,o出oF)-→(C',o")and sent the remaining parts of the states owned by other threads in the ∑L∑F,then there exist o',n,M',b,Cand∑'such that system.The commands C and C must not change the frame states (a)g"=o'世oF, during their executions (see,e.g.,conditions 1(a)and 1(b)).These (b)(C,∑世∑F)→n(C','∑F), oF and >F quantifications in RGSim-T are crucial to admit the (c)R,G,I=(C,o,M')so(C',). parallel compositionality and the frame rules (the B-FRAME rule in Fig.7 and the FRAME rule in Fig.9). (d)((o,>)(a',>),b)G*True,and We then define R,G,I =PC<CIQ by hiding the initial (e)if n=0,we need M'<M and b=false,otherwise b=true. states via the precondition P and hiding the metric M.((s, h), (s, h)) |= B iff JBKs⊎s = true ((s, h), (s, h)) |= own(x) iff dom(s ⊎ s) = {x} ((s, h), (s, h)) |= E1 7→ E2 iff h = {JE1Ks⊎s ❀ JE2Ks⊎s} ((s, h), (s, h)) |= emp iff s = h = s = h = ∅ f1⊥f2 iff (dom(f1)∩dom(f2)=∅) f1⊎f2 def = f1∪f2 , if f1⊥f2 (s1, h1)⊥(s2, h2) iff (s1⊥s2) ∧ (h1⊥h2) (s1, h1) ⊎ (s2, h2) def = (s1 ∪ s2, h1 ∪ h2) , if (s1, h1)⊥(s2, h2) (σ1, Σ1) ⊎ (σ2, Σ2) def = (σ1 ⊎ σ2, Σ1 ⊎ Σ2) , if σ1⊥σ2 and Σ1⊥Σ2 S ::= (σ, Σ) (S, S ′ , b) |= [P] iff (S |= P) ∧ (S = S ′ ) (S, S ′ , b) |= P ⋉ Q iff (S |= P) ∧ (S ′ |= Q) (S, S ′ , b) |= P ∝ Q iff (S |= P) ∧ (S ′ |= Q) ∧ (b=true) (S, S ′ , b) |= R1 ∗ R2 iff ∃S1, S2, S ′ 1 , S ′ 2 . (S = S1 ⊎ S2) ∧ (S ′ = S ′ 1 ⊎ S′ 2 ) ∧ ((S1, S ′ 1 , b) |= R1) ∧ ((S2, S ′ 2 , b) |= R2) (S, S ′ , b) |= R+ iff ((S, S ′ , b) |= R) ∨ (∃S′′, b′ , b′′ . ((S, S ′′, b′ ) |= R) ∧ ((S ′′ , S ′ , b′′) |= R+) ∧ (b = b ′ ∨ b ′′)) Id def = [true] Emp def = emp ⋉ emp True def = true ⋉ true I ⊲ R iff ([I] ⇒ R) ∧ (R ⇒ I ⋉ I) ∧ Precise(I) Sta(P, R) iff ∀S, S ′ , b. (S |=P) ∧ ((S, S ′ , b) |=R) =⇒ (S ′ |=P) Figure 6. Semantics of assertions (part I). states, which is a state assertion like P and Q. We define the fence I ⊲ R in a similar way as in our previous work [10] and LRG [3], which says that I precisely determines the boundaries of the states of the transitions in R (see Fig. 6). The formal definition of the precise requirement Precise(I) is given in TR [13], which follows its usual meaning as in separation logic but is now interpreted over relational states. 4.2 Definition of RGSim-T Our simulation RGSim-T is parameterized over the rely/guarantee conditions R and G to specify the interferences between threads and their environments, and a precise invariant I to logically deter￾mine the boundaries of the shared states and fence R and G. The simulation also takes a metric M, which was referred to as |T | in our previous informal explanations in Sec. 2. We leave its type unspecified here, which can be instantiated by program verifiers, as long as it is equipped with a well-founded order <. The formal definition below follows the intuition explained in Sec. 2. Readers who are interested only in the proof theory could skip this definition, which can be viewed as the meta-theory of our program logic presented in Sec. 4.3 and Sec. 5. Definition 2 (RGSim-T). R, G, I |= {P}C C{Q} iff for all σ and Σ, if (σ, Σ) |= P, then there exists M such that R, G, I |= (C, σ, M)Q (C, Σ). Here R, G, I |= (C, σ, M) Q (C, Σ) is the largest rela￾tion such that whenever R, G, I |= (C, σ, M) Q (C, Σ), then (σ, Σ) |= I ∗ true and the following are true: 1. for any C ′ , σ ′′ , σF and ΣF , if (C, σ ⊎ σF ) −→ (C ′ , σ′′) and Σ⊥ΣF , then there exist σ ′ , n, M′ , b, C ′ and Σ ′ such that (a) σ ′′ = σ ′ ⊎ σF , (b) (C, Σ ⊎ ΣF ) −→n (C ′ , Σ ′ ⊎ ΣF ), (c) R, G, I |= (C ′ , σ′ , M′ )Q (C ′ , Σ ′ ), (d) ((σ, Σ),(σ ′ , Σ ′ ), b) |= G + ∗ True, and (e) if n= 0, we need M′ <M and b=false, otherwise b=true. 2. for any e, C ′ , σ ′′ , σF and σF , if (C, σ⊎σF ) e −→ (C ′ , σ′′) and Σ⊥ΣF , then there exist σ ′ , M′ , C ′ and Σ ′ such that (a) σ ′′ = σ ′ ⊎ σF , (b) (C, Σ ⊎ ΣF ) e −→+ (C ′ , Σ ′ ⊎ ΣF ), (c) R, G, I |= (C ′ , σ′ , M′ )Q (C ′ , Σ ′ ), and (d) ((σ, Σ),(σ ′ , Σ ′ ), true) |= G + ∗ True. 3. for any b, σ ′ and Σ ′ , if ((σ, Σ),(σ ′ , Σ ′ ), b) |= R + ∗ Id, then there exists M′ such that (a) R, G, I |= (C, σ′ , M′ )Q (C, Σ ′ ), and (b) if b = false, we need M′ = M. 4. if C = skip, then for any ΣF such that Σ⊥ΣF , there exist n and Σ ′ such that (a) (C, Σ ⊎ ΣF ) −→n (skip, Σ ′ ⊎ ΣF ), (b) (σ, Σ ′ ) |= Q, (c) if n > 0, then ((σ, Σ),(σ, Σ ′ ), true) |= G + ∗ True. 5. for any σF and ΣF , if (C, σ⊎σF ) −→ abort and Σ⊥ΣF , then (C, Σ ⊎ ΣF ) −→+ abort. The simulation R, G, I |= (C, σ, M) Q (C, Σ) relates the executions of the target configuration (C, σ) (with its metric M) to the source (C, Σ), under the interferences with the environment specified by R and G. It first requires that the relational state (σ, Σ) satisfy I ∗ true, I for the shared part and true for the local part, establishing a consistency relation between the states at the two levels. For every silent step of (C, σ) (condition 1, let’s first ignore the frame states σF and ΣF which will be discussed later), the source could make n steps (n ≥ 0) correspondingly (1(b)), and the simulation is preserved afterwards with a new metric M′ (1(c)). Here we use −→ n to represent n-step silent transitions. If n = 0 in 1(b) (i.e., the source does not move), the metric must decrease along the associated well-founded order (M′ < M in 1(e)), otherwise we do not have any restrictions over M′ . We also require that the related steps at the two levels satisfy the guarantee condition G + ∗True (1(d)), the transitive closure G + for the shared part and True for the private. If the target step corresponds to no source moves (n = 0), we use false as the corresponding effect bit, otherwise the bit should be true (1(e)). If a target step produces an event e, the requirements (condition 2) are similar to those in condition 1, except that we know for sure that target step corresponds to one or more source steps that produce the same e. The simulation should be preserved after environment transi￾tions satisfying R + ∗ Id, R + for the shared part and Id for the private (condition 3). If the corresponding effect bit of the envi￾ronment transition is true, we know there are one or more source moves, therefore there are no restrictions over the metric M′ for the resulting code (which could be larger than M). Otherwise, the met￾ric should be unaffected under the environment interference (i.e., M′ = M in 3(b)). If C terminates (condition 4), the corresponding C must also terminate and the resulting states satisfy the postcondition Q. Fi￾nally, if C is unsafe, then C must be unsafe too (condition 5). Inspired by Vafeiadis [24], we directly embed the framing as￾pect of separation logic in Def. 2. At each condition, we introduce the frame states σF and ΣF at the target and source levels to repre￾sent the remaining parts of the states owned by other threads in the system. The commands C and C must not change the frame states during their executions (see, e.g., conditions 1(a) and 1(b)). These σF and ΣF quantifications in RGSim-T are crucial to admit the parallel compositionality and the frame rules (the B-FRAME rule in Fig. 7 and the FRAME rule in Fig. 9). We then define R, G, I |= {P}C C{Q} by hiding the initial states via the precondition P and hiding the metric M