Lemma 5.2 If (1,02)=a*ld.o=1o',and o2=o2', then (12)=a*ld. Ioa Ipa' Ipa Ipa IP西 IP(I×ID Ipava I*I'pa*a 5.2 Stability Figure 11.Selected Rules for Fence (Assuming precise()) Next we introduce the concept of stability of an assertion p with respect to an action a. 5.3 Invariant-Fenced Actions Definition 5.3(Stability)We say p is stable with respect to the The following definition says an action a is fenced by a precise invariant /(represented as IDa)if and only if a holds over identity action a,i.e.,Sta(p,a)holds.if and only if for all o and o',if transitions satisfying [n,and holds over the beginning and end Fst p and (.')=a,then 'Fst p. states of transitions satisfying a. Informally,Sta(p,a)means the validity of p is preserved by transitions in Tal.Examples of Sta(p,a)are shown below.Follow- Definition 5.7 (Fence)I a holds iff [n=a.a=(I1)and ing RGSep (Vafeiadis and Parkinson 2007).the following lemma precise(/). shows the encoding of stability using the septraction p. It is natural to ask a to hold over identity transitions so that stutter- Lemma 5.4 The following are true: ing steps of processes would also satisfy it.The second requirement is important to determine the boundary of transitions a and a'in ·Sta(r,pxq)if and only if(p-®r)Aemp)*q→r a*a':the boundary can be uniquely determined if a or a'is fenced ·f(p-®r)*q→r,then Sta(r,pxq: by a precise invariant / ·Sta(r,(p×q)*ld)if and only if(p-&r)*q→r Lemma 5.8 If (i2.')=a*a',i Fst I and I a,then there exist unique of and o2 such that '=2.(1.)F a and The separating conjunction a*a'over actions allows us to com- (c2,2)Fd. pose disjoint transitions into one.Naturally,we want the following property about stability to hold: From Lemma 5.8 we can derive the following frame property of If Sta(p,a)and Sta(p',a'),then Sta(p*p',a*a'). the action a*ld. As explained in Sec.3.this property is important to support local reasoning.Unfortunately,it is not true in general,as shown in the Corollary 5.9 If (.)=a*ld.1 FsL I and Ia,then there following example.The example also shows that we cannot get this exists such that'=2 and (1.)E [al. property even with precise p and p'. Figure 11 shows some selected proof rules for the fencing rela- Example5.5 Let a d(G→mlv(G→m)x(G→m+1). tion.The following lemma shows that the property about stability p些G→m,dg(G→2lv(G→m)x(G1→n1+1》.and discussed in the previous section holds given an action fenced by a psh→2，and suppose(1≠2，we can prove Sta(p.dand precise invariant. Sta(p',a').but Sta(p*p',a+a')does not hold. Here is a counterexample.Let the heap h be m.2n). Lemma 5.10 If Sta(p,a),Sta(p',d'),p=I and Ia,we have and h'be n+1,2 n2+1).Then,for any s,s'and i, Sta(p*p'a*a'). we have (s.i,h)Fst p*p'and ((s,i,h),(s',i,h'))F a*a',but (s',i,h)=s p*p'does not hold. Below we give two examples to show invariant fenced actions. In particular,Example 5.12 shows that asking in /a to be precise To establish the property,we seem to need some concept of does not prevent the action a from changing the size of the resource. "precise actions",similar to the requirement of precise assertions in Separation Logic.However,precision alone cannot address our problem.The following example shows that even if we have Example5.11LetI=(1→-*62→-，a1=[61→X*2→Y门， 2=(E1→X*2HYAX>Y)×(E1→X-Y*2→Y),and Sta(p1.(r))and Sta(p2.(r2))for precise pi.r..p2.r2 a3=(C1→X*2→Y)AX<Y)∝(e1→X*2→Y-X).We andr.we do not necessarily have Sta(pi*p2.(r()). have I a,I (ai va).I (a1 v a3).and I (a va va3),but not Io a2 or Io a3. Example5.6 Letp些G→1，n些2一m,g2→m+l p2些1，n些p1,些（→m+l,and suppose(≠h.w Example 5.12 We define List(C.n)as a linked list pointed to by know Sta(pi.(r))and Sta(p2.(r2))are vacuously true. with length n: but Sta(p1*p2,(r1×r)*(r2×r)is false. List(,t0)些t=0Aemp List(C.n+l)些(emp.At≠0A(化-.*(+1Hf)》*List('C,m) The problem is,p and a may specify different resources even if Sta(p,a)holds.To address this issue,we introduce invariant-fenced Let I 3n.List(t,n),and a =(List(t,m)Ams n)(List(t,n)).We actions and use an invariant to identify the specified resource. can prove that /p a holds.Lemma 5.2 If (σ1,σ2) |= a ∗ Id, σ 1 = σ1 σ , and σ 2 = σ2 σ , then (σ 1,σ 2) |= a ∗ Id. 5.2 Stability Next we introduce the concept of stability of an assertion p with respect to an action a. Definition 5.3 (Stability) We say p is stable with respect to the action a, i.e., Sta(p,a) holds, if and only if for all σ and σ , if σ |=sl p and (σ,σ ) |= a, then σ |=sl p. Informally, Sta(p,a) means the validity of p is preserved by transitions in [[a]]. Examples of Sta(p,a) are shown below. Follow￾ing RGSep (Vafeiadis and Parkinson 2007), the following lemma shows the encoding of stability using the septraction p−q. Lemma 5.4 The following are true: • Sta(r, p  q) if and only if ((p−r)∧emp) ∗ q ⇒ r; • If (p−r) ∗ q ⇒ r, then Sta(r, p  q); • Sta(r,(p  q) ∗ Id) if and only if (p−r) ∗ q ⇒ r. The separating conjunction a∗a over actions allows us to com￾pose disjoint transitions into one. Naturally, we want the following property about stability to hold: If Sta(p,a) and Sta(p ,a ), then Sta(p ∗ p ,a ∗ a ). As explained in Sec. 3, this property is important to support local reasoning. Unfortunately, it is not true in general, as shown in the following example. The example also shows that we cannot get this property even with precise p and p . Example 5.5 Let a def = ([1 → n1])∨((2 → n2)  (2 → n2+1)), p def = 1 → n1, a def = ([2 → n2])∨((1 → n1)  (1 → n1+1)), and p def = 2 → n2, and suppose 1 2, we can prove Sta(p,a) and Sta(p ,a ), but Sta(p ∗ p ,a ∗ a ) does not hold. Here is a counterexample. Let the heap h be {1 n1, 2 n2}, and h be {1 n1+1, 2 n2 +1}. Then, for any s, s and i, we have (s,i,h) |=sl p ∗ p and ((s,i,h),(s ,i,h )) |= a ∗ a , but (s ,i,h ) |=sl p ∗ p does not hold.  To establish the property, we seem to need some concept of “precise actions”, similar to the requirement of precise assertions in Separation Logic. However, precision alone cannot address our problem. The following example shows that even if we have Sta(p1,(r1  r 1)) and Sta(p2,(r2  r 2)) for precise p1,r1,r 1, p2,r2 and r 2, we do not necessarily have Sta(p1 ∗ p2,(r1  r 1)∗(r2  r 2)). Example 5.6 Let p1 def = 1 → n1,r1 def = 2 → n2,r 1 def = 2 →n2+1, p2 def = r1, r2 def = p1, r 2 def = 1 → n1+1, and suppose 1 2. We know Sta(p1,(r1  r 1)) and Sta(p2,(r2  r 2)) are vacuously true, but Sta(p1 ∗ p2,(r1  r 1) ∗ (r2  r 2)) is false.  The problem is, p and a may specify different resources even if Sta(p,a) holds. To address this issue, we introduce invariant-fenced actions and use an invariant to identify the specified resource. I [I] I (I  I) I a I a I a∨a I a I a I ∗ I a ∗ a Figure 11. Selected Rules for Fence (Assuming precise(I)) 5.3 Invariant-Fenced Actions The following definition says an action a is fenced by a precise invariant I (represented as I a) if and only if a holds over identity transitions satisfying [I], and I holds over the beginning and end states of transitions satisfying a. Definition 5.7 (Fence) I  a holds iff [I] ⇒ a, a ⇒ (I  I) and precise(I). It is natural to ask a to hold over identity transitions so that stutter￾ing steps of processes would also satisfy it. The second requirement is important to determine the boundary of transitions a and a in a ∗ a : the boundary can be uniquely determined if a or a is fenced by a precise invariant I. Lemma 5.8 If (σ1 σ2,σ ) |= a ∗ a , σ1 |=sl I and I a, then there exist unique σ 1 and σ 2 such that σ = σ 1 σ 2, (σ1,σ 1) |= a and (σ2,σ 2) |= a . From Lemma 5.8 we can derive the following frame property of the action a ∗ Id. Corollary 5.9 If (σ1σ2,σ )|= a ∗ Id, σ1 |=sl I and Ia, then there exists σ 1 such that σ = σ 1 σ2 and (σ1,σ 1) ∈ [[a]]. Figure 11 shows some selected proof rules for the fencing rela￾tion. The following lemma shows that the property about stability discussed in the previous section holds given an action fenced by a precise invariant. Lemma 5.10 If Sta(p,a), Sta(p ,a ), p ⇒ I and I  a, we have Sta(p ∗ p ,a ∗ a ). Below we give two examples to show invariant fenced actions. In particular, Example 5.12 shows that asking I in Ia to be precise does not prevent the action a from changing the size of the resource. Example 5.11 Let I = 1 → ∗ 2 → , a1 = [1 → X ∗ 2 → Y], a2 = ((1 → X ∗ 2 → Y)∧X > Y)  (1 → X −Y ∗ 2 → Y), and a3 = ((1 → X ∗ 2 → Y)∧X < Y)  (1 → X ∗ 2 → Y − X). We have I  a1, I  (a1 ∨a2), I  (a1 ∨a3), and I  (a1 ∨a2 ∨a3), but not I a2 or I a3.  Example 5.12 We define List(,n) as a linked list pointed to by  with length n: List(,0) def =  = 0∧emp List(,n+1) def = (emps ∧ 0∧( → ∗ +1 →  )) ∗List( ,n) Let I = ∃n. List(,n), and a = (List(,m)∧m ≤ n)  (List(,n)). We can prove that I a holds.  7