A Highly-Available Move Operation for Replicated Trees
| Autor: | Kleppmann, M, Mulligan, DP, Gomes, VBF, Beresford, AR |
|---|---|
| Přispěvatelé: | Kleppmann, M [0000-0001-7252-6958], Mulligan, DP [0000-0003-4643-3541], Gomes, VBF [0000-0002-2954-4648], Beresford, AR [0000-0003-0818-6535], Apollo - University of Cambridge Repository |
| Rok vydání: | 2022 |
| Předmět: |
Correctness
Conflict-free replicated data types (CRDTs) distributed filesystems Computer science Distributed computing HOL Drives Synchronization formal verification Block (data storage) computer.programming_language Internet Proof assistant Data models XML JSON distributed collaboration Tree (data structure) Tree structure Computational Theory and Mathematics Software bug Computer bugs Hardware and Architecture Signal Processing computer Software |
| Zdroj: | IEEE Transactions on Parallel and Distributed Systems. 33:1711-1724 |
| ISSN: | 2161-9883 1045-9219 |
| DOI: | 10.1109/tpds.2021.3118603 |
| Popis: | 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 article 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|