Actor's ID should be a long, and should be named AID

[simgrid.git] / src / mc / ModelChecker.cpp

diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp
index faccd3590ea6803db02fe4b9448c8738d0ced1e6..a4feac6be0a1bf825a6cbfda4f8e9561e613da41 100644 (file)
--- a/src/mc/ModelChecker.cpp
+++ b/src/mc/ModelChecker.cpp
@@ -68,8 +68,6 @@ void ModelChecker::start()
   if (res < 0 || not WIFSTOPPED(status) || WSTOPSIG(status) != SIGSTOP)
     xbt_die("Could not wait model-checked process");
 
-  remote_process_->init();
-
   if (not _sg_mc_dot_output_file.get().empty())
     MC_init_dot_output();
 
@@ -107,20 +105,21 @@ void ModelChecker::shutdown()
 {
   XBT_DEBUG("Shutting down model-checker");
 
-  RemoteProcess* process = &this->get_remote_process();
-  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(RemoteProcess& 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,7 +137,7 @@ 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 {
@@ -147,18 +146,6 @@ static void MC_report_crash(int status)
   }
 }
 
-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");
@@ -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_process().running())
-    kill(get_remote_process().pid(), SIGKILL);
+  shutdown();
   ::exit(status);
 }
 
@@ -264,10 +266,12 @@ void ModelChecker::handle_waitpid()
       // From PTRACE_O_TRACEEXIT:
 #ifdef __linux__
       if (status>>8 == (SIGTRAP | (PTRACE_EVENT_EXIT<<8))) {
-        xbt_assert(ptrace(PTRACE_GETEVENTMSG, remote_process_->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);
-          exit(SIMGRID_MC_EXIT_PROGRAM_CRASH);
+          this->get_remote_process().terminate();
+          this->exit(SIMGRID_MC_EXIT_PROGRAM_CRASH);
         }
       }
 #endif
@@ -286,7 +290,8 @@ void ModelChecker::handle_waitpid()
 
       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_process().terminate();
@@ -297,7 +302,7 @@ void ModelChecker::handle_waitpid()
 
 void ModelChecker::wait_for_requests()
 {
-  this->resume(get_remote_process());
+  this->resume();
   if (this->get_remote_process().running())
     checker_side_.dispatch();
 }
@@ -307,7 +312,7 @@ 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_process_->clear_cache();
@@ -376,6 +381,17 @@ 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{MessageType::FINALIZE, 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);