From de0765cca8da736799b534113602a9cb8bc32809 Mon Sep 17 00:00:00 2001 From: Gabriel Corona Date: Thu, 12 Nov 2015 12:21:31 +0100 Subject: [PATCH] [mc] Merge Server class into ModelChecker The distinction was mainly there because Server class was only useful in split-process mode. Now the other mode does not exist and the Server class is always used. --- src/mc/ModelChecker.cpp | 401 ++++++++++++++++++++++++++++++- src/mc/ModelChecker.hpp | 32 ++- src/mc/Process.cpp | 1 - src/mc/Server.cpp | 369 ---------------------------- src/mc/Server.hpp | 50 ---- src/mc/mc_base.cpp | 5 +- src/mc/mc_global.cpp | 46 +--- src/mc/mc_private.h | 7 +- src/mc/simgrid_mc.cpp | 10 +- src/xbt/log.c | 2 +- tools/cmake/DefinePackages.cmake | 2 - 11 files changed, 432 insertions(+), 493 deletions(-) delete mode 100644 src/mc/Server.cpp delete mode 100644 src/mc/Server.hpp diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp index 7b2ad841a4..785d614320 100644 --- a/src/mc/ModelChecker.cpp +++ b/src/mc/ModelChecker.cpp @@ -6,20 +6,53 @@ #include -#include "simgrid/sg_config.h" // sg_cfg_get_boolean +#include +#include +#include +#include +#include +#include + +#include +#include + +#include +#include +#include + +#include "simgrid/sg_config.h" #include "ModelChecker.hpp" #include "PageStore.hpp" +#include "ModelChecker.hpp" +#include "mc_protocol.h" +#include "mc_private.h" +#include "mc_ignore.h" +#include "mcer_ignore.h" +#include "mc_exit.h" +#include "src/mc/mc_liveness.h" -::simgrid::mc::ModelChecker* mc_model_checker = NULL; +extern "C" { + +XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_ModelChecker, mc, "ModelChecker"); + +} + +::simgrid::mc::ModelChecker* mc_model_checker = nullptr; + +using simgrid::mc::remote; + +// Hardcoded index for now: +#define SOCKET_FD_INDEX 0 +#define SIGNAL_FD_INDEX 1 namespace simgrid { namespace mc { ModelChecker::ModelChecker(pid_t pid, int socket) : + pid_(pid), socket_(socket), hostnames_(xbt_dict_new()), page_store_(500), - process_(pid, socket), parent_snapshot_(nullptr) { } @@ -34,12 +67,372 @@ 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, NULL, NULL); + xbt_dict_set(this->hostnames_, hostname, nullptr, nullptr); elt = xbt_dict_get_elm_or_null(this->hostnames_, hostname); assert(elt); } return elt->key; } +void ModelChecker::start() +{ + // Block SIGCHLD (this will be handled with accept/signalfd): + sigset_t set; + sigemptyset(&set); + sigaddset(&set, SIGCHLD); + if (sigprocmask(SIG_BLOCK, &set, nullptr) == -1) + throw std::system_error(errno, std::system_category()); + + sigset_t full_set; + sigfillset(&full_set); + + // Prepare data for poll: + + struct pollfd* socket_pollfd = &fds_[SOCKET_FD_INDEX]; + socket_pollfd->fd = socket_; + socket_pollfd->events = POLLIN; + socket_pollfd->revents = 0; + + int signal_fd = signalfd(-1, &set, 0); + if (signal_fd == -1) + throw std::system_error(errno, std::system_category()); + + struct pollfd* signalfd_pollfd = &fds_[SIGNAL_FD_INDEX]; + signalfd_pollfd->fd = signal_fd; + signalfd_pollfd->events = POLLIN; + signalfd_pollfd->revents = 0; + + XBT_DEBUG("Waiting for the model-checked process"); + int status; + + // The model-checked process SIGSTOP itself to signal it's ready: + pid_t res = waitpid(pid_, &status, __WALL); + if (res < 0 || !WIFSTOPPED(status) || WSTOPSIG(status) != SIGSTOP) + xbt_die("Could not wait model-checked process"); + + assert(process_ == nullptr); + process_ = std::unique_ptr(new Process(pid_, socket_)); + // TODO, avoid direct dependency on sg_cfg + process_->privatized(sg_cfg_get_boolean("smpi/privatize_global_variables")); + + mc_comp_times = xbt_new0(s_mc_comparison_times_t, 1); + + /* Initialize statistics */ + mc_stats = xbt_new0(s_mc_stats_t, 1); + mc_stats->state_size = 1; + + if ((_sg_mc_dot_output_file != nullptr) && (_sg_mc_dot_output_file[0] != '\0')) + MC_init_dot_output(); + + /* Init parmap */ + //parmap = xbt_parmap_mc_new(xbt_os_get_numcores(), XBT_PARMAP_DEFAULT); + + setup_ignore(); + + ptrace(PTRACE_SETOPTIONS, pid_, nullptr, PTRACE_O_TRACEEXIT); + ptrace(PTRACE_CONT, pid_, 0, 0); +} + +void ModelChecker::setup_ignore() +{ + /* Ignore some variables from xbt/ex.h used by exception e for stacks comparison */ + MC_ignore_local_variable("e", "*"); + MC_ignore_local_variable("__ex_cleanup", "*"); + MC_ignore_local_variable("__ex_mctx_en", "*"); + MC_ignore_local_variable("__ex_mctx_me", "*"); + MC_ignore_local_variable("__xbt_ex_ctx_ptr", "*"); + MC_ignore_local_variable("_log_ev", "*"); + MC_ignore_local_variable("_throw_ctx", "*"); + MC_ignore_local_variable("ctx", "*"); + + MC_ignore_local_variable("self", "simcall_BODY_mc_snapshot"); + MC_ignore_local_variable("next_cont" + "ext", "smx_ctx_sysv_suspend_serial"); + MC_ignore_local_variable("i", "smx_ctx_sysv_suspend_serial"); + + /* Ignore local variable about time used for tracing */ + MC_ignore_local_variable("start_time", "*"); + + /* Static variable used for tracing */ + MCer_ignore_global_variable("counter"); + + /* SIMIX */ + MCer_ignore_global_variable("smx_total_comms"); +} + +void ModelChecker::shutdown() +{ + XBT_DEBUG("Shuting down model-checker"); + + simgrid::mc::Process* process = &this->process(); + if (process->running()) { + XBT_DEBUG("Killing process"); + kill(process->pid(), SIGTERM); + process->terminate(); + } +} + +void ModelChecker::resume(simgrid::mc::Process& process) +{ + int res = process.send_message(MC_MESSAGE_CONTINUE); + if (res) + throw std::system_error(res, std::system_category()); + process.cache_flags = (mc_process_cache_flags_t) 0; +} + +static +void throw_socket_error(int fd) +{ + int error = 0; + socklen_t errlen = sizeof(error); + if (getsockopt(fd, SOL_SOCKET, SO_ERROR, (void *)&error, &errlen) == -1) + error = errno; + throw std::system_error(error, std::system_category()); +} + +bool ModelChecker::handle_message(char* buffer, ssize_t size) +{ + s_mc_message_t base_message; + if (size < (ssize_t) sizeof(base_message)) + xbt_die("Broken message"); + memcpy(&base_message, buffer, sizeof(base_message)); + + switch(base_message.type) { + + case MC_MESSAGE_IGNORE_HEAP: + { + s_mc_ignore_heap_message_t message; + if (size != sizeof(message)) + xbt_die("Broken messsage"); + memcpy(&message, buffer, sizeof(message)); + mc_heap_ignore_region_t region = xbt_new(s_mc_heap_ignore_region_t, 1); + *region = message.region; + MC_heap_region_ignore_insert(region); + break; + } + + case MC_MESSAGE_UNIGNORE_HEAP: + { + s_mc_ignore_memory_message_t message; + if (size != sizeof(message)) + xbt_die("Broken messsage"); + memcpy(&message, buffer, sizeof(message)); + MC_heap_region_ignore_remove( + (void *)(std::uintptr_t) message.addr, message.size); + break; + } + + case MC_MESSAGE_IGNORE_MEMORY: + { + s_mc_ignore_memory_message_t message; + if (size != sizeof(message)) + xbt_die("Broken messsage"); + memcpy(&message, buffer, sizeof(message)); + this->process().ignore_region(message.addr, message.size); + break; + } + + case MC_MESSAGE_STACK_REGION: + { + s_mc_stack_region_message_t message; + if (size != sizeof(message)) + xbt_die("Broken messsage"); + memcpy(&message, buffer, sizeof(message)); + stack_region_t stack_region = xbt_new(s_stack_region_t, 1); + *stack_region = message.stack_region; + MC_stack_area_add(stack_region); + } + break; + + case MC_MESSAGE_REGISTER_SYMBOL: + { + s_mc_register_symbol_message_t message; + if (size != sizeof(message)) + xbt_die("Broken message"); + memcpy(&message, buffer, sizeof(message)); + if (message.callback) + xbt_die("Support for client-side function proposition is not implemented."); + XBT_DEBUG("Received symbol: %s", message.name); + + if (_mc_property_automaton == nullptr) + _mc_property_automaton = xbt_automaton_new(); + + simgrid::mc::Process* process = &this->process(); + simgrid::mc::remote_ptr address + = simgrid::mc::remote((int*) message.data); + simgrid::xbt::add_proposition(_mc_property_automaton, + message.name, + [process, address]() { return process->read(address); } + ); + + break; + } + + case MC_MESSAGE_WAITING: + return false; + + case MC_MESSAGE_ASSERTION_FAILED: + MC_report_assertion_error(); + ::exit(SIMGRID_MC_EXIT_SAFETY); + break; + + default: + xbt_die("Unexpected message from model-checked application"); + + } + return true; +} + +bool ModelChecker::handle_events() +{ + char buffer[MC_MESSAGE_LENGTH]; + struct pollfd* socket_pollfd = &fds_[SOCKET_FD_INDEX]; + struct pollfd* signalfd_pollfd = &fds_[SIGNAL_FD_INDEX]; + + while(poll(fds_, 2, -1) == -1) { + switch(errno) { + case EINTR: + continue; + default: + throw std::system_error(errno, std::system_category()); + } + } + + if (socket_pollfd->revents) { + if (socket_pollfd->revents & POLLIN) { + ssize_t size = MC_receive_message(socket_pollfd->fd, buffer, sizeof(buffer), MSG_DONTWAIT); + if (size == -1 && errno != EAGAIN) + throw std::system_error(errno, std::system_category()); + return handle_message(buffer, size); + } + if (socket_pollfd->revents & POLLERR) { + throw_socket_error(socket_pollfd->fd); + } + if (socket_pollfd->revents & POLLHUP) + xbt_die("Socket hang up?"); + } + + if (signalfd_pollfd->revents) { + if (signalfd_pollfd->revents & POLLIN) { + this->handle_signals(); + return true; + } + if (signalfd_pollfd->revents & POLLERR) { + throw_socket_error(signalfd_pollfd->fd); + } + if (signalfd_pollfd->revents & POLLHUP) + xbt_die("Signalfd hang up?"); + } + + return true; +} + +void ModelChecker::loop() +{ + while (this->process().running()) + this->handle_events(); +} + +void ModelChecker::handle_signals() +{ + struct signalfd_siginfo info; + struct pollfd* signalfd_pollfd = &fds_[SIGNAL_FD_INDEX]; + while (1) { + ssize_t size = read(signalfd_pollfd->fd, &info, sizeof(info)); + if (size == -1) { + if (errno == EINTR) + continue; + else + throw std::system_error(errno, std::system_category()); + } else if (size != sizeof(info)) + return throw std::runtime_error( + "Bad communication with model-checked application"); + else + break; + } + this->on_signal(&info); +} + +void ModelChecker::handle_waitpid() +{ + XBT_DEBUG("Check for wait event"); + int status; + pid_t pid; + while ((pid = waitpid(-1, &status, WNOHANG)) != 0) { + if (pid == -1) { + if (errno == ECHILD) { + // No more children: + if (this->process().running()) + xbt_die("Inconsistent state"); + else + break; + } else { + XBT_ERROR("Could not wait for pid"); + throw std::system_error(errno, std::system_category()); + } + } + + if (pid == this->process().pid()) { + + // From PTRACE_O_TRACEEXIT: + if (status>>8 == (SIGTRAP | (PTRACE_EVENT_EXIT<<8))) { + if (ptrace(PTRACE_GETEVENTMSG, pid_, 0, &status) == -1) + xbt_die("Could not get exit status"); + if (WIFSIGNALED(status)) { + MC_report_crash(status); + ::exit(SIMGRID_MC_EXIT_PROGRAM_CRASH); + } + } + + // 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, pid_, 0, WSTOPSIG(status)) == -1) + xbt_die("Could not PTRACE_CONT"); + } + + else if (WIFEXITED(status) || WIFSIGNALED(status)) { + XBT_DEBUG("Child process is over"); + this->process().terminate(); + } + } + } +} + +void ModelChecker::on_signal(const struct signalfd_siginfo* info) +{ + switch(info->ssi_signo) { + case SIGCHLD: + this->handle_waitpid(); + break; + default: + break; + } +} + +void ModelChecker::wait_client(simgrid::mc::Process& process) +{ + this->resume(process); + while (this->process().running()) { + if (!this->handle_events()) + return; + } +} + +void ModelChecker::simcall_handle(simgrid::mc::Process& process, unsigned long pid, int value) +{ + s_mc_simcall_handle_message m; + memset(&m, 0, sizeof(m)); + m.type = MC_MESSAGE_SIMCALL_HANDLE; + m.pid = pid; + m.value = value; + process.send_message(m); + process.cache_flags = (mc_process_cache_flags_t) 0; + while (process.running()) { + if (!this->handle_events()) + return; + } +} + } } diff --git a/src/mc/ModelChecker.hpp b/src/mc/ModelChecker.hpp index c9e58d9efd..eaed239e9f 100644 --- a/src/mc/ModelChecker.hpp +++ b/src/mc/ModelChecker.hpp @@ -9,9 +9,13 @@ #include +#include +#include + #include #include #include +#include #include "mc_forward.hpp" #include "src/mc/Process.hpp" @@ -22,19 +26,17 @@ namespace simgrid { namespace mc { /** State of the model-checker (global variables for the model checker) - * - * Each part of the state of the model chercker represented as a global - * variable prevents some sharing between snapshots and must be ignored. - * By moving as much state as possible in this structure allocated - * on the model-checker heap, we avoid those issues. */ class ModelChecker { + pid_t pid_; + int socket_; + struct pollfd fds_[2]; /** String pool for host names */ // TODO, use std::unordered_set with heterogeneous comparison lookup (C++14) xbt_dict_t /* */ hostnames_; // This is the parent snapshot of the current state: PageStore page_store_; - Process process_; + std::unique_ptr process_; public: mc_snapshot_t parent_snapshot_; @@ -43,9 +45,10 @@ public: ModelChecker& operator=(ModelChecker const&) = delete; ModelChecker(pid_t pid, int socket); ~ModelChecker(); + Process& process() { - return process_; + return *process_; } PageStore& page_store() { @@ -57,6 +60,21 @@ public: { return &snapshot == this->parent_snapshot_; } + + void start(); + void shutdown(); + void resume(simgrid::mc::Process& process); + void loop(); + bool handle_events(); + void wait_client(simgrid::mc::Process& process); + void simcall_handle(simgrid::mc::Process& process, unsigned long pid, int value); +private: + void setup_ignore(); + bool handle_message(char* buffer, ssize_t size); + void handle_signals(); + void handle_waitpid(); + void on_signal(const struct signalfd_siginfo* info); + }; } diff --git a/src/mc/Process.cpp b/src/mc/Process.cpp index f0ee0f230c..2a883bd76d 100644 --- a/src/mc/Process.cpp +++ b/src/mc/Process.cpp @@ -33,7 +33,6 @@ #include "mc_ignore.h" #include "mc_smx.h" -#include "src/mc/Server.hpp" #include "src/mc/Process.hpp" #include "src/mc/AddressSpace.hpp" #include "src/mc/ObjectInformation.hpp" diff --git a/src/mc/Server.cpp b/src/mc/Server.cpp deleted file mode 100644 index d490313082..0000000000 --- a/src/mc/Server.cpp +++ /dev/null @@ -1,369 +0,0 @@ -/* Copyright (c) 2015. The SimGrid Team. - * All rights reserved. */ - -/* This program is free software; you can redistribute it and/or modify it - * under the terms of the license (GNU LGPL) which comes with this package. */ - -#include -#include - -#include -#include -#include -#include -#include -#include - -#include -#include -#include - -#include "ModelChecker.hpp" -#include "mc_protocol.h" -#include "src/mc/Server.hpp" -#include "mc_private.h" -#include "mc_ignore.h" -#include "mcer_ignore.h" -#include "mc_exit.h" -#include "src/mc/mc_liveness.h" - -using simgrid::mc::remote; - -extern "C" { - -XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_Server, mc, "MC server logic"); - -} - -// HArdcoded index for now: -#define SOCKET_FD_INDEX 0 -#define SIGNAL_FD_INDEX 1 - -namespace simgrid { -namespace mc { - -Server* server = nullptr; - -Server::Server(pid_t pid_, int socket_) - : pid(pid_), socket(socket_) {} - -void Server::start() -{ - // Block SIGCHLD (this will be handled with accept/signalfd): - sigset_t set; - sigemptyset(&set); - sigaddset(&set, SIGCHLD); - if (sigprocmask(SIG_BLOCK, &set, NULL) == -1) - throw std::system_error(errno, std::system_category()); - - sigset_t full_set; - sigfillset(&full_set); - - // Prepare data for poll: - - struct pollfd* socket_pollfd = &fds[SOCKET_FD_INDEX]; - socket_pollfd->fd = socket; - socket_pollfd->events = POLLIN; - socket_pollfd->revents = 0; - - int signal_fd = signalfd(-1, &set, 0); - if (signal_fd == -1) - throw std::system_error(errno, std::system_category()); - - struct pollfd* signalfd_pollfd = &fds[SIGNAL_FD_INDEX]; - signalfd_pollfd->fd = signal_fd; - signalfd_pollfd->events = POLLIN; - signalfd_pollfd->revents = 0; - - XBT_DEBUG("Waiting for the model-checked process"); - int status; - - // The model-checked process SIGSTOP itself to signal it's ready: - pid_t res = waitpid(pid, &status, __WALL); - if (res < 0 || !WIFSTOPPED(status) || WSTOPSIG(status) != SIGSTOP) - xbt_die("Could not wait model-checked process"); - - // The model-checked process is ready, we can read its memory layout: - MC_init_model_checker(pid, socket); - - ptrace(PTRACE_SETOPTIONS, pid, nullptr, PTRACE_O_TRACEEXIT); - ptrace(PTRACE_CONT, pid, 0, 0); -} - -void Server::shutdown() -{ - XBT_DEBUG("Shuting down model-checker"); - - simgrid::mc::Process* process = &mc_model_checker->process(); - if (process->running()) { - XBT_DEBUG("Killing process"); - kill(process->pid(), SIGTERM); - process->terminate(); - } -} - -void Server::resume(simgrid::mc::Process& process) -{ - int res = process.send_message(MC_MESSAGE_CONTINUE); - if (res) - throw std::system_error(res, std::system_category()); - process.cache_flags = (mc_process_cache_flags_t) 0; -} - -static -void throw_socket_error(int fd) -{ - int error = 0; - socklen_t errlen = sizeof(error); - if (getsockopt(fd, SOL_SOCKET, SO_ERROR, (void *)&error, &errlen) == -1) - error = errno; - throw std::system_error(error, std::system_category()); -} - -bool Server::handle_message(char* buffer, ssize_t size) -{ - s_mc_message_t base_message; - if (size < (ssize_t) sizeof(base_message)) - xbt_die("Broken message"); - memcpy(&base_message, buffer, sizeof(base_message)); - - switch(base_message.type) { - - case MC_MESSAGE_IGNORE_HEAP: - { - s_mc_ignore_heap_message_t message; - if (size != sizeof(message)) - xbt_die("Broken messsage"); - memcpy(&message, buffer, sizeof(message)); - mc_heap_ignore_region_t region = xbt_new(s_mc_heap_ignore_region_t, 1); - *region = message.region; - MC_heap_region_ignore_insert(region); - break; - } - - case MC_MESSAGE_UNIGNORE_HEAP: - { - s_mc_ignore_memory_message_t message; - if (size != sizeof(message)) - xbt_die("Broken messsage"); - memcpy(&message, buffer, sizeof(message)); - MC_heap_region_ignore_remove( - (void *)(std::uintptr_t) message.addr, message.size); - break; - } - - case MC_MESSAGE_IGNORE_MEMORY: - { - s_mc_ignore_memory_message_t message; - if (size != sizeof(message)) - xbt_die("Broken messsage"); - memcpy(&message, buffer, sizeof(message)); - mc_model_checker->process().ignore_region( - message.addr, message.size); - break; - } - - case MC_MESSAGE_STACK_REGION: - { - s_mc_stack_region_message_t message; - if (size != sizeof(message)) - xbt_die("Broken messsage"); - memcpy(&message, buffer, sizeof(message)); - stack_region_t stack_region = xbt_new(s_stack_region_t, 1); - *stack_region = message.stack_region; - MC_stack_area_add(stack_region); - } - break; - - case MC_MESSAGE_REGISTER_SYMBOL: - { - s_mc_register_symbol_message_t message; - if (size != sizeof(message)) - xbt_die("Broken message"); - memcpy(&message, buffer, sizeof(message)); - if (message.callback) - xbt_die("Support for client-side function proposition is not implemented."); - XBT_DEBUG("Received symbol: %s", message.name); - - if (_mc_property_automaton == NULL) - _mc_property_automaton = xbt_automaton_new(); - - simgrid::mc::Process* process = &mc_model_checker->process(); - simgrid::mc::remote_ptr address - = simgrid::mc::remote((int*) message.data); - simgrid::xbt::add_proposition(_mc_property_automaton, - message.name, - [process, address]() { return process->read(address); } - ); - - break; - } - - case MC_MESSAGE_WAITING: - return false; - - case MC_MESSAGE_ASSERTION_FAILED: - MC_report_assertion_error(); - ::exit(SIMGRID_MC_EXIT_SAFETY); - break; - - default: - xbt_die("Unexpected message from model-checked application"); - - } - return true; -} - -bool Server::handle_events() -{ - char buffer[MC_MESSAGE_LENGTH]; - struct pollfd* socket_pollfd = &fds[SOCKET_FD_INDEX]; - struct pollfd* signalfd_pollfd = &fds[SIGNAL_FD_INDEX]; - - while(poll(fds, 2, -1) == -1) { - switch(errno) { - case EINTR: - continue; - default: - throw std::system_error(errno, std::system_category()); - } - } - - if (socket_pollfd->revents) { - if (socket_pollfd->revents & POLLIN) { - ssize_t size = MC_receive_message(socket_pollfd->fd, buffer, sizeof(buffer), MSG_DONTWAIT); - if (size == -1 && errno != EAGAIN) - throw std::system_error(errno, std::system_category()); - return handle_message(buffer, size); - } - if (socket_pollfd->revents & POLLERR) { - throw_socket_error(socket_pollfd->fd); - } - if (socket_pollfd->revents & POLLHUP) - xbt_die("Socket hang up?"); - } - - if (signalfd_pollfd->revents) { - if (signalfd_pollfd->revents & POLLIN) { - this->handle_signals(); - return true; - } - if (signalfd_pollfd->revents & POLLERR) { - throw_socket_error(signalfd_pollfd->fd); - } - if (signalfd_pollfd->revents & POLLHUP) - xbt_die("Signalfd hang up?"); - } - - return true; -} - -void Server::loop() -{ - while (mc_model_checker->process().running()) - this->handle_events(); -} - -void Server::handle_signals() -{ - struct signalfd_siginfo info; - struct pollfd* signalfd_pollfd = &fds[SIGNAL_FD_INDEX]; - while (1) { - ssize_t size = read(signalfd_pollfd->fd, &info, sizeof(info)); - if (size == -1) { - if (errno == EINTR) - continue; - else - throw std::system_error(errno, std::system_category()); - } else if (size != sizeof(info)) - return throw std::runtime_error( - "Bad communication with model-checked application"); - else - break; - } - this->on_signal(&info); -} - -void Server::handle_waitpid() -{ - XBT_DEBUG("Check for wait event"); - int status; - pid_t pid; - while ((pid = waitpid(-1, &status, WNOHANG)) != 0) { - if (pid == -1) { - if (errno == ECHILD) { - // No more children: - if (mc_model_checker->process().running()) - xbt_die("Inconsistent state"); - else - break; - } else { - XBT_ERROR("Could not wait for pid"); - throw std::system_error(errno, std::system_category()); - } - } - - if (pid == mc_model_checker->process().pid()) { - - // From PTRACE_O_TRACEEXIT: - if (status>>8 == (SIGTRAP | (PTRACE_EVENT_EXIT<<8))) { - if (ptrace(PTRACE_GETEVENTMSG, pid, 0, &status) == -1) - xbt_die("Could not get exit status"); - if (WIFSIGNALED(status)) { - MC_report_crash(status); - ::exit(SIMGRID_MC_EXIT_PROGRAM_CRASH); - } - } - - // 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, pid, 0, WSTOPSIG(status)) == -1) - xbt_die("Could not PTRACE_CONT"); - } - - else if (WIFEXITED(status) || WIFSIGNALED(status)) { - XBT_DEBUG("Child process is over"); - mc_model_checker->process().terminate(); - } - } - } -} - -void Server::on_signal(const struct signalfd_siginfo* info) -{ - switch(info->ssi_signo) { - case SIGCHLD: - this->handle_waitpid(); - break; - default: - break; - } -} - -void Server::wait_client(simgrid::mc::Process& process) -{ - this->resume(process); - while (mc_model_checker->process().running()) { - if (!simgrid::mc::server->handle_events()) - return; - } -} - -void Server::simcall_handle(simgrid::mc::Process& process, unsigned long pid, int value) -{ - s_mc_simcall_handle_message m; - memset(&m, 0, sizeof(m)); - m.type = MC_MESSAGE_SIMCALL_HANDLE; - m.pid = pid; - m.value = value; - process.send_message(m); - process.cache_flags = (mc_process_cache_flags_t) 0; - while (process.running()) { - if (!simgrid::mc::server->handle_events()) - return; - } -} - -} -} diff --git a/src/mc/Server.hpp b/src/mc/Server.hpp deleted file mode 100644 index 62f9394b04..0000000000 --- a/src/mc/Server.hpp +++ /dev/null @@ -1,50 +0,0 @@ -/* Copyright (c) 2015. The SimGrid Team. - * All rights reserved. */ - -/* This program is free software; you can redistribute it and/or modify it - * under the terms of the license (GNU LGPL) which comes with this package. */ - -#ifndef SIMGRID_MC_SERVER_HPP -#define SIMGRID_MC_SERVER_HPP - -#include - -#include -#include - -#include -#include - -#include "src/mc/Process.hpp" -#include "mc_exit.h" - -namespace simgrid { -namespace mc { - -class Server { -private: - pid_t pid; - int socket; - struct pollfd fds[2]; -public: - Server(pid_t pid, int socket); - void start(); - void shutdown(); - void resume(simgrid::mc::Process& process); - void loop(); - bool handle_events(); - void wait_client(simgrid::mc::Process& process); - void simcall_handle(simgrid::mc::Process& process, unsigned long pid, int value); -private: - bool handle_message(char* buffer, ssize_t size); - void handle_signals(); - void handle_waitpid(); - void on_signal(const struct signalfd_siginfo* info); -}; - -extern Server* server; - -} -} - -#endif diff --git a/src/mc/mc_base.cpp b/src/mc/mc_base.cpp index 294ef168cc..01f56bf61e 100644 --- a/src/mc/mc_base.cpp +++ b/src/mc/mc_base.cpp @@ -18,7 +18,6 @@ #ifdef HAVE_MC #include "src/mc/Process.hpp" #include "src/mc/ModelChecker.hpp" -#include "src/mc/Server.hpp" #include "mc_smx.h" #endif @@ -43,7 +42,7 @@ void MC_wait_for_requests(void) { #ifdef HAVE_MC if (mc_mode == MC_MODE_SERVER) { - simgrid::mc::server->wait_client(mc_model_checker->process()); + mc_model_checker->wait_client(mc_model_checker->process()); return; } #endif @@ -233,7 +232,7 @@ void MC_simcall_handle(smx_simcall_t req, int value) xbt_dynar_foreach_ptr(mc_model_checker->process().smx_process_infos, i, pi) { if (req == &pi->copy.simcall) { - simgrid::mc::server->simcall_handle( + mc_model_checker->simcall_handle( mc_model_checker->process(), pi->copy.pid, value); return; } diff --git a/src/mc/mc_global.cpp b/src/mc/mc_global.cpp index ab95c54313..0806e5303e 100644 --- a/src/mc/mc_global.cpp +++ b/src/mc/mc_global.cpp @@ -28,7 +28,6 @@ #include "mc_record.h" #ifdef HAVE_MC -#include "src/mc/Server.hpp" #include #include #include "../xbt/mmalloc/mmprivate.h" @@ -80,7 +79,7 @@ const char *colors[13]; /******************************* Initialisation of MC *******************************/ /*********************************************************************************/ -static void MC_init_dot_output() +void MC_init_dot_output() { /* FIXME : more colors */ colors[0] = "blue"; @@ -127,49 +126,6 @@ void MC_init() } } -void MC_init_model_checker(pid_t pid, int socket) -{ - mc_model_checker = new simgrid::mc::ModelChecker(pid, socket); - - // TODO, avoid direct dependency on sg_cfg - mc_model_checker->process().privatized(sg_cfg_get_boolean("smpi/privatize_global_variables")); - - mc_comp_times = xbt_new0(s_mc_comparison_times_t, 1); - - /* Initialize statistics */ - mc_stats = xbt_new0(s_mc_stats_t, 1); - mc_stats->state_size = 1; - - if ((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0] != '\0')) - MC_init_dot_output(); - - /* Init parmap */ - //parmap = xbt_parmap_mc_new(xbt_os_get_numcores(), XBT_PARMAP_DEFAULT); - - /* Ignore some variables from xbt/ex.h used by exception e for stacks comparison */ - MC_ignore_local_variable("e", "*"); - MC_ignore_local_variable("__ex_cleanup", "*"); - MC_ignore_local_variable("__ex_mctx_en", "*"); - MC_ignore_local_variable("__ex_mctx_me", "*"); - MC_ignore_local_variable("__xbt_ex_ctx_ptr", "*"); - MC_ignore_local_variable("_log_ev", "*"); - MC_ignore_local_variable("_throw_ctx", "*"); - MC_ignore_local_variable("ctx", "*"); - - MC_ignore_local_variable("self", "simcall_BODY_mc_snapshot"); - MC_ignore_local_variable("next_cont" - "ext", "smx_ctx_sysv_suspend_serial"); - MC_ignore_local_variable("i", "smx_ctx_sysv_suspend_serial"); - - /* Ignore local variable about time used for tracing */ - MC_ignore_local_variable("start_time", "*"); - - /* Static variable used for tracing */ - MCer_ignore_global_variable("counter"); - - /* SIMIX */ - MCer_ignore_global_variable("smx_total_comms"); -} #endif /******************************* Core of MC *******************************/ diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h index c917c22acd..00c1dd9c6e 100644 --- a/src/mc/mc_private.h +++ b/src/mc/mc_private.h @@ -48,12 +48,7 @@ typedef struct s_mc_function_index_item s_mc_function_index_item_t, *mc_function /********************************* MC Global **********************************/ -/** Initialisation of the model-checker - * - * @param pid PID of the target process - * @param socket FD for the communication socket **in server mode** (or -1 otherwise) - */ -void MC_init_model_checker(pid_t pid, int socket); +XBT_PRIVATE void MC_init_dot_output(); XBT_PRIVATE extern FILE *dot_output; XBT_PRIVATE extern const char* colors[13]; diff --git a/src/mc/simgrid_mc.cpp b/src/mc/simgrid_mc.cpp index 72e32d157a..b6d30da9ad 100644 --- a/src/mc/simgrid_mc.cpp +++ b/src/mc/simgrid_mc.cpp @@ -32,10 +32,10 @@ #include "mc_base.h" #include "mc_private.h" #include "mc_protocol.h" -#include "src/mc/Server.hpp" #include "mc_safety.h" #include "mc_comm_pattern.h" #include "mc_liveness.h" +#include "mc_exit.h" XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_main, mc, "Entry point for simgrid-mc"); @@ -88,12 +88,12 @@ static int do_child(int socket, char** argv) static int do_parent(int socket, pid_t child) { XBT_DEBUG("Inside the parent process"); - if (simgrid::mc::server) + if (mc_model_checker) xbt_die("MC server already present"); try { mc_mode = MC_MODE_SERVER; - simgrid::mc::server = new simgrid::mc::Server(child, socket); - simgrid::mc::server->start(); + mc_model_checker = new simgrid::mc::ModelChecker(child, socket); + mc_model_checker->start(); int res = 0; if (_sg_mc_comms_determinism || _sg_mc_send_determinism) res = MC_modelcheck_comm_determinism(); @@ -101,7 +101,7 @@ static int do_parent(int socket, pid_t child) res = MC_modelcheck_safety(); else res = MC_modelcheck_liveness(); - simgrid::mc::server->shutdown(); + mc_model_checker->shutdown(); return res; } catch(std::exception& e) { diff --git a/src/xbt/log.c b/src/xbt/log.c index 9a506a08b6..50bb65ba84 100644 --- a/src/xbt/log.c +++ b/src/xbt/log.c @@ -654,7 +654,7 @@ static void xbt_log_connect_categories(void) XBT_LOG_CONNECT(mc_process); XBT_LOG_CONNECT(mc_protocol); XBT_LOG_CONNECT(mc_RegionSnaphot); - XBT_LOG_CONNECT(mc_Server); + XBT_LOG_CONNECT(mc_ModelChecker); XBT_LOG_CONNECT(mc_state); #endif XBT_LOG_CONNECT(mc_global); diff --git a/tools/cmake/DefinePackages.cmake b/tools/cmake/DefinePackages.cmake index 698958cbd9..f00067fd42 100644 --- a/tools/cmake/DefinePackages.cmake +++ b/tools/cmake/DefinePackages.cmake @@ -683,8 +683,6 @@ set(MC_SRC src/mc/mc_client.h src/mc/mc_protocol.h src/mc/mc_protocol.cpp - src/mc/Server.cpp - src/mc/Server.hpp src/mc/mc_smx.h src/mc/mc_smx.cpp src/mc/mc_xbt.hpp -- 2.20.1