Parallel and Distributed Bounded Model Checking of Multi-threaded Programs
We introduce a structure-aware parallelisation technique for context-bounded analysis of concurrent programs. The key intuition consists in decomposing the set of concurrent traces into symbolic subsets that are separately explored by multiple instances of the same decision procedure running in parallel. Since the decision procedures do not cooperate but rather work on different partitions of the search space assigned upfront, the approach is naturally suited to distribution. We experiment with our technique on a selection of multi-threaded C programs known for being particularly hard to analyse. The experimental results show significant analysis speedups and excellent scalability, especially on the most complex programs and for large bounds. Our approach significantly outperforms parallel state-of-the-art solvers.
Tue 25 FebDisplayed time zone: Tijuana, Baja California change
10:55 - 12:35 | |||
10:55 25mTalk | On the fly MHP Analysis Main Conference | ||
11:20 25mTalk | Detecting and Reproducing Error-Code Propagation Bugs in MPI Implementations Main Conference Daniel DeFreez University of California, Davis, Antara Bhowmick University of California, Davis, Ignacio Laguna Lawrence Livermore National Laboratory, Cindy Rubio-González University of California, Davis | ||
11:45 25mTalk | Parallel and Distributed Bounded Model Checking of Multi-threaded Programs Main Conference | ||
12:10 25mTalk | Parallel Race Detection with Futures Main Conference Yifan Xu Washington University in St. Louis, Kyle Singer Washington University in St. Louis, I-Ting Angelina Lee Washington University in St. Louis |