On abstraction and compositionality for weak-memory linearisability

Abstract

Linearisability is the de facto standard correctness condition for concurrent objects. Classical linearisability assumes that the e ect of a method is captured entirely by the allowed sequences of calls and returns. This assumption is inadequate in the presence of relaxed memory models, where happens-before relations are also of importance. In this paper, we develop hb-linearisability for relaxed memory models by extending the classical notion with happens-before information. We con- sider two variants: Real time hb-linearisability, which adopts the classical view that time runs on a single global clock, and causal hb-linearisability, which eschews real-time and is appropriate for systems without a global clock. For both variants, we prove abstraction (so that programmers can reason about a client program using the sequential speci cation of an object rather than its more complex concurrent implementation) and composition (so that reasoning about independent objects can be con- ducted in isolation).