X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/796f23636eb16207bead6887a0529a39dfedf8eb..92cfd3dc96cc1a8f7c69707c80aaf70d61cbcbbf:/src/mc/ModelChecker.cpp

diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp
index 141400a9e8..3a9fb8513f 100644
--- a/src/mc/ModelChecker.cpp
+++ b/src/mc/ModelChecker.cpp
@@ -10,7 +10,7 @@
 #include "src/mc/mc_config.hpp"
 #include "src/mc/mc_exit.hpp"
 #include "src/mc/mc_private.hpp"
-#include "src/mc/remote/RemoteSimulation.hpp"
+#include "src/mc/remote/RemoteProcess.hpp"
 #include "xbt/automaton.hpp"
 #include "xbt/system_error.hpp"
 
@@ -33,8 +33,8 @@ using simgrid::mc::remote;
 namespace simgrid {
 namespace mc {
 
-ModelChecker::ModelChecker(std::unique_ptr<RemoteSimulation> remote_simulation, int sockfd)
-    : checker_side_(sockfd), remote_simulation_(std::move(remote_simulation))
+ModelChecker::ModelChecker(std::unique_ptr<RemoteProcess> remote_simulation, int sockfd)
+    : checker_side_(sockfd), remote_process_(std::move(remote_simulation))
 {
 }
 
@@ -62,14 +62,12 @@ void ModelChecker::start()
   int status;
 
   // The model-checked process SIGSTOP itself to signal it's ready:
-  const pid_t pid = remote_simulation_->pid();
+  const pid_t pid = remote_process_->pid();
 
   pid_t res = waitpid(pid, &status, WAITPID_CHECKED_FLAGS);
   if (res < 0 || not WIFSTOPPED(status) || WSTOPSIG(status) != SIGSTOP)
     xbt_die("Could not wait model-checked process");
 
-  remote_simulation_->init();
-
   if (not _sg_mc_dot_output_file.get().empty())
     MC_init_dot_output();
 
@@ -95,7 +93,7 @@ static constexpr auto ignored_local_variables = {
 
 void ModelChecker::setup_ignore()
 {
-  const RemoteSimulation& process = this->get_remote_simulation();
+  const RemoteProcess& process = this->get_remote_process();
   for (auto const& var : ignored_local_variables)
     process.ignore_local_variable(var.first, var.second);
 
@@ -107,20 +105,21 @@ void ModelChecker::shutdown()
 {
   XBT_DEBUG("Shutting down model-checker");
 
-  RemoteSimulation* process = &this->get_remote_simulation();
-  if (process->running()) {
+  RemoteProcess& process = get_remote_process();
+  if (process.running()) {
     XBT_DEBUG("Killing process");
-    kill(process->pid(), SIGKILL);
-    process->terminate();
+    finalize_app(true);
+    kill(process.pid(), SIGKILL);
+    process.terminate();
   }
 }
 
-void ModelChecker::resume(RemoteSimulation& process)
+void ModelChecker::resume()
 {
   int res = checker_side_.get_channel().send(MessageType::CONTINUE);
   if (res)
     throw xbt::errno_error();
-  process.clear_cache();
+  remote_process_->clear_cache();
 }
 
 static void MC_report_crash(int status)
@@ -138,27 +137,15 @@ static void MC_report_crash(int status)
   for (auto const& s : mc_model_checker->getChecker()->get_textual_trace())
     XBT_INFO("  %s", s.c_str());
   dumpRecordPath();
-  session->log_state();
+  session_singleton->log_state();
   if (xbt_log_no_loc) {
     XBT_INFO("Stack trace not displayed because you passed --log=no_loc");
   } else {
     XBT_INFO("Stack trace:");
-    mc_model_checker->get_remote_simulation().dump_stack();
+    mc_model_checker->get_remote_process().dump_stack();
   }
 }
 
-static void MC_report_assertion_error()
-{
-  XBT_INFO("**************************");
-  XBT_INFO("*** PROPERTY NOT VALID ***");
-  XBT_INFO("**************************");
-  XBT_INFO("Counter-example execution trace:");
-  for (auto const& s : mc_model_checker->getChecker()->get_textual_trace())
-    XBT_INFO("  %s", s.c_str());
-  dumpRecordPath();
-  session->log_state();
-}
-
 bool ModelChecker::handle_message(const char* buffer, ssize_t size)
 {
   s_mc_message_t base_message;
@@ -166,6 +153,15 @@ bool ModelChecker::handle_message(const char* buffer, ssize_t size)
   memcpy(&base_message, buffer, sizeof(base_message));
 
   switch(base_message.type) {
+    case MessageType::INITIAL_ADDRESSES: {
+      s_mc_message_initial_addresses_t message;
+      xbt_assert(size == sizeof(message), "Broken message. Got %d bytes instead of %d.", (int)size, (int)sizeof(message));
+      memcpy(&message, buffer, sizeof(message));
+
+      get_remote_process().init(message.mmalloc_default_mdp, message.maxpid, message.actors, message.dead_actors);
+      break;
+    }
+
     case MessageType::IGNORE_HEAP: {
       s_mc_message_ignore_heap_t message;
       xbt_assert(size == sizeof(message), "Broken message");
@@ -176,7 +172,7 @@ bool ModelChecker::handle_message(const char* buffer, ssize_t size)
       region.fragment = message.fragment;
       region.address  = message.address;
       region.size     = message.size;
-      get_remote_simulation().ignore_heap(region);
+      get_remote_process().ignore_heap(region);
       break;
     }
 
@@ -184,7 +180,7 @@ bool ModelChecker::handle_message(const char* buffer, ssize_t size)
       s_mc_message_ignore_memory_t message;
       xbt_assert(size == sizeof(message), "Broken message");
       memcpy(&message, buffer, sizeof(message));
-      get_remote_simulation().unignore_heap((void*)(std::uintptr_t)message.addr, message.size);
+      get_remote_process().unignore_heap((void*)(std::uintptr_t)message.addr, message.size);
       break;
     }
 
@@ -192,7 +188,7 @@ bool ModelChecker::handle_message(const char* buffer, ssize_t size)
       s_mc_message_ignore_memory_t message;
       xbt_assert(size == sizeof(message), "Broken message");
       memcpy(&message, buffer, sizeof(message));
-      this->get_remote_simulation().ignore_region(message.addr, message.size);
+      this->get_remote_process().ignore_region(message.addr, message.size);
       break;
     }
 
@@ -200,7 +196,7 @@ bool ModelChecker::handle_message(const char* buffer, ssize_t size)
       s_mc_message_stack_region_t message;
       xbt_assert(size == sizeof(message), "Broken message");
       memcpy(&message, buffer, sizeof(message));
-      this->get_remote_simulation().stack_areas().push_back(message.stack_region);
+      this->get_remote_process().stack_areas().push_back(message.stack_region);
     } break;
 
     case MessageType::REGISTER_SYMBOL: {
@@ -213,7 +209,7 @@ bool ModelChecker::handle_message(const char* buffer, ssize_t size)
       if (property_automaton == nullptr)
         property_automaton = xbt_automaton_new();
 
-      const RemoteSimulation* process = &this->get_remote_simulation();
+      const RemoteProcess* process    = &this->get_remote_process();
       RemotePtr<int> address          = remote((int*)message.data);
       xbt::add_proposition(property_automaton, message.name.data(),
                            [process, address]() { return process->read(address); });
@@ -225,7 +221,15 @@ bool ModelChecker::handle_message(const char* buffer, ssize_t size)
       return false;
 
     case MessageType::ASSERTION_FAILED:
-      MC_report_assertion_error();
+      XBT_INFO("**************************");
+      XBT_INFO("*** PROPERTY NOT VALID ***");
+      XBT_INFO("**************************");
+      XBT_INFO("Counter-example execution trace:");
+      for (auto const& s : getChecker()->get_textual_trace())
+        XBT_INFO("  %s", s.c_str());
+      dumpRecordPath();
+      session_singleton->log_state();
+
       this->exit(SIMGRID_MC_EXIT_SAFETY);
 
     default:
@@ -237,9 +241,7 @@ bool ModelChecker::handle_message(const char* buffer, ssize_t size)
 /** Terminate the model-checker application */
 void ModelChecker::exit(int status)
 {
-  // TODO, terminate the model checker politely instead of exiting rudely
-  if (get_remote_simulation().running())
-    kill(get_remote_simulation().pid(), SIGKILL);
+  shutdown();
   ::exit(status);
 }
 
@@ -252,7 +254,7 @@ void ModelChecker::handle_waitpid()
     if (pid == -1) {
       if (errno == ECHILD) {
         // No more children:
-        xbt_assert(not this->get_remote_simulation().running(), "Inconsistent state");
+        xbt_assert(not this->get_remote_process().running(), "Inconsistent state");
         break;
       } else {
         XBT_ERROR("Could not wait for pid");
@@ -260,15 +262,16 @@ void ModelChecker::handle_waitpid()
       }
     }
 
-    if (pid == this->get_remote_simulation().pid()) {
+    if (pid == this->get_remote_process().pid()) {
       // From PTRACE_O_TRACEEXIT:
 #ifdef __linux__
       if (status>>8 == (SIGTRAP | (PTRACE_EVENT_EXIT<<8))) {
-        xbt_assert(ptrace(PTRACE_GETEVENTMSG, remote_simulation_->pid(), 0, &status) != -1,
-                   "Could not get exit status");
+        long ptrace_res = ptrace(PTRACE_GETEVENTMSG, remote_process_->pid(), 0, &status);
+        xbt_assert(ptrace_res != -1, "Could not get exit status");
         if (WIFSIGNALED(status)) {
           MC_report_crash(status);
-          mc_model_checker->exit(SIMGRID_MC_EXIT_PROGRAM_CRASH);
+          this->get_remote_process().terminate();
+          this->exit(SIMGRID_MC_EXIT_PROGRAM_CRASH);
         }
       }
 #endif
@@ -278,19 +281,20 @@ void ModelChecker::handle_waitpid()
         XBT_DEBUG("Stopped with signal %i", (int) WSTOPSIG(status));
         errno = 0;
 #ifdef __linux__
-        ptrace(PTRACE_CONT, remote_simulation_->pid(), 0, WSTOPSIG(status));
+        ptrace(PTRACE_CONT, remote_process_->pid(), 0, WSTOPSIG(status));
 #elif defined BSD
-        ptrace(PT_CONTINUE, remote_simulation_->pid(), (caddr_t)1, WSTOPSIG(status));
+        ptrace(PT_CONTINUE, remote_process_->pid(), (caddr_t)1, WSTOPSIG(status));
 #endif
         xbt_assert(errno == 0, "Could not PTRACE_CONT");
       }
 
       else if (WIFSIGNALED(status)) {
         MC_report_crash(status);
-        mc_model_checker->exit(SIMGRID_MC_EXIT_PROGRAM_CRASH);
+        this->get_remote_process().terminate();
+        this->exit(SIMGRID_MC_EXIT_PROGRAM_CRASH);
       } else if (WIFEXITED(status)) {
         XBT_DEBUG("Child process is over");
-        this->get_remote_simulation().terminate();
+        this->get_remote_process().terminate();
       }
     }
   }
@@ -298,8 +302,8 @@ void ModelChecker::handle_waitpid()
 
 void ModelChecker::wait_for_requests()
 {
-  this->resume(get_remote_simulation());
-  if (this->get_remote_simulation().running())
+  this->resume();
+  if (this->get_remote_process().running())
     checker_side_.dispatch();
 }
 
@@ -308,11 +312,11 @@ void ModelChecker::handle_simcall(Transition const& transition)
   s_mc_message_simcall_handle_t m;
   memset(&m, 0, sizeof(m));
   m.type  = MessageType::SIMCALL_HANDLE;
-  m.pid_              = transition.pid_;
+  m.aid_              = transition.aid_;
   m.times_considered_ = transition.times_considered_;
   checker_side_.get_channel().send(m);
-  this->remote_simulation_->clear_cache();
-  if (this->remote_simulation_->running())
+  this->remote_process_->clear_cache();
+  if (this->remote_process_->running())
     checker_side_.dispatch();
 }
 bool ModelChecker::simcall_is_visible(int aid)
@@ -336,7 +340,7 @@ bool ModelChecker::simcall_is_visible(int aid)
 
   XBT_DEBUG("is_visible(%d) is returning %s", aid, answer.value ? "true" : "false");
 
-  this->remote_simulation_->clear_cache();
+  this->remote_process_->clear_cache();
   return answer.value;
 }
 
@@ -377,6 +381,20 @@ std::string ModelChecker::simcall_dot_label(int aid, int times_considered)
   return answer;
 }
 
+void ModelChecker::finalize_app(bool terminate_asap)
+{
+  s_mc_message_int_t m;
+  memset(&m, 0, sizeof m);
+  m.type  = MessageType::FINALIZE;
+  m.value = terminate_asap;
+  int res = checker_side_.get_channel().send(m);
+  xbt_assert(res == 0, "Could not ask the app to finalize on need");
+
+  s_mc_message_t answer;
+  ssize_t s = checker_side_.get_channel().receive(answer);
+  xbt_assert(s != -1, "Could not receive answer to FINALIZE");
+}
+
 bool ModelChecker::checkDeadlock()
 {
   int res = checker_side_.get_channel().send(MessageType::DEADLOCK_CHECK);