Characterizing Progress Properties via Contextual Refinements 229 Wait-freedom Lock-freedom Starvation-freedom w Obstruction-freedom Deadlock-freedom Sequential termination Fig.1.Relationships between Progress Properties By extending earlier equivalence results on linearizability [4],our contextual refinement framework can serve as a new alternative definition for the full cor- rectness properties of concurrent objects.The contextual refinement implied by linearizability and a progress guarantee precisely characterizes the properties at the abstract level that are preserved by the object implementation.When prov- ing these properties of a client of the object,we can soundly replace the concrete method implementations by its abstract operations.On the other hand,since the contextual refinement also implies linearizability and the progress property,we can potentially borrow ideas from existing proof methods for contextual refine- ments,such as simulations (e.g.,[13])and logical relations (e.g.,[2]),to verify linearizability and the progress guarantee together. In the remainder of this paper,we first informally explain our framework in Section 2.We then introduce the formal setting in Section 3;including the definition of linearizability as the safety criterion of objects.We formulate the progress properties in Section 4 and the contextual refinement framework in Section 5.We discuss related work and conclude in Section 6. 2 Informal Account In this section,we informally describe our results.We first give an overview of linearizability and its equivalence to the basic contextual refinement.Then we explain the progress properties and summarize our new equivalence results. Linearizability and Contextual Refinement.Linearizability is a standard safety criterion for concurrent objects 9.Intuitively,linearizability describes atomic behaviors of object implementations.It requires that each method call should appear to take effect instantaneously at some moment between its invo- cation and return. Linearizability intuitively establishes a correspondence between the object implementation II and the intended atomic operations I7A.This correspondence can also be understood as a contertual refinement.Informally,we say that II is a contextual refinement of IA,IIITA,if substituting II for ITA in any context (i.e.,in a client program)does not add observable behaviors.External observers cannot tell that I7A has been replaced by II from monitoring the behaviors of the client program.Characterizing Progress Properties via Contextual Refinements 229 Wait-freedom Lock-freedom Starvation-freedom Obstruction-freedom Deadlock-freedom Sequential termination Fig. 1. Relationships between Progress Properties By extending earlier equivalence results on linearizability [4], our contextual refinement framework can serve as a new alternative definition for the full cor￾rectness properties of concurrent objects. The contextual refinement implied by linearizability and a progress guarantee precisely characterizes the properties at the abstract level that are preserved by the object implementation. When prov￾ing these properties of a client of the object, we can soundly replace the concrete method implementations by its abstract operations. On the other hand, since the contextual refinement also implies linearizability and the progress property, we can potentially borrow ideas from existing proof methods for contextual refine￾ments, such as simulations (e.g., [13]) and logical relations (e.g., [2]), to verify linearizability and the progress guarantee together. In the remainder of this paper, we first informally explain our framework in Section 2. We then introduce the formal setting in Section 3; including the definition of linearizability as the safety criterion of objects. We formulate the progress properties in Section 4 and the contextual refinement framework in Section 5. We discuss related work and conclude in Section 6. 2 Informal Account In this section, we informally describe our results. We first give an overview of linearizability and its equivalence to the basic contextual refinement. Then we explain the progress properties and summarize our new equivalence results. Linearizability and Contextual Refinement. Linearizability is a standard safety criterion for concurrent objects [9]. Intuitively, linearizability describes atomic behaviors of object implementations. It requires that each method call should appear to take effect instantaneously at some moment between its invo￾cation and return. Linearizability intuitively establishes a correspondence between the object implementation Π and the intended atomic operations ΠA. This correspondence can also be understood as a contextual refinement. Informally, we say that Π is a contextual refinement of ΠA, Π ΠA, if substituting Π for ΠA in any context (i.e., in a client program) does not add observable behaviors. External observers cannot tell that ΠA has been replaced by Π from monitoring the behaviors of the client program.