Progress of Concurrent Objects with Partial Methods（Extended Version）

Progress of Concurrent Objects with Partial Methods (Extended Version) HONGJIN LIANG and XINYU FENG*,Nanjing University,China and University of Science and Technology of China,China Various progress properties have been proposed for concurrent objects,such as wait-freedom,lock-freedom, starvation-freedom and deadlock-freedom.However,none of them applies to concurrent objects with partial methods,Le.,methods that are supposed not to return under certain circumstances.A typical example is the lock_acquire method,which must not return when the lock has already been acquired. In this paper we propose two new progress properties,partial starvation-freedom(PSF)and partial deadlock- freedom(PDF),for concurrent objects with partial methods.We also design four patterns to write abstract specifications for PSF or PDF objects under strongly or weakly fair scheduling,so that these objects contextually refine the abstract specifications.Our Abstraction Theorem shows the equivalence between PSF(or PDF)and the progress-aware contextual refinement.Finally,we generalize the program logic LiLi to have a new logic to verify the PSF(or PDF)property and linearizability of concurrent objects. CCS Concepts:.Theory of computation-Hoare logic;Program specifications;Program verifica- tion:Abstraction; Additional Key Words and Phrases:Concurrent Objects,Progress,Refinement,Partial Methods ACM Reference Format: Hongjin Liang and Xinyu Feng.2018.Progress of Concurrent Objects with Partial Methods(Extended Version). 1,1 (January 2018),149 pages.https://doi.org/10.1145/nnnnnnn.nnnnnnn INTRODUCTION A concurrent object consists of shared data and a set of methods which provide an interface for client threads to access the shared data.Linearizability [Herlihy and Wing 1990]has been used as a standard definition of the correctness of concurrent object implementations.It describes safety and functionality,but has no requirement about termination of object methods.Various progress properties,such as wait-freedom,lock-freedom,starvation-freedom and deadlock-freedom,have been proposed to specify termination of object methods.In their textbook Herlihy and Shavit [2008] give a systematic introduction of these properties. Recent work [Filipovic et al.2009]has shown the equivalence between linearizability and a contextual refinement.The result has been further extended [Gotsman and Yang 2011;Liang and Feng 2016;Liang et al.2013]to show that,when progress properties are taken into account,one may have the corresponding progress-aware contextual refinement to reestablish the equivalence. The equivalence results allow us to build abstractions for linearizable objects so that safety and progress of the client code can be reasoned about at a more abstract level. However,none of these progress-related results applies to concurrent objects with partial meth- ods!A method is partial if it is supposed not to return under certain circumstances.A typical example is the lock_acquire method,which must not return when the lock has already been acquired.Concurrent objects with partial methods simply do not satisfy any of the aforementioned Corresponding author. Authors'address:Hongjin Liang.hongjin@nju.edu.cn;Xinyu Feng,xyfeng@nju.edu.cn,State Key Laboratory for Novel Software Technology,Nanjing University,163 Xianlin Road,Nanjing.210023,China,University of Science and Technology of China,443 Huangshan Road,Hefei,230000,China. 2018.XXXX-XXXX/2018/1-ART$15.00 https://doi.org/10.1145/nnnnnnn.nnnnnnn Vol.1.No.1,Article.Publication date:January 2018

