The fundamental tension between \emph{availability} and \emph{consistency} shapes the design of distributed storage systems. Classical results capture extreme points of this trade-off: the CAP theorem shows that strong models like linearizability preclude availability under partitions, while weak models like causal consistency remain implementable without coordination. These theorems apply to simple read-write interfaces, leaving open a precise explanation of the combinations of object semantics and consistency models that admit available implementations. This paper develops a general semantic framework in which storage specifications combine operation semantics and consistency models. The framework encompasses a broad range of objects (key-value stores, counters, sets, CRDTs, and transactional databases) and consistency models (from causal consistency and sequential consistency to snapshot isolation and transactional and non-transactional SQL). Within this framework, we prove the \emph{Arbitration-Free Consistency} (AFC) theorem, showing that an object specification within a consistency model admits an available implementation if and only if it is \emph{arbitration-free}, that is, it does not require a total arbitration order to resolve visibility or read dependencies. The AFC theorem unifies and generalizes previous results, revealing arbitration-freedom as the fundamental property that delineates coordination-free consistency from inherently synchronized behavior.
翻译:可用性与一致性之间的基本张力塑造了分布式存储系统的设计。经典结论捕捉了这种权衡的极端点:CAP定理表明,在分区情况下,像线性一致性这样的强模型会排除可用性,而像因果一致性这样的弱模型则无需协调即可实现。这些定理适用于简单的读写接口,但对于何种对象语义与一致性模型的组合能够支持可用实现,尚未给出精确解释。本文发展了一个通用的语义框架,其中存储规约结合了操作语义与一致性模型。该框架涵盖了广泛的对象(键值存储、计数器、集合、CRDT和事务数据库)与一致性模型(从因果一致性、顺序一致性到快照隔离以及事务性与非事务性SQL)。在此框架内,我们证明了无仲裁一致性定理,表明一致性模型内的对象规约允许可用实现,当且仅当它是无仲裁的,即不需要一个全仲裁序来解决可见性或读依赖。AFC定理统一并推广了先前的结果,揭示了无仲裁性作为区分免协调一致性与固有同步行为的基本属性。