[mc] Don't leave model-checked processes around

In some cases, we terminate the model-checker brutally inside of its
event loop instead of letting the event loop and the model checker
terminate cleanly. In this case, the model-checked process could still
be left alive.

Because the model-checker was still around, tesh was still waiting on
the pipe and ended-up timing out.

We now SIGKILL the model-checked process when exiting the
model-checker brutally.

diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp
index 15d5d83..1bbf9e6 100644 (file)
--- a/src/mc/ModelChecker.cpp
+++ b/src/mc/ModelChecker.cpp
@@ -277,7 +277,7 @@ bool ModelChecker::handle_message(char* buffer, ssize_t size)
 
   case MC_MESSAGE_ASSERTION_FAILED:
     MC_report_assertion_error();
 
   case MC_MESSAGE_ASSERTION_FAILED:
     MC_report_assertion_error();

-    ::exit(SIMGRID_MC_EXIT_SAFETY);
+    this->exit(SIMGRID_MC_EXIT_SAFETY);

     break;
 
   default:
     break;
 
   default:


@@ -287,6 +287,15 @@ bool ModelChecker::handle_message(char* buffer, ssize_t size)
   return true;
 }
 
   return true;
 }
 

+/** Terminate the model-checker aplication */
+void ModelChecker::exit(int status)
+{
+  // TODO, terminate the model checker politely instead of exiting rudel
+  if (process().running())
+    kill(process().pid(), SIGKILL);
+  ::exit(status);
+}
+

 bool ModelChecker::handle_events()
 {
   char buffer[MC_MESSAGE_LENGTH];
 bool ModelChecker::handle_events()
 {
   char buffer[MC_MESSAGE_LENGTH];


@@ -384,7 +393,7 @@ void ModelChecker::handle_waitpid()
           xbt_die("Could not get exit status");
         if (WIFSIGNALED(status)) {
           MC_report_crash(status);
           xbt_die("Could not get exit status");
         if (WIFSIGNALED(status)) {
           MC_report_crash(status);

-          ::exit(SIMGRID_MC_EXIT_PROGRAM_CRASH);
+          mc_model_checker->exit(SIMGRID_MC_EXIT_PROGRAM_CRASH);

         }
       }
 
         }
       }
 

diff --git a/src/mc/ModelChecker.hpp b/src/mc/ModelChecker.hpp
index 7f770c3..cd5021b 100644 (file)
--- a/src/mc/ModelChecker.hpp
+++ b/src/mc/ModelChecker.hpp
@@ -70,6 +70,7 @@ public:
   {
     mc_model_checker->wait_client(mc_model_checker->process());
   }
   {
     mc_model_checker->wait_client(mc_model_checker->process());
   }

+  void exit(int status);

 private:
   void setup_ignore();
   bool handle_message(char* buffer, ssize_t size);
 private:
   void setup_ignore();
   bool handle_message(char* buffer, ssize_t size);

diff --git a/src/mc/mc_comm_determinism.cpp b/src/mc/mc_comm_determinism.cpp
index 9525f92..018a90a 100644 (file)
--- a/src/mc/mc_comm_determinism.cpp
+++ b/src/mc/mc_comm_determinism.cpp
@@ -145,7 +145,7 @@ static void deterministic_comm_pattern(int process, mc_comm_pattern_t comm, int
         xbt_free(initial_global_state->send_diff);
         initial_global_state->send_diff = NULL;
         MC_print_statistics(mc_stats);
         xbt_free(initial_global_state->send_diff);
         initial_global_state->send_diff = NULL;
         MC_print_statistics(mc_stats);

-        exit(SIMGRID_MC_EXIT_NON_DETERMINISM);
+        mc_model_checker->exit(SIMGRID_MC_EXIT_NON_DETERMINISM);

       }else if(_sg_mc_comms_determinism && (!initial_global_state->send_deterministic && !initial_global_state->recv_deterministic)) {
         XBT_INFO("****************************************************");
         XBT_INFO("***** Non-deterministic communications pattern *****");
       }else if(_sg_mc_comms_determinism && (!initial_global_state->send_deterministic && !initial_global_state->recv_deterministic)) {
         XBT_INFO("****************************************************");
         XBT_INFO("***** Non-deterministic communications pattern *****");


@@ -157,7 +157,7 @@ static void deterministic_comm_pattern(int process, mc_comm_pattern_t comm, int
         xbt_free(initial_global_state->recv_diff);
         initial_global_state->recv_diff = NULL;
         MC_print_statistics(mc_stats);
         xbt_free(initial_global_state->recv_diff);
         initial_global_state->recv_diff = NULL;
         MC_print_statistics(mc_stats);

-        exit(SIMGRID_MC_EXIT_NON_DETERMINISM);
+        mc_model_checker->exit(SIMGRID_MC_EXIT_NON_DETERMINISM);

       } 
     }
   }
       } 
     }
   }