Relaxed Memory Model Zoo

Real-Time Causal Consistency (RTCausal)
← Back to the map

Real-Time Causal Consistency RTCausal

2011 · Mahajan, Alvisi, Dahlin · theoretical, formal · axiomatic formalism

A strengthening of causal consistency due to Mahajan, Alvisi & Dahlin: in addition to causality it enforces a real-time condition — causally concurrent writes that do not overlap in real time must be applied in their real-time order. Viotti & Vukolić (ACM Computing Surveys 2016, Eq. 28) express it as RealTimeCausality = Causality ∧ RealTime, so it is strictly stronger than the causal consistency of that framework — causal convergence (CCv), not causal memory, to which it is incomparable. It is incomparable to causal+: real-time causality does not imply strong convergence, and causal+ does not imply the real-time ordering (V-V §3.5, correcting Lloyd et al.'s original classification).

Cat model

Not expressible in cat author-extrapolated

The real-time condition — causally concurrent writes that do not overlap in real time must be ordered — refers to wall-clock intervals; cat's vocabulary has no notion of real time. Mahajan et al. 2011

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 stronger than
  • Causal Convergence (CCv) — 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.
Incomparable with
  • Causal Consistency — RealTimeCausality = CCv ∧ RealTime, and CCv is incomparable to causal memory. This replaces a strictly_weaker edge that read the Viotti-Vukolić containment (Eq. 28) as being against causal memory; it is against CCv. Witnesses, both Bouajjani et al. POPL 2017 Fig. 2: history (2a) is CM but not CCv, hence not real-time causal; history (2b) is CCv and not CM, and admits a real-time schedule — pa's writes all completing before pb starts — whose arbitration order (pa's writes before wr(x,2)) extends rb, so RealTime (V-V Eq. 9, rb ⊆ ar) holds. RealTime constrains arbitration only, not visibility, so rd(z)▷0 may still miss wr(z,1): it is real-time causal but not CM.
  • Causal+ (Convergent Causal) Consistency — Causal+ and real-time causal consistency are incomparable (Viotti & Vukolić 2016, §3.5): real-time causality does not imply strong convergence, and causal+ does not impose real-time ordering — each forbids a behaviour the other allows. (V-V correct Lloyd et al.'s original claim that real-time causal is stronger than causal+.)

References