R,G,I{P A arem(C)}C{Q A arem(skip)} (U2B) R,G,I上{P}C<C{Q} FsL (p]Cla] p台ap' ksp]Cg]qbg+∈{a,b} (仙oll x Lall)→G*TrueIG pVg→I*true (pll llgll)→G*True IG pvg→i*true ·(ATOM) (ATOM+) [,G,IF{p}(C){9 [,G,I上{p}(C)H9 P÷(B=B)*I [n,G,IHp)(C){q}Sta(p,q},R*ld)IR PA Bp'+(wf(1)Aemp)R,G,Ip'}C(p} (ATOM-R) (WHILE) R,G,IF(p)(C){q} R,G,IF {p)while (B)CIpA-B} R,G,IF(p)C(q} R,G,Ip)C(}Sta(p',R'+ld)I'R',G}p'I'*true G+G (FRAME) R,G,IF{p小w}CILgJw} (HIDE-W) R*R,G*G,I*I'Hp*p)Clq*p} Figure 9.Selected unary inference rules. local t; 1 1oca11:=100; {x=XA arem(S）Awf(1)} /unfolding cas i>0A wf(i)arem(skip) 2 while (true){ 2 while (i>0){ {x=xA arem(S)} if (x =t) 3 t :x; x=X=t A arem(S) (i>0A wf(1-1)A arem(skip)} 3 x=X=t A arem(S')V x=x=tAarem(X+;S）】 {i0A wf(i)A arem(skip)} x=tA arem(S)A wf(1) x:=t+1; 4 cas(&x,t,t+1); x=X=t+1A arem(S)A wf(1) x=X A arem(S)A wf(1) (b)local termination: (a)looping a counter:I (x=X) R=G兽(IaxI)V☑ I些empR=G些Emp Figure 10.Proofs for two small examples. at least one of them is the special sign.,which has no knowledge The U2B rule,as explained in Sec.2.turns unary proofs to about the remaining source code C.Therefore we know the follow- binary ones.It says that if the remaining source code is C at the ing holds (for any P and C): beginning of the target C.and it becomes skip at the end of C. (P A arem(C)A wf(1))*(wf(1)A emp)(P A arem(C)A wf(2)) then we know C is simulated by C. The ATOM rule allows us to reason sequentially about the target One may think a more natural definition of the disjoint union is code in the atomic block.We use Hs [p]C[g]to represent the total to require the two Ds be the same.But this would break the FRAME correctness of C in sequential separation logic.The corresponding rule (see Fig.9).For example,we can prove: rules are mostly standard and elided here.Note that C only accesses Emp,Emp,emp{=XA arem(X++)x++{x=X A arem(skip) the target state o,therefore in our sequential rules we require the source state and the auxiliary data w and D in p should With the FRAME rule and the separating conjunction based on remain unchanged in g.We can lift C's total correctness to the the alternative definition of disjoint union,we would derive the concurrent setting as long as its overall transition over the shared following: states satisfies the guarantee G.Here we assume the environment Emp,Emp,emp {(x=XA arem(X++))arem(X++)} is identity transitions.To allow general environment behaviors,we x++(=X A arem(skip))arem(++)} can apply the ATOM-R rule later,which requires that R be fenced which is reduced to an invalid judgment: by I and the pre-and post-conditions be stable w.r.t.R. The ATOM rule is similar to the ATOM rule,except that it Emp,Emp,emp {x =X A arem(X++)}x++{false executes the source code simultaneously with the target atomic We require in p*g that either p or g should not specify the source step.We use pg for the multi-step executions from the source code,therefore in this example the precondition after applying the code specified by p to the code specified by g,which is defined frame rule is invalid (thus the whole judgment is valid). in the bottom part of Fig.8.We also write pg for the usual The stability of p w.r.t.an action R,defined at the bottom part of implication p=g.Then,the AToM rule says,we can execute the Fig.8.specifies how the number of tokens of a program(specified source code before or after the steps of C,as long as the overall by p)could change under R's interferences.As a simple example transition (including the source steps and the target steps)with the for the following p,Ri and R2,Sta(p,R1)holds while Sta(p,R2) effect bit true satisfies G for the shared parts. does not hold: The WHILE rule is the key to proving the preservation of termi- p些(10→0*20台0)V(10→1*20片0)Awf(1) nation.As we informally explained in Sec.2,we should be able to decrease the number of tokens at the beginning of each loop itera- R1兽(10→0*20片0)x(10→1*20片0) tion.And we should re-establish the invariant p between the states R2兰(10→0*20÷0)×(10→1*20÷0) and the number of tokens at the end of each iteration.Below we 5.2 Unary Inference Rules give two examples,each of which shows a typical application of the WHILE rule. The judgment for unary reasoning is in the form of R,G,I pCg.We present some of the rules in Fig.9.R, G, I ⊢ {P ∧ arem(C)}C{Q ∧ arem(skip)} R, G, I ⊢ {P}C C{Q} (U2B) ⊢SL [p]C[q] (TpU ⋉ TqU) ⇒ G ∗ True I ⊲ G p ∨ q ⇒ I ∗ true [I], G, I ⊢ {p}hCi{q} (ATOM) p ⇛a p ′ ⊢SL [p ′ ]C[q ′ ] q ′ ⇛b q + ∈ {a, b} (TpU ∝ TqU) ⇒ G ∗ True I ⊲ G p ∨ q ⇒ I ∗ true [I], G, I ⊢ {p}hCi{q} (ATOM+) [I], G, I ⊢ {p}hCi{q} Sta({p, q}, R ∗ Id) I ⊲ R R, G, I ⊢ {p}hCi{q} (ATOM-R) p ⇒ (B = B) ∗ I p ∧ B ⇒ p ′ ∗ (wf(1) ∧ emp) R, G, I ⊢ {p ′}C{p} R, G, I ⊢ {p}while (B) C{p ∧ ¬B} (WHILE) R, G, I ⊢ {p}C{q} R, G, I ⊢ {⌊p⌋w}C{⌊q⌋w} (HIDE-W) R, G, I ⊢ {p}C{q} Sta(p ′ , R′ ∗ Id) I ′ ⊲ {R′ , G′} p ′ ⇒ I ′ ∗ true G+ ⇒ G R ∗ R′ , G ∗ G′ , I ∗ I ′ ⊢ {p ∗ p ′}C{q ∗ p ′} (FRAME) Figure 9. Selected unary inference rules. 1 local t;  x = X ∧ arem(S ′ ) ∧ wf(1) 2 while (true) {  x = X ∧ arem(S ′ ) 3 < t := x; >  x = X = t ∧ arem(S ′ ) ∨ x = X 6= t ∧ arem(S ′ ) ∧ wf(1) 4 cas(&x, t, t+1);  x = X ∧ arem(S ′ ) ∧ wf(1) 5 } // unfolding cas < if (x = t)  x = X = t ∧ arem(S ′ )  x = X = t ∧ arem(X++;S ′ ) x := t + 1;  x = X = t + 1 ∧ arem(S ′ ) ∧ wf(1) > (a) looping a counter: I def = (x = X) R = G def = (I ∝ I) ∨ [I] 1 local i := 100;  i ≥ 0 ∧ wf(i) ∧ arem(skip) 2 while (i > 0) {  i > 0 ∧ wf(i-1) ∧ arem(skip) 3 i--;  i ≥ 0 ∧ wf(i) ∧ arem(skip) 4 } (b) local termination: I def = emp R = G def = Emp Figure 10. Proofs for two small examples. at least one of them is the special sign •, which has no knowledge about the remaining source code C. Therefore we know the follow￾ing holds (for any P and C): (P ∧ arem(C) ∧ wf(1)) ∗ (wf(1) ∧ emp) ⇔ (P ∧ arem(C) ∧ wf(2)) One may think a more natural definition of the disjoint union is to require the two Ds be the same. But this would break the FRAME rule (see Fig. 9). For example, we can prove: Emp, Emp, emp ⊢ {x = X ∧ arem(X++)} x++ {x = X ∧ arem(skip)} With the FRAME rule and the separating conjunction based on the alternative definition of disjoint union, we would derive the following: Emp, Emp, emp ⊢ {(x = X ∧ arem(X++)) ∗ arem(X++)} x++ {(x = X ∧ arem(skip)) ∗ arem(X++)} which is reduced to an invalid judgment: Emp, Emp, emp ⊢ {x = X ∧ arem(X++)} x++ {false} We require in p ∗ q that either p or q should not specify the source code, therefore in this example the precondition after applying the frame rule is invalid (thus the whole judgment is valid). The stability of p w.r.t. an action R, defined at the bottom part of Fig. 8, specifies how the number of tokens of a program (specified by p) could change under R’s interferences. As a simple example, for the following p, R1 and R2, Sta(p, R1) holds while Sta(p, R2) does not hold: p def = (10 7→ 0 ∗ 20 Z⇒ 0) ∨ ((10 7→ 1 ∗ 20 Z⇒ 0) ∧ wf(1)) R1 def = (10 7→ 0 ∗ 20 Z⇒ 0) ∝ (10 7→ 1 ∗ 20 Z⇒ 0) R2 def = (10 7→ 0 ∗ 20 Z⇒ 0) ⋉ (10 7→ 1 ∗ 20 Z⇒ 0) 5.2 Unary Inference Rules The judgment for unary reasoning is in the form of R, G, I ⊢ {p}C{q}. We present some of the rules in Fig. 9. The U2B rule, as explained in Sec. 2, turns unary proofs to binary ones. It says that if the remaining source code is C at the beginning of the target C, and it becomes skip at the end of C, then we know C is simulated by C. The ATOM rule allows us to reason sequentially about the target code in the atomic block. We use ⊢SL [p]C[q] to represent the total correctness of C in sequential separation logic. The corresponding rules are mostly standard and elided here. Note that C only accesses the target state σ, therefore in our sequential rules we require the source state Σ and the auxiliary data w and D in p should remain unchanged in q. We can lift C’s total correctness to the concurrent setting as long as its overall transition over the shared states satisfies the guarantee G. Here we assume the environment is identity transitions. To allow general environment behaviors, we can apply the ATOM-R rule later, which requires that R be fenced by I and the pre- and post-conditions be stable w.r.t. R. The ATOM+ rule is similar to the ATOM rule, except that it executes the source code simultaneously with the target atomic step. We use p ⇛+ q for the multi-step executions from the source code specified by p to the code specified by q, which is defined in the bottom part of Fig. 8. We also write p ⇛0 q for the usual implication p ⇒ q. Then, the ATOM+ rule says, we can execute the source code before or after the steps of C, as long as the overall transition (including the source steps and the target steps) with the effect bit true satisfies G for the shared parts. The WHILE rule is the key to proving the preservation of termi￾nation. As we informally explained in Sec. 2, we should be able to decrease the number of tokens at the beginning of each loop itera￾tion. And we should re-establish the invariant p between the states and the number of tokens at the end of each iteration. Below we give two examples, each of which shows a typical application of the WHILE rule