Weak Release-Acquire WRA
The weakening of RA giving the most minimal guarantees a model needs to be causally consistent. Modification order plays no role at all: RA's write-coherence and read-coherence are replaced by weak-read-coherence, which uses the per-location restriction of happens-before rather than mo to decide which of two writes to the same location is the later, and RMW atomicity weakens to 'no two RMW events read from the same write'. Consequently WRA does not provide SC-per-location — even single-location programs may behave non-sequentially (Lahav & Boker Ex. 3.7: WW, Oscillating, SF). It is a fragment of the weak RC11 model, has been considered as a candidate shared-memory semantics in its own right, and is equivalent to the weak causal consistency CC.
Cat model
Expressible in cat author-extrapolated
irr-hb, weak-read-coherence over hb|loc — cat states the per-location restriction of a relation directly — and the weakened RMW condition. Per-execution; mo is not used at all. Lahav & Boker 2022
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
- yes No out-of-thin-air
Ordering relationships
- Strictly weaker than
- Release-Acquire (C/C++11 RA fragment) — WRA drops modification order entirely, replacing RA's write-coherence and read-coherence with weak-read-coherence over hb|loc; Lahav & Boker note that write-coherence implies [W];hb|loc;[W] subset of mo, so read-coherence implies weak-read-coherence and RA contains WRA (Prop. 3.2). Strictness is Ex. 3.7, three single-location programs (WW, Oscillating, SF) allowed by WRA and forbidden by RA: WRA does not provide SC-per-location, so even one-location programs may behave non-sequentially.
- Equivalent to
- Weak Causal Consistency (CC) — 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
- Ori Lahav, Udi Boker. Decidable Verification under a Causally Consistent Shared Memory. PLDI 2020, 2020. doi:10.1145/3385412.3385966
- Ori Lahav, Udi Boker. What's Decidable about Causally Consistent Shared Memory?. ACM Trans. Program. Lang. Syst. 44(2), Article 8, 2022. doi:10.1145/3505273