MC: isend/irecv are not blocking

Also, add some debug info to the MC exploration

diff --git a/src/mc/api.cpp b/src/mc/api.cpp
index 92317db..219547c 100644 (file)
--- a/src/mc/api.cpp
+++ b/src/mc/api.cpp
@@ -449,14 +449,18 @@ void Api::dump_record_path() const
 smx_simcall_t Api::mc_state_choose_request(simgrid::mc::State* state) const
 {
   RemoteProcess& process = mc_model_checker->get_remote_process();
+  XBT_DEBUG("Search for an actor to run. %zu actors to consider", process.actors().size());
   for (auto& actor : process.actors()) {
     /* Only consider the actors that were marked as interleaving by the checker algorithm */
     if (not state->actor_states_[actor.copy.get_buffer()->get_pid()].is_todo())
       continue;
 
     smx_simcall_t res = MC_state_choose_request_for_process(process, state, actor.copy.get_buffer());
-    if (res)
+    if (res) {
+      XBT_DEBUG("Let's run actor %ld, going for transition %s", actor.copy.get_buffer()->get_pid(),
+                SIMIX_simcall_name(*res));
       return res;
+    }
   }
   return nullptr;
 }

diff --git a/src/mc/checker/SafetyChecker.cpp b/src/mc/checker/SafetyChecker.cpp
index b1af40f..a4610dc 100644 (file)
--- a/src/mc/checker/SafetyChecker.cpp
+++ b/src/mc/checker/SafetyChecker.cpp
@@ -280,15 +280,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));

diff --git a/src/mc/remote/AppSide.cpp b/src/mc/remote/AppSide.cpp
index 2841ecb..5ad3e54 100644 (file)
--- a/src/mc/remote/AppSide.cpp
+++ b/src/mc/remote/AppSide.cpp
@@ -107,6 +107,7 @@ void AppSide::handle_actor_enabled(const s_mc_message_actor_enabled_t* msg) cons
 {
   bool res = mc::actor_is_enabled(kernel::actor::ActorImpl::by_pid(msg->aid));
   s_mc_message_int_t answer{MessageType::ACTOR_ENABLED_REPLY, res};
+  XBT_DEBUG("Actor %ld %s enabled", msg->aid, (res ? "IS" : "is NOT"));
   xbt_assert(channel_.send(answer) == 0, "Could not send ACTOR_ENABLED_REPLY");
 }
 
@@ -275,6 +276,7 @@ void AppSide::unignore_heap(void* address, std::size_t size) const
 void AppSide::declare_symbol(const char* name, int* value) const
 {
   s_mc_message_register_symbol_t message;
+  memset(&message, 0, sizeof(message));
   message.type = MessageType::REGISTER_SYMBOL;
   xbt_assert(strlen(name) + 1 <= message.name.size(), "Symbol is too long");
   strncpy(message.name.data(), name, message.name.size());

diff --git a/src/s4u/s4u_Comm.cpp b/src/s4u/s4u_Comm.cpp
index c77b32a..c034a25 100644 (file)
--- a/src/s4u/s4u_Comm.cpp
+++ b/src/s4u/s4u_Comm.cpp
@@ -230,7 +230,7 @@ Comm* Comm::start()
                                              copy_data_function_,
                                              get_data<void>(),
                                              detached_};
-    pimpl_ = kernel::actor::simcall_blocking(
+    pimpl_ = kernel::actor::simcall(
         [&observer] {
           return kernel::activity::CommImpl::isend(
               observer.get_issuer(), observer.get_mailbox(), observer.get_payload_size(), observer.get_rate(),
@@ -249,7 +249,7 @@ Comm* Comm::start()
                                              copy_data_function_,
                                              get_data<void>(),
                                              rate_};
-    pimpl_ = kernel::actor::simcall_blocking(
+    pimpl_ = kernel::actor::simcall(
         [&observer] {
           return kernel::activity::CommImpl::irecv(
               observer.get_issuer(), observer.get_mailbox(), observer.get_dst_buff(), observer.get_dst_buff_size(),

diff --git a/src/simix/libsmx.cpp b/src/simix/libsmx.cpp
index 9914b02..bd350ae 100644 (file)
--- a/src/simix/libsmx.cpp
+++ b/src/simix/libsmx.cpp
@@ -48,7 +48,7 @@ void simcall_comm_send(smx_actor_t sender, smx_mailbox_t mbox, double task_size,
     simgrid::kernel::actor::CommIsendSimcall send_observer{
         sender,  mbox,          task_size, rate, static_cast<unsigned char*>(src_buff), src_buff_size, match_fun,
         nullptr, copy_data_fun, data,      false};
-    comm = simgrid::kernel::actor::simcall_blocking(
+    comm = simgrid::kernel::actor::simcall(
         [&send_observer] {
           return simgrid::kernel::activity::CommImpl::isend(
               send_observer.get_issuer(), send_observer.get_mailbox(), send_observer.get_payload_size(),
@@ -110,7 +110,7 @@ void simcall_comm_recv(smx_actor_t receiver, smx_mailbox_t mbox, void* dst_buff,
 
     simgrid::kernel::actor::CommIrecvSimcall observer{
         receiver, mbox, static_cast<unsigned char*>(dst_buff), dst_buff_size, match_fun, copy_data_fun, data, rate};
-    comm = simgrid::kernel::actor::simcall_blocking(
+    comm = simgrid::kernel::actor::simcall(
         [&observer] {
           return simgrid::kernel::activity::CommImpl::irecv(
               observer.get_issuer(), observer.get_mailbox(), observer.get_dst_buff(), observer.get_dst_buff_size(),