From: mlaurent <mathieu.laurent@ens-rennes.fr>
Date: Thu, 9 Nov 2023 09:34:39 +0000 (+0100)
Subject: Merge branch 'master' of https://framagit.org/simgrid/simgrid
X-Git-Tag: v3.35~83
X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/9fc682676a33abb6a4cc527c09a34db3c33e5711?hp=-c

Merge branch 'master' of https://framagit.org/simgrid/simgrid
---

9fc682676a33abb6a4cc527c09a34db3c33e5711
diff --combined src/mc/explo/DFSExplorer.cpp
index ee49e31d9b,a7c9dcf021..8d85325ef7
--- a/src/mc/explo/DFSExplorer.cpp
+++ b/src/mc/explo/DFSExplorer.cpp
@@@ -8,8 -8,10 +8,10 @@@
  #include "src/mc/mc_exit.hpp"
  #include "src/mc/mc_private.hpp"
  #include "src/mc/mc_record.hpp"
+ #include "src/mc/remote/mc_protocol.h"
  #include "src/mc/transition/Transition.hpp"
  
+ #include "xbt/asserts.h"
  #include "xbt/log.h"
  #include "xbt/string.hpp"
  #include "xbt/sysdep.h"
@@@ -81,7 -83,7 +83,7 @@@ void DFSExplorer::log_state() // overri
    XBT_INFO("DFS exploration ended. %ld unique states visited; %lu backtracks (%lu transition replays, %lu states "
             "visited overall)",
             State::get_expanded_states(), backtrack_count_, Transition::get_replayed_transitions(),
 -	   visited_states_count_);
 +           visited_states_count_);
    Exploration::log_state();
  }
  
@@@ -136,29 -138,19 +138,23 @@@ void DFSExplorer::run(
      const aid_t next = reduction_mode_ == ReductionMode::odpor ? state->next_odpor_transition()
                                                                 : std::get<0>(state->next_transition_guided());
  
-     if (next < 0) {
-       // If there is no more transition in the current state ), backtrace
-       XBT_VERB("%lu actors remain, but none of them need to be interleaved (depth %zu).", state->get_actor_count(),
-                stack_.size() + 1);
 +
-       if (state->get_actor_count() == 0) {
-         get_remote_app().finalize_app();
-         XBT_VERB("Execution came to an end at %s (state: %ld, depth: %zu)", get_record_trace().to_string().c_str(),
-                  state->get_num(), stack_.size());
+     if (next < 0 || not state->is_actor_enabled(next)) {
+       if (next >= 0) { // Actor is not enabled, then
+         XBT_INFO("Reduction %s wants to execute a disabled transition %s. If it's ODPOR, ReversibleRace is suboptimal.",
+                  to_c_str(reduction_mode_),
+                  state->get_actors_list().at(next).get_transition()->to_string(true).c_str());
+         if (reduction_mode_ == ReductionMode::odpor) {
+           XBT_INFO("Current trace:");
+           for (auto elm : get_textual_trace())
+             XBT_ERROR("%s", elm.c_str());
++	  // Remove the disabled transition from the wakeup tree so that ODPOR doesn't try it again
++	  state->remove_subtree_at_aid(next);
++	  state->add_sleep_set(state->get_actors_list().at(next).get_transition());
+         }
        }
- 
-       this->backtrack();
-       continue;
-     }
-     if (not state->is_actor_enabled(next)) {
-       // if ODPOR picked an actor that is not enabled -- ReversibleRace is an overapproximation
-       xbt_assert(reduction_mode_ == ReductionMode::odpor,
-                  "Only ODPOR should be fool enough to try to execute a disabled transition");
-       XBT_VERB("Preventing ODPOR exploration from executing a disabled transition. The reversibility of the race "
-                "must have been overapproximated");
- 
-       state->remove_subtree_at_aid(next);
-       state->add_sleep_set(state->get_actors_list().at(next).get_transition());
+       // If there is no more transition in the current state (or if ODPOR picked an actor that is not enabled --
+       // ReversibleRace is an overapproximation), backtrace
        XBT_VERB("%lu actors remain, but none of them need to be interleaved (depth %zu).", state->get_actor_count(),
                 stack_.size() + 1);
  
@@@ -356,6 -348,9 +352,6 @@@ std::shared_ptr<State> DFSExplorer::nex
      XBT_DEBUG("\tPerformed ODPOR 'clean-up'. Sleep set has:");
      for (const auto& [aid, transition] : state->get_sleep_set())
        XBT_DEBUG("\t  <%ld,%s>", aid, transition->to_string().c_str());
 -    if (not state->has_empty_tree()) {
 -      return state;
 -    }
    }
    return nullptr;
  }
@@@ -373,19 -368,15 +369,19 @@@ void DFSExplorer::backtrack(
       * ("eventually looks like C", viz. the `~_E` relation)
       */
      for (auto e_prime = static_cast<odpor::Execution::EventHandle>(0); e_prime <= last_event.value(); ++e_prime) {
 +      XBT_DEBUG("ODPOR: Now considering all possible race with `%u`", 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 (const auto v = execution_seq_.get_odpor_extension_from(e, e_prime, prev_state); v.has_value()) {
            switch (prev_state.insert_into_wakeup_tree(v.value(), execution_seq_.get_prefix_before(e))) {
              case odpor::WakeupTree::InsertionResult::root: {
 -              XBT_DEBUG("ODPOR: Reversible race with `%u` unaccounted for in the wakeup tree for "
 -                        "the execution prior to event `%u`:",
 -                        e_prime, e);
 +              XBT_DEBUG("ODPOR: Reversible race with `%u`(%ld: %.20s) unaccounted for in the wakeup tree for "
 +                        "the execution prior to event `%u`(%ld: %.20s):",
 +                        e_prime, stack_[e_prime]->get_transition_out()->aid_,
 +                        stack_[e_prime]->get_transition_out()->to_string(true).c_str(), e,
 +                        prev_state.get_transition_out()->aid_,
 +                        prev_state.get_transition_out()->to_string(true).c_str());
                break;
              }
              case odpor::WakeupTree::InsertionResult::interior_node: {