Don't compute the dependencies locally in the checker, but through the observers...

[simgrid.git] / src / mc / checker / SafetyChecker.cpp

diff --git a/src/mc/checker/SafetyChecker.cpp b/src/mc/checker/SafetyChecker.cpp
index ac21b5f..edabda4 100644 (file)
--- a/src/mc/checker/SafetyChecker.cpp
+++ b/src/mc/checker/SafetyChecker.cpp
@@ -1,4 +1,4 @@
-/* Copyright (c) 2016-2021. The SimGrid Team. All rights reserved.          */
+/* Copyright (c) 2016-2022. 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. */
@@ -89,7 +89,12 @@ void SafetyChecker::run()
 
     // Backtrack if we reached the maximum depth
     if (stack_.size() > (std::size_t)_sg_mc_max_depth) {
-      XBT_WARN("/!\\ Max depth reached ! /!\\ ");
+      if (reductionMode_ == ReductionMode::dpor) {
+        XBT_ERROR("/!\\ Max depth of %d reached! THIS WILL PROBABLY BREAK the dpor reduction /!\\",
+                  _sg_mc_max_depth.get());
+        XBT_ERROR("/!\\ If bad things happen, disable dpor with --cfg=model-check/reduction:none /!\\");
+      } else
+        XBT_WARN("/!\\ Max depth reached ! /!\\ ");
       this->backtrack();
       continue;
     }
@@ -110,7 +115,7 @@ void SafetyChecker::run()
     // req is now the transition of the process that was selected to be executed
 
     if (req == nullptr) {
-      XBT_DEBUG("There remains %zu actors, but no more processes to interleave. (depth %zu)",
+      XBT_DEBUG("There remains %zu actors, but none to interleave (depth %zu).",
                 mc_model_checker->get_remote_process().actors().size(), stack_.size() + 1);
 
       if (mc_model_checker->get_remote_process().actors().empty())
@@ -130,11 +135,13 @@ void SafetyChecker::run()
     api::get().mc_inc_executed_trans();
 
     /* Actually answer the request: let execute the selected request (MCed does one step) */
-    api::get().execute(state->transition_, &state->executed_req_);
+    RemotePtr<simgrid::kernel::actor::SimcallObserver> remote_observer =
+        api::get().execute(state->transition_, &state->executed_req_);
 
     /* Create the new expanded state (copy the state of MCed into our MCer data) */
     ++expanded_states_count_;
     auto next_state = std::make_unique<State>(expanded_states_count_);
+    next_state->remote_observer_ = remote_observer;
 
     if (_sg_mc_termination)
       this->check_non_termination(next_state.get());
@@ -146,7 +153,7 @@ void SafetyChecker::run()
     /* If this is a new state (or if we don't care about state-equality reduction) */
     if (visited_state_ == nullptr) {
       /* Get an enabled process and insert it in the interleave set of the next state */
-      auto actors = api::get().get_actors(); 
+      auto actors = api::get().get_actors();
       for (auto& remoteActor : actors) {
         auto actor = remoteActor.copy.get_buffer();
         if (get_session().actor_is_enabled(actor->get_pid())) {
@@ -193,7 +200,7 @@ void SafetyChecker::backtrack()
           XBT_DEBUG("Simcall %s and %s with same issuer", SIMIX_simcall_name(state->executed_req_),
                     SIMIX_simcall_name(prev_state->executed_req_));
           break;
-        } else if (api::get().simcall_check_dependency(&state->internal_req_, &prev_state->internal_req_)) {
+        } else if (api::get().requests_are_dependent(state->remote_observer_, state->remote_observer_)) {
           if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
             XBT_DEBUG("Dependent Transitions:");
             int value              = prev_state->transition_.times_considered_;
@@ -276,15 +283,18 @@ SafetyChecker::SafetyChecker(Session* session) : Checker(session)
   auto initial_state = std::make_unique<State>(expanded_states_count_);
 
   XBT_DEBUG("**************************************************");
-  XBT_DEBUG("Initial state");
 
   /* Get an enabled actor and insert it in the interleave set of the initial state */
   auto actors = api::get().get_actors();
+  XBT_DEBUG("Initial state. %zu actors to consider", actors.size());
   for (auto& actor : actors)
     if (get_session().actor_is_enabled(actor.copy.get_buffer()->get_pid())) {
       initial_state->mark_todo(actor.copy.get_buffer());
-      if (reductionMode_ != ReductionMode::none)
+      if (reductionMode_ == ReductionMode::dpor) {
+        XBT_DEBUG("Actor %ld is TODO, DPOR is ON so let's go for this one.", actor.copy.get_buffer()->get_pid());
         break;
+      }
+      XBT_DEBUG("Actor %ld is TODO", actor.copy.get_buffer()->get_pid());
     }
 
   stack_.push_back(std::move(initial_state));