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 an implementation and demonstrate its value by testing a number of benchmark programs using parallel assertions. We discuss the challenges of evaluating assertions in the presence of weak memory models, and show how ongoing work to formalize the semantics under weak memory models lead to an optimization that gives a 2x speedup while allowing more bugs to be expressed.
Daniel Schwartz-Narbonne received his BS in Engineering Science (Physics Option) from the University of Toronto in 2006. Since then, he has been a PhD student at Princeton University, working to provide hardware and software designers with the tools they need to manage increasing concurrency and develop correct programs. His work is partially funded by a NSERC grant.