Add reversible race calculator

Determining whether or not a race between
two events is reversible is a critical component
of ODPOR. It turns out that we need to specialize
the race detection to the action types themselves.
Knowing the types of the transitions will help us
determine whether the race is reversible.

diff --git a/MANIFEST.in b/MANIFEST.in
index 6ed7f62..b9ca4f9 100644 (file)
--- a/MANIFEST.in
+++ b/MANIFEST.in
@@ -2195,6 +2195,8 @@ include src/mc/explo/odpor/ClockVector_test.cpp
 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/odpor/ReversibleRaceCalculator.cpp
+include src/mc/explo/odpor/ReversibleRaceCalculator.hpp
 include src/mc/explo/odpor/WakeupTree.cpp
 include src/mc/explo/odpor/WakeupTree.hpp
 include src/mc/explo/odpor/WakeupTree_test.cpp

diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp
index 5844878..cdc31df 100644 (file)
--- a/src/mc/explo/DFSExplorer.cpp
+++ b/src/mc/explo/DFSExplorer.cpp
@@ -295,37 +295,22 @@ void DFSExplorer::run()
        * The intuition is that some subsequence of `v` may enable `p`, so
        * we want to be sure that search "in that direction"
        */
-      const aid_t p = executed_transition->aid_;
       execution_seq_.push_transition(std::move(executed_transition));
       xbt_assert(execution_seq_.get_latest_event_handle().has_value(),
                  "No events are contained in the SDPOR/OPDPOR execution "
                  "even though one was just added");
 
       const auto next_E_p = execution_seq_.get_latest_event_handle().value();
