Understanding Eventual Consistency
Sebastian Burckhardt, Alexey Gotsman, Hongseok Yang · 2013
Modern geo-replicated databases underlying large-scale In- ternet services guarantee immediate availability and tolerate network partitions at the expense of providing only weak forms of consistency, commonly dubbed eventual consistency. At the moment there is a lot of confusion about the semantics of eventual consistency, as different systems implement it with different sets of features and in subtly dif- ferent forms, stated either informally or using disparate and low-level formalisms. We address this problem by proposing a framework for formal and declarative specification of the semantics of eventually consistent sys- tems using axioms. Our framework is fully customisable: by varying the set of axioms, we can rigorously define the semantics of systems that combine any subset of typical guarantees or features, including conflict resolution policies, session guarantees, causality guarantees, multiple consistency levels and transactions. We prove that our speci- fications are validated by an example abstract implementation, based on algorithms used in real-world systems. These results demonstrate that our framework provides system architects with a tool for explor- ing the design space, and lays the foundation for formal reasoning about eventually consistent systems.