Linearizability and Liveness).It supports verification of both mutex- (a)abstract operation INC:<x++>; based pessimistic algorithms(including fine-grained ones such as dfInc: lock-coupling lists)and optimistic ones such as optimistic lists and 1 local b :false,ri lazy lists.The unified approach allows us to prove in the same logic 2 while (!b){b :cas(&L,0,cid);/lock L for instance,the lock-coupling list algorithm is starvation-free if we 3 r :x;x :=r 1;/critical section use fair locks,e.g.,ticket locks [25],and is deadlock-free if regular 4 L :0;/unlock L test-and-set (TAS)based spin locks are used.Our work is based on (b)deadlock-free implementation df Inc using a test-and-set lock earlier work on concurrency verification,but we make the following new contributions: sfInc: 11oca11,0,r: 2 i:=getAndInc(next); We divide environment interference that affects progress of a 3 o :owner;while (i !o)o :owner; thread into two classes.namely blocking and delay.We show 4 r=x;x:=r+1; /critical section different occurrences of them correspond to the classification of owner :i+1; progress into wait-freedom,lock-freedom,starvation-freedom (c)starvation-free implementation sf Inc using a ticket lock and deadlock-freedom (see Sec.2.2.1 and Sec.6).Recognizing the two classes of interference allows us to come up with Figure 1.Counters different mechanisms in our program logic to reason about them separately.Our logic also provides parameterized specifications which can be instantiated to choose different combinations of objects too in Sec.6.Finally,we summarize the examples we have the mechanisms.This gives us a unified program logic that can verified in Sec.7.and discuss related work and conclude in Sec.8. verify different progress properties using the same set of rules. We propose two novel mechanisms.definite actions and strat- 2.Informal Development ified tokens,to reason about blocking and delay,respectively Below we first give an overview of the traditional rely-guarantee They are also our key techniques to avoid circularity in rely. logic for safety proofs [18],and the way to encode linearizability guarantee style liveness reasoning.A definite action character- verification in the logic.Then we explain the challenges and our izes a thread's progress that does not rely on the progress of the ideas in supporting liveness verification under fair scheduling. environment.Each blocked thread waits for a queue of definite actions.Starvation-freedom requires the length of the queue be 2.1 Background strictly decreasing,while deadlock-freedom allows disciplined queue jumps based on the token-transfer ideas [16.24].To avoid Rely-guarantee reasoning.In rely-guarantee reasoning [18]. circular delay,we further generalize the token-transfer ideas by each thread is verified in isolation under some assumptions on stratifying tokens into multiple levels,which enables us to verify its environment (i.e.,the other threads in the system).The judgment complex algorithms that involve both nested locks and rollbacks is in the form of R,GPC,where the pre-and post- (e.g.,the optimistic list algorithm). conditions P and Q specify the initial and final states respectively. The rely condition R specifies the assumptions on the environ- By verifying linearizability and progress together,we can pro- ment,which are the permitted state transitions that the environment vide progress-aware abstractions for concurrent objects (see threads may have.The guarantee condition G specifies the possible Sec.5).Our logic is based on termination-preserving simula- transitions made by the thread itself.To ensure that parallel threads tions as the meta-theory,which establish contextual refinements can collaborate,the guarantee of each thread needs to satisfy the that assume fair scheduling at both the concrete and the abstract rely of every other thread. levels.We prove the contextual refinements are equivalent to linearizability and starvation-freedom/deadlock-freedom.The Encoding linearizability verification.As a working example. refinements allow us to replace object implementations with Fig.1(b)shows a counter object dfInc implemented with a test- progress-aware abstract specifications when the client code is and-set (TAS)lock L.Verifying linearizability of dfInc requires verified.As far as we know,our abstraction for deadlock-free us to prove it has the same abstract behaviors as INC in Fig.1(a), (and linearizable)objects has never been proposed before. which increments the counter x atomically. We have applied our logic to verify simple objects with coarse- Following previous work [21,24,31],one can extend a rely- grained synchronization using TAS locks,ticket locks [25]and guarantee logic to verify linearizability.We use an assertion various queue locks (including Anderson array-based locks. arem(C)to specify as an auxiliary state the abstract operation C to CLH locks and MCS locks)[13].For examples with more be fulfilled,and logically execute C at the linearization point (LP) permissive locking schemes,we have successfully verified the of the concrete implementation.For dfInc,we prove a judgment in two-lock queues,and various fine-grained and optimistic list the form of R.GP A arem(INC)dfIncfQ A arem(skip) algorithms.To the best of our knowledge,we are the first to Here R and G specify the object's actions (i.e.,lock acquire and formally verify the starvation-freedom/deadlock-freedom of release,and the counter updates at both the concrete and the abstract lock-coupling lists,optimistic lists and lazy lists. sides)made by the environment and the current thread respectively. P and O are relational assertions specifying the consistency relation Notice that with the assumption of fair scheduling,wait-freedom between the program states at the concrete and the abstract sides. and lock-freedom are equivalent to starvation-freedom and deadlock- The postcondition arem(skip)shows that at the end of df Inc there freedom,respectively.Therefore our logic can also be applied to is no abstract operation to fulfill. verify wait-free and lock-free algorithms.We discuss this in Sec.6. 2.2 In the rest of this paper,we first analyze the challenges and Challenges of Progress Verification explain our approach informally in Sec.2.Then we give the basic Progress properties of objects such as deadlock-freedom and technical setting in Sec.3,and present our logic in Sec.4,whose starvation-freedom have various termination requirements of ob- soundness theorem,together with the abstraction theorem,is given ject methods.They must be satisfied with interference from other in Sec.5.We discuss how our logic supports wait-free and lock-free threads considered,which makes the verification challenging. 386Linearizability and Liveness). It supports verification of both mutex￾based pessimistic algorithms (including fine-grained ones such as lock-coupling lists) and optimistic ones such as optimistic lists and lazy lists. The unified approach allows us to prove in the same logic, for instance, the lock-coupling list algorithm is starvation-free if we use fair locks, e.g., ticket locks [25], and is deadlock-free if regular test-and-set (TAS) based spin locks are used. Our work is based on earlier work on concurrency verification, but we make the following new contributions: • We divide environment interference that affects progress of a thread into two classes, namely blocking and delay. We show different occurrences of them correspond to the classification of progress into wait-freedom, lock-freedom, starvation-freedom and deadlock-freedom (see Sec. 2.2.1 and Sec. 6). Recognizing the two classes of interference allows us to come up with different mechanisms in our program logic to reason about them separately. Our logic also provides parameterized specifications, which can be instantiated to choose different combinations of the mechanisms. This gives us a unified program logic that can verify different progress properties using the same set of rules. • We propose two novel mechanisms, definite actions and strat￾ified tokens, to reason about blocking and delay, respectively. They are also our key techniques to avoid circularity in rely￾guarantee style liveness reasoning. A definite action character￾izes a thread’s progress that does not rely on the progress of the environment. Each blocked thread waits for a queue of definite actions. Starvation-freedom requires the length of the queue be strictly decreasing, while deadlock-freedom allows disciplined queue jumps based on the token-transfer ideas [16, 24]. To avoid circular delay, we further generalize the token-transfer ideas by stratifying tokens into multiple levels, which enables us to verify complex algorithms that involve both nested locks and rollbacks (e.g., the optimistic list algorithm). • By verifying linearizability and progress together, we can pro￾vide progress-aware abstractions for concurrent objects (see Sec. 5). Our logic is based on termination-preserving simula￾tions as the meta-theory, which establish contextual refinements that assume fair scheduling at both the concrete and the abstract levels. We prove the contextual refinements are equivalent to linearizability and starvation-freedom/deadlock-freedom. The refinements allow us to replace object implementations with progress-aware abstract specifications when the client code is verified. As far as we know, our abstraction for deadlock-free (and linearizable) objects has never been proposed before. • We have applied our logic to verify simple objects with coarse￾grained synchronization using TAS locks, ticket locks [25] and various queue locks (including Anderson array-based locks, CLH locks and MCS locks) [13]. For examples with more permissive locking schemes, we have successfully verified the two-lock queues, and various fine-grained and optimistic list algorithms. To the best of our knowledge, we are the first to formally verify the starvation-freedom/deadlock-freedom of lock-coupling lists, optimistic lists and lazy lists. Notice that with the assumption of fair scheduling, wait-freedom and lock-freedom are equivalent to starvation-freedom and deadlock￾freedom, respectively. Therefore our logic can also be applied to verify wait-free and lock-free algorithms. We discuss this in Sec. 6. In the rest of this paper, we first analyze the challenges and explain our approach informally in Sec. 2. Then we give the basic technical setting in Sec. 3, and present our logic in Sec. 4, whose soundness theorem, together with the abstraction theorem, is given in Sec. 5. We discuss how our logic supports wait-free and lock-free (a) abstract operation INC: <x++>; dfInc : 1 local b := false, r; 2 while (!b) { b := cas(&L, 0, cid); } // lock L 3 r := x; x := r + 1; // critical section 4 L := 0; // unlock L (b) deadlock-free implementation dfInc using a test-and-set lock sfInc : 1 local i, o, r; 2 i := getAndInc(next); 3 o := owner; while (i != o) { o := owner; } 4 r := x; x := r + 1; // critical section 5 owner := i + 1; (c) starvation-free implementation sfInc using a ticket lock Figure 1. Counters. objects too in Sec. 6. Finally, we summarize the examples we have verified in Sec. 7, and discuss related work and conclude in Sec. 8. 2. Informal Development Below we first give an overview of the traditional rely-guarantee logic for safety proofs [18], and the way to encode linearizability verification in the logic. Then we explain the challenges and our ideas in supporting liveness verification under fair scheduling. 2.1 Background Rely-guarantee reasoning. In rely-guarantee reasoning [18], each thread is verified in isolation under some assumptions on its environment (i.e., the other threads in the system). The judgment is in the form of R, G ` {P}C{Q}, where the pre- and post￾conditions P and Q specify the initial and final states respectively. The rely condition R specifies the assumptions on the environ￾ment, which are the permitted state transitions that the environment threads may have. The guarantee condition G specifies the possible transitions made by the thread itself. To ensure that parallel threads can collaborate, the guarantee of each thread needs to satisfy the rely of every other thread. Encoding linearizability verification. As a working example, Fig. 1(b) shows a counter object dfInc implemented with a test￾and-set (TAS) lock L. Verifying linearizability of dfInc requires us to prove it has the same abstract behaviors as INC in Fig. 1(a), which increments the counter x atomically. Following previous work [21, 24, 31], one can extend a rely￾guarantee logic to verify linearizability. We use an assertion arem(C) to specify as an auxiliary state the abstract operation C to be fulfilled, and logically execute C at the linearization point (LP) of the concrete implementation. For dfInc, we prove a judgment in the form of R, G ` {P ∧ arem(INC)}dfInc{Q ∧ arem(skip)}. Here R and G specify the object’s actions (i.e., lock acquire and release, and the counter updates at both the concrete and the abstract sides) made by the environment and the current thread respectively. P and Q are relational assertions specifying the consistency relation between the program states at the concrete and the abstract sides. The postcondition arem(skip) shows that at the end of dfInc there is no abstract operation to fulfill. 2.2 Challenges of Progress Verification Progress properties of objects such as deadlock-freedom and starvation-freedom have various termination requirements of ob￾ject methods. They must be satisfied with interference from other threads considered, which makes the verification challenging. 386