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.
翻译:我们为异步分布式系统定义了一个公理化无时间框架,结合良构性与一致性公理,该框架统一并推广了现有方法的表达能力。1)它将经典的按进程串行化与全局可见性相结合。2)定义了物理可实现性良构公理,以防止物理上不可能的因果循环,同时允许可能且有用的可见性循环,以支持面向同步的抽象。3)允许以可选且正交的方式添加基于时间的约束(来自逻辑或物理时钟,可以是偏序或全序),同时保持模型本身的无时间性。4)同时实现了从内存到通用抽象、从顺序到并发规约(无论是全序还是偏序)以及超越串行执行的推广。5)定义了基本一致性公理:单调可见性、局部可见性与封闭过去。这些公理被我们称为串行一致性的模型所满足,但也可作为构建新型一致性模型的基础组件,这些模型的历史无法用任何串行执行解释。6)重新审视了经典的流水线与因果一致性,揭示了先前PRAM与因果内存公理模型的缺陷。7)引入收敛性与仲裁性作为一致性模型的安全性属性,摒弃了将安全性与活性混为一谈的最终一致性概念。8)提出并证明了异步分布式系统的CLAM定理:几乎所有数据抽象的任意无等待实现都无法同时满足封闭过去、局部可见性、仲裁性与单调可见性。尽管在技术上不可直接比较,CLAM定理在实践中强于CAP定理,因为它允许在高可用分区容错系统中对设计空间与可能的权衡进行推理。