for all f∈dom(Π)：Π(f)=(x,C)(f）=(g,C) dom(Π①=dom(T) D,R,G(PA (=y)A arem(C)A(Ek,...E1))C(P A arem(skip)} t,t.t≠t→Gt台R wffAct(R,D) P→-Enabled(D) (OBJ) D,R,GF{P}ΠT 卫AB→p pA BA (Enabled(D)VQ)p(A emp)D.R.GHp')CIp p→J Sta(J,RVGD≤D wffAct((R,D)J÷(R,G:DQ) D,R,GHIP)Cig -(WHL) (HIDE-◇) D,R,GF (p}while(B)CHpA-B] D,R,GH(Lplo}C(lglo} FpC[q]q台kq (P×kLq)→G D,Id,G(p)(C){q}Sta({p.9},R) (ATOM) (ATOM-R) D,Id,GH[p)(C)g} D,R,GH(p)(C)a} Figure 7.Inference rules. requires the thread be waiting for its environment to perform a finite wffAct(R,D)ifft.R→[DeA(t≠t.D]VDe) number of definite actions. Sta(p,R)iff ,,u,w,C. Definition 1 (Definite Progress).(R,G:DQ)iff the (6,(uw),C)=p)A(6,6)F)→(6'，(，w),C)Fp following hold for all t: p台9ift,o,∑，u,w,C,∑e ((o,),(u,w),C)=p)A(E⊥F)→3C, (1)either =Qt ((C,EWEF)(C','WF))A((a,>),(u,w),C)q or there exists t'such that t't and Enabled(D); (2)for any t't and 6',if (,',0)RA(D).then Figure 8.Auxiliary defs.used in logic rules (simplified version). f(G)<f(G): (3)for any 6',if(6,6,0)ERVGt,then f()<f(). sequential separation logic.The corresponding rules are standard Here f is a function that maps the relational states to some metrics and elided here.We use pg for the zero or multiple-step over which there is a well-founded order < executions from the abstract code specified by p to the code specified Ignoring the index 0 above,the definition says either O holds by g,which is defined in Fig.8.Then,the ATOM rule allows us to over or the definite action D of some environment thread t' execute zero-or-more steps of the abstract code with the execution is enabled.Also we require the metric f()to decrease when of C.as long as the overall transition (including the abstract steps a definite action is performed.Besides,the metric should never and the concrete steps)satisfies the relational guarantee G.We can increase at any step of the execution. lift C's total correctness to the concurrent setting as long as the To ensure that the metric f decreases regardless of the time when environment consists of identity transitions only.To allow a weaker the environment's definite actions take place,the definite progress R,we can apply the ATOM-R rule later,which requires that the pre- should always hold.This is enforced by finding a stronger assertion and post-conditions be stable with respect to R. J such that p=J and Sta(,RVG)hold,that is,J is an invariant 4.2.4 Example:Ticket Locks that holds at every program point of the loop.If(R,G:DQ) We prove the starvation-freedom of the ticket lock implementation happens to satisfy the two premises,we can use(R,G:DQ) in Fig.9 using our logic rules.We have informally discussed in directly as,but in practice it could be easier to prove the stability Sec.2 the verification of the counter using a ticket lock(sfInc in requirement by finding a stronger/.The definition of stability Fig.1(c)).To simplify the presentation,here we erase the increment Sta(p,R)is given in Fig.8. in the critical section and focus on the progress property of the code Notice in (R,G:D'Q)we can use D'instead of D to in Fig.9.With an empty critical section,the code functions just as simplify the proof,as long as D'D and wffAct(R,D')are skip,so Fig.9 proves it is linearizable with respect to skip.The satisfied.The premise D'D.defined in Fig.6.says D'specifies proofs of sfInc (including its starvation-freedom and linearizability a subset of definite actions in D.For instance,if D consists of with respect to the atomic INC in Fig.1(a))are given in TR [22]. multiple definite actions and is in the form of DA...ADD' To help specify the queue of the threads requesting the lock,we may contain only a subset of these D(1 k n).The way to introduce an auxiliary array ticket.As shown in Fig.9,each array exclude in D'irrelevant definite actions can simplify the proof of cell ticketi records the ID of the unique thread which gets the the condition(2)of definite progress(see Definition 1). ticket number i.Here we use cid for the current thread ID. Given the definite progress condition,we know o will be We then define some predicates to describe the lock status. eventually true because each definite action will definitely happen. lock(tl,n,n2)contains the auxiliary ticket array in addition to Then the loop starts to consume O-tokens and needs to finally owner and next,where ownerni and nextn2,and tl is terminate,following our argument at the beginning. the list of the threads recorded in ticket[ni],...,ticket[n2-1]. We also use locked(tl,n,n2)for the case when tl is not empty. 4.2.3 More Inference Rules That is,the lock is acquired by the first thread in tl,while the The HIDE-O rule allows us to discard the tokens (by using) other threads in tl are waiting for the lock in order.Besides,we use when the termination of code C is already established,which is locklrre(tl,n1,n2)short for lock(tl,n,n2)A (t).That is,the useful for modular verification of nested loops. thread t is"irrelevant"to the lock:it does not request the lock.The formal definitions are given in TR [22]. ATOM rules for refinement reasoning.The ATOM rule allows us The bottom of Fig.9 defines the precondition P and the guaran- to logically execute the abstract code simultaneously with every tee condition G of the code.Gt specifies the possible atomic actions concrete step (let's first ignore the index k in the premises of the of a thread t.Lock:adds the thread t at the end of rl of the threads rule).We use[p]C[g]to represent the total correctness of C in requesting the lock and increments next.It corresponds to line 2 392for all f ∈ dom(Π) : Π(f) = (x, C) Γ(f) = (y, C0 ) dom(Π) = dom(Γ) D, R, G ` {P ∧ (x = y) ∧ arem(C0 ) ∧ (Ek, . . . , E1)}C{P ∧ arem(skip)} ∀t,t 0 . t 6= t 0 =⇒ Gt ⇒ Rt 0 wffAct(R, D) P ⇒ ¬Enabled(D) D, R, G ` {P}ΠΓ (OBJ) p ∧ B ⇒ p 0 p ∧ B ∧ (Enabled(D) ∨ Q) ⇒ p 0 ∗ (♦ ∧ emp) D, R, G ` {p 0}C{p} p ⇒ J Sta(J, R ∨ G) D0 6 D wffAct(R, D0 ) J ⇒ (R, G: D0 f −→Q) D, R, G ` {p}while (B){C}{p ∧ ¬B} (WHL) D, R, G ` {p}C{q} D, R, G ` {bpc♦}C{bqc♦} (HIDE-♦) ` [p]C[q 0 ] q 0 Vk q (TpU nk TqU) ⇒ G D, Id, G ` {p}hCi{q} (ATOM) D, Id, G ` {p}hCi{q} Sta({p, q}, R) D, R, G ` {p}hCi{q} (ATOM-R) Figure 7. Inference rules. requires the thread be waiting for its environment to perform a finite number of definite actions. Definition 1 (Definite Progress). S |= (R, G : D f −→ Q) iff the following hold for all t: (1) either S |= Qt, or there exists t 0 such that t 0 6= t and S |= Enabled(Dt 0 ); (2) for any t 0 6= t and S 0 , if (S, S 0 , 0) |= Rt ∧ hDt 0i, then ft(S 0 ) < ft(S); (3) for any S 0 , if (S, S 0 , 0) |= Rt ∨ Gt, then ft(S 0 ) ≤ ft(S). Here f is a function that maps the relational states S to some metrics over which there is a well-founded order <. Ignoring the index 0 above, the definition says either Q holds over S or the definite action Dt 0 of some environment thread t 0 is enabled. Also we require the metric f(S) to decrease when a definite action is performed. Besides, the metric should never increase at any step of the execution. To ensure that the metric f decreases regardless of the time when the environment’s definite actions take place, the definite progress should always hold. This is enforced by finding a stronger assertion J such that p ⇒ J and Sta(J, R∨ G) hold, that is, J is an invariant that holds at every program point of the loop. If (R, G : D f −→ Q) happens to satisfy the two premises, we can use (R, G : D f −→ Q) directly as J, but in practice it could be easier to prove the stability requirement by finding a stronger J. The definition of stability Sta(p, R) is given in Fig. 8. Notice in (R, G : D 0 f −→ Q) we can use D 0 instead of D to simplify the proof, as long as D 0 6 D and wffAct(R, D 0 ) are satisfied. The premise D 0 6 D, defined in Fig. 6, says D 0 specifies a subset of definite actions in D. For instance, if D consists of multiple definite actions and is in the form of D1 ∧ . . . ∧ Dn, D 0 may contain only a subset of these Dk (1 ≤ k ≤ n). The way to exclude in D 0 irrelevant definite actions can simplify the proof of the condition (2) of definite progress (see Definition 1). Given the definite progress condition, we know Q will be eventually true because each definite action will definitely happen. Then the loop starts to consume ♦-tokens and needs to finally terminate, following our argument at the beginning. 4.2.3 More Inference Rules The HIDE-♦ rule allows us to discard the tokens (by using b c♦) when the termination of code C is already established, which is useful for modular verification of nested loops. ATOM rules for refinement reasoning. The ATOM rule allows us to logically execute the abstract code simultaneously with every concrete step (let’s first ignore the index k in the premises of the rule). We use ` [p]C[q] to represent the total correctness of C in wffAct(R, D) iff ∀t. Rt ⇒ [Dt] ∧ (∀t 0 6= t. [Dt 0 ] ∨ Dt 0 ) Sta(p, R) iff ∀S, S0 , u, w, C. ((S, (u, w), C) |= p) ∧ ((S, S0 ) |= R) =⇒ (S0 , (u, w), C) |= p p V q iff ∀t, σ, Σ, u, w, C, ΣF . (((σ, Σ), (u, w), C) |= p) ∧ (Σ⊥ΣF ) =⇒ ∃C0 , Σ0 . ((C, Σ]ΣF ) −_∗ t (C0 , Σ0]ΣF )) ∧ ((σ, Σ0 ), (u, w), C0 ) |=q Figure 8. Auxiliary defs. used in logic rules (simplified version). sequential separation logic. The corresponding rules are standard and elided here. We use p V q for the zero or multiple-step executions from the abstract code specified by p to the code specified by q, which is defined in Fig. 8. Then, the ATOM rule allows us to execute zero-or-more steps of the abstract code with the execution of C, as long as the overall transition (including the abstract steps and the concrete steps) satisfies the relational guarantee G. We can lift C’s total correctness to the concurrent setting as long as the environment consists of identity transitions only. To allow a weaker R, we can apply the ATOM-R rule later, which requires that the pre￾and post-conditions be stable with respect to R. 4.2.4 Example: Ticket Locks We prove the starvation-freedom of the ticket lock implementation in Fig. 9 using our logic rules. We have informally discussed in Sec. 2 the verification of the counter using a ticket lock (sfInc in Fig. 1(c)). To simplify the presentation, here we erase the increment in the critical section and focus on the progress property of the code in Fig. 9. With an empty critical section, the code functions just as skip, so Fig. 9 proves it is linearizable with respect to skip. The proofs of sfInc (including its starvation-freedom and linearizability with respect to the atomic INC in Fig. 1(a)) are given in TR [22]. To help specify the queue of the threads requesting the lock, we introduce an auxiliary array ticket. As shown in Fig. 9, each array cell ticket[i] records the ID of the unique thread which gets the ticket number i. Here we use cid for the current thread ID. We then define some predicates to describe the lock status. lock(tl, n1, n2) contains the auxiliary ticket array in addition to owner and next, where owner 7→ n1 and next 7→ n2, and tl is the list of the threads recorded in ticket[n1], . . . , ticket[n2 − 1]. We also use locked(tl, n1, n2) for the case when tl is not empty. That is, the lock is acquired by the first thread in tl, while the other threads in tl are waiting for the lock in order. Besides, we use lockIrrt(tl, n1, n2) short for lock(tl, n1, n2) ∧ (t 6∈ tl). That is, the thread t is “irrelevant” to the lock: it does not request the lock. The formal definitions are given in TR [22]. The bottom of Fig. 9 defines the precondition P and the guaran￾tee condition G of the code. Gt specifies the possible atomic actions of a thread t. Lockt adds the thread t at the end of tl of the threads requesting the lock and increments next. It corresponds to line 2 392