Verifying strong eventual consistency in distributed systems
Open Access
- 12 October 2017
- journal article
- Published by Association for Computing Machinery (ACM) in Proceedings of the ACM on Programming Languages
- Vol. 1 (OOPSLA), 1-28
- https://doi.org/10.1145/3133933
Abstract
Data replication is used in distributed systems to maintain up-to-date copies of shared data across multiple computers in a network. However, despite decades of research, algorithms for achieving consistency in replicated systems are still poorly understood. Indeed, many published algorithms have later been shown to be incorrect, even some that were accompanied by supposed mechanised proofs of correctness. In this work, we focus on the correctness of Conflict-free Replicated Data Types (CRDTs), a class of algorithm that provides strong eventual consistency guarantees for replicated data. We develop a modular and reusable framework in the Isabelle/HOL interactive proof assistant for verifying the correctness of CRDT algorithms. We avoid correctness issues that have dogged previous mechanised proofs in this area by including a network model in our formalisation, and proving that our theorems hold in all possible network behaviours. Our axiomatic network model is a standard abstraction that accurately reflects the behaviour of real-world computer networks. Moreover, we identify an abstract convergence theorem, a property of order relations, which provides a formal definition of strong eventual consistency. We then obtain the first machine-checked correctness theorems for three concrete CRDTs: the Replicated Growable Array, the Observed-Remove Set, and an Increment-Decrement Counter. We find that our framework is highly reusable, developing proofs of correctness for the latter two CRDTs in a few hours and with relatively little CRDT-specific codeOther Versions
Funding Information
- Engineering and Physical Sciences Research Council (EP/K008528)
- Boeing
This publication has 64 references indexed in Scilit:
- Replicated abstract data types: Building blocks for collaborative applicationsJournal of Parallel and Distributed Computing, 2011
- Eventually consistentCommunications of the ACM, 2009
- An Approach to Ensuring Consistency in Peer-to-Peer Real-Time Group EditorsComputer Supported Cooperative Work (CSCW), 2006
- Formal design and verification of operational transformation algorithms for copies convergenceTheoretical Computer Science, 2006
- Formal Specification of a Web Services ProtocolElectronic Notes in Theoretical Computer Science, 2004
- Consistency maintenance in real-time collaborative graphics editing systemsACM Transactions on Computer-Human Interaction, 2002
- Achieving convergence, causality preservation, and intention preservation in real-time cooperative editing systemsACM Transactions on Computer-Human Interaction, 1998
- Logical time: capturing causality in distributed systemsComputer, 1996
- Consistency in a partitioned network: a surveyACM Computing Surveys, 1985
- Time, clocks, and the ordering of events in a distributed systemCommunications of the ACM, 1978