From 8f063c752da6a7adf2f8c36f94269bc63807dd18 Mon Sep 17 00:00:00 2001 From: Maxwell Pirtle Date: Thu, 4 May 2023 14:29:44 +0200 Subject: [PATCH] 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 --- src/mc/explo/DFSExplorer.cpp | 13 ++++++++----- src/mc/explo/odpor/Execution.cpp | 2 ++ src/mc/explo/odpor/Execution.hpp | 2 ++ src/mc/explo/odpor/Execution_test.cpp | 24 +++++++++++++++++++++++- 4 files changed, 35 insertions(+), 6 deletions(-) diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp index 3f44ee29bf..325915a723 100644 --- a/src/mc/explo/DFSExplorer.cpp +++ b/src/mc/explo/DFSExplorer.cpp @@ -93,14 +93,17 @@ void DFSExplorer::restore_stack(std::shared_ptr 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 fe493cf194..fe84056636 100644 --- a/src/mc/explo/odpor/Execution.cpp +++ b/src/mc/explo/odpor/Execution.cpp @@ -102,6 +102,8 @@ std::optional Execution::get_first_ssdpor_initial_from(EventHandle e, Execution E_prime_v = get_prefix_up_to(e); std::vector 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 672788edf6..b0f7c2df02 100644 --- 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 get_first_ssdpor_initial_from(EventHandle e, std::unordered_set disqualified) const; std::unordered_set get_ssdpor_initials_from(EventHandle e, std::unordered_set disqualified) const; diff --git a/src/mc/explo/odpor/Execution_test.cpp b/src/mc/explo/odpor/Execution_test.cpp index e69a4f9f1f..9033557ff8 100644 --- 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{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{}); + REQUIRE(initial_wrt_event1.has_value()); + REQUIRE(initial_wrt_event1.value() == static_cast(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{}); + REQUIRE(initial_wrt_event2.has_value()); + REQUIRE(initial_wrt_event2.value() == static_cast(3)); + } } } \ No newline at end of file -- 2.20.1