JEPSEN

Writes Follow Reads

Writes follow reads, also known as session causality, ensures that if a process reads a value v, which came from a write w1, and later performs write w2, then w2 must be visible after w1. Once you’ve read something, you can’t change that read’s past.

Writes follow reads is a totally available property. Every node can make progress regardless of network partitions.

Formally

Viotti and Vukolić define writes follow reads in terms of the visibility order (which effects are visible to which reads), the session order (the order of operations on each process) and the arbitration order (essentially, which concurrent updates take precedence): the visibility and session orders, restricted to read/write pairs, must be a subset of the arbitration order.