Interactive debugging of concurrent programs under relaxed memory models

Abstract

Programming environments for sequential programs provide strong debugging support. However, concurrent programs, especially under relaxed memory models, lack powerful interactive debugging tools. In this work, we present Gambit, an interactive debugging environment that uses gdb to run a concrete debugging session on a concurrent program, while employing a symbolic execution on the program trace in the background simultaneously. The symbolic execution is analysed by a theorem prover to answer queries from the programmer on possible scenarios resulting from alternate thread interleavings or due to reorderings on other relaxed memory models. Gambit can help programmers understand complex bug scenarios on alien environments, that is, when the program is deployed in the field under different concurrent schedulers and diverse memory models. While Gambit currently packages three memory models (PSO, TSO and SC) and provides support for constructs like fences and atomic blocks, the framework is extensible, allowing support for other memory models and programming constructs. We have evaluated Gambit on multiple programs and found that Gambit responds to the debug queries quite fast (about a second on an average across our benchmark programs).