228 H.Liang et al. verification of client threads,the concrete implementation I7 of the object meth- ods should be replaced by an abstraction (or specification)IT that consists of equivalent atomic methods.The progress properties should then characterize whether and how the behaviors of a client program will be affected if a client uses I7 instead of IA.In particular,we are interested in systematically study- ing whether the termination of a client using the abstract methods I7A will be preserved when using an implementation II with some progress guarantee. Previous work on verifying the safety of concurrent objects(e.g.,[4,12])has shown that linearizability-a standard safety criterion for concurrent objects- and contextual refinement are equivalent.Informally,an implementation I7 is a contextual refinement of a (more abstract)implementation I7A,if every ob- servable behavior of any client program using II can also be observed when the client uses ITA instead.To obtain equivalence to linearizability,the observable behaviors include I/O events but not divergence (i.e.,non-termination).Re- cently,Gotsman and Yang [6]showed that a client program that diverges using a linearizable and lock-free object must also diverge when using the abstract operations instead.Their work reveals a connection between lock-freedom and a form of contextual refinement which preserves termination as well as safety properties.It is unclear how other progress guarantees affect termination of client programs and how they are related to contextual refinements. This paper studies all five commonly used progress properties and their rela- tionships to contextual refinements.We propose a unified framework in which a certain type of termination-sensitive contextual refinement is equivalent to linearizability together with one of the progress properties.The idea is to iden- tify different observable behaviors for different progress properties.For example, for the contextual refinement for lock-freedom we observe the divergence of the whole program,while for wait-freedom we also need to observe which threads in the program diverge.For lock-based progress properties,e.g.,starvation-freedom and deadlock-freedom,we have to take fair schedulers into account. Our paper makes the following new contributions: We formalize the definitions of the five most common progress properties: wait-freedom,lock-freedom,obstruction-freedom,starvation-freedom,and deadlock-freedom.Our formulation is based on possibly infinite event traces that are operationally generated by any client using the object. Based on our formalization,we prove relationships between the progress properties.For example,wait-freedom implies lock-freedom and starvation- freedom implies deadlock-freedom.These relationships form a lattice shown in Figure 1 (where the arrows represent implications).We close the lattice with a bottom element that we call sequential termination,a progress prop- erty in the sequential setting.It is weaker than any other progress property. We develop a unified framework to characterize progress properties via con- textual refinements.With linearizability,each progress property is proved equivalent to a contextual refinement which takes into account divergence of programs.A companion TR 14 contains the formal proofs of our results.228 H. Liang et al. verification of client threads, the concrete implementation Π of the object meth￾ods should be replaced by an abstraction (or specification) ΠA that consists of equivalent atomic methods. The progress properties should then characterize whether and how the behaviors of a client program will be affected if a client uses Π instead of ΠA. In particular, we are interested in systematically study￾ing whether the termination of a client using the abstract methods ΠA will be preserved when using an implementation Π with some progress guarantee. Previous work on verifying the safety of concurrent objects (e.g., [4,12]) has shown that linearizability—a standard safety criterion for concurrent objects— and contextual refinement are equivalent. Informally, an implementation Π is a contextual refinement of a (more abstract) implementation ΠA, if every ob￾servable behavior of any client program using Π can also be observed when the client uses ΠA instead. To obtain equivalence to linearizability, the observable behaviors include I/O events but not divergence (i.e., non-termination). Re￾cently, Gotsman and Yang [6] showed that a client program that diverges using a linearizable and lock-free object must also diverge when using the abstract operations instead. Their work reveals a connection between lock-freedom and a form of contextual refinement which preserves termination as well as safety properties. It is unclear how other progress guarantees affect termination of client programs and how they are related to contextual refinements. This paper studies all five commonly used progress properties and their rela￾tionships to contextual refinements. We propose a unified framework in which a certain type of termination-sensitive contextual refinement is equivalent to linearizability together with one of the progress properties. The idea is to iden￾tify different observable behaviors for different progress properties. For example, for the contextual refinement for lock-freedom we observe the divergence of the whole program, while for wait-freedom we also need to observe which threads in the program diverge. For lock-based progress properties, e.g., starvation-freedom and deadlock-freedom, we have to take fair schedulers into account. Our paper makes the following new contributions: – We formalize the definitions of the five most common progress properties: wait-freedom, lock-freedom, obstruction-freedom, starvation-freedom, and deadlock-freedom. Our formulation is based on possibly infinite event traces that are operationally generated by any client using the object. – Based on our formalization, we prove relationships between the progress properties. For example, wait-freedom implies lock-freedom and starvation￾freedom implies deadlock-freedom. These relationships form a lattice shown in Figure 1 (where the arrows represent implications). We close the lattice with a bottom element that we call sequential termination, a progress prop￾erty in the sequential setting. It is weaker than any other progress property. – We develop a unified framework to characterize progress properties via con￾textual refinements. With linearizability, each progress property is proved equivalent to a contextual refinement which takes into account divergence of programs. A companion TR [14] contains the formal proofs of our results