Weak Causal Consistency (CC)

2017 · Bouajjani, Enea, Guerraoui, Hamza · theoretical, formal · axiomatic formalism

The weakest notion of causal consistency in the literature: it asks only that some causal order exist which, per operation, explains that operation's return value (axioms AxCausal and AxCausalValue). Unlike causal memory it lets a site order causally unrelated operations one way and revise that ordering later — modelling implementations that speculate on an order and roll back — and unlike causal convergence it requires no global arbitration order. Strictly weaker than both CM and CCv (Bouajjani et al., POPL 2017, Fig. 1), with Fig. 2 history (2c) satisfying CC and neither of the others. Equivalent to the WRA memory model, which is what makes it the causal-consistency counterpart of the C/C++11 release-acquire family.

Cat model

Expressible in cat author-extrapolated

AxCausal and AxCausalValue over an existentially quantified causal order, with a per-operation serialisation of that operation's causal past — the same shape as the Causal and CCv entries, and per-execution. Bouajjani et al. 2017

Properties

Property vector author-extrapolated — set only where the model’s definition pins the cell down (unknown cells are omitted); cells citing a specific source are marked.

Reasoning guarantees: no Coherence
Atomicity guarantees: no Multicopy atomic

Ordering relationships

Strictly weaker than: Causal Consistency — Bouajjani et al., POPL 2017, §4 and Fig. 1: CM and CCv 'are both strictly stronger than CC'. Witness: Fig. 2 history (2c) — pa: wr(x,1) || pb: wr(x,2); rd(x)▷1; rd(x)▷2 — is CC but neither CM nor CCv, since pb revises its ordering of the two writes after already having read one of them.
Causal Convergence (CCv) — Bouajjani et al., POPL 2017, Lemma 2 (after Perrin et al.): every CCv history is CC, since AxArb gives co subset of arb and hence AxCausalArb implies AxCausalValue. Strictness is the same Fig. 2 history (2c), which is CC but not CCv.
Equivalent to: Weak Release-Acquire (WRA) — Lahav & Boker: WRA 'provides the most minimal guarantees required from a model to satisfy causal consistency; it is equivalent to the model called CC studied in' Bouajjani et al. (POPL 2017).

References

Ahmed Bouajjani, Constantin Enea, Rachid Guerraoui, Jad Hamza. On Verifying Causal Consistency. POPL 2017, 2017. doi:10.1145/3009837.3009888
Matthieu Perrin, Achour Mostéfaoui, Claude Jard. Causal Consistency: Beyond Memory. PPoPP 2016, 2016. doi:10.1145/2851141.2851170

Open CC in the interactive map →