Relaxed Memory Model Zoo

Ordering relationships

Strictly weaker than

• Sequential Consistency (SC) — Bouajjani et al., POPL 2017, Example 7: history (2d) satisfies CC, CM and CCv, yet admits no total order over all its operations, so it is not sequentially consistent.
• Causal+ (Convergent Causal) Consistency — Causal+ = Causality ∧ StrongConvergence (Viotti & Vukolić 2016, Eq. 27; Lloyd et al., COPS, SOSP 2011). V-V's Causality (Eq. 26) is the visibility/arbitration causal consistency that Bouajjani et al. name CCv, so this containment is against CCv. Adding strong convergence disallows strictly more behaviours, so CCv is strictly weaker than causal+. Re-homed from the Causal node, where the same note had been read as a containment against causal memory.
• Real-Time Causal Consistency (RTCausal) — RealTimeCausality = Causality ∧ RealTime (Viotti & Vukolić 2016, Eq. 28; Mahajan, Alvisi & Dahlin 2011). V-V's Causality (Eq. 26) is causal convergence, so this containment is against CCv. It adds RealTime (Eq. 9, rb ⊆ ar) — causally concurrent, real-time-non-overlapping writes must be applied in real-time order — disallowing strictly more behaviours, so CCv is strictly weaker than real-time causal consistency. Re-homed from the Causal node, where the same note had been read as a containment against causal memory.

Strictly stronger than

• Weak Causal Consistency (CC) — 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.
• Per-Object Causal Consistency (PO-Causal) — Burckhardt, Gotsman, Yang & Zawirski, POPL 2014, §7: (cross-object) causal consistency imposes the ordering axioms COCV/COCA, while per-object causal consistency imposes only the weaker per-object axioms POCV/POCA over the per-object happens-before order (Viotti & Vukolić 2016, §3.9). COCV/COCA disallow strictly more anomalies, so cross-object causal consistency is strictly stronger than per-object causal consistency. Re-homed from the Causal node: Burckhardt's cross-object causal consistency is the visibility/arbitration one, i.e. CCv, not causal memory.
• Writes-Follow-Reads (Session Guarantee) (WFR) — Unlike the Causal edge to the same node, this one is a derivation rather than a citation. CCv is CausalVisibility ∧ CausalArbitration ∧ RVal (Viotti & Vukolić 2016, Eq. 26), where CausalArbitration is hb ⊆ ar and hb = (so ∪ vis)+. WritesFollowReads is (vis; so|rd→wr) ⊆ ar (Eq. 25). Since vis ⊆ hb and so ⊆ hb, the composite vis;so|rd→wr lies in hb+ = hb ⊆ ar, so CCv satisfies WFR by construction. The converse fails — WFR constrains only write-after-read within a session and says nothing about visibility or the arbitration of anything else — so writes-follow-reads is strictly weaker.

Equivalent to

• Strong Release-Acquire (SRA) — Lahav & Boker, §3.1: ignoring RMWs, SRA is equivalent to the causal convergence model CCv of Bouajjani et al., applied to the standard sequential specification of a read/write key-value store (and to the causal consistency of Cerone et al. restricted to single-instruction transactions). fragment_restricted because the equivalence is stated modulo RMWs: SRA's atomicity axiom has no counterpart in a model over a sequential key-value specification. This edge is the bridge between the C11 family and the distributed causal-consistency cluster.

Incomparable with

• Causal Consistency — Causal memory and causal convergence are incomparable (Perrin, Mostéfaoui & Jard, PPoPP 2016; Bouajjani et al., POPL 2017, §1 and Fig. 1). Both witnesses are in Bouajjani et al. Fig. 2. History (2a) — pa: wr(x,1); rd(x)▷2 || pb: wr(x,2); rd(x)▷1 — is CM but not CCv, because arbitration would have to place wr(x,2) both after and before wr(x,1) (Ex. 5). History (2b) — pa: wr(z,1); wr(x,1); wr(y,1) || pb: wr(x,2); rd(z)▷0; rd(y)▷1; rd(x)▷2 — is CCv but not CM: reading y=1 drags wr(z,1) into pb's causal past behind wr(x,2), which the earlier rd(z)▷0 contradicts (Ex. 6).