Characterizing Progress Properties of Concurrent Objects via Contextual Refinements Hongjin Liang2,Jan Hoffmann2,Xinyu Feng',and Zhong Shao2 1 University of Science and Technology of China 2 Yale University Abstract.Implementations of concurrent objects should guarantee lin- earizability and a progress property such as wait-freedom,lock-freedom, obstruction-freedom,starvation-freedom,or deadlock-freedom.Conven- tional informal or semi-formal definitions of these progress properties describe conditions under which a method call is guaranteed to com- plete,but it is unclear how these definitions can be utilized to formally verify system software in a layered and modular way. In this paper,we propose a unified framework based on contextual refinements to show exactly how progress properties affect the behaviors of client programs.We give formal operational definitions of all common progress properties and prove that for linearizable objects,each progress property is equivalent to a specific type of contextual refinement that preserves termination.The equivalence ensures that verification of such a contextual refinement for a concurrent object guarantees both lineariz- ability and the corresponding progress property.Contextual refinement also enables us to verify safety and liveness properties of client programs at a high abstraction level by soundly replacing concrete method imple- mentations with abstract atomic operations. 1 Introduction A concurrent object consists of shared data and a set of methods that provide an interface for client threads to manipulate and access the shared data.The synchronization of simultaneous data access within the object affects the progress of the execution of the client threads in the system. Various progress properties have been proposed for concurrent objects.The most important ones are wait-freedom,lock-freedom and obstruction-freedom for non-blocking implementations,and starvation-freedom and deadlock-freedom for lock-based implementations.These properties describe conditions under which method calls are guaranteed to successfully complete in an execution.For exam- ple,lock-freedom guarantees that "infinitely often some method call finishes in a finite number of steps"9. Nevertheless,the common informal or semi-formal definitions of the progress properties are difficult to use in a modular and layered program verification be- cause they fail to describe how the progress properties affect clients.In a modular P.R.D'Argenio and H.Melgratti (Eds.):CONCUR 2013,LNCS 8052,Pp.227-241,2013. C Springer-Verlag Berlin Heidelberg 2013
Characterizing Progress Properties of Concurrent Objects via Contextual Refinements Hongjin Liang1,2, Jan Hoffmann2, Xinyu Feng1, and Zhong Shao2 1 University of Science and Technology of China 2 Yale University Abstract. Implementations of concurrent objects should guarantee linearizability and a progress property such as wait-freedom, lock-freedom, obstruction-freedom, starvation-freedom, or deadlock-freedom. Conventional informal or semi-formal definitions of these progress properties describe conditions under which a method call is guaranteed to complete, but it is unclear how these definitions can be utilized to formally verify system software in a layered and modular way. In this paper, we propose a unified framework based on contextual refinements to show exactly how progress properties affect the behaviors of client programs. We give formal operational definitions of all common progress properties and prove that for linearizable objects, each progress property is equivalent to a specific type of contextual refinement that preserves termination. The equivalence ensures that verification of such a contextual refinement for a concurrent object guarantees both linearizability and the corresponding progress property. Contextual refinement also enables us to verify safety and liveness properties of client programs at a high abstraction level by soundly replacing concrete method implementations with abstract atomic operations. 1 Introduction A concurrent object consists of shared data and a set of methods that provide an interface for client threads to manipulate and access the shared data. The synchronization of simultaneous data access within the object affects the progress of the execution of the client threads in the system. Various progress properties have been proposed for concurrent objects. The most important ones are wait-freedom, lock-freedom and obstruction-freedom for non-blocking implementations, and starvation-freedom and deadlock-freedom for lock-based implementations. These properties describe conditions under which method calls are guaranteed to successfully complete in an execution. For example, lock-freedom guarantees that “infinitely often some method call finishes in a finite number of steps” [9]. Nevertheless, the common informal or semi-formal definitions of the progress properties are difficult to use in a modular and layered program verification because they fail to describe how the progress properties affect clients. In a modular P.R. D’Argenio and H. Melgratti (Eds.): CONCUR 2013, LNCS 8052, pp. 227–241, 2013. c Springer-Verlag Berlin Heidelberg 2013
228 H.Liang et al. verification of client threads,the concrete implementation I7 of the object meth- ods should be replaced by an abstraction (or specification)IT that consists of equivalent atomic methods.The progress properties should then characterize whether and how the behaviors of a client program will be affected if a client uses I7 instead of IA.In particular,we are interested in systematically study- ing whether the termination of a client using the abstract methods I7A will be preserved when using an implementation II with some progress guarantee. Previous work on verifying the safety of concurrent objects(e.g.,[4,12])has shown that linearizability-a standard safety criterion for concurrent objects- and contextual refinement are equivalent.Informally,an implementation I7 is a contextual refinement of a (more abstract)implementation I7A,if every ob- servable behavior of any client program using II can also be observed when the client uses ITA instead.To obtain equivalence to linearizability,the observable behaviors include I/O events but not divergence (i.e.,non-termination).Re- cently,Gotsman and Yang [6]showed that a client program that diverges using a linearizable and lock-free object must also diverge when using the abstract operations instead.Their work reveals a connection between lock-freedom and a form of contextual refinement which preserves termination as well as safety properties.It is unclear how other progress guarantees affect termination of client programs and how they are related to contextual refinements. This paper studies all five commonly used progress properties and their rela- tionships to contextual refinements.We propose a unified framework in which a certain type of termination-sensitive contextual refinement is equivalent to linearizability together with one of the progress properties.The idea is to iden- tify different observable behaviors for different progress properties.For example, for the contextual refinement for lock-freedom we observe the divergence of the whole program,while for wait-freedom we also need to observe which threads in the program diverge.For lock-based progress properties,e.g.,starvation-freedom and deadlock-freedom,we have to take fair schedulers into account. Our paper makes the following new contributions: We formalize the definitions of the five most common progress properties: wait-freedom,lock-freedom,obstruction-freedom,starvation-freedom,and deadlock-freedom.Our formulation is based on possibly infinite event traces that are operationally generated by any client using the object. Based on our formalization,we prove relationships between the progress properties.For example,wait-freedom implies lock-freedom and starvation- freedom implies deadlock-freedom.These relationships form a lattice shown in Figure 1 (where the arrows represent implications).We close the lattice with a bottom element that we call sequential termination,a progress prop- erty in the sequential setting.It is weaker than any other progress property. We develop a unified framework to characterize progress properties via con- textual refinements.With linearizability,each progress property is proved equivalent to a contextual refinement which takes into account divergence of programs.A companion TR 14 contains the formal proofs of our results
228 H. Liang et al. verification of client threads, the concrete implementation Π of the object methods should be replaced by an abstraction (or specification) ΠA that consists of equivalent atomic methods. The progress properties should then characterize whether and how the behaviors of a client program will be affected if a client uses Π instead of ΠA. In particular, we are interested in systematically studying whether the termination of a client using the abstract methods ΠA will be preserved when using an implementation Π with some progress guarantee. Previous work on verifying the safety of concurrent objects (e.g., [4,12]) has shown that linearizability—a standard safety criterion for concurrent objects— and contextual refinement are equivalent. Informally, an implementation Π is a contextual refinement of a (more abstract) implementation ΠA, if every observable behavior of any client program using Π can also be observed when the client uses ΠA instead. To obtain equivalence to linearizability, the observable behaviors include I/O events but not divergence (i.e., non-termination). Recently, Gotsman and Yang [6] showed that a client program that diverges using a linearizable and lock-free object must also diverge when using the abstract operations instead. Their work reveals a connection between lock-freedom and a form of contextual refinement which preserves termination as well as safety properties. It is unclear how other progress guarantees affect termination of client programs and how they are related to contextual refinements. This paper studies all five commonly used progress properties and their relationships to contextual refinements. We propose a unified framework in which a certain type of termination-sensitive contextual refinement is equivalent to linearizability together with one of the progress properties. The idea is to identify different observable behaviors for different progress properties. For example, for the contextual refinement for lock-freedom we observe the divergence of the whole program, while for wait-freedom we also need to observe which threads in the program diverge. For lock-based progress properties, e.g., starvation-freedom and deadlock-freedom, we have to take fair schedulers into account. Our paper makes the following new contributions: – We formalize the definitions of the five most common progress properties: wait-freedom, lock-freedom, obstruction-freedom, starvation-freedom, and deadlock-freedom. Our formulation is based on possibly infinite event traces that are operationally generated by any client using the object. – Based on our formalization, we prove relationships between the progress properties. For example, wait-freedom implies lock-freedom and starvationfreedom implies deadlock-freedom. These relationships form a lattice shown in Figure 1 (where the arrows represent implications). We close the lattice with a bottom element that we call sequential termination, a progress property in the sequential setting. It is weaker than any other progress property. – We develop a unified framework to characterize progress properties via contextual refinements. With linearizability, each progress property is proved equivalent to a contextual refinement which takes into account divergence of programs. A companion TR [14] contains the formal proofs of our results
Characterizing Progress Properties via Contextual Refinements 229 Wait-freedom Lock-freedom Starvation-freedom w Obstruction-freedom Deadlock-freedom Sequential termination Fig.1.Relationships between Progress Properties By extending earlier equivalence results on linearizability [4],our contextual refinement framework can serve as a new alternative definition for the full cor- rectness properties of concurrent objects.The contextual refinement implied by linearizability and a progress guarantee precisely characterizes the properties at the abstract level that are preserved by the object implementation.When prov- ing these properties of a client of the object,we can soundly replace the concrete method implementations by its abstract operations.On the other hand,since the contextual refinement also implies linearizability and the progress property,we can potentially borrow ideas from existing proof methods for contextual refine- ments,such as simulations (e.g.,[13])and logical relations (e.g.,[2]),to verify linearizability and the progress guarantee together. In the remainder of this paper,we first informally explain our framework in Section 2.We then introduce the formal setting in Section 3;including the definition of linearizability as the safety criterion of objects.We formulate the progress properties in Section 4 and the contextual refinement framework in Section 5.We discuss related work and conclude in Section 6. 2 Informal Account In this section,we informally describe our results.We first give an overview of linearizability and its equivalence to the basic contextual refinement.Then we explain the progress properties and summarize our new equivalence results. Linearizability and Contextual Refinement.Linearizability is a standard safety criterion for concurrent objects 9.Intuitively,linearizability describes atomic behaviors of object implementations.It requires that each method call should appear to take effect instantaneously at some moment between its invo- cation and return. Linearizability intuitively establishes a correspondence between the object implementation II and the intended atomic operations I7A.This correspondence can also be understood as a contertual refinement.Informally,we say that II is a contextual refinement of IA,IIITA,if substituting II for ITA in any context (i.e.,in a client program)does not add observable behaviors.External observers cannot tell that I7A has been replaced by II from monitoring the behaviors of the client program
Characterizing Progress Properties via Contextual Refinements 229 Wait-freedom Lock-freedom Starvation-freedom Obstruction-freedom Deadlock-freedom Sequential termination Fig. 1. Relationships between Progress Properties By extending earlier equivalence results on linearizability [4], our contextual refinement framework can serve as a new alternative definition for the full correctness properties of concurrent objects. The contextual refinement implied by linearizability and a progress guarantee precisely characterizes the properties at the abstract level that are preserved by the object implementation. When proving these properties of a client of the object, we can soundly replace the concrete method implementations by its abstract operations. On the other hand, since the contextual refinement also implies linearizability and the progress property, we can potentially borrow ideas from existing proof methods for contextual refinements, such as simulations (e.g., [13]) and logical relations (e.g., [2]), to verify linearizability and the progress guarantee together. In the remainder of this paper, we first informally explain our framework in Section 2. We then introduce the formal setting in Section 3; including the definition of linearizability as the safety criterion of objects. We formulate the progress properties in Section 4 and the contextual refinement framework in Section 5. We discuss related work and conclude in Section 6. 2 Informal Account In this section, we informally describe our results. We first give an overview of linearizability and its equivalence to the basic contextual refinement. Then we explain the progress properties and summarize our new equivalence results. Linearizability and Contextual Refinement. Linearizability is a standard safety criterion for concurrent objects [9]. Intuitively, linearizability describes atomic behaviors of object implementations. It requires that each method call should appear to take effect instantaneously at some moment between its invocation and return. Linearizability intuitively establishes a correspondence between the object implementation Π and the intended atomic operations ΠA. This correspondence can also be understood as a contextual refinement. Informally, we say that Π is a contextual refinement of ΠA, Π ΠA, if substituting Π for ΠA in any context (i.e., in a client program) does not add observable behaviors. External observers cannot tell that ΠA has been replaced by Π from monitoring the behaviors of the client program.
230 H.Liang et al. It has been proved [4,12]that linearizability is equivalent to a contextual refine- ment in which the observable behaviors are finite traces of I/O events.Thus this basic contextual refinement can be used to distinguish linearizable objects from non-linearizable ones.But it cannot characterize progress properties of objects. Progress Properties.Figure 2 shows several implementations of a counter with different progress guarantees that we study in this paper.A counter object provides the two methods inc and dec for incrementing and decrementing a shared variable x.The implementations given here are not intended to be prac- tical but merely to demonstrate the meanings of the progress properties.We assume that every command is executed atomically. 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 num- ber of steps [7].Figure 2(a)shows an ideal wait-free implementation in which the increment and the decrement are done atomically.This implementation is obvi- ously 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 more complex and involve arrays and atomic snapshots [1]. Lock-freedom is similar to wait-freedom but only guarantees that some thread will complete an operation in a finite number of steps 7.Typical lock-free imple- mentations(such as the well-known Treiber stack,HSY elimination-backoff stack and Harris-Michael lock-free list)use the atomic compare-and-swap instruction cas in a loop to repeatedly attempt an update until it succeeds.Figure 2(b) shows such an implementation of the counter object.It is lock-free,because whenever inc and dec operations are executed concurrently,there always exists some successful update.Note that this object is not wait-free.For the following program(2.1),the cas instruction in the method called by the left thread may continuously fail due to the continuous updates of x made by the right thread. inc();while(true)inc(); (2.1) Herlihy et al.[8 propose obstruction-freedom which "guarantees progress for any thread that eventually executes in isolation"(i.e.,without other active threads in the system).They present two double-ended queues as examples.In Figure 2(c) we show an obstruction-free counter that may look contrived but nevertheless illustrates the idea of the progress property. The implementation introduces a variable i,and lets inc perform the atomic increment after increasing i to 10 and dec do the atomic decrement after decreas- ing i to 0.Whenever a method is executed in isolation (i.e.,without interference from other threads),it will complete.Thus the object is obstruction-free.It is not lock-free,because for the client inc(O;‖dec(O; (2.2) which executes an increment and a decrement concurrently,it is possible that neither of the method calls returns.For instance,under a specific schedule,every increment over i made by the left thread is immediately followed by a decrement from the right thread
230 H. Liang et al. It has been proved [4,12] that linearizability is equivalent to a contextual refinement in which the observable behaviors are finite traces of I/O events. Thus this basic contextual refinement can be used to distinguish linearizable objects from non-linearizable ones. But it cannot characterize progress properties of objects. Progress Properties. Figure 2 shows several implementations of a counter with different progress guarantees that we study in this paper. A counter object provides the two methods inc and dec for incrementing and decrementing a shared variable x. The implementations given here are not intended to be practical but merely to demonstrate the meanings of the progress properties. We assume that every command is executed atomically. 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 [7]. Figure 2(a) shows an ideal wait-free implementation in which the increment and the decrement are done atomically. This implementation 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 more complex and involve arrays and atomic snapshots [1]. Lock-freedom is similar to wait-freedom but only guarantees that some thread will complete an operation in a finite number of steps [7]. Typical lock-free implementations (such as the well-known Treiber stack, HSY elimination-backoff stack and Harris-Michael lock-free list) use the atomic compare-and-swap instruction cas in a loop to repeatedly attempt an update until it succeeds. Figure 2(b) shows such an implementation of the counter object. It is lock-free, because whenever inc and dec operations are executed concurrently, there always exists some successful update. Note that this object is not wait-free. For the following program (2.1), the cas instruction in the method called by the left thread may continuously fail due to the continuous updates of x made by the right thread. inc(); while(true) inc(); (2.1) Herlihy et al. [8] propose obstruction-freedom which “guarantees progress for any thread that eventually executes in isolation” (i.e., without other active threads in the system). They present two double-ended queues as examples. In Figure 2(c) we show an obstruction-free counter that may look contrived but nevertheless illustrates the idea of the progress property. The implementation introduces a variable i, and lets inc perform the atomic increment after increasing i to 10 and dec do the atomic decrement after decreasing i to 0. Whenever a method is executed in isolation (i.e., without interference from other threads), it will complete. Thus the object is obstruction-free. It is not lock-free, because for the client inc(); dec(); (2.2) which executes an increment and a decrement concurrently, it is possible that neither of the method calls returns. For instance, under a specific schedule, every increment over i made by the left thread is immediately followed by a decrement from the right thread.
Characterizing Progress Properties via Contextual Refinements 231 1 inc(){ 1inc(){ 1inc(){x:=x+1;J 2 while (i<10) 2 TestAndSet_lock(); 2dec(){x:=x-1;] 3 i:=1+1; x:=X+1; (a)Wait-Free (Ideal)Impl. 4 TestAndSet_unlock(); 5 x:=x+1; 51 1 inc(){ 61 2 (d)Deadlock-Free Impl. local t,b; 7 dec(){ 9 do{ 8 while (i>0){ 1 inc(){ t:=X; 9 1:=1-1; 2 Bakery_lock(); 6 b :cas(&x,t,t+1); 10 ] X:=X+1; 6 while(!b); 11 x:=x-1; Bakery_unlock(); 7} 123 5 (b)Lock-Free Impl. (c)Obstruction-Free Impl. (e)Starvation-Free Impl. Fig.2.Counter Objects with Methods inc and dec Wait-freedom,lock-freedom,and obstruction-freedom are progress properties for non-blocking implementations,where a delay of a thread cannot prevent other threads from making progress.In contrast,deadlock-freedom and starvation- freedom are progress properties for lock-based implementations.A delay of a thread holding a lock will block other threads which request the lock. Deadlock-freedom and starvation-freedom are often defined in terms of locks and critical sections.Deadlock-freedom guarantees that some thread will succeed in acquiring the lock,and starvation-freedom states that every thread attempting to acquire the lock will eventually succeed 9.For example,a test-and-set spin lock is deadlock-free but not starvation-free.In a concurrent access,some thread will successfully set the bit and get the lock,but there might be a thread that is continuously failing to get the lock.Lamport's bakery lock is starvation-free. It ensures that threads can acquire locks in the order of their requests. However,as noted by Herlihy and Shavit [10,the above definitions based on locks are unsatisfactory,because it is often difficult to identify a particular field in the object as a lock.Instead,they suggest defining them in terms of method calls.They also notice that the above definitions implicitly assume that every thread acquiring the lock will eventually release it.This assumption requires fair scheduling,i.e.,every thread gets eventually executed. Following Herlihy and Shavit [10,we say an object is deadlock-free,if in each fair execution there always exists some method call that can finish.As an example in Figure 2(d),we use a test-and-set lock to synchronize the incre- ments of the counter.Since some thread is guaranteed to acquire the test-and-set lock,the method call of that thread is guaranteed to finish.Thus the object is deadlock-free.Similarly,a starvation-free object guarantees that every method call can finish in fair executions.Figure 2(e)shows a counter implemented with Lamport's bakery lock.It is starvation-free since the bakery lock ensures that every thread can acquire the lock and hence every method call can eventually complete
Characterizing Progress Properties via Contextual Refinements 231 1 inc() { x := x + 1; } 2 dec() { x := x - 1; } (a) Wait-Free (Ideal) Impl. 1 inc() { 2 local t, b; 3 do { 4 t := x; 5 b := cas(&x,t,t+1); 6 } while(!b); 7 } (b) Lock-Free Impl. 1 inc() { 2 while (i < 10) { 3 i := i + 1; 4 } 5 x := x + 1; 6 } 7 dec() { 8 while (i > 0) { 9 i := i - 1; 10 } 11 x := x - 1; 12 } (c) Obstruction-Free Impl. 1 inc() { 2 TestAndSet_lock(); 3 x := x + 1; 4 TestAndSet_unlock(); 5 } (d) Deadlock-Free Impl. 1 inc() { 2 Bakery_lock(); 3 x := x + 1; 4 Bakery_unlock(); 5 } (e) Starvation-Free Impl. Fig. 2. Counter Objects with Methods inc and dec Wait-freedom, lock-freedom, and obstruction-freedom are progress properties for non-blocking implementations, where a delay of a thread cannot prevent other threads from making progress. In contrast, deadlock-freedom and starvationfreedom are progress properties for lock-based implementations. A delay of a thread holding a lock will block other threads which request the lock. Deadlock-freedom and starvation-freedom are often defined in terms of locks and critical sections. Deadlock-freedom guarantees that some thread will succeed in acquiring the lock, and starvation-freedom states that every thread attempting to acquire the lock will eventually succeed [9]. For example, a test-and-set spin lock is deadlock-free but not starvation-free. In a concurrent access, some thread will successfully set the bit and get the lock, but there might be a thread that is continuously failing to get the lock. Lamport’s bakery lock is starvation-free. It ensures that threads can acquire locks in the order of their requests. However, as noted by Herlihy and Shavit [10], the above definitions based on locks are unsatisfactory, because it is often difficult to identify a particular field in the object as a lock. Instead, they suggest defining them in terms of method calls. They also notice that the above definitions implicitly assume that every thread acquiring the lock will eventually release it. This assumption requires fair scheduling, i.e., every thread gets eventually executed. Following Herlihy and Shavit [10], we say an object is deadlock-free, if in each fair execution there always exists some method call that can finish. As an example in Figure 2(d), we use a test-and-set lock to synchronize the increments of the counter. Since some thread is guaranteed to acquire the test-and-set lock, the method call of that thread is guaranteed to finish. Thus the object is deadlock-free. Similarly, a starvation-free object guarantees that every method call can finish in fair executions. Figure 2(e) shows a counter implemented with Lamport’s bakery lock. It is starvation-free since the bakery lock ensures that every thread can acquire the lock and hence every method call can eventually complete