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

diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp
index 102133f86b..3a9fb8513f 100644
--- a/src/mc/ModelChecker.cpp
+++ b/src/mc/ModelChecker.cpp
@@ -105,11 +105,12 @@ 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();
   }
 }
 
@@ -240,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);
 }
 
@@ -267,10 +266,11 @@ void ModelChecker::handle_waitpid()
       // From PTRACE_O_TRACEEXIT:
 #ifdef __linux__
       if (status>>8 == (SIGTRAP | (PTRACE_EVENT_EXIT<<8))) {
-        int ptrace_res = ptrace(PTRACE_GETEVENTMSG, remote_process_->pid(), 0, &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);
+          this->get_remote_process().terminate();
           this->exit(SIMGRID_MC_EXIT_PROGRAM_CRASH);
         }
       }
@@ -290,6 +290,7 @@ void ModelChecker::handle_waitpid()
 
       else if (WIFSIGNALED(status)) {
         MC_report_crash(status);
+        this->get_remote_process().terminate();
         this->exit(SIMGRID_MC_EXIT_PROGRAM_CRASH);
       } else if (WIFEXITED(status)) {
         XBT_DEBUG("Child process is over");
@@ -311,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();
@@ -380,12 +381,17 @@ std::string ModelChecker::simcall_dot_label(int aid, int times_considered)
   return answer;
 }
 
-void ModelChecker::finalize_app()
+void ModelChecker::finalize_app(bool terminate_asap)
 {
-  int res = checker_side_.get_channel().send(MessageType::FINALIZE);
-  xbt_assert(res == 0, "Could not ask the app to finalize MPI on need");
-  s_mc_message_int_t message;
-  ssize_t s = checker_side_.get_channel().receive(message);
+  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");
 }