Progress of Concurrent Objects with Partial Methods (Extended Version) HONGJIN LIANG and XINYU FENG∗ , Nanjing University, China and University of Science and Technology of China, China Various progress properties have been proposed for concurrent objects, such as wait-freedom, lock-freedom, starvation-freedom and deadlock-freedom. However, none of them applies to concurrent objects with partial methods, i.e., methods that are supposed not to return under certain circumstances. A typical example is the lock_acquire method, which must not return when the lock has already been acquired. In this paper we propose two new progress properties, partial starvation-freedom (PSF) and partial deadlock￾freedom (PDF), for concurrent objects with partial methods. We also design four patterns to write abstract specifications for PSF or PDF objects under strongly or weakly fair scheduling, so that these objects contextually refine the abstract specifications. Our Abstraction Theorem shows the equivalence between PSF (or PDF) and the progress-aware contextual refinement. Finally, we generalize the program logic LiLi to have a new logic to verify the PSF (or PDF) property and linearizability of concurrent objects. CCS Concepts: • Theory of computation → Hoare logic; Program specifications; Program verifica￾tion; Abstraction; Additional Key Words and Phrases: Concurrent Objects, Progress, Refinement, Partial Methods ACM Reference Format: Hongjin Liang and Xinyu Feng. 2018. Progress of Concurrent Objects with Partial Methods (Extended Version). 1, 1 (January 2018), 149 pages. https://doi.org/10.1145/nnnnnnn.nnnnnnn 1 INTRODUCTION A concurrent object consists of shared data and a set of methods which provide an interface for client threads to access the shared data. Linearizability [Herlihy and Wing 1990] has been used as a standard definition of the correctness of concurrent object implementations. It describes safety and functionality, but has no requirement about termination of object methods. Various progress properties, such as wait-freedom, lock-freedom, starvation-freedom and deadlock-freedom, have been proposed to specify termination of object methods. In their textbook Herlihy and Shavit [2008] give a systematic introduction of these properties. Recent work [Filipović et al. 2009] has shown the equivalence between linearizability and a contextual refinement. The result has been further extended [Gotsman and Yang 2011; Liang and Feng 2016; Liang et al. 2013] to show that, when progress properties are taken into account, one may have the corresponding progress-aware contextual refinement to reestablish the equivalence. The equivalence results allow us to build abstractions for linearizable objects so that safety and progress of the client code can be reasoned about at a more abstract level. However, none of these progress-related results applies to concurrent objects with partial meth￾ods! A method is partial if it is supposed not to return under certain circumstances. A typical example is the lock_acquire method, which must not return when the lock has already been acquired. Concurrent objects with partial methods simply do not satisfy any of the aforementioned ∗Corresponding author. Authors’ address: Hongjin Liang, hongjin@nju.edu.cn; Xinyu Feng, xyfeng@nju.edu.cn, State Key Laboratory for Novel Software Technology, Nanjing University, 163 Xianlin Road, Nanjing, 210023, China , University of Science and Technology of China, 443 Huangshan Road, Hefei, 230000, China. 2018. XXXX-XXXX/2018/1-ART $15.00 https://doi.org/10.1145/nnnnnnn.nnnnnnn , Vol. 1, No. 1, Article . Publication date: January 2018