-      for (const auto racing_event_handle : execution_seq_.get_racing_events_of(next_E_p)) {
-        // To determine if the race is reversible, we have to ensure
-        // that actor `p` running `next_E_p` (viz. the event such that
-        // `racing_event -> (E_p) next_E_p` and no other event
-        // "happens-between" the two) is enabled in any equivalent
-        // execution where `racing_event` happens before `next_E_p`.
-        //
-        // Importantly, it is equivalent to checking if in ANY
-        // such equivalent execution sequence where `racing_event`
-        // happens-before `next_E_p` that `p` is enabled in `pre(racing_event, E.p)`.
-        // Thus it suffices to check THIS execution
-        //
-        // If the actor `p` is not enabled at s_[E'], it is not a *reversible* race
+      for (const auto racing_event_handle : execution_seq_.get_reversible_races_of(next_E_p)) {
         const std::shared_ptr<State> prev_state = stack_[racing_event_handle];
-        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 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()) {
-            prev_state->consider_one(q.value());
-            opened_states_.emplace_back(std::move(prev_state));
-          }
+        // 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 best
+        if (const auto q =
+                execution_seq_.get_first_sdpor_initial_from(racing_event_handle, prev_state->get_backtrack_set());
+            q.has_value()) {
+          prev_state->consider_one(q.value());
+          opened_states_.emplace_back(std::move(prev_state));
         }
       }
     } else if (reduction_mode_ == ReductionMode::odpor) {
@@ -437,27 +422,14 @@ void DFSExplorer::backtrack()
      * relation)
      */
     for (auto e_prime = static_cast<odpor::Execution::EventHandle>(0); e_prime <= last_event.value(); ++e_prime) {
-      for (const auto e : execution_seq_.get_racing_events_of(e_prime)) {
-        // To determine if the race is reversible, we have to ensure
-        // that actor `p` running `e_i` (viz. the event such that
-        // `racing_event -> (E_p) e_i` and no other event
-        // "happens-between" the two) is enabled in any equivalent
-        // execution where `racing_event` happens before `e_i`.
-        //
-        // Importantly, it is equivalent to checking if in ANY
-        // such equivalent execution sequence where `racing_event`
-        // happens-before `next_E_p` that `p` is enabled in `pre(racing_event, E.p)`.
-        // Thus it suffices to check THIS execution
-        //
-        // If the actor `p` is not enabled at s_[E'], it is not a *reversible* race
-        const aid_t p     = execution_seq_.get_actor_with_handle(e_prime);
+      for (const auto e : execution_seq_.get_reversible_races_of(e_prime)) {
+        XBT_DEBUG("ODPOR: Reversible race detected between events `%u` and `%u`", e, e_prime);
         State& prev_state = *stack_[e];
-        if (prev_state.is_actor_enabled(p)) {
-          const std::optional<odpor::PartialExecution> v =
-              execution_seq_.get_odpor_extension_from(e, e_prime, prev_state);
-          if (v.has_value()) {
-            prev_state.mark_path_interesting_for_odpor(v.value(), execution_seq_.get_prefix_before(e));
-          }
+        if (const auto v = execution_seq_.get_odpor_extension_from(e, e_prime, prev_state); v.has_value()) {
+          XBT_DEBUG("ODPOR: Reversible race unaccounted for in the wakeup tree for "
+                    "the execution prior to event `%u`, inserting a sequence",
+                    e);
+          prev_state.mark_path_interesting_for_odpor(v.value(), execution_seq_.get_prefix_before(e));
         }
       }
     }

diff --git a/src/mc/explo/odpor/Execution.cpp b/src/mc/explo/odpor/Execution.cpp
index e514141..c95b36e 100644 (file)
--- a/src/mc/explo/odpor/Execution.cpp
+++ b/src/mc/explo/odpor/Execution.cpp
@@ -72,6 +72,12 @@ std::unordered_set<Execution::EventHandle> Execution::get_racing_events_of(Execu
   return racing_events;
 }
 
+std::unordered_set<Execution::EventHandle> Execution::get_reversible_races_of(EventHandle handle) const
+{
+  // TODO: Implement this
+  return std::unordered_set<EventHandle>{};
+}
+
 Execution Execution::get_prefix_before(Execution::EventHandle handle) const
 {
   return Execution(std::vector<Event>{contents_.begin(), contents_.begin() + handle});

diff --git a/src/mc/explo/odpor/Execution.hpp b/src/mc/explo/odpor/Execution.hpp
index cfe24bd..bbdaf97 100644 (file)
--- a/src/mc/explo/odpor/Execution.hpp
+++ b/src/mc/explo/odpor/Execution.hpp
@@ -262,6 +262,25 @@ public:
    */
   std::unordered_set<EventHandle> get_racing_events_of(EventHandle handle) const;
 
+  /**
+   * @brief Returns a set of events which are in a reversible
+   * race with the given event handle `handle`
+   *
+   * Two events `e` and `e'` in an execution `E` are said to
+   * be in a reversible race iff
+   *
+   * 1. `e` and `e'` race
+   * 2. In any equivalent execution sequence `E'` to `E`
+   * where `e` occurs immediately before `e'`, the actor
+   * running `e'` was enabled in the state prior to `e`
+   *
+   * @param handle the event with respect to which
+   * reversible races are computed
+   * @returns a set of event handles from which are in a reversible
+   * race with `handle`
+   */
+  std::unordered_set<EventHandle> get_reversible_races_of(EventHandle handle) const;
+
   /**
    * @brief Computes `pre(e, E)` as described in ODPOR [1]
    *

diff --git a/src/mc/explo/odpor/ReversibleRaceCalculator.cpp b/src/mc/explo/odpor/ReversibleRaceCalculator.cpp
new file mode 100644 (file)
index 0000000..e69de29

diff --git a/src/mc/explo/odpor/ReversibleRaceCalculator.hpp b/src/mc/explo/odpor/ReversibleRaceCalculator.hpp
new file mode 100644 (file)
index 0000000..1396af9
--- /dev/null
+++ b/src/mc/explo/odpor/ReversibleRaceCalculator.hpp
@@ -0,0 +1,43 @@
+/* Copyright (c) 2007-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. */
+
+#ifndef SIMGRID_MC_ODPOR_REVERSIBLE_RACE_CALCULATOR_HPP
+#define SIMGRID_MC_ODPOR_REVERSIBLE_RACE_CALCULATOR_HPP
+
+#include "src/mc/explo/udpor/EventSet.hpp"
+#include "src/mc/explo/udpor/udpor_forward.hpp"
+#include "src/mc/transition/Transition.hpp"
+#include "src/mc/transition/TransitionActorJoin.hpp"
+#include "src/mc/transition/TransitionAny.hpp"
+#include "src/mc/transition/TransitionComm.hpp"
+#include "src/mc/transition/TransitionObjectAccess.hpp"
+#include "src/mc/transition/TransitionRandom.hpp"
+#include "src/mc/transition/TransitionSynchro.hpp"
+
+#include <memory>
+
+namespace simgrid::mc::odpor {
+
+/**
+ * @brief Computes whether a race between two events
+ * in a given execution is a reversible race.
+ *
+ * @note: All of the methods assume that there is
+ * indeed a race between the two events in the
+ * execution; indeed, the question the method answers
+ * is only sensible in the context of a race
+ */
+struct ReversibleRaceCalculator final {
+  static EventSet is_race_reversible(const Execution&, Execution::Handle e1, std::shared_ptr<Transition>);
+  static EventSet is_race_reversible(const Execution&, Execution::Handle e1, std::shared_ptr<Transition>);
+  static EventSet is_race_reversible(const Execution&, Execution::Handle e1, std::shared_ptr<Transition>);
+  static EventSet is_race_reversible(const Execution&, Execution::Handle e1, std::shared_ptr<Transition>);
+
+public:
+  static EventSet is_race_reversible(const Execution&, Execution::Handle e1, Execution::Handle e2);
+};
+
+} // namespace simgrid::mc::odpor
+#endif

diff --git a/tools/cmake/DefinePackages.cmake b/tools/cmake/DefinePackages.cmake
index c395235..35be16c 100644 (file)
--- a/tools/cmake/DefinePackages.cmake
+++ b/tools/cmake/DefinePackages.cmake
@@ -537,6 +537,8 @@ set(MC_SRC_STATELESS
 
   src/mc/explo/odpor/Execution.cpp
   src/mc/explo/odpor/Execution.hpp
+  src/mc/explo/odpor/ReversibleRaceCalculator.cpp
+  src/mc/explo/odpor/ReversibleRaceCalculator.hpp
   src/mc/explo/odpor/WakeupTree.cpp
   src/mc/explo/odpor/WakeupTree.hpp
   src/mc/explo/odpor/WakeupTreeIterator.cpp