A Reversible Debugger for Imperative Parallel Programs with Contracts

We present a reversible debugger for imperative parallel programs with block structures. A program runs in the runtime of abstract machines executed concurrently, where each abstract machine has the instruction set both for forward executions and backward executions. In order to efficiently localize a defect, we annotate a program by contracts with expects and ensures as C++ contracts. When a condition at ensures is violated, there exists some defect. Then, the reversible runtime traces back to the last ensure annotation and check the configuration to find out the source of the problem. By repeating this process, it is possible to localize the defect efficiently, preserving the environment of that particular execution. For controlling executions of parallel blocks, annotations are with the condition expressions of blocks running in parallel and those for variables. We illustrate the debugging process by presenting a prototype implementation by Python.