IMDEA Software

IMDEA initiative

Home > Events > Software Seminar Series > 2013 > Understanding Eventual Consistency

Alexey Gotsman

Tuesday, February 12, 2013

11:00am Meeting room 302 (Mountain View), level 3

Alexey Gotsman, Assistant Research Professor, IMDEA Software Institute

Understanding Eventual Consistency

Abstract:

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 with different sets of features and in subtly different 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 systems 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 specifications 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 exploring the design space, and lays the foundation for formal reasoning about eventually consistent systems. This is joint work with Sebastian Burckhardt (Microsoft Research) and Hongseok Yang (University of Oxford).