sanitize things around FINALIZE_REPLY despite my laziness as it seems to break on...

[simgrid.git] / src / mc / remote / AppSide.cpp

diff --git a/src/mc/remote/AppSide.cpp b/src/mc/remote/AppSide.cpp
index 8d612f1..ec9e43a 100644 (file)
--- a/src/mc/remote/AppSide.cpp
+++ b/src/mc/remote/AppSide.cpp
@@ -34,7 +34,7 @@ namespace simgrid::mc {
 
 std::unique_ptr<AppSide> AppSide::instance_;
 
-AppSide* AppSide::initialize(xbt_dynar_t actors_addr)
+AppSide* AppSide::initialize()
 {
   if (not std::getenv(MC_ENV_SOCKET_FD)) // We are not in MC mode: don't initialize the MC world
     return nullptr;
@@ -73,8 +73,8 @@ AppSide* AppSide::initialize(xbt_dynar_t actors_addr)
   xbt_assert(errno == 0 && raise(SIGSTOP) == 0, "Could not wait for the model-checker (errno = %d: %s)", errno,
              strerror(errno));
 
-  s_mc_message_initial_addresses_t message{MessageType::INITIAL_ADDRESSES, mmalloc_preinit(),
-                                           kernel::actor::ActorImpl::get_maxpid_addr(), actors_addr};
+  s_mc_message_initial_addresses_t message{MessageType::INITIAL_ADDRESSES, mmalloc_get_current_heap(),
+                                           kernel::actor::ActorImpl::get_maxpid_addr()};
   xbt_assert(instance_->channel_.send(message) == 0, "Could not send the initial message with addresses.");
 
   instance_->handle_messages();
@@ -122,13 +122,6 @@ void AppSide::handle_simcall_execute(const s_mc_message_simcall_execute_t* messa
   xbt_assert(channel_.send(answer) == 0, "Could not send response");
 }
 
-void AppSide::handle_actor_enabled(const s_mc_message_actor_enabled_t* msg) const
-{
-  bool res = mc::actor_is_enabled(kernel::EngineImpl::get_instance()->get_actor_by_pid(msg->aid));
-  s_mc_message_int_t answer{MessageType::ACTOR_ENABLED_REPLY, res};
-  xbt_assert(channel_.send(answer) == 0, "Could not send ACTOR_ENABLED_REPLY");
-}
-
 void AppSide::handle_finalize(const s_mc_message_int_t* msg) const
 {
   bool terminate_asap = msg->value;
@@ -137,18 +130,36 @@ void AppSide::handle_finalize(const s_mc_message_int_t* msg) const
     if (XBT_LOG_ISENABLED(mc_client, xbt_log_priority_debug))
       kernel::EngineImpl::get_instance()->display_all_actor_status();
 #if HAVE_SMPI
-    XBT_DEBUG("Smpi_enabled: %d", (int)smpi_enabled());
-    if (smpi_enabled())
+    XBT_DEBUG("Smpi_enabled: %d", SMPI_is_inited());
+    if (SMPI_is_inited())
       SMPI_finalize();
 #endif
   }
   coverage_checkpoint();
-  xbt_assert(channel_.send(MessageType::DEADLOCK_CHECK_REPLY) == 0, // DEADLOCK_CHECK_REPLY, really?
-             "Could not answer to FINALIZE");
+  xbt_assert(channel_.send(MessageType::FINALIZE_REPLY) == 0, "Could not answer to FINALIZE");
   std::fflush(stdout);
   if (terminate_asap)
     ::_Exit(0);
 }
+void AppSide::handle_actors_status() const
+{
+  auto const& actor_list = kernel::EngineImpl::get_instance()->get_actor_list();
+  int count              = actor_list.size();
+
+  struct s_mc_message_actors_status_answer_t answer {
+    MessageType::ACTORS_STATUS_REPLY, count
+  };
+  s_mc_message_actors_status_one_t status[count];
+  int i = 0;
+  for (auto const& [aid, actor] : actor_list) {
+    status[i].aid            = aid;
+    status[i].enabled        = mc::actor_is_enabled(actor);
+    status[i].max_considered = actor->simcall_.observer_->get_max_consider();
+    i++;
+  }
+  xbt_assert(channel_.send(answer) == 0, "Could not send ACTORS_STATUS_REPLY msg");
+  xbt_assert(channel_.send(status, sizeof(status)) == 0, "Could not send ACTORS_STATUS_REPLY data");
+}
 
 #define assert_msg_size(_name_, _type_)                                                                                \
   xbt_assert(received_size == sizeof(_type_), "Unexpected size for " _name_ " (%zd != %zu)", received_size,            \
@@ -180,16 +191,16 @@ void AppSide::handle_messages() const
         handle_simcall_execute((s_mc_message_simcall_execute_t*)message_buffer.data());
         break;
 
-      case MessageType::ACTOR_ENABLED:
-        assert_msg_size("ACTOR_ENABLED", s_mc_message_actor_enabled_t);
-        handle_actor_enabled((s_mc_message_actor_enabled_t*)message_buffer.data());
-        break;
-
       case MessageType::FINALIZE:
         assert_msg_size("FINALIZE", s_mc_message_int_t);
         handle_finalize((s_mc_message_int_t*)message_buffer.data());
         break;
 
+      case MessageType::ACTORS_STATUS:
+        assert_msg_size("ACTORS_STATUS", s_mc_message_t);
+        handle_actors_status();
+        break;
+
       default:
         xbt_die("Received unexpected message %s (%i)", to_c_str(message->type), static_cast<int>(message->type));
         break;
@@ -219,6 +230,9 @@ void AppSide::report_assertion_failure() const
 
 void AppSide::ignore_memory(void* addr, std::size_t size) const
 {
+  if (not MC_is_active())
+    return;
+
   s_mc_message_ignore_memory_t message;
   message.type = MessageType::IGNORE_MEMORY;
   message.addr = (std::uintptr_t)addr;
@@ -228,6 +242,9 @@ void AppSide::ignore_memory(void* addr, std::size_t size) const
 
 void AppSide::ignore_heap(void* address, std::size_t size) const
 {
+  if (not MC_is_active())
+    return;
+
   const s_xbt_mheap_t* heap = mmalloc_get_current_heap();
 
   s_mc_message_ignore_heap_t message;
@@ -248,6 +265,9 @@ void AppSide::ignore_heap(void* address, std::size_t size) const
 
 void AppSide::unignore_heap(void* address, std::size_t size) const
 {
+  if (not MC_is_active())
+    return;
+
   s_mc_message_ignore_memory_t message;
   message.type = MessageType::UNIGNORE_HEAP;
   message.addr = (std::uintptr_t)address;
@@ -267,8 +287,17 @@ void AppSide::declare_symbol(const char* name, int* value) const
   xbt_assert(channel_.send(message) == 0, "Could send REGISTER_SYMBOL message to model-checker");
 }
 
+/** Register a stack in the model checker
+ *
+ *  The stacks are allocated in the heap. The MC handle them specifically
+ *  when we analyze/compare the content of the heap so it must be told where
+ *  they are with this function.
+ */
 void AppSide::declare_stack(void* stack, size_t size, ucontext_t* context) const
 {
+  if (not MC_is_active())
+    return;
+
   const s_xbt_mheap_t* heap = mmalloc_get_current_heap();
 
   s_stack_region_t region;