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

diff --git a/src/kernel/actor/SimcallObserver.cpp b/src/kernel/actor/SimcallObserver.cpp
index e0b4a55..8d13441 100644 (file)
--- a/src/kernel/actor/SimcallObserver.cpp
+++ b/src/kernel/actor/SimcallObserver.cpp
@@ -323,8 +323,10 @@ std::string ActivityWaitSimcall::to_string(int times_considered) const
 {
   std::string res = SimcallObserver::to_string(times_considered);
   auto* comm      = dynamic_cast<activity::CommImpl*>(activity_);
-  if (comm == nullptr)
-    xbt_die("Only Comms are supported here for now");
+  if (comm == nullptr) {
+    res += "ActivityWait on non-Comm (FIXME)"; // FIXME
+    return res;
+  }
 
   if (times_considered == -1) {
     res += "WaitTimeout(comm=" + (XBT_LOG_ISENABLED(mc_observer, xbt_log_priority_verbose)

diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp
index c4cbd9a..fb1bb57 100644 (file)
--- a/src/mc/ModelChecker.cpp
+++ b/src/mc/ModelChecker.cpp
@@ -308,17 +308,29 @@ void ModelChecker::wait_for_requests()
     checker_side_.dispatch();
 }
 
-void ModelChecker::handle_simcall(Transition const& transition)
+RemotePtr<simgrid::kernel::actor::SimcallObserver> ModelChecker::handle_simcall(Transition const& transition)
 {
-  s_mc_message_simcall_handle_t m;
+  s_mc_message_simcall_execute_t m;
   memset(&m, 0, sizeof(m));
-  m.type  = MessageType::SIMCALL_HANDLE;
+  m.type              = MessageType::SIMCALL_EXECUTE;
   m.aid_              = transition.aid_;
   m.times_considered_ = transition.times_considered_;
   checker_side_.get_channel().send(m);
+
+  s_mc_message_simcall_execute_answer_t answer;
+  ssize_t s = checker_side_.get_channel().receive(answer);
+  xbt_assert(s != -1, "Could not receive message");
+  xbt_assert(s == sizeof(answer) && answer.type == MessageType::SIMCALL_EXECUTE_ANSWER,
+             "Received unexpected message %s (%i, size=%i) "
+             "expected MessageType::SIMCALL_EXECUTE_ANSWER (%i, size=%i)",
+             to_c_str(answer.type), (int)answer.type, (int)s, (int)MessageType::SIMCALL_EXECUTE_ANSWER,
+             (int)sizeof(answer));
+
   this->remote_process_->clear_cache();
   if (this->remote_process_->running())
-    checker_side_.dispatch();
+    checker_side_.dispatch(); // The app may send messages while processing the transition
+
+  return remote(answer.observer);
 }
 bool ModelChecker::simcall_is_visible(aid_t aid)
 {
@@ -345,6 +357,30 @@ bool ModelChecker::simcall_is_visible(aid_t aid)
   return answer.value;
 }
 
+bool ModelChecker::requests_are_dependent(RemotePtr<kernel::actor::SimcallObserver> obs1,
+                                          RemotePtr<kernel::actor::SimcallObserver> obs2) const
+{
+  xbt_assert(mc_model_checker != nullptr, "This should be called from the checker side");
+
+  s_mc_message_simcalls_dependent_t m;
+  memset(&m, 0, sizeof(m));
+  m.type = MessageType::SIMCALLS_DEPENDENT;
+  m.obs1 = obs1.local();
+  m.obs2 = obs2.local();
+  checker_side_.get_channel().send(m);
+
+  s_mc_message_simcalls_dependent_answer_t answer;
+  ssize_t s = checker_side_.get_channel().receive(answer);
+  xbt_assert(s != -1, "Could not receive message");
+  xbt_assert(s == sizeof(answer) && answer.type == MessageType::SIMCALLS_DEPENDENT_ANSWER,
+             "Received unexpected message %s (%i, size=%i) "
+             "expected MessageType::SIMCALLS_DEPENDENT_ANSWER (%i, size=%i)",
+             to_c_str(answer.type), (int)answer.type, (int)s, (int)MessageType::SIMCALLS_DEPENDENT_ANSWER,
+             (int)sizeof(answer));
+
+  return answer.value;
+}
+
 std::string ModelChecker::simcall_to_string(MessageType type, aid_t aid, int times_considered)
 {
   xbt_assert(mc_model_checker != nullptr, "This should be called from the checker side");

diff --git a/src/mc/ModelChecker.hpp b/src/mc/ModelChecker.hpp
index ba10b86..486145a 100644 (file)
--- a/src/mc/ModelChecker.hpp
+++ b/src/mc/ModelChecker.hpp
@@ -7,6 +7,7 @@
 #define SIMGRID_MC_MODEL_CHECKER_HPP
 
 #include "src/mc/remote/CheckerSide.hpp"
+#include "src/mc/remote/RemotePtr.hpp"
 #include "src/mc/sosp/PageStore.hpp"
 #include "xbt/base.h"
 #include "xbt/string.hpp"
@@ -49,10 +50,12 @@ public:
   void shutdown();
   void resume();
   void wait_for_requests();
-  void handle_simcall(Transition const& transition);
+  RemotePtr<simgrid::kernel::actor::SimcallObserver> handle_simcall(Transition const& transition);
 
   /* Interactions with the simcall observer */
   bool simcall_is_visible(aid_t aid);
+  bool requests_are_dependent(RemotePtr<kernel::actor::SimcallObserver> obs1,
+                              RemotePtr<kernel::actor::SimcallObserver> obs2) const;
   std::string simcall_to_string(aid_t aid, int times_considered);
   std::string simcall_dot_label(aid_t aid, int times_considered);
 

diff --git a/src/mc/Session.cpp b/src/mc/Session.cpp
index b3470c1..37a0487 100644 (file)
--- a/src/mc/Session.cpp
+++ b/src/mc/Session.cpp
@@ -107,10 +107,11 @@ void Session::take_initial_snapshot()
   initial_snapshot_ = std::make_shared<simgrid::mc::Snapshot>(0);
 }
 
-void Session::execute(Transition const& transition) const
+simgrid::mc::RemotePtr<simgrid::kernel::actor::SimcallObserver> Session::execute(Transition const& transition) const
 {
-  model_checker_->handle_simcall(transition);
+  simgrid::mc::RemotePtr<simgrid::kernel::actor::SimcallObserver> res = model_checker_->handle_simcall(transition);
   model_checker_->wait_for_requests();
+  return res;
 }
 
 void Session::restore_initial_state() const

diff --git a/src/mc/Session.hpp b/src/mc/Session.hpp
index a639246..c962d1f 100644 (file)
--- a/src/mc/Session.hpp
+++ b/src/mc/Session.hpp
@@ -8,6 +8,7 @@
 
 #include "simgrid/forward.h"
 #include "src/mc/ModelChecker.hpp"
+#include "src/mc/remote/RemotePtr.hpp"
 
 #include <functional>
 
@@ -45,7 +46,7 @@ public:
   void close();
 
   void take_initial_snapshot();
-  void execute(Transition const& transition) const;
+  simgrid::mc::RemotePtr<simgrid::kernel::actor::SimcallObserver> execute(Transition const& transition) const;
   void log_state() const;
 
   void restore_initial_state() const;

diff --git a/src/mc/api.cpp b/src/mc/api.cpp
index 219547c..f3e5b16 100644 (file)
--- a/src/mc/api.cpp
+++ b/src/mc/api.cpp
@@ -125,16 +125,12 @@ simgrid::mc::ActorInformation* Api::actor_info_cast(smx_actor_t actor) const
   return process_info;
 }
 
-bool Api::simcall_check_dependency(smx_simcall_t req1, smx_simcall_t req2) const
-{
-  // FIXME: this should be removed now
-  /* Make sure that req1 and req2 are in alphabetic order */
-  if (req1->call_ > req2->call_) {
-    auto temp = req1;
-    req1      = req2;
-    req2      = temp;
-  }
-  return true;
+bool Api::requests_are_dependent(RemotePtr<kernel::actor::SimcallObserver> obs1,
+                                 RemotePtr<kernel::actor::SimcallObserver> obs2) const
+{
+  xbt_assert(mc_model_checker != nullptr, "Must be called from MCer");
+
+  return mc_model_checker->requests_are_dependent(obs1, obs2);
 }
 
 xbt::string const& Api::get_actor_host_name(smx_actor_t actor) const
@@ -563,11 +559,11 @@ void Api::s_close() const
   session_singleton->close();
 }
 
-void Api::execute(Transition& transition, smx_simcall_t simcall) const
+RemotePtr<simgrid::kernel::actor::SimcallObserver> Api::execute(Transition& transition, smx_simcall_t simcall) const
 {
   /* FIXME: once all simcalls have observers, kill the simcall parameter and use mc_model_checker->simcall_to_string() */
   transition.textual = request_to_string(simcall, transition.times_considered_);
-  session_singleton->execute(transition);
+  return session_singleton->execute(transition);
 }
 
 void Api::automaton_load(const char* file) const

diff --git a/src/mc/api.hpp b/src/mc/api.hpp
index 6989844..500967a 100644 (file)
--- a/src/mc/api.hpp
+++ b/src/mc/api.hpp
@@ -111,12 +111,13 @@ public:
   std::list<transition_detail_t> get_enabled_transitions(simgrid::mc::State* state) const;
 
   // SIMCALL APIs
+  bool requests_are_dependent(RemotePtr<kernel::actor::SimcallObserver> obs1,
+                              RemotePtr<kernel::actor::SimcallObserver> obs2) const;
   std::string request_to_string(smx_simcall_t req, int value) const;
   std::string request_get_dot_output(smx_simcall_t req, int value) const;
   smx_actor_t simcall_get_issuer(s_smx_simcall const* req) const;
   RemotePtr<kernel::activity::MailboxImpl> get_mbox_remote_addr(smx_simcall_t const req) const;
   RemotePtr<kernel::activity::ActivityImpl> get_comm_remote_addr(smx_simcall_t const req) const;
-  bool simcall_check_dependency(smx_simcall_t const req1, smx_simcall_t const req2) const;
 
 #if HAVE_SMPI
   int get_smpi_request_tag(smx_simcall_t const& simcall, simgrid::simix::Simcall type) const;
@@ -132,7 +133,7 @@ public:
 
   // SESSION APIs
   void s_close() const;
-  void execute(Transition& transition, smx_simcall_t simcall) const;
+  RemotePtr<simgrid::kernel::actor::SimcallObserver> execute(Transition& transition, smx_simcall_t simcall) const;
 
 // AUTOMATION APIs
 #if SIMGRID_HAVE_MC

diff --git a/src/mc/checker/SafetyChecker.cpp b/src/mc/checker/SafetyChecker.cpp
index a4610dc..edabda4 100644 (file)
--- a/src/mc/checker/SafetyChecker.cpp
+++ b/src/mc/checker/SafetyChecker.cpp
@@ -90,7 +90,8 @@ void SafetyChecker::run()
     // Backtrack if we reached the maximum depth
     if (stack_.size() > (std::size_t)_sg_mc_max_depth) {
       if (reductionMode_ == ReductionMode::dpor) {
-        XBT_ERROR("/!\\ Max depth reached! THIS WILL PROBABLY BREAK the dpor reduction /!\\");
+        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 ! /!\\ ");
@@ -114,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())
@@ -134,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());
@@ -197,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_;

diff --git a/src/mc/mc_state.hpp b/src/mc/mc_state.hpp
index 612fc4c..6892324 100644 (file)
--- a/src/mc/mc_state.hpp
+++ b/src/mc/mc_state.hpp
@@ -27,6 +27,9 @@ public:
   /** The simcall which was executed, going out of that state */
   s_smx_simcall executed_req_;
 
+  /** Observer of the transition leading to that sate */
+  RemotePtr<kernel::actor::SimcallObserver> remote_observer_;
+
   /* Internal translation of the executed_req simcall
    *
    * Simcall::COMM_TESTANY is translated to a Simcall::COMM_TEST

diff --git a/src/mc/remote/AppSide.cpp b/src/mc/remote/AppSide.cpp
index 5ad3e54..4e1221d 100644 (file)
--- a/src/mc/remote/AppSide.cpp
+++ b/src/mc/remote/AppSide.cpp
@@ -93,13 +93,24 @@ void AppSide::handle_deadlock_check(const s_mc_message_t*) const
   s_mc_message_int_t answer{MessageType::DEADLOCK_CHECK_REPLY, deadlock};
   xbt_assert(channel_.send(answer) == 0, "Could not send response");
 }
-void AppSide::handle_simcall_execute(const s_mc_message_simcall_handle_t* message) const
+void AppSide::handle_simcall_execute(const s_mc_message_simcall_execute_t* message) const
 {
   kernel::actor::ActorImpl* actor = kernel::actor::ActorImpl::by_pid(message->aid_);
   xbt_assert(actor != nullptr, "Invalid pid %ld", message->aid_);
-  if (actor->simcall_.observer_ != nullptr)
-    actor->observer_stack_.push_back(actor->simcall_.observer_->clone());
+  simgrid::kernel::actor::SimcallObserver* observer = nullptr;
+  if (actor->simcall_.observer_ != nullptr) {
+    observer = actor->simcall_.observer_->clone();
+    actor->observer_stack_.push_back(observer);
+  }
+  // Finish the RPC from the server: we need to return a pointer to the observer, saved in a stable storage
+  s_mc_message_simcall_execute_answer_t answer{MessageType::SIMCALL_EXECUTE_ANSWER, observer};
+  XBT_DEBUG("send SIMCALL_EXECUTE_ANSWER(%p)", observer);
+  xbt_assert(channel_.send(answer) == 0, "Could not send response");
+
+  // The client may send some messages to the server while processing the transition
   actor->simcall_handle(message->times_considered_);
+
+  // Say the server that the transition is over and that it should proceed
   xbt_assert(channel_.send(MessageType::WAITING) == 0, "Could not send MESSAGE_WAITING to model-checker");
 }
 
@@ -136,9 +147,9 @@ void AppSide::handle_messages() const
         assert_msg_size("MESSAGE_CONTINUE", s_mc_message_t);
         return;
 
-      case MessageType::SIMCALL_HANDLE:
-        assert_msg_size("SIMCALL_HANDLE", s_mc_message_simcall_handle_t);
-        handle_simcall_execute((s_mc_message_simcall_handle_t*)message_buffer.data());
+      case MessageType::SIMCALL_EXECUTE:
+        assert_msg_size("SIMCALL_EXECUTE", s_mc_message_simcall_execute_t);
+        handle_simcall_execute((s_mc_message_simcall_execute_t*)message_buffer.data());
         break;
 
       case MessageType::SIMCALL_IS_VISIBLE: {
@@ -170,6 +181,26 @@ void AppSide::handle_messages() const
         break;
       }
 
+      case MessageType::SIMCALLS_DEPENDENT: {
+        assert_msg_size("SIMCALLS_DEPENDENT", s_mc_message_simcalls_dependent_t);
+        auto msg_simcalls = (s_mc_message_simcalls_dependent_t*)message_buffer.data();
+        auto* obs1        = msg_simcalls->obs1;
+        auto* obs2        = msg_simcalls->obs2;
+        bool res          = true;
+
+        if (obs1 != nullptr && obs2 != nullptr)
+          res = obs1->depends(obs2);
+
+        XBT_DEBUG("return SIMCALLS_DEPENDENT(%s, %s) = %s", obs1->to_string(0).c_str(), obs2->to_string(0).c_str(),
+                  (res ? "true" : "false"));
+
+        // Send result:
+        s_mc_message_simcalls_dependent_answer_t answer{MessageType::SIMCALLS_DEPENDENT_ANSWER, {0}};
+        answer.value = res;
+        xbt_assert(channel_.send(answer) == 0, "Could not send response");
+        break;
+      }
+
       case MessageType::SIMCALL_DOT_LABEL: {
         assert_msg_size("SIMCALL_DOT_LABEL", s_mc_message_simcall_to_string_t);
         auto msg_simcall                = (s_mc_message_simcall_to_string_t*)message_buffer.data();

diff --git a/src/mc/remote/AppSide.hpp b/src/mc/remote/AppSide.hpp
index 544219c..641ceae 100644 (file)
--- a/src/mc/remote/AppSide.hpp
+++ b/src/mc/remote/AppSide.hpp
@@ -31,7 +31,7 @@ public:
 
 private:
   void handle_deadlock_check(const s_mc_message_t* msg) const;
-  void handle_simcall_execute(const s_mc_message_simcall_handle_t* message) const;
+  void handle_simcall_execute(const s_mc_message_simcall_execute_t* message) const;
   void handle_actor_enabled(const s_mc_message_actor_enabled_t* msg) const;
 
 public:

diff --git a/src/mc/remote/RemoteProcess.cpp b/src/mc/remote/RemoteProcess.cpp
index 538939b..fcde1d3 100644 (file)
--- a/src/mc/remote/RemoteProcess.cpp
+++ b/src/mc/remote/RemoteProcess.cpp
@@ -556,7 +556,7 @@ void RemoteProcess::dump_stack() const
   if (unw_init_remote(&cursor, as, context) != 0) {
     _UPT_destroy(context);
     unw_destroy_addr_space(as);
-    XBT_ERROR("Could not initialiez ptrace cursor");
+    XBT_ERROR("Could not initialize ptrace cursor");
     return;
   }
 

diff --git a/src/mc/remote/mc_protocol.h b/src/mc/remote/mc_protocol.h
index de67c9d..112cddf 100644 (file)
--- a/src/mc/remote/mc_protocol.h
+++ b/src/mc/remote/mc_protocol.h
@@ -29,9 +29,10 @@ namespace simgrid {
 namespace mc {
 
 XBT_DECLARE_ENUM_CLASS(MessageType, NONE, INITIAL_ADDRESSES, CONTINUE, IGNORE_HEAP, UNIGNORE_HEAP, IGNORE_MEMORY,
-                       STACK_REGION, REGISTER_SYMBOL, DEADLOCK_CHECK, DEADLOCK_CHECK_REPLY, WAITING, SIMCALL_HANDLE,
-                       SIMCALL_IS_VISIBLE, SIMCALL_IS_VISIBLE_ANSWER, SIMCALL_TO_STRING, SIMCALL_TO_STRING_ANSWER,
-                       SIMCALL_DOT_LABEL, ASSERTION_FAILED, ACTOR_ENABLED, ACTOR_ENABLED_REPLY, FINALIZE);
+                       STACK_REGION, REGISTER_SYMBOL, DEADLOCK_CHECK, DEADLOCK_CHECK_REPLY, WAITING, SIMCALL_EXECUTE,
+                       SIMCALL_EXECUTE_ANSWER, SIMCALL_IS_VISIBLE, SIMCALL_IS_VISIBLE_ANSWER, SIMCALL_TO_STRING,
+                       SIMCALL_TO_STRING_ANSWER, SIMCALLS_DEPENDENT, SIMCALLS_DEPENDENT_ANSWER, SIMCALL_DOT_LABEL,
+                       ASSERTION_FAILED, ACTOR_ENABLED, ACTOR_ENABLED_REPLY, FINALIZE);
 
 } // namespace mc
 } // namespace simgrid
@@ -94,11 +95,15 @@ struct s_mc_message_register_symbol_t {
 };
 
 /* Server -> client */
-struct s_mc_message_simcall_handle_t {
+struct s_mc_message_simcall_execute_t {
   simgrid::mc::MessageType type;
   aid_t aid_;
   int times_considered_;
 };
+struct s_mc_message_simcall_execute_answer_t {
+  simgrid::mc::MessageType type;
+  simgrid::kernel::actor::SimcallObserver* observer;
+};
 
 struct s_mc_message_restore_t {
   simgrid::mc::MessageType type;
@@ -130,5 +135,15 @@ struct s_mc_message_simcall_to_string_answer_t { // MessageType::SIMCALL_TO_STRI
   char value[1024];
 };
 
+struct s_mc_message_simcalls_dependent_t { // MessageType::SIMCALLS_DEPENDENT
+  simgrid::mc::MessageType type;
+  simgrid::kernel::actor::SimcallObserver* obs1;
+  simgrid::kernel::actor::SimcallObserver* obs2;
+};
+struct s_mc_message_simcalls_dependent_answer_t { // MessageType::SIMCALLS_DEPENDENT_ANSWER
+  simgrid::mc::MessageType type;
+  bool value;
+};
+
 #endif // __cplusplus
 #endif