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