2 Hongjin Liang and Xinyu Feng progress properties,and people do not know how to give progress-aware abstract specifications for them either.The existing studies on progress properties and progress-aware 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. We face the following key challenges to address these problems. We need definitions of new progress properties for these objects,and the definitions need to describe the situations in which permanent blocking is allowed.It is important to note that, although deadlock-freedom and starvation-freedom have been used as progress properties for "blocking"algorithms [Herlihy and Shavit 2008],they allow permanent blocking only when the scheduling is unfair.They can specify concurrent objects implemented using locks, but they do not apply to lock objects themselves.For objects like locks,blocking may also be caused by inappropriate method invocations by the client.For instance,if a thread of the client fails to call lock_release after acquiring the lock,the calls to lock_acquire by other threads will be always blocked.Similarly,for a stack object with a partial pop method,if no client threads call push,the calls to pop will be permanently blocked at an empty stack.The question is,how to distinguish the blocking behaviors caused by"bad"clients with those caused by bad object implementations,and blame the objects only for the blocking in the latter case. The abstractions for objects with partial methods should be able to distinguish the objects with different progress guarantees under different scheduling conditions.A natural abstrac- tion for partial methods is the blocking primitive await(B)(C).It is blocked if B does not hold,and executes C atomically if B holds(in this case,we say the code await(B)(C)is enabled).A specification in the form of await(B)(C)can characterize both the atomicity of the functionality and the fact that the method is partial.However,it is not sufficient to serve as a progress-aware abstraction for the following two reasons. Different implementations of the same await block may exhibit different progress prop- erties,requiring different abstractions.For instance,the ticket lock algorithm [Mellor- Crummey and Scott 1991]has stronger progress guarantees than the test-and-set lock algorithm [Herlihy and Shavit 2008].Therefore when progress is concerned it is impossible to use the same partial specification (e.g.,await(1=0){1 cid),where cid is the ID of the current thread)as an abstraction for the lock_acquire methods in both algorithms (even though it may work for both if we consider linearizability only). Even the same implementation may require different abstractions for different scheduling. The blocking primitive await(B)(C)behaves differently under strongly fair and weakly fair scheduling.The former ensures the execution of the primitive as long as it is enabled a sufficient number of times,but the latter requires the primitive to be always enabled to ensure its execution.On the other hand,the distinction between strong and weak fairness is meaningful only if there are blocking primitives.A low-level program consisting of non-blocking primitive instructions only(like most machine instructions)behaves the same .Vol.1,No.1,Article.Publication date:January 2018

:2 Hongjin Liang and Xinyu Feng progress properties, and people do not know how to give progress-aware abstract specifications for them either. The existing studies on progress properties and progress-aware 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. We face the following key challenges to address these problems. • We need definitions of new progress properties for these objects, and the definitions need to describe the situations in which permanent blocking is allowed. It is important to note that, although deadlock-freedom and starvation-freedom have been used as progress properties for “blocking” algorithms [Herlihy and Shavit 2008], they allow permanent blocking only when the scheduling is unfair. They can specify concurrent objects implemented using locks, but they do not apply to lock objects themselves. For objects like locks, blocking may also be caused by inappropriate method invocations by the client. For instance, if a thread of the client fails to call lock_release after acquiring the lock, the calls to lock_acquire by other threads will be always blocked. Similarly, for a stack object with a partial pop method, if no client threads call push, the calls to pop will be permanently blocked at an empty stack. The question is, how to distinguish the blocking behaviors caused by “bad” clients with those caused by bad object implementations, and blame the objects only for the blocking in the latter case. • The abstractions for objects with partial methods should be able to distinguish the objects with different progress guarantees under different scheduling conditions. A natural abstrac￾tion for partial methods is the blocking primitive await(B){C}. It is blocked if B does not hold, and executes C atomically if B holds (in this case, we say the code await(B){C} is enabled). A specification in the form of await(B){C} can characterize both the atomicity of the functionality and the fact that the method is partial. However, it is not sufficient to serve as a progress-aware abstraction for the following two reasons. − Different implementations of the same await block may exhibit different progress prop￾erties, requiring different abstractions. For instance, the ticket lock algorithm [Mellor￾Crummey and Scott 1991] has stronger progress guarantees than the test-and-set lock algorithm [Herlihy and Shavit 2008]. Therefore when progress is concerned it is impossible to use the same partial specification (e.g., await(l=0){l := cid}, where cid is the ID of the current thread) as an abstraction for the lock_acquire methods in both algorithms (even though it may work for both if we consider linearizability only). − Even the same implementation may require different abstractions for different scheduling. The blocking primitive await(B){C} behaves differently under strongly fair and weakly fair scheduling. The former ensures the execution of the primitive as long as it is enabled a sufficient number of times, but the latter requires the primitive to be always enabled to ensure its execution. On the other hand, the distinction between strong and weak fairness is meaningful only if there are blocking primitives. A low-level program consisting of non-blocking primitive instructions only (like most machine instructions) behaves the same , Vol. 1, No. 1, Article . Publication date: January 2018

