Assertions for Debugging Parallel Programs

Abstract

Software engineering is facing a crisis. For decades, computer programs doubled in speed every 18 months, enabling powerful new applications which have literally changed the way we communicate and think. However, the ever-increasing hardware speed that drove this exponential growth also led to an unsustainable increase in power consumption. Modern hardware attempts to side-step this problem by using many slow processors functioning in parallel. Unfortunately, our ability to develop and debug parallel software to take advantage of parallel hardware has not kept pace with the need. In order to reap the benefits offered by parallel computing, we require new tools.

In particular, 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. This dissertation introduces parallel assertions which allow programmers to express these assumptions for parallel programs using simple and intuitive syntax and semantics. I present an implementation and demonstrate its performance using PARSEC benchmarks. I discuss the challenges of evaluating assertions in the presence of weak memory models, and show how my work formalizing the semantics under weak memory models leads to an optimization that gives a 2x speedup while allowing more bugs to be exposed.

I measure the effectiveness of parallel assertions using the University of Michigan Collection of Concurrency Bugs. In 14/17 cases, I was able to write a parallel assertion that would detect the cause of the real-world bug. My research suggests that parallel assertions are a powerful and practical debugging tool.