Repository logo
 

A Highly-Available Move Operation for Replicated Trees

Accepted version
Peer-reviewed

Type

Article

Change log

Abstract

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.

Description

Keywords

Internet, Synchronization, Computer bugs, XML, Software, Drives, Data models, Conflict-free replicated data types (CRDTs), formal verification, distributed filesystems, distributed collaboration

Journal Title

IEEE Transactions on Parallel and Distributed Systems

Conference Name

Journal ISSN

1045-9219
1558-2183

Volume Title

Publisher

Institute of Electrical and Electronics Engineers (IEEE)

Rights

All rights reserved
Sponsorship
Isaac Newton Trust (19.08(m))
Leverhulme Trust (ECF-2019-028)
Engineering and Physical Sciences Research Council (EP/K008528/1)
The Boeing Company; EPSRC “REMS: Rigorous Engineering for Mainstream Systems” programme grant (EP/K008528); Leverhulme Trust Early Career Fellowship, Isaac Newton Trust; Nokia Bell Labs.