Blogs (9) >>
Sun 30 October - Fri 4 November 2016 Amsterdam, Netherlands
Thu 3 Nov 2016 11:20 - 11:45 at Matterhorn 1 - Concurrency Analysis and Model Checking Chair(s): Thomas Gross

Stateless model checking is a powerful technique for testing concurrent programs, but suffers from exponential state space explosion when the test input parameters are too large. Several reduction techniques can mitigate this explosion, but even after pruning equivalent interleavings, the state space size is often intractable. Most prior tools are limited to preempting only on synchronization APIs, which reduces the space further, but can miss unsynchronized thread communication bugs. Data race detection, another concurrency testing approach, focuses on suspicious memory access pairs during a single test execution. It avoids concerns of state space size, but may report races that do not lead to observable failures, which jeopardizes a user’s willingness to use the analysis.

We present Quicksand, a new stateless model checking framework which manages the exploration of many state spaces using different preemption points. It uses state space estimation to prioritize jobs most likely to complete in a fixed CPU budget, and it incorporates data-race analysis to add new preemption points on the fly. Preempting threads during a data race’s instructions can automatically classify the race as buggy or benign, and uncovers new bugs not reachable by prior model checkers. It also enables full verification of all possible schedules when every data race is verified as benign within the CPU budget. In our evaluation, Quicksand found 1.25x as many bugs and verified 4.3x as many tests compared to prior model checking approaches.

Thu 3 Nov
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:30 - 12:10: Concurrency Analysis and Model CheckingOOPSLA at Matterhorn 1
Chair(s): Thomas GrossETH Zurich
10:30 - 10:55
Directed Synthesis of Failing Concurrent Executions
Malavika SamakIndian Institute of Science, Bangalore, Omer TrippIBM Research, USA, Murali Krishna RamanathanIndian Institute of Science, Bangalore
DOI Media Attached
10:55 - 11:20
Maximal Causality Reduction for TSO and PSO
Shiyou HuangTexas A&M University, Jeff HuangTexas A&M University
11:20 - 11:45
Stateless Model Checking with Data-Race Preemption Points
Ben BlumCarnegie Mellon University, Garth GibsonCarnegie Mellon University
DOI Pre-print Media Attached
11:45 - 12:10
Precise and Maximal Race Detection from Incomplete Traces
Jeff HuangTexas A&M University, Arun Krishnakumar RajagopalanTexas A&M University
DOI Media Attached