1.2. Overview 289 contextual refinements have been limited to concurrent objects with total specifications. As an awkward consequence,we cannot treat lock implementations as objects when we study progress of concurrent objects.Instead,we have to treat lock_acquire and lock_release as internal functions of other lock-based objects.Also,without a proper progress-aware abstraction for locks,we have to redo the verification of lock_acquire and lock_release when they are used in different contexts (Liang and Feng,2016),which makes the verification process complex and painful.Note that locks are not the only objects with partial methods. Concurrent sets,stacks and queues may also have methods that intend to block.For instance,it may be sensible for a thread attempting to pop from an empty stack to block,waiting until another thread pushes an item.The reasoning about these objects suffers from the same problems too when progress is concerned. In this tutorial,we specify and verify progress of concurrent objects with partial methods.We define partial starvation-freedom(PSF)and partial deadlock-freedom(PDF)as progress properties for objects with partial methods,and design abstraction patterns under strongly and weakly fair scheduling.We prove that given a linearizable object imple- mentation II with partial methods,the contextual refinement between II and its abstraction II'under a certain kind of fair scheduling is equivalent to PSF/PDF of II.We also extend the program logic LiLi to support partial specifications and to reason about blocking primitives. It verifies the contextual refinement between II and II',which ensures linearizability and the progress property of II. 1.2 Overview The goal of this tutorial is to help the reader understand the various progress properties of concurrent objects. We start with an informal overview of the background in Section 2. We informally describe the traditional four progress properties(wait- freedom,lock-freedom,starvation-freedom and deadlock-freedom), and analyze the challenges in supporting objects with partial methods
1.2. Overview 289 contextual refinements have been limited to concurrent objects with total specifications. As an awkward consequence, we cannot treat lock implementations as objects when we study progress of concurrent objects. Instead, we have to treat lock_acquire and lock_release as internal functions of other lock-based objects. Also, without a proper progress-aware abstraction for locks, we have to redo the verification of lock_acquire and lock_release when they are used in different contexts (Liang and Feng, 2016), which makes the verification process complex and painful. Note that locks are not the only objects with partial methods. Concurrent sets, stacks and queues may also have methods that intend to block. For instance, it may be sensible for a thread attempting to pop from an empty stack to block, waiting until another thread pushes an item. The reasoning about these objects suffers from the same problems too when progress is concerned. In this tutorial, we specify and verify progress of concurrent objects with partial methods. We define partial starvation-freedom (PSF) and partial deadlock-freedom (PDF) as progress properties for objects with partial methods, and design abstraction patterns under strongly and weakly fair scheduling. We prove that given a linearizable object implementation Π with partial methods, the contextual refinement between Π and its abstraction Π0 under a certain kind of fair scheduling is equivalent to PSF/PDF of Π. We also extend the program logic LiLi to support partial specifications and to reason about blocking primitives. It verifies the contextual refinement between Π and Π0 , which ensures linearizability and the progress property of Π. 1.2 Overview The goal of this tutorial is to help the reader understand the various progress properties of concurrent objects. We start with an informal overview of the background in Section 2. We informally describe the traditional four progress properties (waitfreedom, lock-freedom, starvation-freedom and deadlock-freedom), and analyze the challenges in supporting objects with partial methods
290 Introduction In Section 3,we introduce the basic technical settings.We define a simple object language,and the generation of execution traces from the operational semantics.We also define fairness of scheduling over the traces. In Section 4,we define linearizability and the basic contextual refinement which is equivalent to linearizability. In Section 5,we formulate the four traditional progress properties and the two new progress properties for objects with partial methods. In Section 6,we give the progress-aware contextual refinement and the abstraction theorems. In Section 7,we present the program logic LiLi and show the examples we have verified. Finally,we discuss related work in Section 8 and conclude in Section 9
290 Introduction In Section 3, we introduce the basic technical settings. We define a simple object language, and the generation of execution traces from the operational semantics. We also define fairness of scheduling over the traces. In Section 4, we define linearizability and the basic contextual refinement which is equivalent to linearizability. In Section 5, we formulate the four traditional progress properties and the two new progress properties for objects with partial methods. In Section 6, we give the progress-aware contextual refinement and the abstraction theorems. In Section 7, we present the program logic LiLi and show the examples we have verified. Finally, we discuss related work in Section 8 and conclude in Section 9
2 Background A concurrent object usually satisfies linearizability,a standard safety cri- terion,and certain progress property,describing when and how method calls of the object are guaranteed to terminate. In this section,we first give an overview of linearizability.We then introduce the four traditional progress properties (wait-freedom,lock- freedom,starvation-freedom and deadlock-freedom),and explain the need for new progress properties.We also discuss the contextual refine- ment and the Abstraction Theorems.Finally we introduce rely-guarantee reasoning,explain how to encode linearizability verification and discuss the challenges in progress verification. 2.1 Linearizability A concurrent object is linearizable,if each method call appears to take effect instantaneously at some moment between its invocation and return (Herlihy and Wing,1990).Intuitively,linearizability requires the implementation of each method to have the same effect as an atomic specification. Consider the two implementations of the counter object in Fig- ure 2.1(b)and(d).We assume that every primitive command is executed 291
2 Background A concurrent object usually satisfies linearizability, a standard safety criterion, and certain progress property, describing when and how method calls of the object are guaranteed to terminate. In this section, we first give an overview of linearizability. We then introduce the four traditional progress properties (wait-freedom, lockfreedom, starvation-freedom and deadlock-freedom), and explain the need for new progress properties. We also discuss the contextual refinement and the Abstraction Theorems. Finally we introduce rely-guarantee reasoning, explain how to encode linearizability verification and discuss the challenges in progress verification. 2.1 Linearizability A concurrent object is linearizable, if each method call appears to take effect instantaneously at some moment between its invocation and return (Herlihy and Wing, 1990). Intuitively, linearizability requires the implementation of each method to have the same effect as an atomic specification. Consider the two implementations of the counter object in Figure 2.1(b) and (d). We assume that every primitive command is executed 291
292 Background 0 L_initialize(){1 :=0; 1 L_acq(){ 2 local b :false; 3 while(!b){ 4 b :cas(&l,0,cid); 5 6} 10 inc(){ 11 L_acq(); 7Lre1(){ 12 X:=x+1; 81:=0; 13 L_rel(); 9} 14} (a)test-and-set (TAS)lock impl. (b)counter with a TAS lock 15 tkL_initialize(){ 16 owner :=0;next :=0; 17 tkL_acq(){ 28 inc_tkL(){ 18 local i,o; 29 tkL_acq(); 19 i:=getAndInc(&next); 30 x:=x+1; 20 o :owner; 31 tkL_rel(); 21 while(i！=o)[ 32} 22 o :owner; 23 (d)counter with a ticket lock 24} 25 tkL_rel(){ 26 owner :owner +1; 27J INC(){x:=x+1;} (c)ticket lock implementation (e)atomic spec.INC Figure 2.1:Counters with locks. atomically.A counter provides a method inc for incrementing the shared data x.Both implementations use locks to synchronize the increments. Intuitively they have the same effect as the atomic specification INC() in Figure 2.1(e),so they are linearizable
292 Background 0 L_initialize(){ l := 0; } 1 L_acq(){ 2 local b := false; 3 while(!b){ 4 b := cas(&l, 0, cid); 5 } 6 } 7 L_rel(){ 8 l := 0; 9 } (a) test-and-set (TAS) lock impl. 10 inc(){ 11 L_acq(); 12 x:=x+1; 13 L_rel(); 14 } (b) counter with a TAS lock 15 tkL_initialize(){ 16 owner := 0; next := 0; } 17 tkL_acq(){ 18 local i, o; 19 i := getAndInc(&next); 20 o := owner; 21 while(i!=o){ 22 o := owner; 23 } 24 } 25 tkL_rel(){ 26 owner := owner + 1; 27 } (c) ticket lock implementation 28 inc_tkL(){ 29 tkL_acq(); 30 x:=x+1; 31 tkL_rel(); 32 } (d) counter with a ticket lock INC(){ x:=x+1; } (e) atomic spec. INC Figure 2.1: Counters with locks. atomically. A counter provides a method inc for incrementing the shared data x. Both implementations use locks to synchronize the increments. Intuitively they have the same effect as the atomic specification INC() in Figure 2.1(e), so they are linearizable
2.2.Progress Properties 293 The locks themselves could also be viewed as standalone objects. For instance,the test-and-set lock object in Figure 2.1(a)provides the methods L_acq and L_rel for a thread to acquire and release the lock 1. Here cid represents the current thread's ID,which is a positive integer. The counter's implementation code in Figure 2.1(b)can be viewed as a client of this lock object.The lock object is linearizable,because L_acq and L rel both update 1 atomically (if they indeed return).They produce the same effects as the atomic operations L_ACQ and L REL (defined below),respectively: L_ACQ(){1 :cid; LREL()[1:=0;} (2.1.1) However,linearizability does not characterize progress properties of the object implementations.For instance,the following counter object is still linearizable,even if its method never terminates. inc'(){L_acq();x:=x+1;L_rel();while(true)skip; 2.2 Progress Properties Various progress properties have been proposed for concurrent objects, such as wait-freedom and lock-freedom for non-blocking implemen- tations,and starvation-freedom and deadlock-freedom for lock-based implementations.These properties describe conditions under which a method call is guaranteed to successfully finish in an execution.The implementation of the counter in Figure 1.1(a)satisfy lock-freedom.The two implementations in Figure 2.1(b)and(d)satisfy deadlock-freedom and starvation-freedom respectively.We assume that every command is executed atomically. We use the definitions given by Herlihy and Shavit (2011).Infor- mally,an object implementation is wait-free,if it guarantees that every thread can complete any started operation of the data structure in a finite number of steps.We can view that the atomic specification in Figure 2.1(e)is an ideal wait-free implementation in which the incre- ment is done atomically.It is obviously wait-free since it guarantees termination of every method call regardless of interference from other threads.Note that realistic implementations of wait-free counters are
2.2. Progress Properties 293 The locks themselves could also be viewed as standalone objects. For instance, the test-and-set lock object in Figure 2.1(a) provides the methods L_acq and L_rel for a thread to acquire and release the lock l. Here cid represents the current thread’s ID, which is a positive integer. The counter’s implementation code in Figure 2.1(b) can be viewed as a client of this lock object. The lock object is linearizable, because L_acq and L_rel both update l atomically (if they indeed return). They produce the same effects as the atomic operations L_ACQ and L_REL (defined below), respectively: L_ACQ(){ l := cid; } L_REL(){ l := 0; } (2.1.1) However, linearizability does not characterize progress properties of the object implementations. For instance, the following counter object is still linearizable, even if its method never terminates. inc’(){ L_acq(); x:=x+1; L_rel(); while(true) skip; } 2.2 Progress Properties Various progress properties have been proposed for concurrent objects, such as wait-freedom and lock-freedom for non-blocking implementations, and starvation-freedom and deadlock-freedom for lock-based implementations. These properties describe conditions under which a method call is guaranteed to successfully finish in an execution. The implementation of the counter in Figure 1.1(a) satisfy lock-freedom. The two implementations in Figure 2.1(b) and (d) satisfy deadlock-freedom and starvation-freedom respectively. We assume that every command is executed atomically. We use the definitions given by Herlihy and Shavit (2011). Informally, an object implementation is wait-free, if it guarantees that every thread can complete any started operation of the data structure in a finite number of steps. We can view that the atomic specification in Figure 2.1(e) is an ideal wait-free implementation in which the increment is done atomically. It is obviously wait-free since it guarantees termination of every method call regardless of interference from other threads. Note that realistic implementations of wait-free counters are