Modern geo-replicated databases underlying large-scale Internet 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 in subtly different forms, stated using disparate and low-level formalisms. Additional difficulties arise from the use of special conflict resolution policies or combinations of different consistency levels. All this complicates the implementation and use of eventually consistent systems.
We address this problem by proposing a framework for formal and declarative specification of the semantics of eventually consistent systems by a set of axioms. We show that our framework can specify a range of existing consistency guarantees and conflict resolution policies. We also prove that our specifications are validated by an example abstract implementation, based on algorithms used in real-world systems. We illustrate the flexibility of our framework by showing how it can be used to specify the semantics of systems combining different consistency levels, as well as transactions. The framework provides developers of eventually consistent systems with a tool for exploring the design space and lays the foundation for formal reasoning about such systems.
This is joint work with Sebastian Burckhardt at Microsoft Research Redmond and Alexey Gotsman at IMDEA Software Institute.