Progress of Concurrent Objects with Partial Methods(Extended Version) 3 under both scheduling.Such a program cannot have the same abstraction with blocking primitives under different scheduling. As a result,if we consider m kinds of progress properties(e.g.,to distinguish ticket locks and test-and-set locks)and the 2 choices of strongly fair and weakly fair scheduling,we may need as many as 2 x m kinds of abstractions for the same functionality.Can we find general patterns for these abstractions? In this paper,we specify and verify progress of concurrent objects with partial methods.We define progress properties and abstraction patterns under strongly and weakly fair scheduling.Then we prove that given a linearizable object implementation II,the contextual refinement between II and its abstraction II'under a certain kind of fair scheduling is equivalent to the progress property of II.We also provide a program logic to verify the contextual refinement between II and II',which ensures linearizability and the progress property of II. Our work is based on earlier work on abstraction for concurrent objects and concurrency verification,but makes the following new contributions: We propose progress properties,partial starvation-freedom(PSF)and partial deadlock-freedom (PDF),for concurrent objects with partial methods.They identify the execution scenarios in which the partial methods are blocked due to inappropriate invocation sequences made by "bad"clients,and allow the object methods to be blocked permanently in these special scenarios.Ticket locks and test-and-set locks satisfy PSF and PDF respectively.Traditional starvation-freedom and deadlock-freedom for objects with total methods can be viewed as specializations of PSF and PDF respectively,if we view total methods as special cases of partial ones that are always enabled to return. We design four general patterns for abstractions for concurrent objects with PSF and PDF progress properties under strongly and weakly fair scheduling,respectively.We start with the basic blocking primitive await(B)(C)and define syntactic wrappers that transform it into non-atomic object specifications which can be refined by the object implementations in the progress-aware contextual refinement.We give distinguished wrappers for different combinations of fairness and progress properties. We prove the equivalence between PSF(or PDF)and the progress-aware contextual refine- ment,where the abstraction is generated by the wrapper,under strong or weak fairness.The equivalence results(called the abstraction theorem)allow us to verify safety and liveness properties of client programs at a high abstraction level,by replacing concrete object imple- mentations with the specifications.Using the natural transitivity of the contextual refinement, it is also possible to verify linearizability and PSF(or PDF)of nested concurrent objects. We design a program logic to verify objects with PSF or PDF progress properties.Our logic is a generalization of the LiLi logic for starvation-free and deadlock-free objects [Liang and Feng 2016].It also provides inference rules for the await(B)(C)statement under strong and weak fairness,so that await commands can also be used in object implementations.The soundness of our logic ensures the progress-aware contextual refinement,and linearizability and PSF(or PDF)under different fairness.We have applied the program logic to verify ticket locks [Mellor-Crummey and Scott 1991],test-and-set locks [Herlihy and Shavit 2008], bounded partial queues with two locks [Herlihy and Shavit 2008]and Treiber stacks [Treiber 1986]with possibly blocking pop methods In the rest of this paper,we first give an informal overview of the background and our key ideas in Sec.2.Then we introduce the object language in Sec.3,and linearizability and the basic contextual refinement in Sec.4.We propose our new progress properties in Sec.5,and give the progress-aware contextual refinement and the abstraction theorem in Sec.6.We present the logic Vol.1.No.1,Article.Publication date:January 2018

