Add workaround for subtlety with state regeneration

Regeneration of the Execution inside DFSExplorer
should be as simple as choosing the prefix relative
to the appropriate backtracking point. However,
it did not appear to function so simple. After
a good amount of debugging, it appears that
the stack contents can change unexpectedly so
(e.g. a transition "in the middle" of the stack
seemingly switches arbitrarily). Until we can
pinpoint the true cause here, we simple resort
to rebuilding the execution based off the new
stack each time we decide to backtrack. The
downside is that all clock vectors have to be
recomputed after each backtrack. For now,
this is something that's OK to live with,
especially considering that this certainly
won't be a bottle neck in performance

diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp
index 3f44ee2..325915a 100644 (file)
--- a/src/mc/explo/DFSExplorer.cpp
+++ b/src/mc/explo/DFSExplorer.cpp
@@ -93,14 +93,17 @@ void DFSExplorer::restore_stack(std::shared_ptr<State> state)
   }
   XBT_DEBUG("Replaced stack by %s", get_record_trace().to_string().c_str());
 
+  // TODO: See if we can simply take a prefix of what
+  // currently exists instead of performing a recomputation.
+  // There seems to be a subtlety here that at the moment
+  // I can't figure out
   if (reduction_mode_ == ReductionMode::sdpor) {
-    if (stack_.empty()) {
-      execution_seq_ = sdpor::Execution();
-    } else {
-      execution_seq_ = execution_seq_.get_prefix_up_to(stack_.size() - 1);
+    execution_seq_ = sdpor::Execution();
+    for (const auto& state : stack_) {
+      execution_seq_.push_transition(state->get_transition_out().get());
     }
-    XBT_DEBUG("Additionally replaced corresponding SDPOR execution stack");
   }
+  XBT_DEBUG("Additionally replaced corresponding SDPOR execution stack");
 }
 
 void DFSExplorer::log_state() // override

diff --git a/src/mc/explo/odpor/Execution.cpp b/src/mc/explo/odpor/Execution.cpp
index fe493cf..fe84056 100644 (file)
--- a/src/mc/explo/odpor/Execution.cpp
+++ b/src/mc/explo/odpor/Execution.cpp
@@ -102,6 +102,8 @@ std::optional<aid_t> Execution::get_first_ssdpor_initial_from(EventHandle e,
   Execution E_prime_v = get_prefix_up_to(e);
   std::vector<sdpor::Execution::EventHandle> v;
 
+  // Note `e + 1` here: `notdep(e, E)` is defined as the
+  // set of events that *occur-after* but don't *happen-after* `e`
   for (auto e_prime = e + 1; e_prime <= next_E_p; ++e_prime) {
     // Any event `e*` which occurs after `e` but which does not
     // happen after `e` is a member of `v`. In addition to marking

diff --git a/src/mc/explo/odpor/Execution.hpp b/src/mc/explo/odpor/Execution.hpp
index 672788e..b0f7c2d 100644 (file)
--- a/src/mc/explo/odpor/Execution.hpp
+++ b/src/mc/explo/odpor/Execution.hpp
@@ -94,6 +94,8 @@ public:
 
   size_t size() const { return this->contents_.size(); }
   bool empty() const { return this->contents_.empty(); }
+  auto begin() const { return this->contents_.begin(); }
+  auto end() const { return this->contents_.end(); }
 
   std::optional<aid_t> get_first_ssdpor_initial_from(EventHandle e, std::unordered_set<aid_t> disqualified) const;
   std::unordered_set<aid_t> get_ssdpor_initials_from(EventHandle e, std::unordered_set<aid_t> disqualified) const;

diff --git a/src/mc/explo/odpor/Execution_test.cpp b/src/mc/explo/odpor/Execution_test.cpp
index e69a4f9..9033557 100644 (file)
--- a/src/mc/explo/odpor/Execution_test.cpp
+++ b/src/mc/explo/odpor/Execution_test.cpp
@@ -17,6 +17,7 @@ TEST_CASE("simgrid::mc::odpor::Execution: Constructing Executions")
   Execution execution;
   REQUIRE(execution.empty());
   REQUIRE(execution.size() == 0);
+  REQUIRE_FALSE(execution.get_latest_event_handle().has_value());
 }
 
 TEST_CASE("simgrid::mc::odpor::Execution: Testing Happens-Before")
@@ -112,7 +113,7 @@ TEST_CASE("simgrid::mc::odpor::Execution: Testing Happens-Before")
   }
 }
 
-TEST_CASE("simgrid::mc::odpor::Execution: Testing Racing Events Initials")
+TEST_CASE("simgrid::mc::odpor::Execution: Testing Racing Events and Initials")
 {
   SECTION("Example 1")
   {
@@ -173,5 +174,26 @@ TEST_CASE("simgrid::mc::odpor::Execution: Testing Racing Events Initials")
 
     // All events are dependent with event 3, but event 0 "happens-before" event 2
     REQUIRE(execution.get_racing_events_of(3) == std::unordered_set<Execution::EventHandle>{1, 2});
+
+    SECTION("Check initials with respect to event 1")
+    {
+      // First, note that v := notdep(1, execution).p == {e2}.{e3} == {e2, e3}
+      // Since e2 -->_E e3, actor 3 is not an initial for E' := pre(1, execution)
+      // with respect to `v`. e2, however, has nothing happening before it in dom_E(v),
+      // so it is an initial of E' wrt. `v`
+      const auto initial_wrt_event1 = execution.get_first_ssdpor_initial_from(1, std::unordered_set<aid_t>{});
+      REQUIRE(initial_wrt_event1.has_value());
+      REQUIRE(initial_wrt_event1.value() == static_cast<aid_t>(1));
+    }
+
+    SECTION("Check initials with respect to event 2")
+    {
+      // First, note that v := notdep(1, execution).p == {}.{e3} == {e3}
+      // e3 has nothing happening before it in dom_E(v), so it is an initial
+      // of E' wrt. `v`
+      const auto initial_wrt_event2 = execution.get_first_ssdpor_initial_from(2, std::unordered_set<aid_t>{});
+      REQUIRE(initial_wrt_event2.has_value());
+      REQUIRE(initial_wrt_event2.value() == static_cast<aid_t>(3));
+    }
   }
 }
\ No newline at end of file