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

We introduce canonical sequentialization, a new approach to verifying unbounded, asynchronous, message-passing programs at compile-time. Our approach builds upon the following observation: due the combinatorial explosion in complexity, programmers do not reason about their systems by case-splitting over all the possible execution orders. Instead, correct programs tend to be well-structured so that the programmer can reason about a small number of representative executions, which we call the program’s canonical sequentialization. We have implemented our approach in a tool called Brisk that synthesizes canonical sequentializations for programs written in Haskell, and evaluated it on a wide variety of distributed systems including benchmarks from the literature and implementations of MapReduce, two-phase commit, and a version of the Disco distributed file-system. We show that unlike model checking, which gets prohibitively slow with just 10 processes Brisk verifies the unbounded versions of the benchmarks in tens of milliseconds, yielding the first concurrency verification tool that is fast enough to be integrated into a design-implement-check cycle.

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