Writes-Follow-Reads (Session Guarantee) WFR
Writes-follow-reads session guarantee of Terry et al. (PDIS 1994), sometimes called session causality: writes issued in a session are ordered after any writes whose effects were observed by earlier reads in that session (Viotti & Vukolić 2016, Eq. 25). One of the four session guarantees. Brzezinski, Sobaniec & Wawrzyniak (PDP 2004) show that causal memory requires all four, so it is strictly weaker than causal memory; and it follows by construction from causal convergence, whose CausalArbitration axiom (hb ⊆ ar) already contains it. Both sources state an implication only — whether the four session guarantees are jointly sufficient for causal consistency is open, see issue #11.
Cat model
Expressible in cat author-extrapolated
Session causality: writes of a session follow the writes their earlier reads observed — an acyclicity condition over po, rf and co on one execution. Terry et al. 1994
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 Convergence (CCv) — 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.
- Causal Consistency — Brzezinski, Sobaniec & Wawrzyniak (PDP 2004) show that causal consistency requires all four session guarantees — read-your-writes, monotonic reads, monotonic writes and writes-follow-reads. Their data-centric models are the classical shared-memory taxonomy (atomic, sequential, causal, processor, PRAM, weak, release, scope, entry), so their causal consistency is causal memory, and this edge is correctly against the Causal node rather than CCv. Causal memory therefore implies writes-follow-reads while the converse fails — one session guarantee constrains far less than a per-site serialisation over the causal order — so writes-follow-reads is strictly weaker. Note this is an implication, not an equality: neither Brzezinski et al. nor Viotti & Vukolić state the converse here (see issue #11), and the earlier gloss 'causal = PRAM ∧ writes-follow-reads, Eq. 25' was wrong twice over — Eq. 25 is the definition of WritesFollowReads, not a theorem about causal consistency, and the sources assert only that causal consistency 'requires and includes them all'.
References
- Douglas B. Terry, Alan J. Demers, Karin Petersen, Mike Spreitzer, Marvin Theimer, Brent B. Welch. Session Guarantees for Weakly Consistent Replicated Data. Parallel and Distributed Information Systems (PDIS), 1994. doi:10.1109/PDIS.1994.331722
- Jerzy Brzezinski, Cezary Sobaniec, Dariusz Wawrzyniak. From Session Causality to Causal Consistency. Euromicro Workshop on Parallel, Distributed and Network-Based Processing (PDP), 2004. doi:10.1109/EMPDP.2004.1271440
- Paolo Viotti, Marko Vukolić. Consistency in Non-Transactional Distributed Storage Systems. ACM Computing Surveys 49(1), 2016. doi:10.1145/2926965