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.
prev up ariadne tutorial