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.

diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp
index 3e9e519..e7738b5 100644 (file)
--- 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,
         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<aid_t> q =
               execution_seq_.get_first_sdpor_initial_from(racing_event_handle, prev_state->get_backtrack_set());
           if (q.has_value()) {
           const std::optional<aid_t> 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 da266b0..9d49c60 100644 (file)
--- 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")
 {
 
 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[]")
 }
 
 TEST_CASE("simgrid::mc::ClockVector: Testing operator[]")

diff --git a/src/mc/explo/odpor/Execution.cpp b/src/mc/explo/odpor/Execution.cpp
index f3b44e7..d190a72 100644 (file)
--- 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}));
 }
 
   contents_.push_back(Event({t, max_clock_vector}));
 }
 

-void Execution::pop_latest()
-{
-  contents_.pop_back();
-}
-

 std::unordered_set<Execution::EventHandle> Execution::get_racing_events_of(Execution::EventHandle target) const
 {
   std::unordered_set<Execution::EventHandle> racing_events;
 std::unordered_set<Execution::EventHandle> Execution::get_racing_events_of(Execution::EventHandle target) const
 {
   std::unordered_set<Execution::EventHandle> racing_events;


@@ -89,6 +84,16 @@ std::optional<aid_t> Execution::get_first_sdpor_initial_from(EventHandle e,
     return std::nullopt;
   }
 
     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
   // 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 6013d21..dca1c5d 100644 (file)
--- 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
   /**
    * @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
    *
    * 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'`
    */
    *
    * @returns an actor not contained in `disqualified` which
    * can serve as an initial to reverse the race between `e`
    * and `e'`
    */

-  std::optional<aid_t> get_first_sdpor_initial_from(EventHandle e, std::unordered_set<aid_t> disqualified) const;
+  std::optional<aid_t> get_first_sdpor_initial_from(EventHandle e, std::unordered_set<aid_t> backtrack_set) const;

 
   /**
    * @brief Determines the event associated with
 
   /**
    * @brief Determines the event associated with


@@ -200,16 +224,6 @@ public:
    */
   bool happens_before(EventHandle e1, EventHandle e2) const;
 
    */
   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
    *
   /**
    * @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 d8d3bb3..8d2f014 100644 (file)
--- 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")
   {
 
   SECTION("Example 3: Testing 'Lock' Example")
   {

+    // In this example,

     const auto a1 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 2);
     const auto a2 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 2);
     const auto a3 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 2);
     const auto a1 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 2);
     const auto a2 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 2);
     const auto a3 = std::make_shared<IndependentAction>(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<Execution::EventHandle>{0});
   }
 
     REQUIRE(execution.get_racing_events_of(4) == std::unordered_set<Execution::EventHandle>{0});
   }

+
+  SECTION("Example 4: Indirect Races")
+  {
+    const auto a0 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
+    const auto a1 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 2);
+    const auto a2 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 1);
+    const auto a3 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
+    const auto a4 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 6);
+    const auto a5 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 2);
+    const auto a6 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 3);
+    const auto a7 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 3);
+    const auto a8 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 4);
+    const auto a9 = std::make_shared<ConditionallyDependentAction>(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<Execution::EventHandle>{});
+
+    // Events 0 and 1 are independent
+    REQUIRE(execution.get_racing_events_of(1) == std::unordered_set<Execution::EventHandle>{});
+
+    // Events 1 and 2 are independent
+    REQUIRE(execution.get_racing_events_of(2) == std::unordered_set<Execution::EventHandle>{});
+
+    // Events 1 and 3 are independent; the rest are executed by the same actor
+    REQUIRE(execution.get_racing_events_of(3) == std::unordered_set<Execution::EventHandle>{});
+
+    // 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<Execution::EventHandle>{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<Execution::EventHandle>{4});
+
+    // The same logic that applied to event 5 applies to event 6
+    REQUIRE(execution.get_racing_events_of(6) == std::unordered_set<Execution::EventHandle>{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<Execution::EventHandle>{});
+
+    // Event 8 is independent with everything
+    REQUIRE(execution.get_racing_events_of(8) == std::unordered_set<Execution::EventHandle>{});
+
+    // 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<Execution::EventHandle>{6});
+  }

 }
\ No newline at end of file
 }
\ No newline at end of file