Progress of Concurrent Objects with Partial Methods (Extended Version) :3 under both scheduling. Such a program cannot have the same abstraction with blocking primitives under different scheduling. As a result, if we consider m kinds of progress properties (e.g., to distinguish ticket locks and test-and-set locks) and the 2 choices of strongly fair and weakly fair scheduling, we may need as many as 2 × m kinds of abstractions for the same functionality. Can we find general patterns for these abstractions? In this paper, we specify and verify progress of concurrent objects with partial methods. We define progress properties and abstraction patterns under strongly and weakly fair scheduling. Then we prove that given a linearizable object implementation Π, the contextual refinement between Π and its abstraction Π ′ under a certain kind of fair scheduling is equivalent to the progress property of Π. We also provide a program logic to verify the contextual refinement between Π and Π ′ , which ensures linearizability and the progress property of Π. Our work is based on earlier work on abstraction for concurrent objects and concurrency verification, but makes the following new contributions: • We propose progress properties, partial starvation-freedom (PSF) and partial deadlock-freedom (PDF), for concurrent objects with partial methods. They identify the execution scenarios in which the partial methods are blocked due to inappropriate invocation sequences made by “bad” clients, and allow the object methods to be blocked permanently in these special scenarios. Ticket locks and test-and-set locks satisfy PSF and PDF respectively. Traditional starvation-freedom and deadlock-freedom for objects with total methods can be viewed as specializations of PSF and PDF respectively, if we view total methods as special cases of partial ones that are always enabled to return. • We design four general patterns for abstractions for concurrent objects with PSF and PDF progress properties under strongly and weakly fair scheduling, respectively. We start with the basic blocking primitive await(B){C} and define syntactic wrappers that transform it into non-atomic object specifications which can be refined by the object implementations in the progress-aware contextual refinement. We give distinguished wrappers for different combinations of fairness and progress properties. • We prove the equivalence between PSF (or PDF) and the progress-aware contextual refine￾ment, where the abstraction is generated by the wrapper, under strong or weak fairness. The equivalence results (called the abstraction theorem) allow us to verify safety and liveness properties of client programs at a high abstraction level, by replacing concrete object imple￾mentations with the specifications. Using the natural transitivity of the contextual refinement, it is also possible to verify linearizability and PSF (or PDF) of nested concurrent objects. • We design a program logic to verify objects with PSF or PDF progress properties. Our logic is a generalization of the LiLi logic for starvation-free and deadlock-free objects [Liang and Feng 2016]. It also provides inference rules for the await(B){C} statement under strong and weak fairness, so that await commands can also be used in object implementations. The soundness of our logic ensures the progress-aware contextual refinement, and linearizability and PSF (or PDF) under different fairness. We have applied the program logic to verify ticket locks [Mellor-Crummey and Scott 1991], test-and-set locks [Herlihy and Shavit 2008], bounded partial queues with two locks [Herlihy and Shavit 2008] and Treiber stacks [Treiber 1986] with possibly blocking pop methods. In the rest of this paper, we first give an informal overview of the background and our key ideas in Sec. 2. Then we introduce the object language in Sec. 3, and linearizability and the basic contextual refinement in Sec. 4. We propose our new progress properties in Sec. 5, and give the progress-aware contextual refinement and the abstraction theorem in Sec. 6. We present the logic , Vol. 1, No. 1, Article . Publication date: January 2018

