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 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