论文标题
在$δ$ -CRDT中验证强大的最终一致性
Verifying Strong Eventual Consistency in $δ$-CRDTs
论文作者
论文摘要
无冲突复制的数据类型（CRDT）是一种自然结构，可以在分布式设置中传达有关共享计算的信息，在该设置中，协调开销可能无法容忍，并且允许单个参与者暂时与整体计算相差。在这种情况下，有两种经典方法：基于状态和操作的CRDT。前者定义了一个可交换，联想和愿意的联接行动，他们的州单调联合了半亮点。基于州的CRDS可以进一步分为经典和$δ$ - 州CRDT。每次更新后，前者都会传达其全州，而后者仅传达变化的状态。基于OP的CRDT交流操作（不是状态），因此使其更新非数字。尽管基于OP的CRDT几乎不需要交换信息，但它们要求相对强大的网络保证（确切的信息传递），而基于州的CRDT则遇到了相反的问题。两者都满足最终的一致性（SEC）。 我们认为，$δ$ -State CRDTS（1）都需要有效负载大小的沟通开销较小，并且（2）可以忍受相对较弱的网络环境，使其成为现实使用CRDT的理想候选者。我们的中心直觉是状态，$δ$ - 州和基于OP的CRDT之间的一对。我们在Isabelle Interactive Theorem宣传中正式化了这种直觉，并表明基于州的CRDT达到了SEC。我们在伊莎贝尔（Isabelle）中提出了一个放松的网络模型，并表明基于州的CRDT仍保持SEC。最后，我们扩展了工作，以表明$δ$ - 州CRDT仅在仅在相对较弱的网络条件下传达$δ$ - 州片段时保持SEC。
Conflict-free replicated data types (CRDTs) are a natural structure with which to communicate information about a shared computation in a distributed setting where coordination overhead may not be tolerated, and individual participants are allowed to temporarily diverge from the overall computation. Within this setting, there are two classical approaches: state- and operation-based CRDTs. The former define a commutative, associative, and idempotent join operation, and their states a monotone join semi-lattice. State-based CRDTs may be further distinguished into classical- and $δ$-state CRDTs. The former communicate their full state after each update, whereas the latter communicate only the changed state. Op-based CRDTs communicate operations (not state), thus making their updates non-idempotent. Whereas op-based CRDTs require little information to be exchanged, they demand relatively strong network guarantees (exactly-once message delivery), and state-based CRDTs suffer the opposite problem. Both satisfy strong eventual consistency (SEC). We posit that $δ$-state CRDTs both (1) require less communication overhead from payload size, and (2) tolerate relatively weak network environments, making them an ideal candidate for real-world use of CRDTs. Our central intuition is a pair of reductions between state-, $δ$-state, and op-based CRDTs. We formalize this intuition in the Isabelle interactive theorem prover and show that state-based CRDTs achieve SEC. We present a relaxed network model in Isabelle and show that state-based CRDTs still maintain SEC. Finally, we extend our work to show that $δ$-state CRDTs maintain SEC when only communicating $δ$-state fragments, even under relatively weak network conditions.
