11oca11,0,r; 了k if(G,G)=P×kQ 2 <i :getAndInc(next);ticket [i]:=cid > C((6,),PxkQ) maxL otherwise 3 o :[owner];while (i !o){o :[owner]; c((6.6'),[P]) 智 0 if(6,6)卡[] 4 [owner]:i +1; maxL otherwise c((6,6'),D) 鸣 0 if(6.6')ED P3t,n1:n2.locklrrt(tl,n1,n2)Gt Lockt V Unlockt maxL otherwise Lockt,n1,n2.locklrrt(tl,n1,n2)locked(tl::t,n1,n2+1) C((,'),RAR')max(C((,G'),R),C((,G'),R')) Unlock:,n1,n2.locked(t::tl,n1,n2)x locklrrt(,n1+1,n2) C((6,'),RVR)min(C((6,G),R),C((6,G'),R)) DVil,n1:n2.locked(t:n1:n2)locklrrt(tl,n+1,n2) c((,6'),LRJo) 0 if c((6.6).R)=0 k些3m1,n2,tlh1,2.tlocked,(n1,i,n2A(o≤n1） maxL otherwise Qt3n2,tl2.locked(t::112,i,n2)A (oi) (6,6)LRJo iff C((,'),R)=0 f()=k iff 6 3n1.(ownern1)*true A(i-n1 =k) (,)R iff C((),R)=k andk<maxL Figure 9.Proofs for the ticket lock(with auxiliary code in gray). R→R iff ve,s',k.((6,',k)ER)(6,',k)ER' u ::(nk;...:n1)(1<k<maxL) of Fig.9.Unlockt releases the lock by incrementing owner and de queuing the thread t which currently holds the lock.It corresponds (nm,,n)<k(nm,,ni)if（付i>k.(m=n)》A(nk<nk) to line 4 of Fig.9.The rely condition R includes all the G made (nm,,n)≈k(nm,,n1)if（i≥k.(=ni)》 by the environment threads t' u<u'iff 3k.u <k u' u≤u'iff u<u'Vu=u Next we define the definite action D.As we explained in Sec.2,D.requires that whenever the thread t holds a lock with (u,w)<k (u',w')iff (u <k u')v(k=0Au=u'Aw=w') ownern,it should eventually release the lock by incrementing (u,w)≈k(u',w）ifu≈kA(k=0→w=w) owner to n+1.We can prove the side conditions about well- formedness of specifications in the oBJ rule hold. Figure 10.Levels of state transitions and tokens. The key to verifying the loop at line 3 is to find a metric function f and prove definite progressJ(R,G':DQ)for a To interpret the level numbers in the assertion semantics,we de- stableJ.As shown in Fig.9,we define/to say that the thread fine C((,)R)in Fig.10 which assigns a level to the transition t is requesting the lock.Here tlockedt.(n,i,n2)is similar (')given the specification R.That is,if C((,)R)=k. to locked(th::t::tl2,n1,n2).It also says that the thread t takes we say R views (as a level-k transition.We let k maxL if the ticket number i.specifies the case when th is empty (thus the transition does not satisfy R.Given the level function,we can owneri).We also strengthen the guarantee condition G of the now define the semantics ofRo,which picks out the transitions loop to ld,the identity transitions. that R views as level-0 ones.For the following example R, The metric function f maps each state to the difference between i and owner at that state,which describes the number R些(PxoQ)V(P'x1Q) of threads ahead of t in the waiting queue.We use the usual<order Ro is equivalent to P xo Q.Besides,R=Ro means that R on natural numbers as the associated well-founded order.Then,we views all state transitions as level-0 ones,thus any state transitions can verifyJ→(R,G':D∠Q). of R should not delay the progress of other threads. Finally,we prove that the loop terminates with one -token when We use (',k)ER as a shorthand for C((,)R)=k O holds or D is enabled.Then we can conclude linearizability and (k<maxL).Then the implication RR'is redefined under this starvation-freedom of the ticket lock implementation in Fig.9. new interpretation,as shown in Fig.10. -tokens in assertions.To ensure the progress of the whole 4.3 Adding Delay for Deadlock-Free Objects system,we require the steps of delaying actions to pay -tokens. As we explained in Sec.2,deadlock-free objects allow the progress Since we allow multi-levels of transitions to delay other threads, of a thread to be delayed by its environment,as long as the whole the -tokens are stratified accordingly.Thus we introduce the new system makes progress.Correspondingly,to verify deadlock-free assertion (Ex,...,E1)in Fig.4,whose semantics is defined in objects,we extend our logic with a delay mechanism.First we find Fig.5.It says the number of each level-j -tokens is no less than out the delaying actions and stratify them for objects with rollbacks Ei.Here u is a sequence (nk,...,n)recording the numbers of where a delaying action may trigger more steps of other delaying tokens at different levels,as defined in Fig.10.We overload as the actions.Then,we introduce -tokens (we usehere to distinguish dictionary order for the sequence of natural numbers.The ordering them from -tokens for loops)to bound the number of delaying over u and other related definitions are also given in Fig.10. actions in each method,so we avoid infinite delays without whole- 4.3.1 Inference Rules Revisited system progress. To use the logic to verify deadlock-free objects,we need to first Multi-level rely/guarantee assertions.As shown in Fig.4,we find in each object method the actions that may delay the progress index the rely/guarantee assertion P Q with a natural number k of others.Since some of these actions may be further delayed by and call it a level-k action.We require 0<k<maxL,where maxL others,we assign levels to them to ensure each action can only be is a predefined upper bound of all levels.Intuitively,P could delayed by ones at higher levels.We specify the actions and their make other threads do more actions at a level k'<k.Thus P oQ levels in the rely/guarantee conditions.We also need to decide an cannot make other threads do any more actions,i.e.,it cannot delay upper bound of these execution steps at each level and specify them other threads.P1Q could make other threads do more actions as the number of -tokens in the precondition of each method. at level 0 but no more at level 1,thus we avoid the problem of Below we revisit the inference rules in Fig.7 and explain their use delay-caused circular dependency discussed in Sec.2.2.2. of multi-level actions and -tokens.In the OBJ rule,we specify in the 3931 local i, o, r; 2 <i := getAndInc(next); ticket[i] := cid >; 3 o := [owner]; while (i != o) { o := [owner]; } 4 [owner] := i + 1; Pt def = ∃tl, n1, n2. lockIrrt(tl, n1, n2) Gt def = Lockt ∨ Unlockt Lockt def = ∃tl, n1, n2. lockIrrt(tl, n1, n2) n locked(tl::t, n1, n2 + 1) Unlockt def = ∃tl, n1, n2. locked(t::tl, n1, n2) n lockIrrt(tl, n1+1, n2) Dt def = ∀tl, n1, n2. locked(t::tl, n1, n2) ❀ lockIrrt(tl, n1 + 1, n2) Jt def = ∃n1, n2, tl1, tl2. tlockedtl1,t,tl2 (n1, i, n2) ∧ (o ≤ n1) Qt def = ∃n2, tl2. locked(t::tl2, i, n2) ∧ (o ≤ i) f(S) = k iff S |= ∃n1. (owner 7→ n1) ∗ true ∧ (i − n1 = k) Figure 9. Proofs for the ticket lock (with auxiliary code in gray). of Fig. 9. Unlockt releases the lock by incrementing owner and de￾queuing the thread t which currently holds the lock. It corresponds to line 4 of Fig. 9. The rely condition Rt includes all the Gt 0 made by the environment threads t 0 . Next we define the definite action D. As we explained in Sec. 2, Dt requires that whenever the thread t holds a lock with owner 7→ n1, it should eventually release the lock by incrementing owner to n1 + 1. We can prove the side conditions about well￾formedness of specifications in the OBJ rule hold. The key to verifying the loop at line 3 is to find a metric function f and prove definite progress J ⇒ (R, G0 : D f −→Q) for a stable J. As shown in Fig. 9, we define Jt to say that the thread t is requesting the lock. Here tlockedtl1,t,tl2 (n1, i, n2) is similar to locked(tl1 :: t :: tl2, n1, n2). It also says that the thread t takes the ticket number i. Qt specifies the case when tl1 is empty (thus owner 7→ i). We also strengthen the guarantee condition G 0 of the loop to Id, the identity transitions. The metric function f maps each state S to the difference between i and owner at that state, which describes the number of threads ahead of t in the waiting queue. We use the usual < order on natural numbers as the associated well-founded order. Then, we can verify J ⇒ (R, G0 : D f −→Q). Finally, we prove that the loop terminates with one ♦-token when Q holds or D is enabled. Then we can conclude linearizability and starvation-freedom of the ticket lock implementation in Fig. 9. 4.3 Adding Delay for Deadlock-Free Objects As we explained in Sec. 2, deadlock-free objects allow the progress of a thread to be delayed by its environment, as long as the whole system makes progress. Correspondingly, to verify deadlock-free objects, we extend our logic with a delay mechanism. First we find out the delaying actions and stratify them for objects with rollbacks where a delaying action may trigger more steps of other delaying actions. Then, we introduce -tokens (we use  here to distinguish them from ♦-tokens for loops) to bound the number of delaying actions in each method, so we avoid infinite delays without whole￾system progress. Multi-level rely/guarantee assertions. As shown in Fig. 4, we index the rely/guarantee assertion P nk Q with a natural number k and call it a level-k action. We require 0 ≤ k < maxL, where maxL is a predefined upper bound of all levels. Intuitively, P nk Q could make other threads do more actions at a level k 0 < k. Thus P n0 Q cannot make other threads do any more actions, i.e., it cannot delay other threads. P n1 Q could make other threads do more actions at level 0 but no more at level 1, thus we avoid the problem of delay-caused circular dependency discussed in Sec. 2.2.2. L((S, S0 ), P nk Q) def =  k if (S, S0 ) |= P nk Q maxL otherwise L((S, S0 ), [P]) def =  0 if (S, S0 ) |= [P] maxL otherwise L((S, S0 ), D) def =  0 if (S, S0 ) |= D maxL otherwise L((S, S0 ), R ∧ R0 ) def = max(L((S, S0 ), R), L((S, S0 ), R0 )) L((S, S0 ), R ∨ R0 ) def = min(L((S, S0 ), R), L((S, S0 ), R0 )) L((S, S0 ), bRc0) def =  0 if L((S, S0 ), R) = 0 maxL otherwise (S, S0 ) |= bRc0 iff L((S, S0 ), R) = 0 (S, S0 , k) |= R iff L((S, S0 ), R) = k and k < maxL R ⇒ R0 iff ∀S, S0 , k. ((S, S0 , k) |= R) =⇒ (S, S0 , k) |= R0 u ::= (nk, . . . , n1) (1 ≤ k < maxL) (n 0m, . . . , n0 1 ) <k (nm, . . . , n1) iff (∀i > k. (n 0 i = ni)) ∧ (n 0 k < nk) (n 0m, . . . , n0 1 ) ≈k (nm, . . . , n1) iff (∀i ≥ k. (n 0 i = ni)) u < u0 iff ∃k. u <k u 0 u ≤ u 0 iff u < u0 ∨ u = u 0 (u, w) <k (u 0 , w0 ) iff (u <k u 0 ) ∨ (k = 0 ∧ u = u 0 ∧ w = w0 ) (u, w) ≈k (u 0 , w0 ) iff u ≈k u 0 ∧ (k = 0 =⇒ w = w0 ) Figure 10. Levels of state transitions and tokens. To interpret the level numbers in the assertion semantics, we de￾fine L((S, S 0 ), R) in Fig. 10 which assigns a level to the transition (S, S 0 ), given the specification R. That is, if L((S, S 0 ), R) = k, we say R views (S, S 0 ) as a level-k transition. We let k = maxL if the transition does not satisfy R. Given the level function, we can now define the semantics of bRc0, which picks out the transitions that R views as level-0 ones. For the following example R, R def = (P n0 Q) ∨ (P 0 n1 Q0 ) bRc0 is equivalent to P n0 Q. Besides, R ⇒ bRc0 means that R views all state transitions as level-0 ones, thus any state transitions of R should not delay the progress of other threads. We use (S, S 0 , k) |= R as a shorthand for L((S, S 0 ), R) = k (k < maxL). Then the implication R ⇒ R 0 is redefined under this new interpretation, as shown in Fig. 10. -tokens in assertions. To ensure the progress of the whole system, we require the steps of delaying actions to pay -tokens. Since we allow multi-levels of transitions to delay other threads, the -tokens are stratified accordingly. Thus we introduce the new assertion (Ek, . . . , E1) in Fig. 4, whose semantics is defined in Fig. 5. It says the number of each level-j -tokens is no less than Ej . Here u is a sequence (nk, . . . , n1) recording the numbers of - tokens at different levels, as defined in Fig. 10. We overload < as the dictionary order for the sequence of natural numbers. The ordering over u and other related definitions are also given in Fig. 10. 4.3.1 Inference Rules Revisited To use the logic to verify deadlock-free objects, we need to first find in each object method the actions that may delay the progress of others. Since some of these actions may be further delayed by others, we assign levels to them to ensure each action can only be delayed by ones at higher levels. We specify the actions and their levels in the rely/guarantee conditions. We also need to decide an upper bound of these execution steps at each level and specify them as the number of -tokens in the precondition of each method. Below we revisit the inference rules in Fig. 7 and explain their use of multi-level actions and -tokens. In the OBJ rule, we specify in the 393