Abstract
Linearisability is the de facto standard correctness condition for concurrent objects. Classical linearisability assumes that the effect 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 consider 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 specification of an object rather than its more complex concurrent implementation) and composition (so that reasoning about independent objects can be conducted in isolation).