Progress of Concurrent Objects with Partial Methods 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,ie.,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.Proc.ACM Program. 20 Lang.2,POPL,Article 20 (January 2018),31 pages.https://doi.org/10.1145/3158108 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 [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. "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 Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page.Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted.To copy otherwise,or republish,to post on servers or to redistribute to lists,requires prior specific permission and/or a fee.Request permissions from permissions@acm.org. 2018 Association for Computing Machinery. 2475-1421/2018/1-ART20 https:/doi.org/10.1145/3158108 Proceedings of the ACM on Programming Languages,Vol.2,No.POPL,Article 20.Publication date:January 2018
20 Progress of Concurrent Objects with Partial Methods 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 deadlockfreedom (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 verification; 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. Proc. ACM Program. Lang. 2, POPL, Article 20 (January 2018), 31 pages. https://doi.org/10.1145/3158108 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. ∗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. Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from permissions@acm.org. © 2018 Association for Computing Machinery. 2475-1421/2018/1-ART20 https://doi.org/10.1145/3158108 Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 20. Publication date: January 2018
20:2 Hongjin Liang and Xinyu Feng 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 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 Proceedings of the ACM on Programming Languages,Vol.2,No.POPL,Article 20.Publication date:January 2018
20:2 Hongjin Liang and Xinyu Feng However, none of these progress-related results applies to concurrent objects with partial methods! 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 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 abstraction 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 properties, requiring different abstractions. For instance, the ticket lock algorithm [MellorCrummey 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 Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 20. Publication date: January 2018
Progress of Concurrent Objects with Partial Methods 20:3 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 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. Proceedings of the ACM on Programming Languages,Vol.2,No.POPL,Article 20.Publication date:January 2018
Progress of Concurrent Objects with Partial Methods 20:3 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 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 refinement, 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 implementations 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. Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 20. Publication date: January 2018
20:4 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 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 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 Proceedings of the ACM on Programming Languages,Vol.2,No.POPL,Article 20.Publication date:January 2018
20: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 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 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 Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 20. Publication date: January 2018
Progress of Concurrent Objects with Partial Methods 205 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 produce the same effects as the atomic operations L_ACQ and L_REL(defined below),respectively: L_ACQ(){1 cid; L_REL(){1 :=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);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). Proceedings of the ACM on Programming Languages,Vol.2,No.POPL,Article 20.Publication date:January 2018
Progress of Concurrent Objects with Partial Methods 20:5 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 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 starvationfreedom 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). Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 20. Publication date: January 2018
20:6 Hongjin Liang and Xinyu Feng 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 behavior of any client program using II can also be observed when the client uses II'instead.Then, when verifying a client of II,we can soundly replace II with its abstraction II'. There has been much work(e.g.,[Filipovic et al.2009;Gotsman and Yang 2012;Liang et al.2013]) studying abstraction theorems,which relate linearizability and progress properties with contextual refinements.It has been proved that linearizability of II is equivalent to a contextual refinement between II and its atomic specification I,where the observable behaviors are finite traces of I/O events.When taking progress properties into account,the corresponding contextual refinement should be sensitive to termination or divergence(non-termination).For instance,deadlock-freedom or starvation-freedom of linearizable objects is shown equivalent to a contextual refinement which observes(possibly infinite)full traces of I/O events in fair executions.Then,a client which diverges with II in a fair execution must also have a diverging execution when using the abstraction II' Deadlock-free and starvation-free objects could be distinguished by different abstractions.The abstraction for starvation-free objects is the atomic specification I,while for deadlock-free ones the abstraction has to be non-atomic [Liang and Feng 2016]. The counter implementation inc_tkL()in Fig.1(d)is a progress-aware contextual refinement of the atomic counter INC in Fig.1(e),but inc()in Fig.1(b)is not.To see the difference,consider the client program(2.2).Under fair scheduling,the client calling inc()may generate an empty I/O event trace because it may not print out 1.However,the empty trace cannot be generated when replacing inc()with inc_tkL()or INC(),because the resulting program must print out 1. 2.2 Problems and Our Solutions The existing progress properties and the corresponding contextual refinement are proposed for concurrent objects with total methods only,i.e.,methods that should always return when executed sequentially.They do not apply to objects with partial methods,such as the lock objects in Fig.1(a) and(c),which intend to block at certain situations.We have outlined the key challenges in rea- soning about progress properties of objects with partial methods in Sec.1.We give more detailed explanations here. 2.2.1 Atomic Specifications Need to Be Partial.The specifications defined in (2.1)can characterize the atomic behaviors of lock objects,but they fail to specify that L_ACQ should be partial in the sense that it should be blocked when the lock is unavailable. To address the problem,we introduce the atomic partial specification I,where each method specification is in the form of await(B)(C).For the lock objects,we can define the atomic partial specification I as follows. L_ACQ'(){await (1=0){1 :cid } L_REL(){1:=0;) (2.3) The await block naturally specifies the atomicity of method functionality,just like the traditional atomic specification(C)(which can be viewed as syntactic sugar for await(true)(C)),therefore r may serve as a specification for linearizable objects.It also shows the fact that the object method is partial,with explicit specification of the enabling condition B.Below we use the atomic partial specification as the starting point to characterize the progress of objects. 2.2.2 Deadlock-Freedom and Starvation-Freedom Do Not Apply.We need new progress properties for objects with partial methods.Consider the following client program(2.4)using the test-and-set lock in Fig.1(a).One of the method calls never finishes. L_acq();II L_acq(); (2.4) Proceedings of the ACM on Programming Languages,Vol.2,No.POPL,Article 20.Publication date:January 2018
20:6 Hongjin Liang and Xinyu Feng Contextual refinement gives the desired notion of correctness. Informally, an object implementation Π is a contextual refinement of a (more abstract) implementation Π ′ , if every observable behavior of any client program using Π can also be observed when the client uses Π ′ instead. Then, when verifying a client of Π, we can soundly replace Π with its abstraction Π ′ . There has been much work (e.g., [Filipović et al. 2009; Gotsman and Yang 2012; Liang et al. 2013]) studying abstraction theorems, which relate linearizability and progress properties with contextual refinements. It has been proved that linearizability of Π is equivalent to a contextual refinement between Π and its atomic specification Γ, where the observable behaviors are finite traces of I/O events. When taking progress properties into account, the corresponding contextual refinement should be sensitive to termination or divergence (non-termination). For instance, deadlock-freedom or starvation-freedom of linearizable objects is shown equivalent to a contextual refinement which observes (possibly infinite) full traces of I/O events in fair executions. Then, a client which diverges with Π in a fair execution must also have a diverging execution when using the abstraction Π ′ . Deadlock-free and starvation-free objects could be distinguished by different abstractions. The abstraction for starvation-free objects is the atomic specification Γ, while for deadlock-free ones the abstraction has to be non-atomic [Liang and Feng 2016]. The counter implementation inc_tkL() in Fig. 1(d) is a progress-aware contextual refinement of the atomic counter INC in Fig. 1(e), but inc() in Fig. 1(b) is not. To see the difference, consider the client program (2.2). Under fair scheduling, the client calling inc() may generate an empty I/O event trace because it may not print out 1. However, the empty trace cannot be generated when replacing inc() with inc_tkL() or INC(), because the resulting program must print out 1. 2.2 Problems and Our Solutions The existing progress properties and the corresponding contextual refinement are proposed for concurrent objects with total methods only, i.e., methods that should always return when executed sequentially. They do not apply to objects with partial methods, such as the lock objects in Fig. 1(a) and (c), which intend to block at certain situations. We have outlined the key challenges in reasoning about progress properties of objects with partial methods in Sec. 1. We give more detailed explanations here. 2.2.1 Atomic Specifications Need to Be Partial. The specifications defined in (2.1) can characterize the atomic behaviors of lock objects, but they fail to specify that L_ACQ should be partial in the sense that it should be blocked when the lock is unavailable. To address the problem, we introduce the atomic partial specification Γ, where each method specification is in the form of await(B){C}. For the lock objects, we can define the atomic partial specification Γ as follows. L_ACQ'(){ await (l = 0) { l := cid }; } L_REL(){ l := 0; } (2.3) The await block naturally specifies the atomicity of method functionality, just like the traditional atomic specification ⟨C⟩ (which can be viewed as syntactic sugar for await(true){C}), therefore Γ may serve as a specification for linearizable objects. It also shows the fact that the object method is partial, with explicit specification of the enabling condition B. Below we use the atomic partial specification as the starting point to characterize the progress of objects. 2.2.2 Deadlock-Freedom and Starvation-Freedom Do Not Apply. We need new progress properties for objects with partial methods. Consider the following client program (2.4) using the test-and-set lock in Fig. 1(a). One of the method calls never finishes. L_acq(); || L_acq(); (2.4) Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 20. Publication date: January 2018
Progress of Concurrent Objects with Partial Methods 20:7 Table 1.Client(2.5)with different locks."Yes"means it must print out 1."No"otherwise. spec.(2.3)ticket locks(Fig.1(c)) test-and-set locks(Fig.1(a)) Strong Fairness Yes Yes No Weak Fairness No Yes No It shows that the test-and-set lock object does not satisfy the traditional deadlock-freedom or starvation-freedom property we just presented.Neither does the ticket lock object in Fig.1(c). The problem is that L_acq intends to block when the lock is not available.The non-termination in the above example(2.4)is just the intention of a correct lock implementation;otherwise the lock cannot guarantee mutual exclusion. Our solution.We define two new progress properties for objects with partial methods,which we call partial starvation-freedom (PSF)and partial deadlock-freedom (PDF).PSF requires that in each fair execution trace by any client with the object II,either each method invocation eventually returns (as required in starvation-freedom),or each pending method invocation must be continuously disabled.The latter case intuitively says that this non-termination is caused by the "bad"client,e.g., by inappropriate invocations of the methods.Similarly,PDF requires that in each fair execution trace by any client with the object II,either there always exists a method invocation that eventually returns(as in deadlock-freedom),or each pending method invocation must be continuously disabled. But how do we formally say that a method is disabled?When we informally say this,we actually refer to the enabling condition B in await(B)(C)in the object's atomic partial specification I. However,we may not be able to infer such a condition from the concrete implementation II. To address this problem,our definitions of PSFr(II)and PDFr(II)are parameterized with the specification I(the actual definitions take more parameters,as shown in Sec.5). We can prove the lock objects in Fig.1(a)and (c)satisfy PDF and PSF respectively.We can also show that starvation-freedom and deadlock-freedom are special cases of our PSF and PDF respectively,by instantiating the parameter I with specifications in the form of await(true)(C). 2.2.3 Atomic Partial Specifications Are Insufficient for Progress-Aware Abstractions.Although the atomic partial specification I describes the atomic functionality and the enabling condition of each method,it is insufficient to serve as a progress-aware abstraction for the following reasons. First,the progress of the await command itself is affected by the fairness of scheduling,such as strong fairness and weak fairness. Strong fairness:Every thread which is infinitely often enabled will execute infinitely often. Then,await(B)(C)is not executed only if B is continuously false after some point in the execution trace. Weak fairness:Every thread which is eventually always enabled will execute infinitely often. Then,await(B){C)may not be executed when B is infinitely often false.This fairness notion is weaker than strong fairness. As a result,the choice of fair scheduling will affect the behaviors of a program or a specification with await commands.To see this,we consider the following client program(2.5). [_lace;[_]REL;print(1);II while(true){[_lace;[_]REL; (2.5) where [lace and []REL represent holes to be filled with method calls of lock acquire and release, respectively.Table 1 shows the behaviors of the client with different locks.If the client calls the abstract specifications in(2.3),it must execute print(1)under strongly fair scheduling,but may not do so under weakly fair scheduling.This is because the call of L_ACQ'could be infinitely Proceedings of the ACM on Programming Languages,Vol.2,No.POPL,Article 20.Publication date:January 2018
Progress of Concurrent Objects with Partial Methods 20:7 Table 1. Client (2.5) with different locks. “Yes” means it must print out 1, “No” otherwise. spec. (2.3) ticket locks (Fig. 1(c)) test-and-set locks (Fig. 1(a)) Strong Fairness Yes Yes No Weak Fairness No Yes No It shows that the test-and-set lock object does not satisfy the traditional deadlock-freedom or starvation-freedom property we just presented. Neither does the ticket lock object in Fig. 1(c). The problem is that L_acq intends to block when the lock is not available. The non-termination in the above example (2.4) is just the intention of a correct lock implementation; otherwise the lock cannot guarantee mutual exclusion. Our solution. We define two new progress properties for objects with partial methods, which we call partial starvation-freedom (PSF) and partial deadlock-freedom (PDF). PSF requires that in each fair execution trace by any client with the object Π, either each method invocation eventually returns (as required in starvation-freedom), or each pending method invocation must be continuously disabled. The latter case intuitively says that this non-termination is caused by the “bad” client, e.g., by inappropriate invocations of the methods. Similarly, PDF requires that in each fair execution trace by any client with the object Π, either there always exists a method invocation that eventually returns (as in deadlock-freedom), or each pending method invocation must be continuously disabled. But how do we formally say that a method is disabled? When we informally say this, we actually refer to the enabling condition B in await(B){C} in the object’s atomic partial specification Γ. However, we may not be able to infer such a condition from the concrete implementation Π. To address this problem, our definitions of PSFΓ (Π) and PDFΓ (Π) are parameterized with the specification Γ (the actual definitions take more parameters, as shown in Sec. 5). We can prove the lock objects in Fig. 1(a) and (c) satisfy PDF and PSF respectively. We can also show that starvation-freedom and deadlock-freedom are special cases of our PSF and PDF respectively, by instantiating the parameter Γ with specifications in the form of await(true){C}. 2.2.3 Atomic Partial Specifications Are Insufficient for Progress-Aware Abstractions. Although the atomic partial specification Γ describes the atomic functionality and the enabling condition of each method, it is insufficient to serve as a progress-aware abstraction for the following reasons. First, the progress of the await command itself is affected by the fairness of scheduling, such as strong fairness and weak fairness. • Strong fairness: Every thread which is infinitely often enabled will execute infinitely often. Then, await(B){C} is not executed only if B is continuously false after some point in the execution trace. • Weak fairness: Every thread which is eventually always enabled will execute infinitely often. Then, await(B){C} may not be executed when B is infinitely often false. This fairness notion is weaker than strong fairness. As a result, the choice of fair scheduling will affect the behaviors of a program or a specification with await commands. To see this, we consider the following client program (2.5). [ _ ]acq; [ _ ]rel; print(1); || while(true){ [ _ ]acq; [ _ ]rel; } (2.5) where [ _ ]acq and [ _ ]rel represent holes to be filled with method calls of lock acquire and release, respectively. Table 1 shows the behaviors of the client with different locks. If the client calls the abstract specifications in (2.3), it must execute print(1) under strongly fair scheduling, but may not do so under weakly fair scheduling. This is because the call of L_ACQ' could be infinitely Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 20. Publication date: January 2018
20:8 Hongjin Liang and Xinyu Feng Table 2.Wrappers for atomic specifications. PSF PDF Strong Fairness wr(await(B)(C]) wrF(await(B)(C]) Weak Fairness WrPSE(await(B)C)） wrpp(await(B)(C)) often enabled and infinitely often disabled in an execution,making its termination sensitive to the fairness of scheduling. Also note that the two fairness notions coincide when the program does not contain blocking operations.Therefore,regardless of strongly or weakly fair scheduling,the client(2.5)using ticket locks always executes print(1),but it may not do so if using test-and-set locks instead (see Table 1). As a result,for the same object implementation,we may need different abstractions under different scheduling.As shown in Table 1,the specification(2.3)cannot serve as the specification of the test-and-set locks under both strong fairness and weak fairness. Second,even under the same scheduling,different implementations demonstrate different progress, therefore need different abstractions.As shown in Table 1,the different lock implementations have different behaviors,even under the same scheduling. For the above two reasons,we need different abstractions for different combinations of fairness and progress.For PSF and PDF under strong and weak fairness respectively,we may need four different abstractions.Can we systematically generate all of them? Our solution.We define code wrappers over the basic blocking primitive await(B)(C)to generate the abstractions.The code wrappers are syntactic transformations that transform await(B)(C)into possibly non-atomic object specifications which can be refined by the object implementations in the progress-aware contextual refinement.As shown in Table 2,the four wrappers correspond to all combinations of fairness and progress.The definitions are shown in Sec.6.Here we only give some high-level intuitions using the lock objects as examples. First,we observe that the lock specification(2.3)can already serve as an abstraction for ticket locks under strong fairness,or for test-and-set locks under weak fairness.In general,the wrapper wr can be an identity function,i.e.,the atomic partial specifications are already proper abstractions for PSF objects (not only for locks)under strong fairness.But wr is subtle.The atomic partial specifications are insufficient as abstractions for general PDF objects under weak fairness,which we will explain in detail in Sec.6. Second,as we have seen from Table 1,the lock specification(2.3)does not work for PSF locks under weak fairness nor for PDF locks under strong fairness.Then the role of the wrapper wr (or wr)is to generate the same PSF(or PDF)behaviors even though the fairness of scheduling is weaker (or stronger). To guarantee PSF,the idea is to create some kind of"fairness"on termination,ie.,every method call can get the chance to terminate.Given weakly fair scheduling,this requires the enabling condition of the abstraction to continuously remain true.As a result,a possible way to define wr(LACQ)is to keep a queue of threads requesting the lock,and a thread can acquire the lock only when it is at the head of the queue. To support PDF under strongly fair scheduling,we have to allow non-termination even if the enabling condition is infinitely often true.For the client(2.5),the call of L_ACQ'in the specifica- tion(2)under strongly fair scheduling always terminates.Then wrneeds to incorporate with some kind of delaying mechanisms,so that the termination of L_ACQ'of the left thread could be delayed every time when the right thread succeeds in acquiring the lock. Proceedings of the ACM on Programming Languages,Vol.2,No.POPL,Article 20.Publication date:January 2018
20:8 Hongjin Liang and Xinyu Feng Table 2. Wrappers for atomic specifications. PSF PDF Strong Fairness wrsfair PSF (await(B){C}) wrsfair PDF (await(B){C}) Weak Fairness wrwfair PSF (await(B){C}) wrwfair PDF (await(B){C}) often enabled and infinitely often disabled in an execution, making its termination sensitive to the fairness of scheduling. Also note that the two fairness notions coincide when the program does not contain blocking operations. Therefore, regardless of strongly or weakly fair scheduling, the client (2.5) using ticket locks always executes print(1), but it may not do so if using test-and-set locks instead (see Table 1). As a result, for the same object implementation, we may need different abstractions under different scheduling. As shown in Table 1, the specification (2.3) cannot serve as the specification of the test-and-set locks under both strong fairness and weak fairness. Second, even under the same scheduling, different implementations demonstrate different progress, therefore need different abstractions. As shown in Table 1, the different lock implementations have different behaviors, even under the same scheduling. For the above two reasons, we need different abstractions for different combinations of fairness and progress. For PSF and PDF under strong and weak fairness respectively, we may need four different abstractions. Can we systematically generate all of them? Our solution. We define code wrappers over the basic blocking primitive await(B){C} to generate the abstractions. The code wrappers are syntactic transformations that transform await(B){C} into possibly non-atomic object specifications which can be refined by the object implementations in the progress-aware contextual refinement. As shown in Table 2, the four wrappers correspond to all combinations of fairness and progress. The definitions are shown in Sec. 6. Here we only give some high-level intuitions using the lock objects as examples. First, we observe that the lock specification (2.3) can already serve as an abstraction for ticket locks under strong fairness, or for test-and-set locks under weak fairness. In general, the wrapper wrsfair PSF can be an identity function, i.e., the atomic partial specifications are already proper abstractions for PSF objects (not only for locks) under strong fairness. But wrwfair PDF is subtle. The atomic partial specifications are insufficient as abstractions for general PDF objects under weak fairness, which we will explain in detail in Sec. 6. Second, as we have seen from Table 1, the lock specification (2.3) does not work for PSF locks under weak fairness nor for PDF locks under strong fairness. Then the role of the wrapper wrwfair PSF (or wrsfair PDF) is to generate the same PSF (or PDF) behaviors even though the fairness of scheduling is weaker (or stronger). To guarantee PSF, the idea is to create some kind of “fairness” on termination, i.e., every method call can get the chance to terminate. Given weakly fair scheduling, this requires the enabling condition of the abstraction to continuously remain true. As a result, a possible way to define wrwfair PSF (L_ACQ’) is to keep a queue of threads requesting the lock, and a thread can acquire the lock only when it is at the head of the queue. To support PDF under strongly fair scheduling, we have to allow non-termination even if the enabling condition is infinitely often true. For the client (2.5), the call of L_ACQ' in the specification (2.3) under strongly fair scheduling always terminates. Then wrsfair PDF needs to incorporate with some kind of delaying mechanisms, so that the termination of L_ACQ' of the left thread could be delayed every time when the right thread succeeds in acquiring the lock. Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 20. Publication date: January 2018
Progress of Concurrent Objects with Partial Methods 209 (MName) f9… (PVar)x,y,z· (Expr） =x|n|E+E|. (BExp)B ::true l false I E=E B .. (Stmt) :=x:=Ex:=[E]I[E]:E I print(E)x :cons(E,....E)|dispose(E) 1 skip x:=f(E)|return E I C;C if (B)Celse C I while (B)(C) 1 await(B)(C) (ODecl) II,r : f(,x1.C1).....fn(Pn.xn.Cn) (Prog) W = let II in Cill...lCn (Thrd)C:=C end Fig.2.Syntax of the programming language. 2.2.4 Other Results.We also have the following new results in addition to the new progress properties and code wrappers. Abstraction theorem.We prove the abstraction theorem,saying that our new progress properties PSF and PDF(together with linearizability)are equivalent to contextual refinements where the abstractions are generated by the corresponding wrappers.On the one hand,the theorem justifies the abstractions generated by our wrappers,showing that they are refined by linearizable and PSF (or PDF)object implementations.On the other hand,it also justifies our formulation of PSF and PDF by showing that they imply progress-aware contextual refinements. The abstraction theorem also allows us to verify safety and progress properties of whole programs (consisting of clients and objects)in a modular way-after proving linearizability and PSF(or PDF) of an object II with respect to its atomic partial specification I,we can replace II with the abstraction generated by applying the corresponding wrapper over T,and then reason about properties of the whole program at the high abstraction level. Program logic.Finally we design a program logic as the proof method for verifying PSF and PDF objects.It ensures linearizability and PSF (or PDF)of an object II with respect to its atomic partial specification I.The logic is a generalization of our previous program logic LiLi for starvation-free and deadlock-free objects [Liang and Feng 2016],plus new inference rules for the await statement under strong and weak fairness.We will explain the details in Sec.7. 3 THE LANGUAGE Figure 2 shows the syntax of the language.A program W consists of an object declaration II and n parallel threads C as clients sharing the object.To simplify the language,we assume there is only one object in each program.Each II maps method names fi to annotated method implementations (P,xi,Ci),where xi and Ci are the formal parameter and the method body respectively,and the assertion Pi is an annotated precondition over the object state to ensure the safe execution of the method.It is defined in Fig.3 and is used in the operational semantics explained below.A thread C is either a command C,or an end flag marking termination of the thread.The commands include the standard ones used in separation logic,where x:=[E]and [E]:=E'read and write the heap at the location E respectively,and x:=cons(E,...,E)and dispose(E)allocate and free memory cells respectively.In addition,we have method call (x:=f(E))and return (return E)commands. The print(E)command generates externally observable events,which are used to define trace refinements in Sec.4.The await(B)(C)command is the only blocking primitive in the language.It blocks the current thread if B does not hold,otherwise C is executed atomically together with the testing of B. Proceedings of the ACM on Programming Languages,Vol.2,No.POPL,Article 20.Publication date:January 2018
Progress of Concurrent Objects with Partial Methods 20:9 (MName) f ,д . . . (PVar) x,y,z . . . (Expr) E ::= x | n | E + E | . . . (BExp) B ::= true | false | E = E | ¬B | . . . (Stmt) C ::= x := E | x := [E] | [E] := E | print(E) | x := cons(E,. . . ,E) | dispose(E) | skip | x := f (E) | return E | C;C | if (B) C else C | while (B){C} | await(B){C} (ODecl) Π, Γ ::= {f1 ❀ (P1,x1,C1),. . . , fn ❀ (Pn,xn,Cn )} (Prog) W ::= let Π in Cˆ 1 ∥ . . . ∥Cˆ n (Thrd) Cˆ ::= C | end Fig. 2. Syntax of the programming language. 2.2.4 Other Results. We also have the following new results in addition to the new progress properties and code wrappers. Abstraction theorem. We prove the abstraction theorem, saying that our new progress properties PSF and PDF (together with linearizability) are equivalent to contextual refinements where the abstractions are generated by the corresponding wrappers. On the one hand, the theorem justifies the abstractions generated by our wrappers, showing that they are refined by linearizable and PSF (or PDF) object implementations. On the other hand, it also justifies our formulation of PSF and PDF by showing that they imply progress-aware contextual refinements. The abstraction theorem also allows us to verify safety and progress properties of whole programs (consisting of clients and objects) in a modular way — after proving linearizability and PSF (or PDF) of an object Π with respect to its atomic partial specification Γ, we can replace Π with the abstraction generated by applying the corresponding wrapper over Γ, and then reason about properties of the whole program at the high abstraction level. Program logic. Finally we design a program logic as the proof method for verifying PSF and PDF objects. It ensures linearizability and PSF (or PDF) of an object Π with respect to its atomic partial specification Γ. The logic is a generalization of our previous program logic LiLi for starvation-free and deadlock-free objects [Liang and Feng 2016], plus new inference rules for the await statement under strong and weak fairness. We will explain the details in Sec. 7. 3 THE LANGUAGE Figure 2 shows the syntax of the language. A program W consists of an object declaration Π and n parallel threads Cˆ as clients sharing the object. To simplify the language, we assume there is only one object in each program. Each Π maps method names fi to annotated method implementations (Pi ,xi ,Ci ), where xi and Ci are the formal parameter and the method body respectively, and the assertion Pi is an annotated precondition over the object state to ensure the safe execution of the method. It is defined in Fig. 3 and is used in the operational semantics explained below. A thread Cˆ is either a command C, or an end flag marking termination of the thread. The commands include the standard ones used in separation logic, where x := [E] and [E] := E ′ read and write the heap at the location E respectively, and x := cons(E,. . . ,E) and dispose(E) allocate and free memory cells respectively. In addition, we have method call (x := f (E)) and return (return E) commands. The print(E) command generates externally observable events, which are used to define trace refinements in Sec. 4. The await(B){C} command is the only blocking primitive in the language. It blocks the current thread if B does not hold, otherwise C is executed atomically together with the testing of B. Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 20. Publication date: January 2018
20:10 Hongjin Liang and Xinyu Feng (ThrdID) E Nat (Store) 5,s PVar-Val (Heap) h,h∈ Nat-Val (Data) 0,∑ =(s,h) (CallStk) K.k = oI(sI,x,C) (ThrdPool) K,区 = {t1K1,,tn→Kn} (PState) S,S = (Gc,Go,K) (LState) s,6 = (oc,0o,) (ExecCtxt) E = []I E;C (Pre) 乎(Data) (AbsFun) ∈Data凵Datd (Event)e ::=(t,f,n)(t,ret,n)I (t,obj)I (t,obj.abort)I (t,out,n) I(t,clt)I(t.clt,abort)(t,term)|(spawn,n) (BldSet)△ (PEvent)t=(e,△c,△o) (ETrace) ::=eIe:8 (co-inductive) (PTrace)T :=E I::T (co-inductive) en(C)B if 3E.C'.C=E[await(B)(C] true otherwise (ao,x)B iff [B](oo-swx.s》=true Ak≠o e B iff [B]ac.s true btids(let IIinCll.…lCn,(oc,oo,K)》些(tlK()=oA-(ce卡en(Ch, {tIK(t)≠oA-(oo,K(t)上en(Ct)) Fig.3.States and event traces. We make the following assumptions to simplify the technical setting.There are no regular function calls in either clients or objects.Therefore x:=f(E)can only be executed in client code to call object methods,and return E always returns from object methods to clients.Each object method takes only one argument and each method body ends with a return command.Object methods never execute the print(E)command and therefore do not generate external events.The command C in await(B)(C)cannot contain await,print,and method calls and returns.It cannot contain loops either so that it always terminates. Operational semantics.The operational semantics rules shown in Fig.4 consist of three parts, including state transitions made by the whole program,by individual threads,and by clients or object methods,respectively.We define program states S in Fig.3,where we use two sets of notations to represent states at the concrete and the abstract levels respectively when we study refinement.To ensure that the client code does not touch the object data,in S we separate the data accessed by clients(oc)and by object methods (oo).S also contains a thread pool K mapping thread IDs t to the corresponding method call stacks k.Recall that the only function call allowed in the language is the method invocation made by a client and there are no nested function calls, therefore each k is either empty(o,which means the thread is executing the client code),or contains only one stack frame(sI,x,C),where s is the local store for the local variables of the method,x is the(client)variable recording the return value,and C is the continuation(the remaining client code to be executed after the return of the method). Figure 4(a)shows that the execution of the program W follows the non-deterministic interleaving semantics,which is defined based on thread transitions defined in Fig.4(b).Each transition over program configurations is labelled with a program event t,a triple in the form of(e,Ac,Ao).The event e is generated by thread transitions.As defined in Fig.3,(t,f,n)records the invocation of the method f with the argument n in the thread t,and(t,ret,n)is for a method return with the return value n.(t,obj)and(t,clt)record a regular object step and a regular client step respectively, while(t,obj,abort)and(t,clt,abort)are for aborting of the thread in the object and client code Proceedings of the ACM on Programming Languages,Vol.2,No.POPL,Article 20.Publication date:January 2018
20:10 Hongjin Liang and Xinyu Feng (ThrdID) t ∈ Nat (Store) s,s ∈ PVar ⇀ Val (Heap) h,h ∈ Nat ⇀ Val (Data) σ,Σ ::= (s,h) (CallStk) κ,k ::= ◦ | (sl ,x,C) (ThrdPool) K ,K ::= {t1 ❀ κ1,. . . ,tn ❀ κn } (PState) S,S ::= (σc ,σo ,K ) (LState) ς,δ ::= (σc ,σo ,κ) (ExecCtxt) E ::= [ ] | E;C (Pre) P ∈ P(Data) (AbsFun) φ ∈ Data ⇀ Data (Event) e ::= (t, f ,n) | (t,ret,n) | (t,obj) | (t,obj,abort) | (t,out,n) | (t,clt) | (t,clt,abort) | (t,term) | (spawn,n) (BIdSet) ∆ ∈ P(ThrdID) (PEvent) ι ::= (e,∆c ,∆o ) (ETrace) E ::= ϵ | e ::E (co-inductive) (PTrace) T ::= ϵ | ι ::T (co-inductive) en(Cˆ) def = ( B if ∃E,C ′ . Cˆ = E[await(B){C ′ }] true otherwise (σo ,κ) |= B iff JBK((σo .s)⊎(κ.sl )) = true ∧ κ , ◦ σc |= B iff JBKσc .s = true btids(let Π in Cˆ 1 ∥ . . . ∥Cˆ n, (σc ,σo ,K )) def = ({t | K (t) = ◦ ∧ ¬(σc |= en(Cˆ t ))}, {t | K (t) , ◦ ∧ ¬((σo ,K (t)) |= en(Cˆ t ))}) Fig. 3. States and event traces. We make the following assumptions to simplify the technical setting. There are no regular function calls in either clients or objects. Therefore x := f (E) can only be executed in client code to call object methods, and return E always returns from object methods to clients. Each object method takes only one argument and each method body ends with a return command. Object methods never execute the print(E) command and therefore do not generate external events. The command C in await(B){C} cannot contain await, print, and method calls and returns. It cannot contain loops either so that it always terminates. Operational semantics. The operational semantics rules shown in Fig. 4 consist of three parts, including state transitions made by the whole program, by individual threads, and by clients or object methods, respectively. We define program states S in Fig. 3, where we use two sets of notations to represent states at the concrete and the abstract levels respectively when we study refinement. To ensure that the client code does not touch the object data, in S we separate the data accessed by clients (σc ) and by object methods (σo ). S also contains a thread pool K mapping thread IDs t to the corresponding method call stacks κ. Recall that the only function call allowed in the language is the method invocation made by a client and there are no nested function calls, therefore each κ is either empty (◦, which means the thread is executing the client code), or contains only one stack frame (sl ,x,C), where sl is the local store for the local variables of the method, x is the (client) variable recording the return value, and C is the continuation (the remaining client code to be executed after the return of the method). Figure 4(a) shows that the execution of the programW follows the non-deterministic interleaving semantics, which is defined based on thread transitions defined in Fig. 4(b). Each transition over program configurations is labelled with a program event ι, a triple in the form of (e,∆c ,∆o ). The event e is generated by thread transitions. As defined in Fig. 3, (t, f ,n) records the invocation of the method f with the argument n in the thread t, and (t,ret,n) is for a method return with the return value n. (t,obj) and (t,clt) record a regular object step and a regular client step respectively, while (t,obj,abort) and (t,clt,abort) are for aborting of the thread in the object and client code Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 20. Publication date: January 2018