PDL Abstract

Soundness Proofs for Iterative Deepening

Carnegie Mellon University Parallel Data Lab Technical Report CMU-PDL-16-103. September 2016.

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