A sound and complete definition of linearizability on weak memory models

TL;DR

This paper demonstrates that the standard definition of linearizability remains valid and complete across all hardware weak memory models when interpreted with an abstracted specification behavior.

Contribution

It proves that redefinitions of linearizability are unnecessary for weak memory models, enabling the use of existing verification techniques.

Findings

Standard linearizability is sound on all weak memory models.

Existing tools for linearizability can be used without modification.

Reinterpretation of specifications abstracts weak memory effects.

Abstract

Linearizability is a widely accepted notion of correctness for concurrent objects. Recent research has investigated redefining linearizability for particular hardware weak memory models, in particular for TSO. In this paper, we provide an overview of this research and show that such redefinitions of linearizability are not required: under an interpretation of specification behaviour which abstracts from weak memory effects, the standard definition of linearizability is sound and complete on all hardware weak memory models. We prove our result with respect to a definition of object refinement which takes a weak memory model as a parameter. The main consequence of our findings is that we can leverage the range of existing techniques and tools for standard linearizability when verifying concurrent objects running on hardware weak memory models.