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

In this talk, I will present our framework for specifying various eventually consistent systems and reasoning about their correctness and performance. My explanation will not assume prior knowledge on eventual consistency, programming languages and verification. It will be mostly based on examples. If time permits, I will briefly sketch interesting research challenges regarding eventually consistent systems, which touch on multiple CS disciplines, such as systems, programming languages and algorithms.

This is joint work with Sebastian Burckhardt at Microsoft Research Redmond, Alexey Gotsman at IMDEA Software Institute and Marek Zawirski at INRIA & UPMC-LIP6.

Short bio

Dr Yang is a University Lecturer (corresponding to an Associate Professor in the US system) in the Department of Computer Science, University of Oxford; and a tutorial fellow at Worcester College. He received a PhD from University of Illinois at Urbana-Champaign, USA (2001), and was a postdoc in KAIST and Seoul National University (2001-2006). He held a lectureship (corresponding to an Assistant Professorship in the US system) at Queen Mary, University of London (2006-2011) until he joined Oxford. He was also an EPSRC Advanced Research Fellow from 2007 to 2012.

Resources

• talk slide