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 implemen￾tation Π 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 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 Γ, 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