A Framework for Establishing Strong Eventual Consistency for Conflict-Free Replicated Datatypes

Victor B. F. Gomes 📧, Martin Kleppmann 📧, Dominic P. Mulligan 📧 and Alastair R. Beresford 📧

July 7, 2017

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

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 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.
BSD License

Topics

Theories of CRDT

Used by