Blogs (9) >>
SPLASH 2016
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

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:30 - 12:10
Concurrency Analysis and Model CheckingOOPSLA at Matterhorn 1
Chair(s): Thomas Gross ETH Zurich
10:30
25m
Talk
Directed Synthesis of Failing Concurrent Executions
OOPSLA
Malavika Samak Indian Institute of Science, Bangalore, Omer Tripp IBM Research, USA, Murali Krishna Ramanathan Indian Institute of Science, Bangalore
DOI Media Attached
10:55
25m
Talk
Maximal Causality Reduction for TSO and PSO
OOPSLA
Shiyou Huang Texas A&M University, Jeff Huang Texas A&M University
DOI
11:20
25m
Talk
Stateless Model Checking with Data-Race Preemption Points
OOPSLA
Ben Blum Carnegie Mellon University, Garth Gibson Carnegie Mellon University
DOI Pre-print Media Attached
11:45
25m
Talk
Precise and Maximal Race Detection from Incomplete Traces
OOPSLA
Jeff Huang Texas A&M University, Arun Krishnakumar Rajagopalan Texas A&M University
DOI Media Attached