Stateless Model Checking Concurrent Programs with Maximal Causality Reduction
We present maximal causality reduction (MCR), a new technique for stateless model checking. MCR systematically explores the state-space of concurrent programs with a provably minimal number of executions. Each execution corresponds to a distinct maximal causal model extracted from a given execution trace, which captures the largest possible set of causally equivalent executions. Moreover, MCR is embarrassingly parallel by shifting the runtime exploration cost to offline analysis. We have designed and implemented MCR using a constraint-based approach and compared with iterative context bounding (ICB) and dynamic partial order reduction (DPOR) on both benchmarks and real-world programs. MCR reduces the number of executions explored by ICB and ICB+DPOR by orders of magnitude, and significantly improves the scalability, efficiency, and effectiveness of the state-of-the-art for both state-space exploration and bug finding. In our experiments, MCR has also revealed several new data races and null pointer dereference errors in frequently studied real-world programs.
Jeff Huang is currently an Assistant Professor in the Department of Computer Science and Engineering at Texas A&M University. His research focuses on developing techniques and tools for improving software performance and reliability based on fundamental program analyses and programming language theory. His research has won awards including ACM SIGSOFT Outstanding Dissertation Award, SIGPLAN PLDI Distinguished Paper Award, SIGPLAN Research Highlights, and Google Faculty Research Award.
Mon 15 Jun Times are displayed in time zone: Tijuana, Baja California change
|16:00 - 16:25|
|Asynchronous Programming, Analysis and Testing with State Machines|
Pantazis DeligiannisImperial College London, Alastair DonaldsonImperial College London, Jeroen Ketema, Akash LalMicrosoft Research India, Paul ThomsonImperial College LondonMedia Attached
|16:25 - 16:50|
|Stateless Model Checking Concurrent Programs with Maximal Causality Reduction|
Jeff HuangTexas A&M UniversityMedia Attached
|16:50 - 17:15|
|Synthesizing racy tests|
Malavika SamakIndian Institute of Science, Bangalore, Murali Krishna RamanathanIndian Institute of Science, Bangalore, Suresh JagannathanPurdue UniversityMedia Attached
|17:15 - 17:40|
|The Push/Pull model of transactions|
Research PapersMedia Attached