A highly-available move operation for replicated trees
A highly-available move operation for replicated trees
复制标题
复制树的高可用移动操作
DOI：
--
复制
发表时间：
2021
影响因子：
5.3
通讯作者：
A. Beresford
中科院分区：
文献类型：
--
作者：
Martin Kleppmann;Dominic P. Mulligan;Victor B. F. Gomes;A. Beresford
复制树数据结构是分布式文件系统（如Google Drive和Dropbox）以及具有JSON或XML数据模型的协作应用程序的基本构建块。这些系统需要支持移动操作，允许子树移动到树中的新位置。然而，这样的移动操作是很难实现正确的，如果不同的副本可以同时执行任意移动操作，我们演示了在谷歌驱动器和Dropbox的并发移动所产生的错误。在本文中，我们提出了一个CRDT算法，处理任意并发修改的树，同时确保树结构仍然有效（特别是，没有循环引入），并保证所有副本收敛到相同的一致性状态。我们的算法不需要副本之间的同步协调，使其在面对网络分区高度可用。我们正式证明了我们的算法使用Isabelle/HOL证明助手的正确性，并评估我们的正式验证的实现在地理复制设置的性能。
Replicated tree data structures are a fundamental building block of distributed filesystems, such as Google Drive and Dropbox, and collaborative applications with a JSON or XML data model. These systems need to support a move operation that allows a subtree to be moved to a new location within the tree. However, such a move operation is difficult to implement correctly if different replicas can concurrently perform arbitrary move operations, and we demonstrate bugs in Google Drive and Dropbox that arise with concurrent moves. In this paper we present a CRDT algorithm that handles arbitrary concurrent modifications on trees, while ensuring that the tree structure remains valid (in particular, no cycles are introduced), and guaranteeing that all replicas converge towards the same consistent state. Our algorithm requires no synchronous coordination between replicas, making it highly available in the face of network partitions. We formally prove the correctness of our algorithm using the Isabelle/HOL proof assistant, and evaluate the performance of our formally verified implementation in a geo-replicated setting.
通过操作转换同时编辑 JSON 对象
DOI：
10.1145/2851613.2852003
发表时间：
2016
期刊：
Proceedings of the 31st Annual ACM Symposium on Applied Computing
影响因子：
--
作者：
Tim Jungnickel;Tobias Herb
通讯作者：
Tobias Herb