Correctness of Trap-Based Breakpoint Implementations (Abstract)
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.