Verifying distributed programs via canonical sequentialization

被引：24

作者：

Bakst, Alexander ^{[1
]}

Gleissenthall, Klaus V. ^{[1
]}

Kici, Rami Gökhan ^{[1
]}

Jhala, Ranjit ^{[1
]}

机构：

[1] University of California, San Diego, United States

来源：

Proceedings of the ACM on Programming Languages | 2017年 / 1卷 / OOPSLA期

关键词：

File organization - Message passing;

D O I：

10.1145/3133934

中图分类号：

学科分类号：

摘要：

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. Brisk verifies 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. © 2017 Association for Computing Machinery.

引用