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 Times are displayed in time zone: Tijuana, Baja California change
13:30 - 15:00: Distributed SystemsOOPSLA at Regency C Chair(s): Wolfgang De MeuterVrije Universiteit Brussel | |||
13:30 - 13:52 Talk | Geo-Distribution of Actor-Based Services OOPSLA 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 | ||
13:52 - 14:15 Talk | Paxos Made EPR: Decidable Reasoning about Distributed Protocols OOPSLA Oded PadonTel Aviv University, Giuliano LosaUniversity of California at Los Angeles, USA, Mooly SagivTel Aviv University, Sharon ShohamTel Aviv university DOI | ||
14:15 - 14:37 Talk | Verifying Strong Eventual Consistency in Distributed Systems OOPSLA Victor B. F. GomesUniversity of Cambridge, UK, Martin KleppmannUniversity of Cambridge, Dominic P. MulliganUniversity of Cambridge, Alastair R. BeresfordUniversity of Cambridge, UK DOI | ||
14:37 - 15:00 Talk | Verifying Distributed Programs via Canonical Sequentialization OOPSLA 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 |