Parallel Assertions for Debugging Parallel Programs [abstract] (IEEE Xplore, PDF)
Daniel Schwartz-Narbonne, Feng Liu, Tarun Pondicherry, David I. August, and Sharad Malik
2011 9th IEEE/ACM International Conference on Formal Methods and Models for Codesign (MEMOCODE), July 2011.
A parallel program must execute correctly even in the presence of unpredictable
thread interleavings. This interleaving makes it hard to write correct parallel
programs, and also makes it hard to find bugs in incorrect parallel programs. A
range of tools have been developed to help debug parallel programs, ranging
from atomicity-violation and data-race detectors to model-checkers and theorem
provers. One technique that has been successful for debugging sequential
programs, but less effective for parallel programs, is running the program
using assertion predicates provided by the developer. These assertions allow
programmers to specify and check their assumptions. In a multi-threaded
program, the programmer's assumptions include both the current state, and any
actions (e.g. access to shared memory) that other, parallel executing threads
might take. We introduce parallel assertions which allow programmers to express
these assumptions for parallel programs using simple and intuitive syntax and
semantics. We present a proof-of-concept implementation, and demonstrate its
value by testing a number of benchmark programs using parallel assertions.