Skip to content

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:

  1. 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. The Execution 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. Each State now contains a WakeupTree which DFSExplorer manipulates as it performs its search. The trees can be iterated over in post-fix order using the WakeupTreeIterator and contain methods for specific portions of the ODPOR pseudocode as outlined in their documentation. Note that a WakeupTree does not maintain a reference to an Execution, even though they are technically defined with respect to one. This is to prevent having a large number of amount of copies of Execution. It may be possible in the future to introduce an ExecutionView or equivalent which would allow a single execution (viz. that of DFSExplorer) 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.
  1. 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's Execution 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 (inside DFSExplorer::backtrack() when we have a full execution).

  2. Sleep sets now contain pointers to transitions instead of simply a Transition. The prior implementation stored only the Transition sub-object slice of each transition that was inserted which meant that the implementation was incorrect (since a Transition always says it is dependent with everything else and, further, other transitions might say they’re independent with a raw Transition object). Note this resulted in changes to the outputs in the teshsuite.

  3. 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 the ActorJoin’s target.
  • All actions are dependent if they are executed by the same actor.

For Reviewers

  1. 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.
  2. 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.
  3. Many of the methods of Execution and WakeupTree are a bit complicated. Please identify whether you think they are unclear are not tested thoroughly enough.
  4. 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.

Merge request reports