Consistent Breakpoints

In a sequential program, a breakpoint represents an intermediate state of the computation. In any program with multiple threads of control, the location of meaningful global states is problematic. This results from the fact that there is only a partial ordering of the individual states of each thread.

In Ariadne/AVE, this problem is solved by using Lamport's happened before relation to analyze the execution history and place breakpoints before or after abstract events. In this way, every thread is halted at the last point where it could have influenced another process of interest. This often allows the user to stop the program in states that would be difficult to specify using local state predicates.

After the program has been halted in a globally consistent state, debugging control can be passed to a state-based debugger, which can be used for fine-grained detection of errors in the source code. For more information on this topic, see Shende et al.

Ariadne tutorial