From d2e206d0539afade3722f7aa9f7a65ad8a714253 Mon Sep 17 00:00:00 2001 From: Gabriel Corona Date: Fri, 26 Feb 2016 11:02:54 +0100 Subject: [PATCH] [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. --- src/mc/ModelChecker.cpp | 13 +++++++++++-- src/mc/ModelChecker.hpp | 1 + src/mc/mc_comm_determinism.cpp | 4 ++-- 3 files changed, 14 insertions(+), 4 deletions(-) diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp index 15d5d835fc..1bbf9e6440 100644 --- 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(); - ::exit(SIMGRID_MC_EXIT_SAFETY); + this->exit(SIMGRID_MC_EXIT_SAFETY); break; default: @@ -287,6 +287,15 @@ bool ModelChecker::handle_message(char* buffer, ssize_t size) 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]; @@ -384,7 +393,7 @@ void ModelChecker::handle_waitpid() 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 7f770c3c82..cd5021bb3c 100644 --- a/src/mc/ModelChecker.hpp +++ b/src/mc/ModelChecker.hpp @@ -70,6 +70,7 @@ public: { 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); diff --git a/src/mc/mc_comm_determinism.cpp b/src/mc/mc_comm_determinism.cpp index 9525f92664..018a90afa4 100644 --- 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); - 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 *****"); @@ -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); - exit(SIMGRID_MC_EXIT_NON_DETERMINISM); + mc_model_checker->exit(SIMGRID_MC_EXIT_NON_DETERMINISM); } } } -- 2.20.1