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 (i0){ 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 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
232 H.Liang et al. Table 1.Characterizing Progress Properties via Contextual Refinements IT ITA Wait-Free Lock-Free Obstruction-Free Deadlock-Free Starvation-Free A (t,Div.) Div. Div. Div. (t,Div.) (t,Div.) Div. Div.if Isolating Div.if Fair (t,Div.)if Fair Our Results.None of the above definitions of the five progress properties describes their guarantees regarding the behaviors of client code.In this paper, we define several contextual refinements to characterize the effects over client behaviors when the client uses objects with some progress properties.We show that linearizability together with a progress property is equivalent to a certain termination-sensitive contextual refinement.Table 1 summarizes our results. For each progress property,the new contextual refinement II IA is de- fined with respect to a divergence behavior and/or a specific scheduling at the implementation level (the third row in Table 1)and at the abstract side (the second row),in addition to the I/O events in the basic contextual refinement for linearizability. For wait-freedom,we need to observe the divergence of each individual thread t,represented by "(t,Div.)"in Table 1,at both the concrete and the abstract levels.We show that,if the thread t of a client program diverges when the client uses a linearizable and wait-free object 17,then thread t must also diverge when using ITA instead. The case for lock-freedom is similar,except that we now consider the diver- gence behaviors of the whole client program rather than individual threads (denoted by "Div."in Table 1).If a client diverges when using a linearizable and lock-free object I7,it must also diverge when it uses ITa instead. For obstruction-freedom,we consider the behaviors of isolating executions at the concrete side (denoted by "Div.if Isolating"in Table 1).In those executions,eventually only one thread is running.We show that,if a client diverges in an isolating execution when it uses a linearizable and obstruction- free object I7,it must also diverge in some abstract execution. For deadlock-freedom,we only care about fair executions at the concrete level(denoted by“Div.if Fair”in Table 1). -For starvation-freedom,we observe the divergence of each individual thread at both levels and restrict our considerations to fair executions for the con- crete side ("(t,Div.)if Fair"in Table 1).Any thread using II can diverge in a fair execution,only if it also diverges in some abstract execution. These new contextual refinements can characterize linearizable objects with progress properties.We will formalize the results and give examples in Section 5. 3 Formal Setting and Linearizability In this section,we formalize linearizability and show its equivalence to a contex- tual refinement that preserves safety properties only.This equivalence is the basis of our new results that relate progress properties and contextual refinements
232 H. Liang et al. Table 1. Characterizing Progress Properties via Contextual Refinements Π ΠA Wait-Free Lock-Free Obstruction-Free Deadlock-Free Starvation-Free ΠA (t, Div.) Div. Div. Div. (t, Div.) Π (t, Div.) Div. Div. if Isolating Div. if Fair (t, Div.) if Fair Our Results. None of the above definitions of the five progress properties describes their guarantees regarding the behaviors of client code. In this paper, we define several contextual refinements to characterize the effects over client behaviors when the client uses objects with some progress properties. We show that linearizability together with a progress property is equivalent to a certain termination-sensitive contextual refinement. Table 1 summarizes our results. For each progress property, the new contextual refinement Π ΠA is de- fined with respect to a divergence behavior and/or a specific scheduling at the implementation level (the third row in Table 1) and at the abstract side (the second row), in addition to the I/O events in the basic contextual refinement for linearizability. – For wait-freedom, we need to observe the divergence of each individual thread t, represented by “(t, Div.)” in Table 1, at both the concrete and the abstract levels. We show that, if the thread t of a client program diverges when the client uses a linearizable and wait-free object Π, then thread t must also diverge when using ΠA instead. – The case for lock-freedom is similar, except that we now consider the divergence behaviors of the whole client program rather than individual threads (denoted by “Div.” in Table 1). If a client diverges when using a linearizable and lock-free object Π, it must also diverge when it uses ΠA instead. – For obstruction-freedom, we consider the behaviors of isolating executions at the concrete side (denoted by “Div. if Isolating” in Table 1). In those executions, eventually only one thread is running. We show that, if a client diverges in an isolating execution when it uses a linearizable and obstructionfree object Π, it must also diverge in some abstract execution. – For deadlock-freedom, we only care about fair executions at the concrete level (denoted by “Div. if Fair” in Table 1). – For starvation-freedom, we observe the divergence of each individual thread at both levels and restrict our considerations to fair executions for the concrete side (“(t, Div.) if Fair” in Table 1). Any thread using Π can diverge in a fair execution, only if it also diverges in some abstract execution. These new contextual refinements can characterize linearizable objects with progress properties. We will formalize the results and give examples in Section 5. 3 Formal Setting and Linearizability In this section, we formalize linearizability and show its equivalence to a contextual refinement that preserves safety properties only. This equivalence is the basis of our new results that relate progress properties and contextual refinements.
Characterizing Progress Properties via Contextual Refinements 233 (Erpr)E ::=..(BErp)B ::=..(Instr)c ::print(E)... (Stmt)C ::skip c:=f(E)return E end (C)C;C if (B)C else C while (B){C] (Prog)W ::skip let II in Cll...C (ODecl)II::=f(1,C1),...,fn(n,Cn)} Fig.3.Syntax of the Programming Language (State）S=. (ThrdID)t∈Nat (Eut)e ::=(t,f,n)(t,ret,n)|(t,obj)(t,obj,abort) (t,out,n)(t,clt)(t,clt,abort)(t,term)(spawn,n) (ETrace)T ::=ee::T (co-inductive) Fig.4.States and Event Traces Language and Semantics.We use a similar language as in previous work of Liang and Feng [12.As shown in Figure 3,a program W consists of several client threads that run in parallel.Each thread could call the methods declared in the object I7.A method f is defined as a pair (C),where x is the formal argument and C is the method body.The object I7 could be either concrete with fine-grained code that we want to verify,or abstract (usually denoted as ITA in the following)that we consider as the specification.For the latter case, each method body should be an atomic operation of the form(C)and it should be always safe to execute it.For simplicity,we assume there is only one object in the program W and each method takes one argument only. Most commands are standard.Clients can use print(E)to produce observable external events.We do not allow the object's methods to produce external events. To simplify the semantics,we also assume there are no nested method calls.To discuss progress properties later,we introduce an auxiliary command end.It is a special marker that can be added at the end of a thread,but is not supposed to be used directly by programmers.The skip statement plays two roles here:a state- ment that has no computation effects or a flag to show the end of an execution. We use S for a program state.Program transitions (W,S)(W',S')gener- ate events e defined in Figure 4.A method invocation event(t,f,n)is produced when thread t executes z:=f(E),where n is the value of the argument E.A return(t,ret,n)is produced with the return value n.print(E)generates an out- put (t,out,n),and end generates a termination marker (t,term).Other steps generate either normal object actions (t,obj)(for steps inside method calls)or silent client actions (t,clt)(for client steps other than print(E)).For transi- tions leading to the error state abort (e.g.,invalid memory access),fault events are produced:(t,obj,abort)by the object method code and (t,clt,abort)by the client code.We also introduce an auxiliary event (spawn,n),saying that n threads are spawned.It will be useful later when defining fair scheduling(in Sec- tion 4).We write tid(e)for the thread ID in the event e.The predicate is_clt(e)
Characterizing Progress Properties via Contextual Refinements 233 (Expr) E ::= ... (BExp) B ::= ... (Instr) c ::= print(E) | ... (Stmt) C ::= skip | c | x := f(E) | return E | end | C | C; C | if (B) C else C | while (B){C} (Prog) W ::= skip | let Π in C ...C (ODecl) Π ::= {f1 ❀ (x1, C1),...,fn ❀ (xn, Cn)} Fig. 3. Syntax of the Programming Language (State) S ::= ... (ThrdID) t ∈ Nat (Evt) e ::= (t,f,n) | (t, ret, n) | (t, obj) | (t, obj, abort) | (t, out, n) | (t, clt) | (t, clt, abort) | (t, term) | (spawn, n) (ETrace) T ::= | e ::T (co-inductive) Fig. 4. States and Event Traces Language and Semantics. We use a similar language as in previous work of Liang and Feng [12]. As shown in Figure 3, a program W consists of several client threads that run in parallel. Each thread could call the methods declared in the object Π. A method f is defined as a pair (x, C), where x is the formal argument and C is the method body. The object Π could be either concrete with fine-grained code that we want to verify, or abstract (usually denoted as ΠA in the following) that we consider as the specification. For the latter case, each method body should be an atomic operation of the form C and it should be always safe to execute it. For simplicity, we assume there is only one object in the program W and each method takes one argument only. Most commands are standard. Clients can use print(E) to produce observable external events. We do not allow the object’s methods to produce external events. To simplify the semantics, we also assume there are no nested method calls. To discuss progress properties later, we introduce an auxiliary command end. It is a special marker that can be added at the end of a thread, but is not supposed to be used directly by programmers. The skip statement plays two roles here: a statement that has no computation effects or a flag to show the end of an execution. We use S for a program state. Program transitions (W, S) e −→ (W , S ) generate events e defined in Figure 4. A method invocation event (t,f,n) is produced when thread t executes x := f(E), where n is the value of the argument E. A return (t, ret, n) is produced with the return value n. print(E) generates an output (t, out, n), and end generates a termination marker (t, term). Other steps generate either normal object actions (t, obj) (for steps inside method calls) or silent client actions (t, clt) (for client steps other than print(E)). For transitions leading to the error state abort (e.g., invalid memory access), fault events are produced: (t, obj, abort) by the object method code and (t, clt, abort) by the client code. We also introduce an auxiliary event (spawn, n), saying that n threads are spawned. It will be useful later when defining fair scheduling (in Section 4). We write tid(e) for the thread ID in the event e. The predicate is clt(e)
234 H.Liang et al. TIW,S](T W,S'.(W,S)(W',S)v (W,S)abort} HIW,s]{get hist(T)I TE TIW,S]} OlW,S]get-obsv(T)I TE TIW,S]} Fig.5.Generation of Finite Event Traces states that the event e is either a silent client action,an output,or a client fault.We write is_inv(e)and is-ret(e)to denote that e is a method invocation and a return,respectively.The predicate is-abt(e)denotes a fault of the object or the client.Method invocations,returns and object faults are called history events,which will be used to define linearizability below.Outputs,client faults and object faults are called observable events. An event trace T is a finite or infinite sequence of events.We write T(i)for the i-th event of T.last(T)is the last event in a finite T.The trace T(1..i)is the sub-trace T(1),...,T(i)of T,and T is the length of T (IT]=w if T is infinite). The trace Tlt represents the sub-trace of T consisting of all events whose thread ID is t.We can use get-hist(T)to project T to the sub-trace consisting of all the history events,and get-obsv(T)for the sub-trace of all the observable events. Finite traces of history events are called histories. In Figure 5,we define TW,S]for the prefix-closed set of finite traces pro- duced by the executions of (W,S).We use (W,S)(W,S)for zero or multiple-step program transitions that generate the trace T.We also define HW,S]and OW,S]to get histories and finite observable traces produced by the executions of(W,S).The TR [14]contains more details about the language. Linearizability and Basic Contextual Refinement.We formulate lineariz- ability following its standard definition [11].Below we sketch the basic concepts. Detailed formal definitions can be found in the companion TR 14]. Linearizability is defined using histories.We say a return e2 matches an invo- cation e1,denoted as match(e1,e2),iff they have the same thread ID.An invo- cation is pending in T if no matching return follows it.We can use pend_inv(T) to get the set of pending invocations in T.We handle pending invocations in a history T in the standard way [11:we append zero or more return events to T,and drop the remaining pending invocations.The result is denoted by completions(T).It is a set of histories,and for each history in it,every invoca- tion has a matching return event. Definition 1 (Linearizable Histories).T Slin Tiff 1.Vt.Tt=Tt; 2.there erists a bijectionπ：{l,,lTl}→{1，，lT'}such that i.T()= T'(r()andi,j.i<jA is-ret(T(i)A is_inv(Ti)→π()<π(j) That is,T is linearizable w.r.t.T'if the latter is a permutation of the former, preserving the order of events in the same threads and the order of the non- overlapping method calls.Then an object is linearizable iff each of its concurrent histories after completions is linearizable w.r.t.some legal sequential history
234 H. Liang et al. T W, S def = {T | ∃W , S . (W, S) T −→∗ (W , S ) ∨ (W, S) T −→∗ abort} HW, S def = {get hist(T ) | T ∈ T W, S } OW, S def = {get obsv(T ) | T ∈ T W, S } Fig. 5. Generation of Finite Event Traces states that the event e is either a silent client action, an output, or a client fault. We write is inv(e) and is ret(e) to denote that e is a method invocation and a return, respectively. The predicate is abt(e) denotes a fault of the object or the client. Method invocations, returns and object faults are called history events, which will be used to define linearizability below. Outputs, client faults and object faults are called observable events. An event trace T is a finite or infinite sequence of events. We write T (i) for the i-th event of T . last(T ) is the last event in a finite T . The trace T (1..i) is the sub-trace T (1),...,T (i) of T , and |T | is the length of T (|T | = ω if T is infinite). The trace T |t represents the sub-trace of T consisting of all events whose thread ID is t. We can use get hist(T ) to project T to the sub-trace consisting of all the history events, and get obsv(T ) for the sub-trace of all the observable events. Finite traces of history events are called histories. In Figure 5, we define T W, S for the prefix-closed set of finite traces produced by the executions of (W, S). We use (W, S) T −→ ∗ (W , S ) for zero or multiple-step program transitions that generate the trace T . We also define HW, S and OW, S to get histories and finite observable traces produced by the executions of (W, S). The TR [14] contains more details about the language. Linearizability and Basic Contextual Refinement. We formulate linearizability following its standard definition [11]. Below we sketch the basic concepts. Detailed formal definitions can be found in the companion TR [14]. Linearizability is defined using histories. We say a return e2 matches an invocation e1, denoted as match(e1, e2), iff they have the same thread ID. An invocation is pending in T if no matching return follows it. We can use pend inv(T ) to get the set of pending invocations in T . We handle pending invocations in a history T in the standard way [11]: we append zero or more return events to T , and drop the remaining pending invocations. The result is denoted by completions(T ). It is a set of histories, and for each history in it, every invocation has a matching return event. Definition 1 (Linearizable Histories). T lin T iff 1. ∀t. T |t = T |t; 2. there exists a bijection π : {1,..., |T |} → {1,..., |T |} such that ∀i. T (i) = T (π(i)) and ∀i, j. i < j ∧ is ret(T (i)) ∧ is inv(T (j)) =⇒ π(i) < π(j). That is, T is linearizable w.r.t. T if the latter is a permutation of the former, preserving the order of events in the same threads and the order of the nonoverlapping method calls. Then an object is linearizable iff each of its concurrent histories after completions is linearizable w.r.t. some legal sequential history.
Characterizing Progress Properties via Contextual Refinements 235 We use ITA D(Sa,T)to mean that T'is a legal sequential history generated by any client using the specification I7 with an abstract initial state sa Definition 2 (Linearizability of Objects).The object's implementation IT is linearizable u.r.t.ⅡA under a refinement mapping p,denoted byⅡ≤eⅡA,if Vn,C1,...,Cn,S,Sa,T.TE HI(let I in Cill...IICn),S]A ((S)=Sa) =→3Tc,T'.Te∈completions(T)AⅡA>(Sa,T)A Te Zin T'. Here the partial mapping p:State-State relates concrete states to abstract ones. The side condition (S)=Sa in the above definition requires the initial concrete state S to be well-formed in that it represents a valid abstract state Sa.For instance,may need S to contain a linked list and relate it to an abstract mathematical set in Sa for a set object.Besides,o should always require the client states in S and Sa to be identical. Next we define a contextual refinement between the concrete object and its specification,which is equivalent to linearizability. Definition 3 (Basic Contextual Refinement).II IA iff Vn,C1,...,Cn,S,Sa.((S)=Sa) =→OI(letⅡinCl..‖Cn),S]cOI(letⅡin Cll..lCn),Sal Remember that OW,S]represents the prefix-closed set of observable event traces generated during the executions of(W,S),which is defined in Figure 5. Following Filipovic et al.[4],we can prove that linearizability is equivalent to this contextual refinement.We give the proofs in the TR [14]. Theorem4(Basic Equivalence).Ⅱ≤eⅡA→ⅡSeⅡA: Theorem 4 allows us to use I IA to identify linearizable objects.However, we cannot use it to characterize progress properties of objects.For the following example,ITEIA holds although no concrete method call of f could finish(we assume this object contains a method f only). Ⅱ(f):hile(true)skip;ⅡA(f):skip; C:print(1);f();print(1); The reason is that II ITA considers a prefir-closed set of event traces at the abstract side.For the above client C,the observable behaviors of let I7 in C can all be found in the prefix-closed set of behaviors produced by let IA in C. 4 Formalizing Progress Properties We define progress in Figure 6 as properties over both event traces T and object implementations I7.We say an object implementation II has a progress property P iff all its event traces have the property.Here we use T to generate the event traces.Its definition in Figure 6 is similar to TIW,S]of Figure 5,but TlW,S] is for the set of finite or infinite event traces produced by complete executions. We use (W,S).to denote the existence of a T-labelled infinite execution. (W,S)T(skip,)represents a terminating execution that produces T.By using W,we append end at the end of each thread to explicitly mark the
Characterizing Progress Properties via Contextual Refinements 235 We use ΠA (Sa, T ) to mean that T is a legal sequential history generated by any client using the specification ΠA with an abstract initial state Sa. Definition 2 (Linearizability of Objects). The object’s implementation Π is linearizable w.r.t. ΠA under a refinement mapping ϕ, denoted by Π ϕ ΠA, iff ∀n, C1,...,Cn, S, Sa,T. T ∈ H(let Π in C1 ...Cn), S ∧ (ϕ(S) = Sa) =⇒ ∃Tc, T . Tc ∈ completions(T ) ∧ ΠA (Sa, T ) ∧ Tc lin T . Here the partial mapping ϕ:StateState relates concrete states to abstract ones. The side condition ϕ(S) = Sa in the above definition requires the initial concrete state S to be well-formed in that it represents a valid abstract state Sa. For instance, ϕ may need S to contain a linked list and relate it to an abstract mathematical set in Sa for a set object. Besides, ϕ should always require the client states in S and Sa to be identical. Next we define a contextual refinement between the concrete object and its specification, which is equivalent to linearizability. Definition 3 (Basic Contextual Refinement). Π ϕ ΠA iff ∀n, C1,...,Cn, S, Sa. (ϕ(S) = Sa) =⇒ O(let Π in C1 ...Cn), S ⊆ O(let ΠA in C1 ...Cn), Sa . Remember that OW, S represents the prefix-closed set of observable event traces generated during the executions of (W, S), which is defined in Figure 5. Following Filipovi´c et al. [4], we can prove that linearizability is equivalent to this contextual refinement. We give the proofs in the TR [14]. Theorem 4 (Basic Equivalence). Π ϕ ΠA ⇐⇒ Π ϕ ΠA. Theorem 4 allows us to use Π ϕ ΠA to identify linearizable objects. However, we cannot use it to characterize progress properties of objects. For the following example, Π ϕ ΠA holds although no concrete method call of f could finish (we assume this object contains a method f only). Π(f) : while(true) skip; ΠA(f) : skip; C : print(1); f(); print(1); The reason is that Π ϕ ΠA considers a prefix-closed set of event traces at the abstract side. For the above client C, the observable behaviors of let Π in C can all be found in the prefix-closed set of behaviors produced by let ΠA in C. 4 Formalizing Progress Properties We define progress in Figure 6 as properties over both event traces T and object implementations Π. We say an object implementation Π has a progress property P iff all its event traces have the property. Here we use Tω to generate the event traces. Its definition in Figure 6 is similar to T W, S of Figure 5, but TωW, S is for the set of finite or infinite event traces produced by complete executions. We use (W, S) T −→ω · to denote the existence of a T -labelled infinite execution. (W, S) T −→ ∗ (skip, ) represents a terminating execution that produces T . By using W , we append end at the end of each thread to explicitly mark the
236 H.Liang et al. Definition.An object I7 satisfies P under a refinement mapping P(IT),iff n,Ci.,Cn,S,T.T∈TI(letⅡinCl.llCn),S]A(S∈dom(p)=→P(T). T.IW,S]{(spawn,IW):T (（w,s)“.V(w],S)工*(skip,-)V(wJ,S)T*abort} Llet II in Cill...Cn let II in (Ci;end)ll...l(Cn;end) llet II in Ci ll...Il C n tnum((spawn,n)::T)n pend_inv(T)eli.e=T(i)A is_inv(e)A3j.(j>imatch(e,T(j)))} prog-t(T)iff Vi,e.eE pend_jnv(T(1..i))=j.j>iA match(e,T(j)) prog-s(T)i证i,e.e∈pend_inv(T(1.i)=→3j.j>iAis-ret(T)】 abt(T)iff 3i.is_abt(T(i)) sched(T)证lTl=w A pend_inv(T)≠0=→3e.e∈pend_inv(T)AI(Tltid())川=w fair(T)i证lT|=w=→t∈[1.tnum(T)小.l(Tl)川=w V last(Tl)=(t,term) iso(T)iff T=w=→3t,i.(付i.j≥i=→tid(T)=t) wait-free iff sched prog-t V abt starvation-free iff fair=prog-t V abt lock-free iff sched prog-s V abt deadlock-free iff fair prog-s V abt obstruction-free iff sched A iso=prog-t V abt Fig.6.Formalizing Progress Properties lock-free wait-free V prog-s starvation-free←→wait-free V-fair obstruction-free←→lock-free V-iso deadlock-free lock-free V-fair Fig.7.Relationships between Progress Properties termination of the thread.We also insert the spawning event(spawn,n)at the beginning of T,where n is the number of threads in W.Then we can use tnum(T) to get the number n,which is needed to define fairness,as shown below. Before formulating each progress property over event traces,we first define some auxiliary properties in Figure 6.prog-t(T)guarantees that every method call in T eventually finishes.prog-s(T)guarantees that some pending method call finishes.Different from prog-t,the return event T(j)in prog-s does not have to be a matching return of the pending invocation e.abt(T)says that T ends with a fault event. There are three useful conditions on scheduling.The basic requirement for a good schedule is sched.If T is infinite and there exist pending calls,then at least one pending thread should be scheduled infinitely often.In fact,there are two possible reasons causing a method call of thread t to pend.Either t is no longer scheduled,or it is always scheduled but the method call never finishes.sched rules out the bad schedule where no thread with an invoked method is active. For instance,the following infinite trace does not satisfy sched
236 H. Liang et al. Definition. An object Π satisfies P under a refinement mapping ϕ, Pϕ(Π), iff ∀n, C1,. . . ,Cn, S,T. T ∈ Tω(let Π in C1...Cn), S ∧ (S ∈dom(ϕ)) =⇒ P(T ). TωW, S def = {(spawn, |W|)::T | (W, S) T −→ω · ∨ (W, S) T −→∗(skip, ) ∨ (W, S) T −→∗abort} let Π in C1 ...Cn def = let Π in (C1; end)...(Cn; end) |let Π in C1 ... Cn| def = n tnum((spawn, n)::T ) def = n pend inv(T ) def = {e | ∃i. e=T (i) ∧ is inv(e) ∧ ¬∃j. (j>i ∧ match(e, T (j)))} prog-t(T ) iff ∀i, e. e ∈ pend inv(T (1..i)) =⇒ ∃j. j > i ∧ match(e, T (j)) prog-s(T ) iff ∀i, e. e ∈ pend inv(T (1..i)) =⇒ ∃j. j > i ∧ is ret(T (j)) abt(T ) iff ∃i. is abt(T (i)) sched(T ) iff |T | = ω ∧ pend inv(T ) = ∅ =⇒ ∃e. e ∈ pend inv(T ) ∧ |(T |tid(e))| = ω fair(T ) iff |T | = ω =⇒ ∀t ∈ [1..tnum(T )]. |(T |t)| = ω ∨ last(T |t)=(t, term) iso(T ) iff |T | = ω =⇒ ∃t, i. (∀j. j ≥ i =⇒ tid(T (j)) = t) wait-free iff sched =⇒ prog-t ∨ abt starvation-free iff fair =⇒ prog-t ∨ abt lock-free iff sched =⇒ prog-s ∨ abt deadlock-free iff fair =⇒ prog-s ∨ abt obstruction-free iff sched ∧ iso =⇒ prog-t ∨ abt Fig. 6. Formalizing Progress Properties lock-free ⇐⇒ wait-free ∨ prog-s starvation-free ⇐⇒ wait-free ∨ ¬fair obstruction-free ⇐⇒ lock-free ∨ ¬iso deadlock-free ⇐⇒ lock-free ∨ ¬fair Fig. 7. Relationships between Progress Properties termination of the thread. We also insert the spawning event (spawn, n) at the beginning of T , where n is the number of threads in W. Then we can use tnum(T ) to get the number n, which is needed to define fairness, as shown below. Before formulating each progress property over event traces, we first define some auxiliary properties in Figure 6. prog-t(T ) guarantees that every method call in T eventually finishes. prog-s(T ) guarantees that some pending method call finishes. Different from prog-t, the return event T (j) in prog-s does not have to be a matching return of the pending invocation e. abt(T ) says that T ends with a fault event. There are three useful conditions on scheduling. The basic requirement for a good schedule is sched. If T is infinite and there exist pending calls, then at least one pending thread should be scheduled infinitely often. In fact, there are two possible reasons causing a method call of thread t to pend. Either t is no longer scheduled, or it is always scheduled but the method call never finishes. sched rules out the bad schedule where no thread with an invoked method is active. For instance, the following infinite trace does not satisfy sched.