Reasoning About Eventual Consistency with Replicated Data Types (Alexey Gotsman – IMDEA Software Institute)

HASLab Seminar

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). The associated paper appeared in POPL’14:
http://software.imdea.org/~gotsman/papers/distrmm-popl14.pdf

Advertisements

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s