Strong Eventual Consistency and Conflict-free Replicated Data Types

The Eventual Consistency (EC) approach, which does not restrict concurrent updates to replicas of an object, is essential to scalability of cloud computing. However, reconciling conflicts remains difficult, and published EC approaches are ad-hoc and error-prone; the literature offers little guidance on designing a correct EC system. Our model, Strong Eventual Consistency or SEC, is simple and theoretically sound: conflict freedom ensures safety and liveness despite any number of failures, thus providing a solution to the well-known CAP problem. We show some simple mathematical properties (monotonicity in a semi-lattice and/or commutativity) that ensure absence of conflict. In Conflict-free Replicated Data Types (CRDTs), updates are unsynchronised, and replicas provably converge to a correct common state. CRDTs remain responsive, available and scalable despite high network latency, faults, or disconnection. In this talk, we present sufficient conditions for SEC and a strong equivalence between the conditions. We show that SEC is incomparable to sequential consistency. We present some basic CRDTs, and study in depth advanced CRDTs such as sets, graphs, and a sequence CRDT for co-operative text editing.

Joint work with Nuno Preguiça, Carlos Baquero and Marek Zawirski