恰到好处的一致性：协调可用性和安全性
Just-Right Consistency: reconciling availability and safety
摘要：
根据CAP定理，分布式数据存储系统可以保证分区下的一致性（CP）或分区下的可用性（AP），但不能同时保证两者。这导致了CP数据库和AP数据库之间的分裂，CP数据库中的更新是同步的，AP数据库中的更新是异步的。然而，没有内在的理由将所有更新都等同对待：简单地说，系统应该尽可能可用，并且同步到足以使应用程序正确。基于以下见解，我们提供了一种原则性的正确一致性方法来设计此类应用程序，协调正确性与可用性和性能：（i）无重复数据类型（CRDTs）数据模型以直观和原则性的方式支持异步更新。(ii)涉及联合或相互排序更新的不变量与AP兼容，并且可以由transmittance Causal Consistency（transmittance Causal consistency）保证，transmittance causal consistency是不损害可用性的最强一致性模型。关于其余的“CAP敏感”不变量：（iii）对于有界计数器的常见模式，我们提供了被证明正确且有效的封装数据类型;（iv）在一般情况下，静态分析可以识别何时不需要同步以确保正确性。我们的Antidote云数据库系统支持CRDTs、事务因果一致性和有界计数器数据类型。支持工具通过静态分析和CAP敏感不变量的证明来帮助设计应用程序。该系统支持工业级应用程序，并已在几个地理分布数据中心的数百台服务器上进行了实验测试。
英文摘要：
By the CAP Theorem, a distributed data storage system can ensure either Consistency under Partition (CP) or Availability under Partition (AP), but not both. This has led to a split between CP databases, in which updates are synchronous, and AP databases, where they are asynchronous. However, there is no inherent reason to treat all updates identically: simply, the system should be as available as possible, and synchronised just enough for the application to be correct. We offer a principled Just-Right Consistency approach to designing such applications, reconciling correctness with availability and performance, based on the following insights:(i) The Conflict-Free Replicated Data Type (CRDTs) data model supports asynchronous updates in an intuitive and principled way.(ii) Invariants involving joint or mutually-ordered updates are compatible with AP and can be guaranteed by Transactional Causal Consistency, the strongest consistency model that does not compromise availability. Regarding the remaining, "CAP-sensitive" invariants:(iii) For the common pattern of Bounded Counters, we provide encapsulated data type that is proven correct and is efficient; (iv) in the general case, static analysis can identify when synchronisation is not necessary for correctness.Our Antidote cloud database system supports CRDTs, Transactional Causal Consistency and the Bounded Counter data type. Support tools help design applications by static analysis and proof of CAP-sensitive invariants. This system supports industrial-grade applications and has been tested experimentally with hundreds of servers across several geo-distributed data centres.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
