Eventual Consistency (basic) EC
Basic eventual consistency for replicated data stores, defined axiomatically over abstract executions with visibility and arbitration relations (in analogy to weak shared-memory models) by two axioms: EVENTUAL guarantees an update cannot stay invisible to infinitely many operations on the same object, so if updates stop replicas converge to the same state; THINAIR forbids out-of-thin-air values. Causal (and further sequential/linearizable) consistency are obtained by adding successively stronger ordering axioms (POCV/POCA, then COCV/COCA) on top of it, so eventual consistency is strictly weaker than causal consistency. First given a formal definition in MSR-TR-2013-39 (2013).
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
- Atomicity guarantees
- no Multicopy atomic
Ordering relationships
- Strictly weaker than
- Per-Object Causal Consistency (PO-Causal) — Burckhardt, Gotsman, Yang & Zawirski, POPL 2014, §7: an execution is per-object causally consistent iff it is eventually consistent (EVENTUAL+THINAIR) AND satisfies the per-object ordering axioms POCV/POCA. Adding those axioms disallows strictly more anomalies (e.g. Fig. 14(b), §3.1), so eventual consistency is strictly weaker than per-object causal consistency.
References
- Sebastian Burckhardt, Alexey Gotsman, Hongseok Yang. Understanding Eventual Consistency. Microsoft Research Technical Report MSR-TR-2013-39, 2013. www.microsoft.com/en-us/research/publication/understanding-eventual-consistency/
- Sebastian Burckhardt, Alexey Gotsman, Hongseok Yang, Marek Zawirski. Replicated Data Types: Specification, Verification, Optimality. POPL 2014, 2014. doi:10.1145/2535838.2535848