Hongjin Liang and Xinyu Feng L_initialize(){1 :=0; tkL_initialize(){owner =0;next :=0; L_acq(){ tkL_acq({ 1 local b :false; 1 local i,o; 2 while(!b){b :cas(&1,0,cid); 2 i:=getAndInc(&next); 3 o :owner;while(i!=o){o :owner; } L_rel(){ 31:=0; tkL_rel(){ 4 owner :owner +1; (a)test-and-set lock implementation (c)ticket lock implementation inc(){L_acq();x:=x+1;L_rel(); inc_tkL(){tkL_acq();x:=x+1;tkL_rel(); (b)counter with a test-and-set lock (d)counter with a ticket lock INC()[x:=x+1;} (e)atomic spec.INC Fig.1.Counters with locks. in Sec.7 and show the examples we have verified in Sec.8.Finally,we discuss related work and conclude in Sec.9. 2 BACKGROUND AND OVERVIEW OF KEY IDEAS Below we first give an overview of linearizability,starvation-freedom,deadlock-freedom and contextual refinement.Then we analyze the problems in defining progress of concurrent objects with partial methods,and explain our solutions informally. 2.1 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. 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.1(b)and(d).We assume that every primitive command is executed 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 Fig.1(e),so they are linearizable. The locks themselves could also be viewed as standalone objects.For instance,the test-and-set lock object in Fig.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 number.The counter's implementation code in Fig.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 Vol.1,No.1,Article.Publication date:January 2018

:4 Hongjin Liang and Xinyu Feng L_initialize(){ l := 0; } L_acq(){ 1 local b := false; 2 while(!b){ b := cas(&l, 0, cid); } } L_rel(){ 3 l := 0; } (a) test-and-set lock implementation inc(){ L_acq(); x:=x+1; L_rel(); } (b) counter with a test-and-set lock tkL_initialize(){ owner := 0; next := 0; } tkL_acq(){ 1 local i, o; 2 i := getAndInc(&next); 3 o := owner; while(i!=o){ o := owner; } } tkL_rel(){ 4 owner := owner + 1; } (c) ticket lock implementation inc_tkL(){ tkL_acq(); x:=x+1; tkL_rel(); } (d) counter with a ticket lock INC(){x:=x+1;} (e) atomic spec. INC Fig. 1. Counters with locks. in Sec. 7 and show the examples we have verified in Sec. 8. Finally, we discuss related work and conclude in Sec. 9. 2 BACKGROUND AND OVERVIEW OF KEY IDEAS Below we first give an overview of linearizability, starvation-freedom, deadlock-freedom and contextual refinement. Then we analyze the problems in defining progress of concurrent objects with partial methods, and explain our solutions informally. 2.1 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. 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. 1(b) and (d). We assume that every primitive command is executed 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 Fig. 1(e), so they are linearizable. The locks themselves could also be viewed as standalone objects. For instance, the test-and-set lock object in Fig. 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 number. The counter’s implementation code in Fig. 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 , Vol. 1, No. 1, Article . Publication date: January 2018

Progress of Concurrent Objects with Partial Methods(Extended Version) 心 produce the same effects as the atomic operations L_ACQ and L_REL(defined below),respectively: L_ACQ(){1 :cid; L_REL()[1:=0;J (2.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; 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 two implementations of the counter in Fig.1(b)and (d)satisfy deadlock-freedom and starvation-freedom respectively. We use the definitions given by Herlihy and Shavit [2011].Both deadlock-freedom and starvation- freedom assume fair scheduling,i.e.,every thread gets eventually executed.For the counters in Fig.1(b)and(d),fairness ensures that every thread holding the lock will eventually release the lock. Deadlock-freedom requires "minimal progress"in fair executions,i.e,there always exists some method call which can finish under fair scheduling,while starvation-freedom requires"maximal progress"in fair executions,i.e.,every method call should eventually finish under fair scheduling. The counter in Fig.1(b)is deadlock-free,because the test-and-set lock(see Fig.1(a))guarantees that eventually some thread will succeed in getting the lock via the cas instruction at line 2,and hence the method call of inc in that thread will eventually finish.It is not starvation-free,because there might be a thread that continuously fails to acquire the lock.For the following client program (2.2),the cas instruction executed by the left thread could always fail if the right thread infinitely often acquires the lock. inc();print(1);II while(true)inc(); (2.2) The counter in Fig.1(d)implemented with a ticket lock is starvation-free.Figure 1(c)shows the details of the ticket lock implementation.It uses two shared variables owner and next,which are equal initially.The threads attempting to acquire the lock form a waiting queue.In tkL_acq,a thread first atomically increments next and reads its old value to a local variable i (line 2).It waits until the lock's owner equals its ticket number i (line 3),then it acquires the lock.In tkL_rel, the thread releases the lock by incrementing owner(line 4).Then the next waiting thread(the thread with ticket number i+1,if there is one)can acquire the lock.We can see that the ticket lock implementation ensures the first-come-first-served property,and hence every thread calling inc_tkL can eventually acquire the lock and finish its method call. Deadlock-freedom and starvation-freedom are progress properties for the so-called "blocking implementations"[Herlihy and Shavit 2008],such as the counters in Fig.1(b)and(d),where a thread holding a lock will block other threads requesting the lock.However,they do not apply to lock objects,e.g.,the ones in Fig.1(a)and (c).We will explain the problems in detail in Sec.2.2 Contextual refinement and the abstraction theorem.It is difficult to use linearizability and progress properties directly in modular verification of client programs of an object,because their definitions fail to describe how the client behaviors are affected.To verify clients,we would like to abstract away the details of the object implementation.This requires a notion of object correctness,telling us that the client behaviors will not change when we replace the object methods'implementations with the corresponding abstract operations(as specifications). Contextual refinement gives the desired notion of correctness.Informally,an object implemen- tation II is a contextual refinement of a(more abstract)implementation II',if every observable Vol.1.No.1,Article.Publication date:January 2018

Progress of Concurrent Objects with Partial Methods (Extended Version) :5 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) 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; } 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 two implementations of the counter in Fig. 1(b) and (d) satisfy deadlock-freedom and starvation-freedom respectively. We use the definitions given by Herlihy and Shavit [2011]. Both deadlock-freedom and starvation￾freedom assume fair scheduling, i.e., every thread gets eventually executed. For the counters in Fig. 1(b) and (d), fairness ensures that every thread holding the lock will eventually release the lock. Deadlock-freedom requires “minimal progress” in fair executions, i.e., there always exists some method call which can finish under fair scheduling, while starvation-freedom requires “maximal progress” in fair executions, i.e., every method call should eventually finish under fair scheduling. The counter in Fig. 1(b) is deadlock-free, because the test-and-set lock (see Fig. 1(a)) guarantees that eventually some thread will succeed in getting the lock via the cas instruction at line 2, and hence the method call of inc in that thread will eventually finish. It is not starvation-free, because there might be a thread that continuously fails to acquire the lock. For the following client program (2.2), the cas instruction executed by the left thread could always fail if the right thread infinitely often acquires the lock. inc(); print(1); || while(true) inc(); (2.2) The counter in Fig. 1(d) implemented with a ticket lock is starvation-free. Figure 1(c) shows the details of the ticket lock implementation. It uses two shared variables owner and next, which are equal initially. The threads attempting to acquire the lock form a waiting queue. In tkL_acq, a thread first atomically increments next and reads its old value to a local variable i (line 2). It waits until the lock’s owner equals its ticket number i (line 3), then it acquires the lock. In tkL_rel, the thread releases the lock by incrementing owner (line 4). Then the next waiting thread (the thread with ticket number i+1, if there is one) can acquire the lock. We can see that the ticket lock implementation ensures the first-come-first-served property, and hence every thread calling inc_tkL can eventually acquire the lock and finish its method call. Deadlock-freedom and starvation-freedom are progress properties for the so-called “blocking implementations” [Herlihy and Shavit 2008], such as the counters in Fig. 1(b) and (d), where a thread holding a lock will block other threads requesting the lock. However, they do not apply to lock objects, e.g., the ones in Fig. 1(a) and (c). We will explain the problems in detail in Sec. 2.2. Contextual refinement and the abstraction theorem. It is difficult to use linearizability and progress properties directly in modular verification of client programs of an object, because their definitions fail to describe how the client behaviors are affected. To verify clients, we would like to abstract away the details of the object implementation. This requires a notion of object correctness, telling us that the client behaviors will not change when we replace the object methods’ implementations with the corresponding abstract operations (as specifications). Contextual refinement gives the desired notion of correctness. Informally, an object implemen￾tation Π is a contextual refinement of a (more abstract) implementation Π ′ , if every observable , Vol. 1, No. 1, Article . Publication date: January 2018