Ben Blum
Carnegie Mellon University
The Iterative Deepening algorithm allows stateless model checkers to adjust preemption points on-the-fly. It uses dynamic data-race detection to avoid necessarily preempting on every shared memory access, and ignores false-positive data race candidates arising from certain heap allocation patterns. An Iterative Deepening test that reaches completion soundly verifies all possible thread interleavings of that test.
KEYWORDS: concurrency, stateless model checking, data race analysis, verification
FULL TR: pdf