Replicated Data Types: Specification, Verification, Optimality
Replicated Data Types: Specification, Verification, Optimality
复制标题
DOI：
10.1145/2535838.2535848
复制
发表时间：
2014-01-01
影响因子：
--
通讯作者：
Zawirski, Marek
中科院分区：
文献类型：
--
作者：
Burckhardt, Sebastian;Gotsman, Alexey;Zawirski, Marek
地理分布式系统通常依赖于复制的最终一致的数据存储来实现可用性和性能。为了解决不同副本的更新冲突，研究人员和从业者提出了专门的一致性协议，称为复制数据类型，它实现寄存器、计数器、集合或列表等对象。然而，关于复制数据类型的推理还无法与抽象数据类型和并发数据类型的类似工作相提并论，缺乏规范、正确性证明和最优性结果。为了填补这一空白，我们提出了一个框架，用于使用事件关系来指定复制数据类型，并使用复制感知模拟来验证其实现。我们将其应用于 4 种数据类型的 7 个现有实现，并具有重要的冲突解决策略和优化（最后写入者获胜寄存器、计数器、多值寄存器和观察删除集）。我们还提出了一种新颖的技术，用于获得数据类型实现的最坏情况空间开销的下限，并用它来证明 4 种实现的最优性。最后，我们展示了如何公理地指定多个对象的复制存储的一致性，类似于之前对弱内存模型的工作。总的来说，我们的工作提供了基础推理工具来支持复制最终一致存储的研究。
Geographically distributed systems often rely on replicated eventually consistent data stores to achieve availability and performance. To resolve conflicting updates at different replicas, researchers and practitioners have proposed specialized consistency protocols, called replicated data types, that implement objects such as registers, counters, sets or lists. Reasoning about replicated data types has however not been on par with comparable work on abstract data types and concurrent data types, lacking specifications, correctness proofs, and optimality results.To fill in this gap, we propose a framework for specifying replicated data types using relations over events and verifying their implementations using replication-aware simulations. We apply it to 7 existing implementations of 4 data types with nontrivial conflict-resolution strategies and optimizations (last-writer-wins register, counter, multi-value register and observed-remove set). We also present a novel technique for obtaining lower bounds on the worst-case space overhead of data type implementations and use it to prove optimality of 4 implementations. Finally, we show how to specify consistency of replicated stores with multiple objects axiomatically, in analogy to prior work on weak memory models. Overall, our work provides foundational reasoning tools to support research on replicated eventually consistent stores.