Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
cosmetics
[simgrid.git] / src / mc / remote / AppSide.cpp
index 9db7806..b62e060 100644 (file)
@@ -11,7 +11,7 @@
 #include "src/kernel/actor/SimcallObserver.hpp"
 #include "src/mc/mc_base.hpp"
 #include "src/mc/mc_config.hpp"
-#include "src/mc/remote/RemoteProcess.hpp"
+#include "src/mc/sosp/RemoteProcessMemory.hpp"
 #if HAVE_SMPI
 #include "src/smpi/include/private.hpp"
 #endif
@@ -23,7 +23,6 @@
 #include <cerrno>
 #include <cstdio> // setvbuf
 #include <cstdlib>
-#include <cstring>
 #include <memory>
 #include <numeric>
 #include <sys/ptrace.h>
@@ -46,7 +45,7 @@ AppSide* AppSide::initialize()
   if (instance_)
     return instance_.get();
 
-  simgrid::mc::cfg_do_model_check = true;
+  simgrid::mc::model_checking_mode = ModelCheckingMode::APP_SIDE;
 
   setvbuf(stdout, nullptr, _IOLBF, 0);
 
@@ -76,8 +75,9 @@ AppSide* AppSide::initialize()
   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_get_current_heap(),
-                                           kernel::actor::ActorImpl::get_maxpid_addr()};
+  s_mc_message_initial_addresses_t message = {};
+  message.type                = MessageType::INITIAL_ADDRESSES;
+  message.mmalloc_default_mdp              = mmalloc_get_current_heap();
   xbt_assert(instance_->channel_.send(message) == 0, "Could not send the initial message with addresses.");
 
   instance_->handle_messages();
@@ -99,7 +99,9 @@ void AppSide::handle_deadlock_check(const s_mc_message_t*) const
     engine->display_all_actor_status();
   }
   // Send result:
-  s_mc_message_int_t answer{MessageType::DEADLOCK_CHECK_REPLY, deadlock};
+  s_mc_message_int_t answer = {};
+  answer.type  = MessageType::DEADLOCK_CHECK_REPLY;
+  answer.value = deadlock;
   xbt_assert(channel_.send(answer) == 0, "Could not send response");
 }
 void AppSide::handle_simcall_execute(const s_mc_message_simcall_execute_t* message) const
@@ -113,8 +115,7 @@ void AppSide::handle_simcall_execute(const s_mc_message_simcall_execute_t* messa
   xbt_assert(channel_.send(MessageType::WAITING) == 0, "Could not send MESSAGE_WAITING to model-checker");
 
   // Finish the RPC from the server: return a serialized observer, to build a Transition on Checker side
-  s_mc_message_simcall_execute_answer_t answer;
-  memset(&answer, 0, sizeof(answer));
+  s_mc_message_simcall_execute_answer_t answer = {};
   answer.type = MessageType::SIMCALL_EXECUTE_ANSWER;
   std::stringstream stream;
   if (actor->simcall_.observer_ != nullptr) {
@@ -170,9 +171,10 @@ void AppSide::handle_actors_status() const
     i++;
   }
 
-  struct s_mc_message_actors_status_answer_t answer {
-    MessageType::ACTORS_STATUS_REPLY, num_actors, total_transitions
-  };
+  struct s_mc_message_actors_status_answer_t answer = {};
+  answer.type             = MessageType::ACTORS_STATUS_REPLY;
+  answer.count            = num_actors;
+  answer.transition_count = total_transitions;
 
   xbt_assert(channel_.send(answer) == 0, "Could not send ACTORS_STATUS_REPLY msg");
   if (answer.count > 0) {
@@ -217,12 +219,17 @@ void AppSide::handle_actors_status() const
     }
     XBT_DEBUG("Deliver ACTOR_TRANSITION_PROBE payload");
 
-    for (const auto& probe : probes) {
-      size_t size = sizeof(s_mc_message_simcall_probe_one_t);
-      xbt_assert(channel_.send(&probe, size) == 0, "Could not send ACTOR_TRANSITION_PROBE payload (%zu bytes)", size);
-    }
+    for (const auto& probe : probes)
+      xbt_assert(channel_.send(probe) == 0, "Could not send ACTOR_TRANSITION_PROBE payload");
   }
 }
+void AppSide::handle_actors_maxpid() const
+{
+  s_mc_message_int_t answer = {};
+  answer.type               = MessageType::ACTORS_MAXPID_REPLY;
+  answer.value              = kernel::actor::ActorImpl::get_maxpid();
+  xbt_assert(channel_.send(answer) == 0, "Could not send response");
+}
 
 #define assert_msg_size(_name_, _type_)                                                                                \
   xbt_assert(received_size == sizeof(_type_), "Unexpected size for " _name_ " (%zd != %zu)", received_size,            \
@@ -266,6 +273,11 @@ void AppSide::handle_messages() const
         handle_actors_status();
         break;
 
+      case MessageType::ACTORS_MAXPID:
+        assert_msg_size("ACTORS_MAXPID", s_mc_message_t);
+        handle_actors_maxpid();
+        break;
+
       default:
         xbt_die("Received unexpected message %s (%i)", to_c_str(message->type), static_cast<int>(message->type));
         break;
@@ -300,7 +312,7 @@ void AppSide::ignore_memory(void* addr, std::size_t size) const
   if (not MC_is_active())
     return;
 
-  s_mc_message_ignore_memory_t message;
+  s_mc_message_ignore_memory_t message = {};
   message.type = MessageType::IGNORE_MEMORY;
   message.addr = (std::uintptr_t)addr;
   message.size = size;
@@ -314,7 +326,7 @@ void AppSide::ignore_heap(void* address, std::size_t size) const
 
   const s_xbt_mheap_t* heap = mmalloc_get_current_heap();
 
-  s_mc_message_ignore_heap_t message;
+  s_mc_message_ignore_heap_t message = {};
   message.type    = MessageType::IGNORE_HEAP;
   message.address = address;
   message.size    = size;
@@ -335,7 +347,7 @@ void AppSide::unignore_heap(void* address, std::size_t size) const
   if (not MC_is_active())
     return;
 
-  s_mc_message_ignore_memory_t message;
+  s_mc_message_ignore_memory_t message = {};
   message.type = MessageType::UNIGNORE_HEAP;
   message.addr = (std::uintptr_t)address;
   message.size = size;
@@ -347,8 +359,7 @@ 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));
+  s_mc_message_register_symbol_t 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() - 1);
@@ -370,14 +381,13 @@ void AppSide::declare_stack(void* stack, size_t size, ucontext_t* context) const
 
   const s_xbt_mheap_t* heap = mmalloc_get_current_heap();
 
-  s_stack_region_t region;
-  memset(&region, 0, sizeof(region));
+  s_stack_region_t region = {};
   region.address = stack;
   region.context = context;
   region.size    = size;
   region.block   = ((char*)stack - (char*)heap->heapbase) / BLOCKSIZE + 1;
 
-  s_mc_message_stack_region_t message;
+  s_mc_message_stack_region_t message = {};
   message.type         = MessageType::STACK_REGION;
   message.stack_region = region;
   xbt_assert(channel_.send(message) == 0, "Could not send STACK_REGION to model-checker");