]> AND Public Git Repository - simgrid.git/blobdiff - src/mc/remote/AppSide.cpp
Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Merge branch 'fluidio' into 'master'
[simgrid.git] / src / mc / remote / AppSide.cpp
index c361f58603148bee52f764749c4dd2ff58e87e94..cbc819b4075954a3f6b496365df74d9354e28ee8 100644 (file)
@@ -10,6 +10,7 @@
 #include "src/kernel/actor/ActorImpl.hpp"
 #include "src/kernel/actor/SimcallObserver.hpp"
 #include "src/mc/mc_base.hpp"
+#include "src/mc/mc_config.hpp"
 #include "src/mc/remote/RemoteProcess.hpp"
 #if HAVE_SMPI
 #include "src/smpi/include/private.hpp"
@@ -43,7 +44,7 @@ AppSide* AppSide::initialize()
   if (instance_)
     return instance_.get();
 
-  _sg_do_model_check = 1;
+  simgrid::mc::cfg_do_model_check = true;
 
   setvbuf(stdout, nullptr, _IOLBF, 0);
 
@@ -136,9 +137,7 @@ void AppSide::handle_finalize(const s_mc_message_int_t* msg) const
 #endif
   }
   coverage_checkpoint();
-  xbt_assert(channel_.send(MessageType::DEADLOCK_CHECK_REPLY) ==
-                 0, // DEADLOCK_CHECK_REPLY because I'm too lazy to create another message type with no content (FIXME)
-             "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);
@@ -147,11 +146,12 @@ void AppSide::handle_actors_status() const
 {
   auto const& actor_list = kernel::EngineImpl::get_instance()->get_actor_list();
   int count              = actor_list.size();
+  XBT_DEBUG("Serialize the actors to answer ACTORS_STATUS from the checker. %d actors to go.", count);
 
   struct s_mc_message_actors_status_answer_t answer {
     MessageType::ACTORS_STATUS_REPLY, count
   };
-  s_mc_message_actors_status_one_t status[count];
+  std::vector<s_mc_message_actors_status_one_t> status(count);
   int i = 0;
   for (auto const& [aid, actor] : actor_list) {
     status[i].aid            = aid;
@@ -160,7 +160,10 @@ void AppSide::handle_actors_status() const
     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");
+  if (answer.count > 0) {
+    size_t size = status.size() * sizeof(s_mc_message_actors_status_one_t);
+    xbt_assert(channel_.send(status.data(), size) == 0, "Could not send ACTORS_STATUS_REPLY data");
+  }
 }
 
 #define assert_msg_size(_name_, _type_)                                                                                \
@@ -232,6 +235,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;
@@ -241,6 +247,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;
@@ -261,6 +270,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;
@@ -270,18 +282,30 @@ void AppSide::unignore_heap(void* address, std::size_t size) const
 
 void AppSide::declare_symbol(const char* name, int* value) const
 {
+  if (not MC_is_active())
+    return;
+
   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());
+  strncpy(message.name.data(), name, message.name.size() - 1);
   message.callback = nullptr;
   message.data     = value;
   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;