Fix two minor bugs in the ODPOR implementation

This commit fixes the following two bugs:

1. When seeding a wakeup tree for the first
time, we forgot to add a `break` statement
to ensure that only one such enabled thread
were placed into the wakeup tree. Before
all such enabled threads were inserted which
amounted to what would have been a brute-force
search :(.

2. When determining whether a sequence is a
candidate for insertion into a wakeup tree,
we may need to check, for all enabled actors
in a given state, whether those actors'
next steps are independent with the sequence
theretofore constructed. This additional
step peforms the work needed to check whether
those actors are contained in the set of
*weak* initials. The method corresponds
to line 6 of the pseudocode of the ODPOR algorithm

diff --git a/src/mc/api/State.cpp b/src/mc/api/State.cpp
index 1680ca0..c8059b5 100644 (file)
--- a/src/mc/api/State.cpp
+++ b/src/mc/api/State.cpp
@@ -220,6 +220,7 @@ void State::seed_wakeup_tree_if_needed(const odpor::Execution& prior)
         for (unsigned times = 0; times < actor.get_max_considered(); ++times) {
           wakeup_tree_.insert(prior, odpor::PartialExecution{actor.get_transition(times)});
         }
+        break; // Only one actor gets inserted (see pseudocode)
       }
     }
   }
@@ -235,26 +236,31 @@ void State::sprout_tree_from_parent_state()
                                            "parent with an empty wakeup tree. This indicates either that ODPOR "
                                            "actor selection in State.cpp is incorrect, or that the code "
                                            "deciding when to make subtrees in ODPOR is incorrect");
-
-  // TODO: This assert should even be bolstered to check that the
-  // the transitions themselves are identical -- not only just
-  // that the actors are the same. When we have to consider
-  // multiple paths for a transition, things get trickier
-  xbt_assert(parent_state_->get_transition_out()->aid_ == min_process_node.value()->get_actor(),
-             "We tried to make a subtree from a parent state who claimed to have executed %ld "
-             "but whose wakeup tree indicates it should have executed %ld. This indicates "
+  xbt_assert((parent_state_->get_transition_out()->aid_ == min_process_node.value()->get_actor()) &&
+                 (parent_state_->get_transition_out()->type_ == min_process_node.value()->get_action()->type_),
+             "We tried to make a subtree from a parent state who claimed to have executed `%s` "
+             "but whose wakeup tree indicates it should have executed `%s`. This indicates "
              "that exploration is not following ODPOR. Are you sure you're choosing actors "
              "to schedule from the wakeup tree?",
-             parent_state_->get_transition_out()->aid_, min_process_node.value()->get_actor());
+             parent_state_->get_transition_out()->to_string(false).c_str(),
+             min_process_node.value()->get_action()->to_string(false).c_str());
   this->wakeup_tree_ = odpor::WakeupTree::make_subtree_rooted_at(min_process_node.value());
 }
 
 void State::remove_subtree_using_current_out_transition()
 {
   if (auto out_transition = get_transition_out(); out_transition != nullptr) {
-    // TODO: Add invariant check here
+    if (const auto min_process_node = wakeup_tree_.get_min_single_process_node(); min_process_node.has_value()) {
+      xbt_assert((out_transition->aid_ == min_process_node.value()->get_actor()) &&
+                     (out_transition->type_ == min_process_node.value()->get_action()->type_),
+                 "We tried to make a subtree from a parent state who claimed to have executed `%s` "
+                 "but whose wakeup tree indicates it should have executed `%s`. This indicates "
+                 "that exploration is not following ODPOR. Are you sure you're choosing actors "
+                 "to schedule from the wakeup tree?",
+                 out_transition->to_string(false).c_str(),
+                 min_process_node.value()->get_action()->to_string(false).c_str());
+    }
   }
-
   wakeup_tree_.remove_min_single_process_subtree();
 }
 

diff --git a/src/mc/api/State.hpp b/src/mc/api/State.hpp
index a015de9..7f0290b 100644 (file)
--- a/src/mc/api/State.hpp
+++ b/src/mc/api/State.hpp
@@ -122,6 +122,11 @@ public:
   {
     sleep_set_.insert_or_assign(t->aid_, Transition(t->type_, t->aid_, t->times_considered_));
   }
+  bool is_actor_sleeping(aid_t actor) const
+  {
+    return std::find_if(sleep_set_.begin(), sleep_set_.end(), [=](const auto& pair) { return pair.first == actor; }) !=
+           sleep_set_.end();
+  }
 
   /**
    * @brief Inserts an arbitrary enabled actor into the wakeup tree

diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp
index cdc31df..af2d8ba 100644 (file)
--- a/src/mc/explo/DFSExplorer.cpp
+++ b/src/mc/explo/DFSExplorer.cpp
@@ -186,6 +186,11 @@ void DFSExplorer::run()
     // in case we want to consider multiple states (eg. during backtrack)
     const aid_t next = reduction_mode_ == ReductionMode::odpor ? state->next_odpor_transition()
                                                                : std::get<0>(state->next_transition_guided());
+    xbt_assert(!state->is_actor_sleeping(next),
+               "We decided to schedule an actor (%ld) that is in the sleep set "
+               "of the current state. By definition, this should be impossible; "
+               "and yet it happened, somehow...",
+               next);
 
     if (next < 0) { // If there is no more transition in the current state, backtrack.
       XBT_VERB("%lu actors remain, but none of them need to be interleaved (depth %zu).", state->get_actor_count(),

diff --git a/src/mc/explo/odpor/Execution.cpp b/src/mc/explo/odpor/Execution.cpp
index 6b84b0f..3aa3df6 100644 (file)
--- a/src/mc/explo/odpor/Execution.cpp
+++ b/src/mc/explo/odpor/Execution.cpp
@@ -53,7 +53,7 @@ std::unordered_set<Execution::EventHandle> Execution::get_racing_events_of(Execu
       // 2. disqualified_events.count(e_j) > 0
       // then e_i --->_E target indirectly (either through
       // e_j directly, or transitively through e_j)
-      if (happens_before(e_i, e_j) and disqualified_events.count(e_j) > 0) {
+      if (disqualified_events.count(e_j) > 0 and happens_before(e_i, e_j)) {
         disqualified_events.insert(e_i);
         break;
       }
@@ -283,7 +283,8 @@ std::optional<PartialExecution> Execution::get_odpor_extension_from(EventHandle
   for (const auto& [aid, astate] : state_at_e.get_actors_list()) {
     // TODO: We have to be able to react appropriately here when adding new
     // types of transitions (multiple choices can be made :( )
-    if (sleeping_actors.count(aid) == 0 and pre_E_e.is_independent_with_execution_of(v, astate.get_transition(0))) {
+    if (astate.is_enabled() and sleeping_actors.count(aid) == 0 and
+        pre_E_e.is_independent_with_execution_of(v, astate.get_transition(0))) {
       return v;
     }
   }