Debugging Multithreaded Programs as if They Were Sequential

Debugging multithread programs is extremely difficult because the basic assumption that underlies sequential program debugging, that is, the program behavior is deterministic under a fixed input, is no longer valid due to the nondeterminism attributed to thread scheduling. It is because the programs behavior is non-deterministic due to the nondeterminism of parallel execution, which makes debugging or testing multithreaded programs extremely difficult. In this paper, we propose a proactive debugging method to restore this basic assumption so that programmers can debug multithreaded programs as if they were sequential. Our approach is based on the synergistic integration of symbolic analysis and dynamic analysis techniques. In particular, symbolic analysis investigates the program behavior under the same input to search whether there is a thread schedule would trigger a bug or a not-yet-explored path. Dynamic analysis is to execute these new paths with the guide of the generated thread schedules, thereby further guiding the symbolic analysis. The net effect of applying this feedback loop is a systematic and complete coverage of the program behavior under a fixed test input. We implement the proposed approach in a prototype tool called proactive-debugger. Our experiments show that proactive-debugger outperforms both ESBMC and Maple, which are two powerful and well-known testing tools for failure detection in multithreaded programs.