From 29fc93df5d19fd8fdf5d52359726988ed5d4fe83 Mon Sep 17 00:00:00 2001 From: Maxwell Pirtle Date: Tue, 16 May 2023 09:39:15 +0200 Subject: [PATCH] Add more docmentation for get_first_sdpor_initial() A very important function at the center of SDPOR was missing significant context that would help a reader understand what exactly was going on with the function. What makes the situation tricky is the fact that the pseudocode's implementation is blended into several lines and computed "on the fly" rather than fully. --- src/mc/explo/DFSExplorer.cpp | 2 +- src/mc/explo/odpor/ClockVector_test.cpp | 45 +++++++++++++++--- src/mc/explo/odpor/Execution.cpp | 15 ++++-- src/mc/explo/odpor/Execution.hpp | 40 +++++++++++----- src/mc/explo/odpor/Execution_test.cpp | 63 +++++++++++++++++++++++++ 5 files changed, 139 insertions(+), 26 deletions(-) diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp index 3e9e5199fe..e7738b58e4 100644 --- a/src/mc/explo/DFSExplorer.cpp +++ b/src/mc/explo/DFSExplorer.cpp @@ -286,7 +286,7 @@ void DFSExplorer::run() if (prev_state->is_actor_enabled(p)) { // NOTE: To incorporate the idea of attempting to select the "best" // backtrack point into SDPOR, instead of selecting the `first` initial, - // we should instead compute all choices and decide which is bes + // we should instead compute all choices and decide which is best const std::optional q = execution_seq_.get_first_sdpor_initial_from(racing_event_handle, prev_state->get_backtrack_set()); if (q.has_value()) { diff --git a/src/mc/explo/odpor/ClockVector_test.cpp b/src/mc/explo/odpor/ClockVector_test.cpp index da266b03a9..9d49c60309 100644 --- a/src/mc/explo/odpor/ClockVector_test.cpp +++ b/src/mc/explo/odpor/ClockVector_test.cpp @@ -10,14 +10,45 @@ using namespace simgrid::mc; TEST_CASE("simgrid::mc::ClockVector: Constructing Vectors") { - ClockVector cv; - REQUIRE(cv.size() == 0); + SECTION("Without values") + { + ClockVector cv; + REQUIRE(cv.size() == 0); + + // Verify `cv` doesn't map any values + REQUIRE_FALSE(cv.get(0).has_value()); + REQUIRE_FALSE(cv.get(1).has_value()); + REQUIRE_FALSE(cv.get(2).has_value()); + REQUIRE_FALSE(cv.get(3).has_value()); + } - // Verify `cv` doesn't map any values - REQUIRE_FALSE(cv.get(0).has_value()); - REQUIRE_FALSE(cv.get(1).has_value()); - REQUIRE_FALSE(cv.get(2).has_value()); - REQUIRE_FALSE(cv.get(3).has_value()); + SECTION("With initial values") + { + ClockVector cv{ + {1, 5}, {3, 1}, {7, 10}, {6, 5}, {8, 1}, {10, 10}, + }; + REQUIRE(cv.size() == 6); + + // Verify `cv` maps each value + REQUIRE(cv.get(1).has_value()); + REQUIRE(cv.get(1).value() == 5); + REQUIRE(cv[1] == 5); + REQUIRE(cv.get(3).has_value()); + REQUIRE(cv.get(3).value() == 1); + REQUIRE(cv[3] == 1); + REQUIRE(cv.get(7).has_value()); + REQUIRE(cv.get(7).value() == 10); + REQUIRE(cv[7] == 10); + REQUIRE(cv.get(6).has_value()); + REQUIRE(cv.get(6).value() == 5); + REQUIRE(cv[6] == 5); + REQUIRE(cv.get(8).has_value()); + REQUIRE(cv.get(8).value() == 1); + REQUIRE(cv[8] == 1); + REQUIRE(cv.get(10).has_value()); + REQUIRE(cv.get(10).value() == 10); + REQUIRE(cv[10] == 10); + } } TEST_CASE("simgrid::mc::ClockVector: Testing operator[]") diff --git a/src/mc/explo/odpor/Execution.cpp b/src/mc/explo/odpor/Execution.cpp index f3b44e74fb..d190a72a1f 100644 --- a/src/mc/explo/odpor/Execution.cpp +++ b/src/mc/explo/odpor/Execution.cpp @@ -24,11 +24,6 @@ void Execution::push_transition(const Transition* t) contents_.push_back(Event({t, max_clock_vector})); } -void Execution::pop_latest() -{ - contents_.pop_back(); -} - std::unordered_set Execution::get_racing_events_of(Execution::EventHandle target) const { std::unordered_set racing_events; @@ -89,6 +84,16 @@ std::optional Execution::get_first_sdpor_initial_from(EventHandle e, return std::nullopt; } + // To actually compute `I_[E'](v) ∩ backtrack(E')`, we must + // first compute `E'` and "move" in the direction of `v`. + // We perform a scan over `E` (this execution) and make + // note of any events which occur after `e` but don't + // "happen-after" `e` by pushing them onto `E'`. Note that + // correctness is still preserved in computing `v` "on-the-fly" + // to determine if an actor `q` is an initial for `E'` after `v`: + // only those events that "occur-before" `v` + // could happen-before `v` for any valid happens-before relation. + // First, grab `E' := pre(e, E)` and determine what actor `p` is // TODO: Instead of copying around these big structs, it // would behoove us to incorporate some way to reference diff --git a/src/mc/explo/odpor/Execution.hpp b/src/mc/explo/odpor/Execution.hpp index 6013d216eb..dca1c5df74 100644 --- a/src/mc/explo/odpor/Execution.hpp +++ b/src/mc/explo/odpor/Execution.hpp @@ -111,20 +111,44 @@ public: /** * @brief Computes the "core" portion the SDPOR algorithm, * viz. the intersection of the backtracking set and the - * set of initials with respect to the end + * set of initials with respect to the *last* event added + * to the execution + * + * The "core" portion of the SDPOR algorithm is found on + * lines 6-9 of the pseudocode: + * + * 6 | let E' := pre(E, e) + * 7 | let v := notdep(e, E).p + * 8 | if I_[E'](v) ∩ backtrack(E') = empty then + * 9 | --> add some q in I_[E'](v) to backtrack(E') + * + * This method computes all of the lines simultaneously, + * returning some actor `q` if it passes line 8 and exists. + * The event `e` and the set `backtrack(E')` are the provided + * arguments to the method. + * + * @param e the event with respect to which to determine + * whether a backtrack point needs to be added for the + * prefix corresponding to the execution prior to `e` + * + * @param backtrack_set The set of actors which should + * not be considered for selection as an SDPOR initial. + * While this set need not necessarily correspond to the + * backtrack set `backtrack(E')`, doing so provides what + * is expected for SDPOR * * See the SDPOR algorithm pseudocode in [1] for more * details for the context of the function. * * @invariant: This method assumes that events `e` and * `e' := get_latest_event_handle()` are in a *reversible* race - * as is the case in SDPOR + * as is explicitly the case in SDPOR * * @returns an actor not contained in `disqualified` which * can serve as an initial to reverse the race between `e` * and `e'` */ - std::optional get_first_sdpor_initial_from(EventHandle e, std::unordered_set disqualified) const; + std::optional get_first_sdpor_initial_from(EventHandle e, std::unordered_set backtrack_set) const; /** * @brief Determines the event associated with @@ -200,16 +224,6 @@ public: */ bool happens_before(EventHandle e1, EventHandle e2) const; - /** - * @brief Removes the last event of the execution, - * if such an event exists - * - * @note: When you remove events from an execution, any views - * of the execution referring to those removed events - * become invalidated - */ - void pop_latest(); - /** * @brief Extends the execution by one more step * diff --git a/src/mc/explo/odpor/Execution_test.cpp b/src/mc/explo/odpor/Execution_test.cpp index d8d3bb320f..8d2f014978 100644 --- a/src/mc/explo/odpor/Execution_test.cpp +++ b/src/mc/explo/odpor/Execution_test.cpp @@ -199,6 +199,7 @@ TEST_CASE("simgrid::mc::odpor::Execution: Testing Racing Events and Initials") SECTION("Example 3: Testing 'Lock' Example") { + // In this example, const auto a1 = std::make_shared(Transition::Type::UNKNOWN, 2); const auto a2 = std::make_shared(Transition::Type::UNKNOWN, 2); const auto a3 = std::make_shared(Transition::Type::UNKNOWN, 2); @@ -214,4 +215,66 @@ TEST_CASE("simgrid::mc::odpor::Execution: Testing Racing Events and Initials") REQUIRE(execution.get_racing_events_of(4) == std::unordered_set{0}); } + + SECTION("Example 4: Indirect Races") + { + const auto a0 = std::make_shared(Transition::Type::UNKNOWN, 1); + const auto a1 = std::make_shared(Transition::Type::UNKNOWN, 2); + const auto a2 = std::make_shared(Transition::Type::UNKNOWN, 1); + const auto a3 = std::make_shared(Transition::Type::UNKNOWN, 1); + const auto a4 = std::make_shared(Transition::Type::UNKNOWN, 6); + const auto a5 = std::make_shared(Transition::Type::UNKNOWN, 2); + const auto a6 = std::make_shared(Transition::Type::UNKNOWN, 3); + const auto a7 = std::make_shared(Transition::Type::UNKNOWN, 3); + const auto a8 = std::make_shared(Transition::Type::UNKNOWN, 4); + const auto a9 = std::make_shared(Transition::Type::UNKNOWN, 2); + + Execution execution; + execution.push_transition(a0.get()); + execution.push_transition(a1.get()); + execution.push_transition(a2.get()); + execution.push_transition(a3.get()); + execution.push_transition(a4.get()); + execution.push_transition(a5.get()); + execution.push_transition(a6.get()); + execution.push_transition(a7.get()); + execution.push_transition(a8.get()); + execution.push_transition(a9.get()); + + // Nothing comes before event 0 + REQUIRE(execution.get_racing_events_of(0) == std::unordered_set{}); + + // Events 0 and 1 are independent + REQUIRE(execution.get_racing_events_of(1) == std::unordered_set{}); + + // Events 1 and 2 are independent + REQUIRE(execution.get_racing_events_of(2) == std::unordered_set{}); + + // Events 1 and 3 are independent; the rest are executed by the same actor + REQUIRE(execution.get_racing_events_of(3) == std::unordered_set{}); + + // 1. Events 3 and 4 race + // 2. Events 2 and 4 do NOT race since 2 --> 3 --> 4 + // 3. Events 1 and 4 do NOT race since 1 is independent of 4 + // 4. Events 0 and 4 do NOT race since 0 --> 2 --> 4 + REQUIRE(execution.get_racing_events_of(4) == std::unordered_set{3}); + + // Events 4 and 5 race; and because everyone before 4 (including 3) either + // a) happens-before, b) races, or c) does not race with 4, 4 is the race + REQUIRE(execution.get_racing_events_of(5) == std::unordered_set{4}); + + // The same logic that applied to event 5 applies to event 6 + REQUIRE(execution.get_racing_events_of(6) == std::unordered_set{5}); + + // The same logic applies, except that this time since events 6 and 7 are run + // by the same actor, they don'tt actually race with one another + REQUIRE(execution.get_racing_events_of(7) == std::unordered_set{}); + + // Event 8 is independent with everything + REQUIRE(execution.get_racing_events_of(8) == std::unordered_set{}); + + // Event 9 is independent with events 7 and 8; event 6, however, is in race with 9. + // The same logic above eliminates events before 6 + REQUIRE(execution.get_racing_events_of(9) == std::unordered_set{6}); + } } \ No newline at end of file -- 2.20.1