PASSERT: A Tool for Debugging Parallel Programs [abstract] (SpringerLink, PDF)
Daniel Schwartz-Narbonne, Feng Liu, David I. August, and Sharad Malik
Proceedings of the 18th International Conference on Computer-Aided Verification (CAV), June 2012.
PASSERT is a new debugging tool for parallel programs which allows programmers
to express correctness criteria using a simple, expressive assertion language.
We demonstrate how these parallel assertions allow the detection and diagnosis
of real world concurrency bugs, detecting 14/17 bugs in an independently
selected set of bugs from open source software. We describe a runtime checker
which allows automatic checking of parallel assertions in C and C++ programs,
with a geometric mean of 6.6x overhead on a set of PARSEC benchmarks. We
improve performace by introducing a relaxed timing semantics for parallel
assertions, which better reflects real memory models, and exposes more bugs
with less overhead (geometric mean overhead 3.5x).