wffAct(R,D)ift.lR」o→D]A(t≠t.[D]VD】 locked:兰（亿→t)envLocked,些3t'.locked,A(t'≠t) p言k9ift,a,∑，u,地，C,p. (((o,),(u,w),C)p)A(ELEr)=3u',w',C,E/. unlocked (L0)notOwnt unlocked V envLockedt ((C.EuEr)(C','))A (((a'),(u',w'),C')Fq) GtLockt V Unlockt A(,世）<k(u,) (<k defined in Fig.10) Lockt unlocked 1 lockedt Unlockt lockedt o unlocked Sta(p,R)iffG,G'.u,地，C,k. (6,(u,e),C)=p)(G,G',k)=R)→3u',w D lockedtunlocked k兰notOwn V locked, (G,(u',w),C=p)A(u',w)≈k(u,世) ∫1ifG=envLocked: where is defined in Fig.10. Q:兰unlocked V locked fi(6)={0if6卡Q: Figure 11.Key auxiliary definitions for inference rules (final notOwncia A◆} version that supersedes definitions in Fig.8). local b false; ((-b)A notOwnciaAA)V (bA lockedeid) while (!b){ precondition the number of -tokens needed for each object method {(unlocked A◆)V(envLockedcid A◆AO)} The side condition wffAct(R,D)is also redefined in Fig.11,which b :cas(L,0,cid); is explained below. (b A lockedcia)V((-b)A notOwncia AA) 4 Decreasing -tokens at the ATOM rule.The thread loses lockedeia tokens when it performs an action that may delay other threads.This [L]:=0: is required by the AToM rule.Depending on whether the atomic notOwneid command may delay others or not,we assign a level k in the premise Figure 12.Proofs for the TAS lock g'g,which is redefined in Fig.11.Similar to pg in Fig.8. it allows us to execute the abstract code.Now it also requires the number of -tokens at level k to be decreased if k 1. code and prove it is linearizable with respect to skip.Here we omit Note k:cannot be arbitrarily chosen.The assignment of the the assertion arem(skip)at each line in the proof,and focus on level k to the atomic operation must be consistent with the level proving deadlock-freedom of the code. specification in G,as required by the third premise. As defined at the top of Fig.12,the action Locke (corresponding Being delayed:increasing tokens at stability checking. When to the successful cas at line 3)is at level 1,which may delay other the progress of the thread t is delayed by a level-k(>1)action threads trying to acquire the lock.The Unlockt action is at level 0, which cannot delay other threads.Also the precondition is given a from its environment thread t',thread t could gain more O-tokens to do more loop iterations.It could also gain more level-k'('<k) -token,which is required to pay for the Lock action. -tokens to execute more level-k'actions.Here increasing tokens The definite action D simply says that the thread t would eventually release the lock when it acquires the lock.It is easy would not affect the soundness of our logic because the environment thread t'must pay a higher-level token for its higher-level delaying to check that the side conditions about R.G and D in the oBJ rule. action.As we explained in Sec.2.3.4,the -tokens at all levels in e.g.,wffAct(R.D).are satisfied. the whole system actually form a tuple which strictly descends along R,G:DQ specifies the queue of definite actions which now the dictionary order,ensuring the whole-system progress. contains at most one environment thread.That is,the metric f() We re-define the stability Sta(p,R)in Fig.11 to reflect the is 1 if the lock is not available,and is 0 otherwise.When an possible increasing of tokens for the thread t.We could reset w and environment thread t'cuts in line by acquiring the lock when the the number at level k'<k in u after the environment step R if this lock is free.the current thread t has to wait for D.,before t itself step is associated with a levelk(1). progresses.Thus in R,G:DQ the current threadt can reset its metric f()when its environment acquires the lock. Allowing queue jumps at definite progress and wffAct. As we explained in Sec.2.3.3,for deadlock-free objects,the environment The detailed proof at the bottom of Fig.12 shows the changes of tokens.We give the current thread one O-token (using the HIDE-O steps could cause queue jumps to delay the progress of the thread t rule)to do its loop at lines 2-4.It consumes this O-token at the Like starvation-free objects,the thread t using deadlock-free objects beginning of the loop body when O holds,as shown in the left may wait for a queue of definite actions made by its environment.A branch of the assertion p before line 3.When O does not hold,as queue jump would make the thread t wait for a longer queue of the shown in p's right branch.the loop does not consume the -token. environment's definite actions. As shown in Definition 1,the definite progress condition(R,G Next we stabilize p.For the left branch,if an environment thread t'acquires the lock,which is a delaying action Locke,we let the D)allows the thread to reset its metric f()for a queue jump current thread regain a O-token.The resulting state just satisfies the when the environment step is associated with level k>1 (i.e.,it is right branch of p.Thus p is already stable. a delaying action).In this case,although the current thread may be The current thread pays its -token when its cas at line 3 blocked for a longer time,the whole system must progress since a succeeds (i.e.,it acquires the lock),as shown in the left branch -token is paid by the environment thread for the delaying action. of the assertion after line 3.If the cas fails,the thread still has to Also the requirement wffAct(R.D)(used at the OBJ rule and acquire the lock in the future and to try one more iteration. the WHL rule)should be revised to allow queue jumps.The new definition is shown in Fig.11.Here we allow a queue jump to disable 4.3.3 Another Example:Nested Locks with Rollback the definite action D of the thread at the head of the queue,so it is not necessary to require Enabled(D)to be preserved when the To demonstrate the use of action levels,we verify the rollback code in Fig.2(b)which we informally discussed in Sec.2.Here we environment step is associated with level k>1. assume all the methods of the object either acquire L1 before L2(as 4.3.2 Example:Test-and-Set Locks in the method of Fig.2(b)),or acquire only one lock. In Fig.12,we verify the test-and-set lock implementation explained Stratified delaying actions.As in the TAS lock example in in Sec.2.Like the ticket lock proofs in Sec.4.2.4,we simplify the Sec.4.3.2,lock acquirements are delaying actions.Here we have 394wffAct(R, D) iff ∀t. bRtc0 ⇒ [Dt] ∧ (∀t 0 6= t. [Dt 0 ] ∨ Dt 0 ) p Vk q iff ∀t, σ, Σ, u, w, C, ΣF . (((σ, Σ), (u, w), C) |= p) ∧ (Σ⊥ΣF ) =⇒ ∃u 0 , w0 , C0 , Σ0 . ((C, Σ]ΣF ) −_∗ t (C0 , Σ0]ΣF )) ∧ (((σ, Σ0 ), (u 0 , w0 ), C0 ) |= q) ∧ (u 0 , w0 ) <k (u, w) (<k defined in Fig. 10) Sta(p, R) iff ∀S, S0 , u, w, C, k. ((S, (u, w), C) |= p) ∧ ((S, S0 , k) |= R) =⇒ ∃u 0 , w0 . ((S0 , (u 0 , w0 ), C) |= p) ∧ ((u 0 , w0 ) ≈k (u, w)) where ≈k is defined in Fig. 10. Figure 11. Key auxiliary definitions for inference rules (final version that supersedes definitions in Fig. 8). precondition the number of -tokens needed for each object method. The side condition wffAct(R, D) is also redefined in Fig. 11, which is explained below. Decreasing -tokens at the ATOM rule. The thread loses - tokens when it performs an action that may delay other threads. This is required by the ATOM rule. Depending on whether the atomic command may delay others or not, we assign a level k in the premise q 0 Vk q, which is redefined in Fig. 11. Similar to p V q in Fig. 8, it allows us to execute the abstract code. Now it also requires the number of -tokens at level k to be decreased if k ≥ 1. Note k cannot be arbitrarily chosen. The assignment of the level k to the atomic operation must be consistent with the level specification in G, as required by the third premise. Being delayed: increasing tokens at stability checking. When the progress of the thread t is delayed by a level-k (k ≥ 1) action from its environment thread t 0 , thread t could gain more ♦-tokens to do more loop iterations. It could also gain more level-k 0 (k 0 < k) -tokens to execute more level-k 0 actions. Here increasing tokens would not affect the soundness of our logic because the environment thread t 0 must pay a higher-level token for its higher-level delaying action. As we explained in Sec. 2.3.4, the -tokens at all levels in the whole system actually form a tuple which strictly descends along the dictionary order, ensuring the whole-system progress. We re-define the stability Sta(p, R) in Fig. 11 to reflect the possible increasing of tokens for the thread t. We could reset w and the number at level k 0 < k in u after the environment step R if this step is associated with a level k (k ≥ 1). Allowing queue jumps at definite progress and wffAct. As we explained in Sec. 2.3.3, for deadlock-free objects, the environment steps could cause queue jumps to delay the progress of the thread t. Like starvation-free objects, the thread t using deadlock-free objects may wait for a queue of definite actions made by its environment. A queue jump would make the thread t wait for a longer queue of the environment’s definite actions. As shown in Definition 1, the definite progress condition (R, G: D f −→Q) allows the thread to reset its metric f(S) for a queue jump when the environment step is associated with level k ≥ 1 (i.e., it is a delaying action). In this case, although the current thread may be blocked for a longer time, the whole system must progress since a -token is paid by the environment thread for the delaying action. Also the requirement wffAct(R, D) (used at the OBJ rule and the WHL rule) should be revised to allow queue jumps. The new definition is shown in Fig. 11. Here we allow a queue jump to disable the definite action D of the thread at the head of the queue, so it is not necessary to require Enabled(D) to be preserved when the environment step is associated with level k ≥ 1. 4.3.2 Example: Test-and-Set Locks In Fig. 12, we verify the test-and-set lock implementation explained in Sec. 2. Like the ticket lock proofs in Sec. 4.2.4, we simplify the lockedt def = (L 7→ t) envLockedt def = ∃t 0 . lockedt 0 ∧ (t 0 6= t) unlocked def = (L 7→ 0) notOwnt def = unlocked ∨ envLockedt Gt def = Lockt ∨ Unlockt Lockt def = unlocked n1 lockedt Unlockt def = lockedt n0 unlocked Dt def = lockedt ❀ unlocked Jt def = notOwnt ∨ lockedt Qt def = unlocked ∨ lockedt ft(S) =  1 if S |= envLockedt 0 if S |= Qt  notOwncid ∧  1 local b := false;  ((¬b) ∧ notOwncid ∧  ∧ ♦) ∨ (b ∧ lockedcid) 2 while (!b) {  (unlocked ∧ ) ∨ (envLockedcid ∧  ∧ ♦) 3 b := cas(L, 0, cid);  (b ∧ lockedcid) ∨ ((¬b) ∧ notOwncid ∧  ∧ ♦) 4 }  lockedcid 5 [L] := 0;  notOwncid Figure 12. Proofs for the TAS lock. code and prove it is linearizable with respect to skip. Here we omit the assertion arem(skip) at each line in the proof, and focus on proving deadlock-freedom of the code. As defined at the top of Fig. 12, the action Lockt (corresponding to the successful cas at line 3) is at level 1, which may delay other threads trying to acquire the lock. The Unlockt action is at level 0, which cannot delay other threads. Also the precondition is given a -token, which is required to pay for the Lockt action. The definite action D simply says that the thread t would eventually release the lock when it acquires the lock. It is easy to check that the side conditions about R, G and D in the OBJ rule, e.g., wffAct(R, D), are satisfied. R, G: D f −→Q specifies the queue of definite actions which now contains at most one environment thread. That is, the metric f(S) is 1 if the lock is not available, and is 0 otherwise. When an environment thread t 0 cuts in line by acquiring the lock when the lock is free, the current thread t has to wait for Dt 0 before t itself progresses. Thus in R, G: D f −→Q the current thread t can reset its metric f(S) when its environment acquires the lock. The detailed proof at the bottom of Fig. 12 shows the changes of tokens. We give the current thread one ♦-token (using the HIDE-♦ rule) to do its loop at lines 2-4. It consumes this ♦-token at the beginning of the loop body when Q holds, as shown in the left branch of the assertion p before line 3. When Q does not hold, as shown in p’s right branch, the loop does not consume the ♦-token. Next we stabilize p. For the left branch, if an environment thread t 0 acquires the lock, which is a delaying action Lockt 0 , we let the current thread regain a ♦-token. The resulting state just satisfies the right branch of p. Thus p is already stable. The current thread pays its -token when its cas at line 3 succeeds (i.e., it acquires the lock), as shown in the left branch of the assertion after line 3. If the cas fails, the thread still has  to acquire the lock in the future and ♦ to try one more iteration. 4.3.3 Another Example: Nested Locks with Rollback To demonstrate the use of action levels, we verify the rollback code in Fig. 2(b) which we informally discussed in Sec. 2. Here we assume all the methods of the object either acquire L1 before L2 (as in the method of Fig. 2(b)), or acquire only one lock. Stratified delaying actions. As in the TAS lock example in Sec. 4.3.2, lock acquirements are delaying actions. Here we have 394