Stateless model checking with data-race preemption points
Abstract
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.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Oct 19, 2016
- Source ID
- 10.1145/3022671.2984036
Entities
People
- Ben Blum
- Garth Gibson
Organizations
- Army Research Office
- Carnegie Mellon University