Introduce SDPOR and ODPOR into Simgrid
Overview
This MR introduces an implementation of ODPOR into Simgrid, as well as a version of SDPOR. You can now tap into the two model checkers with the model-checker/reduction
configuration with --config=model-checker/reduction:odpor
and --config=model-checker/reduction:sdpor
respectively.
Changes
There are a number of large changes in this MR:
- A new directory
src/mc/explo/odpor
was added containing a number of different classes used for both ODPOR and SDPOR.
- The
Execution
class was added to represent the concept bearing the same name in the ODPOR paper. TheExecution
intuitively represents a sequence of steps taken by a program. Importantly, it internally manages a “happens-before” relation over the sequence of transitions using clock vectors. The "happens-before" relation is important in many places in SDPOR and ODPOR, which is the primary reason a dedicated class was added. As new transitions are recorded, clock vectors are computed as appropriate. This allows us to determine “happens-before” in constant-time between points in the execution (called events [which is unfortunately the same name used in UDPOR for a slightly different concept]) — albeit for an up-front cost of traversing the execution stack — and is exactly as described in Section 4 of the original DPOR paper. - The
WakeupTree
class also represents the concept bearing the same name in the ODPOR paper. EachState
now contains aWakeupTree
whichDFSExplorer
manipulates as it performs its search. The trees can be iterated over in post-fix order using theWakeupTreeIterator
and contain methods for specific portions of the ODPOR pseudocode as outlined in their documentation. Note that aWakeupTree
does not maintain a reference to anExecution
, even though they are technically defined with respect to one. This is to prevent having a large number of amount of copies ofExecution
. It may be possible in the future to introduce anExecutionView
or equivalent which would allow a single execution (viz. that ofDFSExplorer
) to have portions of it "shared" to each tree with low cost. Instead,DFSExplorer
will provide its own execution off of which the tree can base its computations.
-
The backtracking portion of
DFSExplorer
now contains a check for SDPOR and adds backtrack points according to the pseudocode described in the ODPOR paper (viz. the first SDPOR algorithm which assumes a computation model under which an action stays enabled once enabled). When run with SDPOR,DFSExplorer
maintains an execution sequence by pushing the latest transitions executed by the application into it.DFSExplorer
'sExecution
instance is then regenerated when a backtrack point is explored, at the same time as the stack of states is regenerated.DFSExplorer
also has specific methods for selecting ODPOR-specific execution paths. The SDPOR algorithm is a rather “minimal” addition: we simply modify the way in which we choose threads when backtracking. ODPOR’s structure is different enough that we needed to add a few special methods (e.g.DFSExplorer::next_odpor_state()
) and change where backtracking occurs for ODPOR (insideDFSExplorer::backtrack()
when we have a full execution). -
Sleep sets now contain pointers to transitions instead of simply a
Transition
. The prior implementation stored only theTransition
sub-object slice of each transition that was inserted which meant that the implementation was incorrect (since aTransition
always says it is dependent with everything else and, further, other transitions might say they’re independent with a rawTransition
object). Note this resulted in changes to the outputs in the teshsuite. -
Several
depends()
methods were corrected. Note this resulted in changes to the outputs in the teshsuite.
-
ActorJoin
is now dependent with any transition executed by theActorJoin
’s target. - All actions are dependent if they are executed by the same actor.
For Reviewers
- Verify that the changes in the
teshsuite
are sensible. Since we changed the dependency relations and sleep sets, several teshsuite tests had different outputs. Any "large" changes probably are attributed to the sleep set implementation. Keep in mind though that these are small examples: only on large examples would we expect to see a very obvious correctness issue. - Whether state equality can be used with ODPOR I don’t know; we may want to prevent backtracking in this case unless we can show we’d maintain correctness (since it wouldn’t technically be a full execution if there were more enabled actors in the state that we noticed had been visited) by stopping the execution early and backtracking.
- Many of the methods of
Execution
andWakeupTree
are a bit complicated. Please identify whether you think they are unclear are not tested thoroughly enough. - Note that a decent amount of the diff can be attributed to changes in the
teshsuite
output and the unit test files, but there is still a large amount of content to understand.
Verifying the correctness of the implementations of ODPOR/SDPOR themselves is very difficult. We should consider adding more test cases as stress tests on the model checking algorithms to see how well they perform or if they can still identify more interesting bugs. Finally, I will be adding more tests as the review is underway and making changes here and there to fix up any remaining TODOs that don’t impede integration.