CITI has stopped operations in 2014, to co-launch NOVA LINCS THIS SITE IS NOT BEING UPDATED SINCE 2013
citi banner
Home Page FCT/UNL UNL
  Home  \  Seminars @ CITI  \  Seminar Page Login  
   
banner bottom
File Top
Reasoning about eventual consistency and replicated data types
{ Mon, 16 Jun 2014, 14h00 }

By: Alexey Gotsman  [ show info ]

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


Hosted by: Computer Systems

Location: DI seminars room

File Bottom