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 JunDisplayed time zone: Tijuana, Baja California change
16:00 - 17:40
|Asynchronous Programming, Analysis and Testing with State Machines|
Pantazis Deligiannis Imperial College London, Alastair F. Donaldson Imperial College London, Jeroen Ketema , Akash Lal Microsoft Research India, Paul Thomson Imperial College LondonMedia Attached
|Stateless Model Checking Concurrent Programs with Maximal Causality Reduction|
Jeff Huang Texas A&M UniversityMedia Attached
|Synthesizing racy tests|
Malavika Samak Indian Institute of Science, Bangalore, Murali Krishna Ramanathan Indian Institute of Science, Bangalore, Suresh Jagannathan Purdue UniversityMedia Attached
|The Push/Pull model of transactions|
Research PapersMedia Attached