26th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE 2018), November 4–9, 2018, Lake Buena Vista, FL, USA

Desktop Layout

Symbolic Execution and Constraint Solving
Research Papers
Concurrency Verification with Maximal Path Causality
Qiuping Yi and Jeff Huang
(Texas A&M University, USA)
Publisher's Version
Abstract: We present a technique that systematically explores the state spaces of concurrent programs across both the schedule space and the input space. The cornerstone is a new model called Maximal Path Causality (MPC), which captures all combinations of thread schedules and program inputs that reach the same path as one equivalency class, and generates a unique schedule+input combination to explore each path. Moreover, the exploration for different paths can be easily parallelized. Our extensive evaluation on both popular concurrency benchmarks and real-world C/C++ applications shows that MPC significantly improves the performance of existing techniques.


Time stamp: 2019-03-26T17:08:05+01:00