Coherent Causal Memory

TL;DR

Coherent causal memory (CCM) offers a memory model that balances formal reasoning capabilities with efficient implementation, allowing for relaxed ordering of writes while maintaining consistency for reasoning and supporting practical programming disciplines.

Contribution

The paper introduces CCM as a memory model that supports assertional reasoning and efficient implementation, differing from sequential consistency mainly in handling write-write races.

Findings

CCM enables assertional reasoning similar to sequential consistency.

CCM can be efficiently implemented on x86-TSO with a simple discipline.

The discipline is more relaxed than traditional SC enforcement, especially for single-writer variables.

Abstract

Coherent causal memory (CCM) is causal memory in which prefixes of an execution can be mapped to global memory states in a consistent way. While CCM requires conflicting pairs of writes to be globally ordered, it allows writes to remain unordered with respect to both reads and nonconflicting writes. Nevertheless, it supports assertional, state-based program reasoning using generalized Owicki-Gries proof outlines (where assertions can be attached to any causal program edge). Indeed, we show that from a reasoning standpoint, CCM differs from sequentially consistent (SC) memory only in that ghost code added by the user is not allowed to introduce new write-write races. While CCM provides most of the formal reasoning leverage of SC memory, it is much more efficiently implemented. As an illustration, we describe a simple programming discipline that provides CCM on top of x86-TSO. The discipline is considerably more relaxed than the one needed to ensure SC; for example, it introduces no burden whatsoever for programs in which at most one thread writes to any variable.