Mon 15 Jun 2015 16:25 - 16:50 at PLDI Main BLUE (Portland 254-255) - Concurrency I Chair(s): Santosh Nagarakatte

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 - 17:40
Concurrency IResearch Papers at PLDI Main BLUE (Portland 254-255)
Chair(s): Santosh NagarakatteRutgers University
16:00
25m
Talk
Asynchronous Programming, Analysis and Testing with State Machines
Research Papers
Pantazis DeligiannisImperial College London, Alastair DonaldsonImperial College London, Jeroen Ketema, Akash LalMicrosoft Research India, Paul ThomsonImperial College London
Media Attached
16:25
25m
Talk
Stateless Model Checking Concurrent Programs with Maximal Causality Reduction
Research Papers
Jeff HuangTexas A&M University
Media Attached
16:50
25m
Talk
Synthesizing racy tests
Research Papers
Malavika SamakIndian Institute of Science, Bangalore, Murali Krishna RamanathanIndian Institute of Science, Bangalore, Suresh JagannathanPurdue University
Media Attached
17:15
25m
Talk
The Push/Pull model of transactions
Research Papers
Eric KoskinenIBM TJ Watson Research Center, Matthew ParkinsonMicrosoft Research, UK
Media Attached