Causal Linearizability

TL;DR

This paper introduces causal linearizability, a new correctness condition for concurrent objects on weak memory models, ensuring composability and correctness even when traditional linearizability does not hold.

Contribution

It proposes causal linearizability and operation-race freedom as new concepts to verify concurrent objects on weak memory models, with application to Linux kernel objects.

Findings

Causal linearizability guarantees correctness on weak memory models.

Operation-race freedom ensures objects behave as if linearizable.

Validated on Linux kernel objects on TSO architecture.

Abstract

Most work on the verification of concurrent objects for shared memory assumes sequential consistency, but most multicore processors support only weak memory models that do not provide sequential consistency. Furthermore, most verification efforts focus on the linearizability of concurrent objects, but there are existing implementations optimized to run on weak memory models that are not linearizable. In this paper, we address these problems by introducing causal linearizability, a correctness condition for concurrent objects running on weak memory models. Like linearizability itself, causal linearizability enables concurrent objects to be composed, under weak constraints on the client's behaviour. We specify these constraints by introducing a notion of operation-race freedom, where programs that satisfy this property are guaranteed to behave as if their shared objects were in fact linearizable. We apply these ideas to objects from the Linux kernel, optimized to run on TSO, the memory model of the x86 processor family.