Title: Reasoning about eventual consistency and replicated data types
By: Alexey Gotsman (IMDEA Software Institute)
Abstract:
Modern 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. Even though the folklore notion of eventual consistency is very weak, in reality, the semantics and programming interfaces of systems implementing it can be very subtle. In particular, such systems can resolve conflicting updates using complex protocols, called replicated data types (aka CRDTs), and can allow varying kinds of anomalous behaviour.
So far the semantics provided by eventually consistent systems have been poorly understood. I will present a novel framework for their formal specification and discuss how recent nontrivial replicated data type implementations fit into it. I will then illustrate the utility of the framework by presenting techniques for proving the correctness of replicated data type implementations.
This is joint work with Sebastian Burckhardt (Microsoft Research), Hongseok Yang (University of Oxford) and Marek Zawirski (INRIA & UPMC-LIP6).
Short bio:
Alexey Gotsman is a tenure-track Assistant Research Professor at the IMDEA Software Institute in Madrid, Spain. Before joining IMDEA, he was a postdoctoral fellow at the University of Cambridge, where he also got his Ph.D.
More info: http://citi.di.fct.unl.pt/seminar/seminar.php?id=232