From: mlaurent <mathieu.laurent@ens-rennes.fr>
Date: Wed, 8 Nov 2023 17:56:03 +0000 (+0100)
Subject: Merge branch 'master' of https://framagit.org/simgrid/simgrid
X-Git-Tag: v3.35~86
X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/861f43e45a240e3568c7db636d36d05ed3f70665?hp=-c

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

861f43e45a240e3568c7db636d36d05ed3f70665
diff --combined src/mc/explo/DFSExplorer.cpp
index 033c525924,0fb95fd182..d279303a5f
--- a/src/mc/explo/DFSExplorer.cpp
+++ b/src/mc/explo/DFSExplorer.cpp
@@@ -81,7 -81,7 +81,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,7 -136,9 +136,9 @@@ 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, backtrack.
+     if (next < 0 || not state->is_actor_enabled(next)) {
+       // 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);
  
@@@ -335,8 -337,6 +337,8 @@@ std::shared_ptr<State> DFSExplorer::nex
      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()) {
 +	XBT_DEBUG("\t    found the following non-empty WuT:\n"
 +		  "%s", state->string_of_wut().c_str());
        return state;
      }
    }
@@@ -356,19 -356,15 +358,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) {
 -      for (const auto e : execution_seq_.get_reversible_races_of(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: {
diff --combined src/mc/explo/odpor/ReversibleRaceCalculator.cpp
index 9b8f6144f0,f449d6a363..7a944a4dd7
--- a/src/mc/explo/odpor/ReversibleRaceCalculator.cpp
+++ b/src/mc/explo/odpor/ReversibleRaceCalculator.cpp
@@@ -13,18 -13,8 +13,18 @@@
  #include <xbt/asserts.h>
  #include <xbt/ex.h>
  
 +XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_odpor_reversible_race, mc_dfs, "ODPOR exploration algorithm of the model-checker");
 +
  namespace simgrid::mc::odpor {
  
 +/**
 +   The reversible race detector should only be used if we already have the assumption
 +   e1 <* e2 (see Source set: a foundation for ODPOR). In particular this means that :
 +   - e1 -->_E e2
 +   - proc(e1) != proc(e2)
 +   - there is no event e3 s.t. e1 --> e3 --> e2
 +*/
 +
  bool ReversibleRaceCalculator::is_race_reversible(const Execution& E, Execution::EventHandle e1,
                                                    Execution::EventHandle e2)
  {
@@@ -153,12 -143,8 +153,12 @@@ bool ReversibleRaceCalculator::is_race_
  bool ReversibleRaceCalculator::is_race_reversible_MutexWait(const Execution& E, Execution::EventHandle e1,
                                                              const Transition* /*e2*/)
  {
 -  // TODO: Get the semantics correct here
 +  // The only possibilities for e1 to satisfy the pre-condition are :
 +    // - MUTEX_ASYNC_LOCK
 +
 +  
    const auto e1_action = E.get_transition_for_handle(e1)->type_;
 +  xbt_assert(e1_action == Transition::Type::MUTEX_UNLOCK);
    return e1_action != Transition::Type::MUTEX_ASYNC_LOCK && e1_action != Transition::Type::MUTEX_UNLOCK;
  }
  
@@@ -213,7 -199,7 +213,7 @@@ bool ReversibleRaceCalculator::is_race_
  {
    // TODO: We need to check if any of the transitions
    // waited on occurred before `e1`
-   return false;
+   return true; // Let's overapproximate to not miss branches
  }
  
  } // namespace simgrid::mc::odpor