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

http://www.pdl.cmu.edu/

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

 

 

 

© 2017. Last updated 6 September, 2016