Relating trace refinement and linearizability

In the late 1980's, Back extended the notion of stepwise refinement of sequential systems to concurrent systems. By doing so he provided a definition of what it means for a concurrent system to be correct with respect to an abstract (potentially sequential) specification. This notion of refinement, referred to as trace refinement, was also independently proposed by Abadi and Lamport and has found widespread acceptance and application within the refinement community. Around the same time as Back's work, Herlihy and Wing proposed linearizability as the correctness notion for concurrent objects. Linearizability has also found widespread acceptance being regarded as the standard notion of correctness for concurrent objects in the concurrent-algorithms community. In this paper, we provide a formal link between trace refinement and linearizability. This allows us to compare the two correctness conditions. Our comparisons show that trace refinement implies linearizability, but that linearizability does not imply trace refinement in general. However, linearizability does imply trace refinement under certain conditions. These conditions relate to (i) the fact that trace refinement can be used to prove both safety and liveness properties, whereas linearizability can only be used to prove safety properties, and (ii) the fact that trace refinement depends on the identification of when operations in the implementation are observed to occur. We discuss the consequences of these differences in the context of verifying concurrent objects.