Write a Blog >>
SPLASH 2017
Sun 22 - Fri 27 October 2017 Vancouver, Canada
Fri 27 Oct 2017 14:15 - 14:37 at Regency C - Distributed Systems Chair(s): Wolfgang De Meuter

Data replication is used in distributed systems to maintain up-to-date copies of shared data across multiple computers in a network. However, despite decades of research, algorithms for achieving consistency in replicated systems are still poorly understood. Indeed, many published algorithms have later been shown to be incorrect, even some that were accompanied by supposed mechanised proofs of correctness. In this work, we focus on the correctness of Conflict-free Replicated Data Types (CRDTs), a class of algorithm that provides strong eventual consistency guarantees for replicated data. We develop a modular and reusable framework in the Isabelle/HOL interactive proof assistant for verifying the correctness of CRDT algorithms. We avoid correctness issues that have dogged previous mechanised proofs in this area by including a network model in our formalisation, and proving that our theorems hold in all possible network behaviours. Our axiomatic network model is a standard abstraction that accurately reflects the behaviour of real-world computer networks. Moreover, we identify an abstract convergence theorem, a property of order relations, which provides a formal definition of strong eventual consistency. We then obtain the first machine-checked correctness theorems for three concrete CRDTs: the Replicated Growable Array, the Observed-Remove Set, and an Increment-Decrement Counter. We find that our framework is highly reusable, developing proofs of correctness for the latter two CRDTs in a few hours and with relatively little CRDT-specific code.

Fri 27 Oct

splash-2017-OOPSLA
13:30 - 15:00: OOPSLA - Distributed Systems at Regency C
Chair(s): Wolfgang De MeuterVrije Universiteit Brussel
splash-2017-OOPSLA150910380000013:30 - 13:52
Talk
Philip A. BernsteinMicrosoft Research, Sebastian BurckhardtMicrosoft Research, Sergey BykovMicrosoft, n.n., Natacha CrooksUniversity of Texas at Austin, USA, Jose FaleiroYale University, USA, Gabriel KliotGoogle, n.n., Alok KumbhareMicrosoft Research, n.n., Muntasir Raihan RahmanMicrosoft, Vivek ShahUniversity of Copenhagen, Denmark, Adriana SzekeresUniversity of Washington, USA, Jorgen ThelinMicrosoft Research, Redmond
DOI
splash-2017-OOPSLA150910515000013:52 - 14:15
Talk
Oded PadonTel Aviv University, Giuliano LosaUniversity of California at Los Angeles, USA, Mooly SagivTel Aviv University, Sharon ShohamTel Aviv university
DOI
splash-2017-OOPSLA150910650000014:15 - 14:37
Talk
Victor B. F. GomesUniversity of Cambridge, UK, Martin KleppmannUniversity of Cambridge, Dominic P. MulliganUniversity of Cambridge, Alastair R. BeresfordUniversity of Cambridge, UK
DOI
splash-2017-OOPSLA150910785000014:37 - 15:00
Talk
Alexander Bakst, Klaus v. GleissenthallUniversity of California at San Diego, USA, Ranjit JhalaUniversity of California at San Diego, USA, Rami Gökhan KıcıUniversity of California at San Diego, USA
DOI