X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/d2cd6190c7a6ba8f102134cf6ab3043f7df8f77e..75ebde707b0c7b13d67e12e94a03d774ad37ba67:/src/mc/ModelChecker.cpp diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp index ea14a19348..f0f149f613 100644 --- a/src/mc/ModelChecker.cpp +++ b/src/mc/ModelChecker.cpp @@ -40,6 +40,12 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_ModelChecker, mc, "ModelChecker"); using simgrid::mc::remote; +#ifdef __linux__ +# define WAITPID_CHECKED_FLAGS __WALL +#else +# define WAITPID_CHECKED_FLAGS 0 +#endif + // Hardcoded index for now: #define SOCKET_FD_INDEX 0 #define SIGNAL_FD_INDEX 1 @@ -48,7 +54,6 @@ namespace simgrid { namespace mc { ModelChecker::ModelChecker(std::unique_ptr process) : - hostnames_(xbt_dict_new()), page_store_(500), process_(std::move(process)), parent_snapshot_(nullptr) @@ -56,22 +61,7 @@ ModelChecker::ModelChecker(std::unique_ptr process) : } -ModelChecker::~ModelChecker() -{ - xbt_dict_free(&this->hostnames_); -} - -const char* ModelChecker::get_host_name(const char* hostname) -{ - // Lookup the host name in the dictionary (or create it): - xbt_dictelm_t elt = xbt_dict_get_elm_or_null(this->hostnames_, hostname); - if (!elt) { - xbt_dict_set(this->hostnames_, hostname, nullptr, nullptr); - elt = xbt_dict_get_elm_or_null(this->hostnames_, hostname); - assert(elt); - } - return elt->key; -} +ModelChecker::~ModelChecker() {} void ModelChecker::start() { @@ -107,7 +97,7 @@ void ModelChecker::start() int status; // The model-checked process SIGSTOP itself to signal it's ready: - pid_t res = waitpid(pid, &status, __WALL); + pid_t res = waitpid(pid, &status, WAITPID_CHECKED_FLAGS); if (res < 0 || !WIFSTOPPED(status) || WSTOPSIG(status) != SIGSTOP) xbt_die("Could not wait model-checked process"); @@ -118,8 +108,14 @@ void ModelChecker::start() setup_ignore(); +#ifdef __linux__ ptrace(PTRACE_SETOPTIONS, pid, nullptr, PTRACE_O_TRACEEXIT); ptrace(PTRACE_CONT, pid, 0, 0); +#elif defined BSD + ptrace(PT_CONTINUE, pid, (caddr_t)1, 0); +#else +# error "no ptrace equivalent coded for this platform" +#endif } static const std::pair ignored_local_variables[] = { @@ -310,10 +306,10 @@ bool ModelChecker::handle_message(char* buffer, ssize_t size) return true; } -/** Terminate the model-checker aplication */ +/** Terminate the model-checker application */ void ModelChecker::exit(int status) { - // TODO, terminate the model checker politely instead of exiting rudel + // TODO, terminate the model checker politely instead of exiting rudely if (process().running()) kill(process().pid(), SIGKILL); ::exit(status); @@ -409,6 +405,7 @@ void ModelChecker::handle_waitpid() if (pid == this->process().pid()) { // From PTRACE_O_TRACEEXIT: +#ifdef __linux__ if (status>>8 == (SIGTRAP | (PTRACE_EVENT_EXIT<<8))) { if (ptrace(PTRACE_GETEVENTMSG, this->process().pid(), 0, &status) == -1) xbt_die("Could not get exit status"); @@ -417,11 +414,18 @@ void ModelChecker::handle_waitpid() mc_model_checker->exit(SIMGRID_MC_EXIT_PROGRAM_CRASH); } } +#endif // We don't care about signals, just reinject them: if (WIFSTOPPED(status)) { XBT_DEBUG("Stopped with signal %i", (int) WSTOPSIG(status)); - if (ptrace(PTRACE_CONT, this->process().pid(), 0, WSTOPSIG(status)) == -1) + errno = 0; +#ifdef __linux__ + ptrace(PTRACE_CONT, this->process().pid(), 0, WSTOPSIG(status)); +#elif defined BSD + ptrace(PT_CONTINUE, this->process().pid(), (caddr_t)1, WSTOPSIG(status)); +#endif + if (errno != 0) xbt_die("Could not PTRACE_CONT"); } @@ -476,9 +480,8 @@ bool ModelChecker::checkDeadlock() if (s == -1) xbt_die("Could not receive message"); if (s != sizeof(message) || message.type != MC_MESSAGE_DEADLOCK_CHECK_REPLY) - xbt_die("%s received unexpected message %s (%i, size=%i) " + xbt_die("Received unexpected message %s (%i, size=%i) " "expected MC_MESSAGE_DEADLOCK_CHECK_REPLY (%i, size=%i)", - MC_mode_name(mc_mode), MC_message_type_name(message.type), (int) message.type, (int) s, (int) MC_MESSAGE_DEADLOCK_CHECK_REPLY, (int) sizeof(message) );