Stateless model checking with data-race preemption points

Tuesday March 1, 2016
Location: CIC Panther Hollow Room
Time: 4:30PM

Ben Blum (Carnegie Mellon University)


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 is prone to false positives: spurious reports of access pairs that cannot be reordered to produce a bug.

In this talk I will discuss Quicksand, a new technique and tool I have built to manage 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. In our evaluation, Quicksand found 1.8x as many bugs compared to stateless model checking without data-race preemption points.

I am planning to submit this research for OOPSLA's March 25th deadline, so any feedback from people experienced in either the research topic or the conference would be much appreciated.


Ben Blum is a 5th year Ph.D. student in the Parallel Data Lab under the advisorship of Garth Gibson.