Write a Blog >>
Thu 21 Jan 2016 10:30 - 10:55 at Grand Bay North - Track 1: Foundations of distributed systems Chair(s): Mooly Sagiv

Today’s Internet services are often expected to stay available and render high responsiveness even in the face of site crashes and network partitions. Theoretical results state that causal consistency is one of the strongest consistency guarantees that is possible under these requirements, and many practical systems provide causally consistent key-value stores. In this paper, we present modular verification of causal consistency for replicated key-value store algorithms and their client programs. Specifically, we formulate separate correctness conditions for key-value store algorithms and for their clients. The interface between the two is a novel operational semantics for causal consistency. We have verified the causal consistency of two key-value store algorithms from the literature using a novel proof technique. We have also implemented a simple automatic model checker for the correctness of client programs. The two independently verified results for the algorithms and clients can be composed to conclude correctness of any of the programs when executed with any of the algorithms. We have developed and checked our framework in Coq, extracted it to OCaml and built executable stores.

Thu 21 Jan

Displayed time zone: Guadalajara, Mexico City, Monterrey change

10:30 - 12:10
Track 1: Foundations of distributed systemsResearch Papers at Grand Bay North
Chair(s): Mooly Sagiv Tel Aviv University
10:30
25m
Talk
Certified Causally Consistent Distributed Key-Value Stores
Research Papers
Media Attached
10:55
25m
Talk
'Cause I'm Strong Enough: Reasoning about Consistency Choices in Distributed Systems
Research Papers
Alexey Gotsman IMDEA, Hongseok Yang University of Oxford, UK, Carla Ferreira Universidade Nova Lisboa, Mahsa Najafzadeh UPMC & INRIA, Marc Shapiro Inria & LIP6
Media Attached
11:20
25m
Talk
A Program Logic for Concurrent Objects under Fair Scheduling
Research Papers
Hongjin Liang University of Science and Technology of China, Xinyu Feng University of Science and Technology of China
Media Attached
11:45
25m
Talk
PSync: a partially synchronous language for fault-tolerant distributed algorithms
Research Papers
Cezara Drăgoi INRIA, ENS, CNRS, Thomas A. Henzinger IST Austria, Damien Zufferey MIT
Link to publication DOI Pre-print Media Attached File Attached