-
Notifications
You must be signed in to change notification settings - Fork 6
Description
When DPOR dictates that a backtracking point is needed, McMini is required to fork itself in order to generate a new "clean-slate" process whose execution it can guide according to the trace leading up to the backtracking point. Currently, McMini regenerates this process through a simple traversal through the transition stack trace, serially running each thread in the target program until it hits the backtracking point.
Such serial execution, while essential when expanding the current backtracking trace, it is unnecessary for_regenerating_ program states. Since DPOR implicitly tracks dependencies between all transitions in the current trace, we can exploit this information to allow threads we know to be independent with each other to run concurrently in the target program. Thus, instead of a single thread running at each step in the regeneration cycle, we could allow several independent threads to run in parallel and wait for all of their executions to finish (almost like a barrier). We could determine which groups of threads to run concurrently using a topological sort of the dependency graph.
We may even be able to exploit knowing the entire dependency graph a priori and use e.g. a shared-memory condition variable to prevent needing to coordinate with the scheduler process (i.e. block), although this may not give us any additional benefit