Correctness of Trap-Based Breakpoint Implementations (Abstract)

Norman Ramsey

It is common for debuggers to implement breakpoints by a combination of planting traps and single stepping. When the target program contains multiple threads of execution, a debugger that is not carefully implemented may miss breakpoints. This paper gives a formal model of a breakpoint in a two-threaded program. The model describes correct and incorrect breakpoint implementations. Automatic search of the model's state space shows that the correct implementation never misses a breakpoint. A similar search finds an execution for which the incorrect implementation does miss a breakpoint. The results apply even to debuggers like {\tt dbx} and {\tt gdb}, which are apparently for single-threaded programs; when the user evaluates an expression containing function calls, the debugger executes the call in the target address space, in effect creating a new thread.

The full paper is available in PostScript form. There is also an HTML version, which suffers from automatic conversion but which is less than one-third the size of the PostScript.