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 OctDisplayed time zone: Tijuana, Baja California change
13:30 - 15:00 | |||
13:30 22mTalk | Geo-Distribution of Actor-Based Services OOPSLA Philip A. Bernstein Microsoft Research, Sebastian Burckhardt Microsoft Research, Sergey Bykov Microsoft, n.n., Natacha Crooks University of Texas at Austin, USA, Jose Faleiro Yale University, USA, Gabriel Kliot Google, n.n., Alok Kumbhare Microsoft Research, n.n., Muntasir Raihan Rahman Microsoft, Vivek Shah University of Copenhagen, Denmark, Adriana Szekeres University of Washington, USA, Jorgen Thelin Microsoft Research, Redmond DOI | ||
13:52 22mTalk | Paxos Made EPR: Decidable Reasoning about Distributed Protocols OOPSLA Oded Padon Tel Aviv University, Giuliano Losa University of California at Los Angeles, USA, Mooly Sagiv Tel Aviv University, Sharon Shoham Tel Aviv university DOI | ||
14:15 22mTalk | Verifying Strong Eventual Consistency in Distributed Systems OOPSLA Victor B. F. Gomes University of Cambridge, UK, Martin Kleppmann University of Cambridge, Dominic P. Mulligan University of Cambridge, Alastair R. Beresford University of Cambridge, UK DOI | ||
14:37 22mTalk | Verifying Distributed Programs via Canonical Sequentialization OOPSLA Alexander Bakst , Klaus v. Gleissenthall University of California at San Diego, USA, Ranjit Jhala University of California at San Diego, USA, Rami Gökhan Kıcı University of California at San Diego, USA DOI | ||