A Framework for Consistency Models in Distributed Systems

Abstract

We define am axiomatic timeless framework for asynchronous distributed systems, together with well-formedness and consistency axioms, which unifies and generalizes the expressive power of current approaches. 1) It combines classic serialization per-process with a global visibility. 2) It defines a physical realizability well-formedness axiom to prevent physically impossible causality cycles, while allowing possible and useful visibility cycles, to allow synchronization-oriented abstractions. 3) Allows adding time-based constraints, from a logical or physical clock, either partially or totally ordered, in an optional and orthogonal way, while keeping models themselves timeless. 4) It simultaneously generalizes from memory to general abstractions, from sequential to concurrent specifications, either total or partial, and beyond serial executions. 5) Defines basic consistency axioms: monotonic visibility, local visibility, and closed past. These are satisfied by what we call serial consistency, but can be used as building blocks for novel consistency models with histories not explainable by any serial execution. 6) Revisits classic pipelined and causal consistency, revealing weaknesses in previous axiomatic models for PRAM and causal memory. 7) Introduces convergence and arbitration as safety properties for consistency models, departing from the use of eventual consistency, which conflates safety and liveness. 8) Formulates and proves the CLAM theorem for asynchronous distributed systems: any wait-free implementation of practically all data abstractions cannot simultaneously satisfy Closed past, Local visibility, Arbitration, and Monotonic visibility. While technically incomparable, the CLAM theorem is practically stronger than the CAP theorem, as it allows reasoning about the design space and possible tradeoffs in highly available partition tolerant systems.