Add first tests for "happens-before"

The happens-before relation is used
extensively by SDPOR and ODPOR during
their computations for determining what
executions should be searched next. This
commit introduces the first round of tests
for the happens-before relation on
artificially constructed executions

diff --git a/MANIFEST.in b/MANIFEST.in
index 5bcbb34..8912990 100644 (file)
--- a/MANIFEST.in
+++ b/MANIFEST.in
@@ -2191,6 +2191,7 @@ include src/mc/explo/LivenessChecker.cpp
 include src/mc/explo/LivenessChecker.hpp
 include src/mc/explo/odpor/Execution.cpp
 include src/mc/explo/odpor/Execution.hpp
+include src/mc/explo/odpor/Execution_test.cpp
 include src/mc/explo/UdporChecker.cpp
 include src/mc/explo/UdporChecker.hpp
 include src/mc/explo/simgrid_mc.cpp

diff --git a/src/mc/explo/odpor/Execution.cpp b/src/mc/explo/odpor/Execution.cpp
index 1bc01d8..fe493cf 100644 (file)
--- a/src/mc/explo/odpor/Execution.cpp
+++ b/src/mc/explo/odpor/Execution.cpp
@@ -102,7 +102,7 @@ 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;
 
-  for (auto e_prime = e; e_prime <= next_E_p; ++e_prime) {
+  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
     // the event in `v`, we also "simulate" running the action `v`
@@ -137,8 +137,9 @@ std::unordered_set<aid_t> Execution::get_ssdpor_initials_from(EventHandle e,
 
 bool Execution::happens_before(Execution::EventHandle e1_handle, Execution::EventHandle e2_handle) const
 {
-  // 1. "happens-before" is a subset of "occurs before"
-  if (e1_handle > e2_handle) {
+  // 1. "happens-before" (-->_E) is a subset of "occurs before" (<_E)
+  // and is an irreflexive relation
+  if (e1_handle >= e2_handle) {
     return false;
   }
 
@@ -146,7 +147,15 @@ bool Execution::happens_before(Execution::EventHandle e1_handle, Execution::Even
   // according to the procedure outlined in section 4 of the original DPOR paper
   const Event& e2     = get_event_with_handle(e2_handle);
   const aid_t proc_e1 = get_actor_with_handle(e1_handle);
-  return e1_handle <= e2.get_clock_vector().get(proc_e1).value_or(0);
+
+  if (const auto e1_in_e2_clock = e2.get_clock_vector().get(proc_e1); e1_in_e2_clock.has_value()) {
+    return e1_handle <= e1_in_e2_clock.value();
+  }
+  // If `e1` does not appear in e2's clock vector, this implies
+  // not only that the transitions associated with `e1` and `e2
+  // are independent, but further that there are no transitive
+  // dependencies between e1 and e2
+  return false;
 }
 
 } // namespace simgrid::mc::odpor
\ No newline at end of file

diff --git a/src/mc/explo/odpor/Execution_test.cpp b/src/mc/explo/odpor/Execution_test.cpp
new file mode 100644 (file)
index 0000000..e69a4f9
--- /dev/null
+++ b/src/mc/explo/odpor/Execution_test.cpp
@@ -0,0 +1,177 @@
+/* Copyright (c) 2017-2023. The SimGrid Team. All rights reserved.               */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#include "src/3rd-party/catch.hpp"
+#include "src/mc/explo/odpor/Execution.hpp"
+#include "src/mc/explo/udpor/udpor_tests_private.hpp"
+#include "src/mc/transition/TransitionComm.hpp"
+
+using namespace simgrid::mc;
+using namespace simgrid::mc::odpor;
+using namespace simgrid::mc::udpor;
+
+TEST_CASE("simgrid::mc::odpor::Execution: Constructing Executions")
+{
+  Execution execution;
+  REQUIRE(execution.empty());
+  REQUIRE(execution.size() == 0);
+}
+
+TEST_CASE("simgrid::mc::odpor::Execution: Testing Happens-Before")
+{
+  SECTION("Example 1")
+  {
+    // We check each permutation for happens before
+    // among the given actions added to the execution
+    const auto a1 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
+    const auto a2 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 2);
+    const auto a3 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 3);
+    const auto a4 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 4);
+
+    Execution execution;
+    execution.push_transition(a1.get());
+    execution.push_transition(a2.get());
+    execution.push_transition(a3.get());
+    execution.push_transition(a4.get());
+
+    SECTION("Happens-before is irreflexive")
+    {
+      REQUIRE_FALSE(execution.happens_before(0, 0));
+      REQUIRE_FALSE(execution.happens_before(1, 1));
+      REQUIRE_FALSE(execution.happens_before(2, 2));
+      REQUIRE_FALSE(execution.happens_before(3, 3));
+    }
+
+    SECTION("Happens-before values for each pair of events")
+    {
+      REQUIRE_FALSE(execution.happens_before(0, 1));
+      REQUIRE_FALSE(execution.happens_before(0, 2));
+      REQUIRE(execution.happens_before(0, 3));
+      REQUIRE_FALSE(execution.happens_before(1, 2));
+      REQUIRE_FALSE(execution.happens_before(1, 3));
+      REQUIRE_FALSE(execution.happens_before(2, 3));
+    }
+
+    SECTION("Happens-before is a subset of 'occurs-before' ")
+    {
+      REQUIRE_FALSE(execution.happens_before(1, 0));
+      REQUIRE_FALSE(execution.happens_before(2, 0));
+      REQUIRE_FALSE(execution.happens_before(3, 0));
+      REQUIRE_FALSE(execution.happens_before(2, 1));
+      REQUIRE_FALSE(execution.happens_before(3, 1));
+      REQUIRE_FALSE(execution.happens_before(3, 2));
+    }
+  }
+
+  SECTION("Example 2")
+  {
+    const auto a1 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 1);
+    const auto a2 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 3);
+    const auto a3 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 3);
+    const auto a4 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 3);
+
+    // Notice that `a5` and `a6` are executed by the same actor; thus, although
+    // the actor is executing independent actions, each still "happen-before"
+    // the another
+
+    Execution execution;
+    execution.push_transition(a1.get());
+    execution.push_transition(a2.get());
+    execution.push_transition(a3.get());
+    execution.push_transition(a4.get());
+
+    SECTION("Happens-before is irreflexive")
+    {
+      REQUIRE_FALSE(execution.happens_before(0, 0));
+      REQUIRE_FALSE(execution.happens_before(1, 1));
+      REQUIRE_FALSE(execution.happens_before(2, 2));
+      REQUIRE_FALSE(execution.happens_before(3, 3));
+    }
+
+    SECTION("Happens-before values for each pair of events")
+    {
+      REQUIRE_FALSE(execution.happens_before(0, 1));
+      REQUIRE_FALSE(execution.happens_before(0, 2));
+      REQUIRE_FALSE(execution.happens_before(0, 3));
+      REQUIRE(execution.happens_before(1, 2));
+      REQUIRE(execution.happens_before(1, 3));
+      REQUIRE(execution.happens_before(2, 3));
+    }
+
+    SECTION("Happens-before is a subset of 'occurs-before'")
+    {
+      REQUIRE_FALSE(execution.happens_before(1, 0));
+      REQUIRE_FALSE(execution.happens_before(2, 0));
+      REQUIRE_FALSE(execution.happens_before(3, 0));
+      REQUIRE_FALSE(execution.happens_before(2, 1));
+      REQUIRE_FALSE(execution.happens_before(3, 1));
+      REQUIRE_FALSE(execution.happens_before(3, 2));
+    }
+  }
+}
+
+TEST_CASE("simgrid::mc::odpor::Execution: Testing Racing Events Initials")
+{
+  SECTION("Example 1")
+  {
+    const auto a1 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
+    const auto a2 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 2);
+    const auto a3 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 1);
+    const auto a4 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
+    const auto a5 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 2);
+
+    Execution execution;
+    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());
+
+    // 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>{});
+
+    // 2 and 1 are executed by different actors and happen right after each other
+    REQUIRE(execution.get_racing_events_of(2) == std::unordered_set<Execution::EventHandle>{1});
+
+    // Although a3 and a4 are dependent, they are executed by the same actor
+    REQUIRE(execution.get_racing_events_of(3) == std::unordered_set<Execution::EventHandle>{});
+
+    // Event 4 is in a race with neither event 0 nor event 2 since those events
+    // "happen-before" event 3 with which event 4 races
+    //
+    // Furthermore, event 1 is run by the same actor and thus also is not in a race.
+    // Hence, only event 3 races with event 4
+    REQUIRE(execution.get_racing_events_of(4) == std::unordered_set<Execution::EventHandle>{3});
+  }
+
+  SECTION("Example 2: Events with multiple races")
+  {
+    const auto a1 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
+    const auto a2 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 2);
+    const auto a3 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
+    const auto a4 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 3);
+
+    Execution execution;
+    execution.push_transition(a1.get());
+    execution.push_transition(a2.get());
+    execution.push_transition(a3.get());
+    execution.push_transition(a4.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>{});
+
+    // Event 2 is independent with event 1 and run by the same actor as event 0
+    REQUIRE(execution.get_racing_events_of(2) == std::unordered_set<Execution::EventHandle>{});
+
+    // 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});
+  }
+}
\ No newline at end of file

diff --git a/tools/cmake/Tests.cmake b/tools/cmake/Tests.cmake
index aab3aab..625ce5e 100644 (file)
--- a/tools/cmake/Tests.cmake
+++ b/tools/cmake/Tests.cmake
@@ -132,6 +132,7 @@ set(UNIT_TESTS  src/xbt/unit-tests_main.cpp
 
 set(MC_UNIT_TESTS src/mc/sosp/Snapshot_test.cpp 
                   src/mc/sosp/PageStore_test.cpp
+                  src/mc/explo/odpor/Execution_test.cpp
                   src/mc/explo/udpor/EventSet_test.cpp
                   src/mc/explo/udpor/Unfolding_test.cpp
                   src/mc/explo/udpor/UnfoldingEvent_test.cpp