assigning a finite number of tokens to each method.A token must Definite actions. First,we introduce a novel notion called a be paid to execute a delaying action. "definite action"D.which models a thread action that,once enabled. Third,we divide actions of a thread into normal ones (which do must be eventually finished regardless of what the environment not delay others)and delaying ones,and further stratify delaying does.In detail,D is in the form of PaQd.It requires in every actions into multiple levels.When a thread is delayed by a level-k execution that Qa should eventually hold if Pa holds,and Pa should action from its environment,it is allowed to execute not only more be preserved (by both the current thread and the environment)until normal actions,but also more delaying actions at lower levels Qa holds.For sfInc,the definite action Pa d of a thread can Allowing one delaying action to trigger more steps of other delaying be defined as follows.Pa says that owner equals the thread's ticket actions is necessary for verifying algorithms with nested locks and number i,and Qa says that owner has been increased to i+1.Tha rollbacks,such as the optimistic lists in Fig.2(a).The stratification is,a thread definitely releases the lock when acquiring it.Of course prevents the circular delay in the example of Fig.2(b) we have to ensure in our logic that D is indeed definite.We will Fourth,our delaying actions and definite actions are all seman explain in detail the logic rule that enforces it in Sec.4.2.2 tically specified as part of object specifications,therefore we can support ad-hoc synchronizaiton and do not rely on built-in synchro- Definite progress.Then we use definite actions to prove termina- nization primitives to enforce ordering of events.Moreover,since tion of loops.We need to first find an assertion specifying the the specifications are all parametrized over states,they are expres- condition when the thread t can progress on its own,i.e.,it is not sive enough to support dynamic locks as in lock-coupling lists.Also blocked.Then we enforce the following principles: our "definite progress"condition allows each blocked thread to de- cide locally and dynamically a queue of definite actions it waits for. 1.If is continuously true,we need to prove the loop terminates There is no need to enforce a global ordering of blocking depen- following the idea of the TERM rule; dencies agreed by every thread.This also provides thread-modular 2.If O is false,the following must always be true: support of dynamic locks. Below we give more details about some of these key ideas. (a)There is a finite queue of definite actions of other threads that the thread t is waiting for,among which there is at least one (from a certain thread t')enabled.The length of the 2.3.1 Using Tokens to Prevent Infinite Loops queue is E. The key to ensuring termination is to require each loop to terminate (b)E decreases whenever one of these definite actions is fin- Earlier work [16,24]requires each round of the loop to consume ished; resources called tokens.The rule for loops is in the following form: (c)The expression E is never increased by any threads (no PAB→P*OR,GF{PCP matter whether O holds or not);and it is non-negative. (TERM) R,GH(P)while (B)CIPA-B) We can see E serves as a well-founded metric.By induction over E Here◇represents one token,and“*”is the normal separating we know eventually O holds,which implies the termination of the ohe one eken tain t ane loop by the above condition 1. These conditions are enforced in our new inference rule for token needs to be consumed to start this new round of loop.Since loops,which extends the TERM rule (in Sec.2.3.1)and is presented the number of tokens strictly decreases,we know the loop must in Sec.4.2.2.The condition 2 shows the use of definite actions terminate when the thread has no token. in our reasoning about progress.We call it the"definite progress" We use this simple idea to enforce termination of loops,and condition. extend it to handle blocking and delay in a concurrent setting The reasoning above implicitly makes use of the fairness as- sumption.The fair scheduling ensures that the environment thread t 2.3.2 Definite Actions and Definite Progress mentioned in the condition 2(a)is scheduled infinitely often.there- fore its definite action will definitely happen.By conditions 2(b) Our approach to cut the blocking-caused circular dependency is and 2(c)we know E will become smaller.In this way E keeps inspired by the implementation of ticket locks,which is used to decreasing until Q holds eventually. implement the starvation-free counter sfInc in Fig.1(c).It uses For sfInc,O is defined as (i owner)and the metric E is the shared variables owner and next to guarantee the first-come- first-served property of the lock.Initially owner equals next.To (i-owner).Whenever an environment thread t'finishes a definite action by releasing the lock,it increases owner,so E decreases. acquire the lock,a thread atomically increments next and reads When E is decreased to 0,the current thread is unblocked.Its loop its old value to a variable i (line 2).The value of i becomes the terminates and it succeeds in acquiring the lock thread's ticket.The thread waits until owner equals its ticket value i (line 3).Finally the lock is released by incrementing owner (line 5) such that the next waiting thread (the thread with ticket i+1.if 2.3.3 Allowing Queue Jumps for Deadlock-Free Objects there is one)can now enter the critical section. The method dfInc in Fig.1(b)implements a deadlock-free counter We can see sfInc is not concerned with the circular dependency using the TAS lock.If the current thread t waits for the lock,we problem.Intuitively the ticket lock algorithm ensures that the threads know the queue of definite actions it waits for is of length one requesting the lock always constitute a queue ti,t2,...,tn.The because it is possible for the thread to acquire the lock immediately head thread,t1.gets the ticket number which equals owner and after the lock is released.However,as we explain in Sec.2.2.1 can immediately acquire the lock.Once it releases the lock (by another thread t'may preempt t and do a successful cas.Then increasing owner),ti is dequeued.Moreover,for any thread t in thread t is blocked and waits for a queue of definite actions again this queue,the number of threads ahead of t never increases.Thus t This delay caused by thread t'can be viewed as a queue jump in our must eventually become the head of the queue and acquire the lock definite-progress-based reasoning.Actually dfInc cannot satisfy Here the dependencies among progress of the threads are in concert the definite progress requirement because we cannot find a strictly with the queue decreasing queue size E.It is not starvation-free. Following this queue principle,we explicitly specify the queue However,the queue jump here is acceptable when verifying of progress dependencies in our logic to avoid circular reasoning deadlock-freedom.This is because thread t'delays t only if t 388assigning a finite number of tokens to each method. A token must be paid to execute a delaying action. Third, we divide actions of a thread into normal ones (which do not delay others) and delaying ones, and further stratify delaying actions into multiple levels. When a thread is delayed by a level-k action from its environment, it is allowed to execute not only more normal actions, but also more delaying actions at lower levels. Allowing one delaying action to trigger more steps of other delaying actions is necessary for verifying algorithms with nested locks and rollbacks, such as the optimistic lists in Fig. 2(a). The stratification prevents the circular delay in the example of Fig. 2(b). Fourth, our delaying actions and definite actions are all seman￾tically specified as part of object specifications, therefore we can support ad-hoc synchronizaiton and do not rely on built-in synchro￾nization primitives to enforce ordering of events. Moreover, since the specifications are all parametrized over states, they are expres￾sive enough to support dynamic locks as in lock-coupling lists. Also our “definite progress” condition allows each blocked thread to de￾cide locally and dynamically a queue of definite actions it waits for. There is no need to enforce a global ordering of blocking depen￾dencies agreed by every thread. This also provides thread-modular support of dynamic locks. Below we give more details about some of these key ideas. 2.3.1 Using Tokens to Prevent Infinite Loops The key to ensuring termination is to require each loop to terminate. Earlier work [16, 24] requires each round of the loop to consume resources called tokens. The rule for loops is in the following form: P ∧ B ⇒ P 0 ∗ ♦ R, G ` {P 0}C{P} R, G ` {P}while (B) C{P ∧ ¬B} (TERM) Here ♦ represents one token, and “∗” is the normal separating conjunction in separation logic. The premise says the precondition P 0 of the loop body C has one less token than P, showing that one token needs to be consumed to start this new round of loop. Since the number of tokens strictly decreases, we know the loop must terminate when the thread has no token. We use this simple idea to enforce termination of loops, and extend it to handle blocking and delay in a concurrent setting. 2.3.2 Definite Actions and Definite Progress Our approach to cut the blocking-caused circular dependency is inspired by the implementation of ticket locks, which is used to implement the starvation-free counter sfInc in Fig. 1(c). It uses the shared variables owner and next to guarantee the first-come￾first-served property of the lock. Initially owner equals next. To acquire the lock, a thread atomically increments next and reads its old value to a variable i (line 2). The value of i becomes the thread’s ticket. The thread waits until owner equals its ticket value i (line 3). Finally the lock is released by incrementing owner (line 5) such that the next waiting thread (the thread with ticket i + 1, if there is one) can now enter the critical section. We can see sfInc is not concerned with the circular dependency problem. Intuitively the ticket lock algorithm ensures that the threads requesting the lock always constitute a queue t1,t2, . . . ,tn. The head thread, t1, gets the ticket number which equals owner and can immediately acquire the lock. Once it releases the lock (by increasing owner), t1 is dequeued. Moreover, for any thread t in this queue, the number of threads ahead of t never increases. Thus t must eventually become the head of the queue and acquire the lock. Here the dependencies among progress of the threads are in concert with the queue. Following this queue principle, we explicitly specify the queue of progress dependencies in our logic to avoid circular reasoning. Definite actions. First, we introduce a novel notion called a “definite action” D, which models a thread action that, once enabled, must be eventually finished regardless of what the environment does. In detail, D is in the form of Pd ❀ Qd. It requires in every execution that Qd should eventually hold if Pd holds, and Pd should be preserved (by both the current thread and the environment) until Qd holds. For sfInc, the definite action Pd ❀ Qd of a thread can be defined as follows. Pd says that owner equals the thread’s ticket number i, and Qd says that owner has been increased to i+ 1. That is, a thread definitely releases the lock when acquiring it. Of course we have to ensure in our logic that D is indeed definite. We will explain in detail the logic rule that enforces it in Sec. 4.2.2. Definite progress. Then we use definite actions to prove termina￾tion of loops. We need to first find an assertion Q specifying the condition when the thread t can progress on its own, i.e., it is not blocked. Then we enforce the following principles: 1. If Q is continuously true, we need to prove the loop terminates following the idea of the TERM rule; 2. If Q is false, the following must always be true: (a) There is a finite queue of definite actions of other threads that the thread t is waiting for, among which there is at least one (from a certain thread t 0 ) enabled. The length of the queue is E. (b) E decreases whenever one of these definite actions is fin￾ished; (c) The expression E is never increased by any threads (no matter whether Q holds or not); and it is non-negative. We can see E serves as a well-founded metric. By induction over E we know eventually Q holds, which implies the termination of the loop by the above condition 1. These conditions are enforced in our new inference rule for loops, which extends the TERM rule (in Sec. 2.3.1) and is presented in Sec. 4.2.2. The condition 2 shows the use of definite actions in our reasoning about progress. We call it the “definite progress” condition. The reasoning above implicitly makes use of the fairness as￾sumption. The fair scheduling ensures that the environment thread t 0 mentioned in the condition 2(a) is scheduled infinitely often, there￾fore its definite action will definitely happen. By conditions 2(b) and 2(c) we know E will become smaller. In this way E keeps decreasing until Q holds eventually. For sfInc, Q is defined as (i = owner) and the metric E is (i − owner). Whenever an environment thread t 0 finishes a definite action by releasing the lock, it increases owner, so E decreases. When E is decreased to 0, the current thread is unblocked. Its loop terminates and it succeeds in acquiring the lock. 2.3.3 Allowing Queue Jumps for Deadlock-Free Objects The method dfInc in Fig. 1(b) implements a deadlock-free counter using the TAS lock. If the current thread t waits for the lock, we know the queue of definite actions it waits for is of length one because it is possible for the thread to acquire the lock immediately after the lock is released. However, as we explain in Sec. 2.2.1, another thread t 0 may preempt t and do a successful cas. Then thread t is blocked and waits for a queue of definite actions again. This delay caused by thread t 0 can be viewed as a queue jump in our definite-progress-based reasoning. Actually dfInc cannot satisfy the definite progress requirement because we cannot find a strictly decreasing queue size E. It is not starvation-free. However, the queue jump here is acceptable when verifying deadlock-freedom. This is because thread t 0 delays t only if t 0 388