From 0b7d1f86375fc32d181c2ab574eed9dadee72db6 Mon Sep 17 00:00:00 2001 From: Gabriel Corona Date: Thu, 10 Mar 2016 15:36:54 +0100 Subject: [PATCH] [mc] Encapsulate model-checker/model-checker communications classes - Channel, for low-lewel message send/receive (currently a wrapper around a socket); - Client, for the client-side logic. --- src/mc/Channel.cpp | 53 +++++++++++++++++++++ src/mc/Channel.hpp | 81 ++++++++++++++++++++++++++++++++ src/mc/ModelChecker.cpp | 8 ++-- src/mc/Process.cpp | 13 +---- src/mc/Process.hpp | 28 ++--------- src/mc/mc_checkpoint.cpp | 2 +- src/mc/mc_client.cpp | 71 ++++++++++++++-------------- src/mc/mc_client.h | 46 ++++++++++++------ src/mc/mc_client_api.cpp | 11 +++-- src/mc/mc_comm_determinism.cpp | 2 +- src/mc/mc_global.cpp | 6 +-- src/mc/mc_ignore.cpp | 8 ++-- src/mc/mc_protocol.cpp | 35 -------------- src/mc/mc_protocol.h | 4 -- src/simix/smx_global.cpp | 2 +- tools/cmake/DefinePackages.cmake | 2 + 16 files changed, 230 insertions(+), 142 deletions(-) create mode 100644 src/mc/Channel.cpp create mode 100644 src/mc/Channel.hpp diff --git a/src/mc/Channel.cpp b/src/mc/Channel.cpp new file mode 100644 index 0000000000..b368eafc3c --- /dev/null +++ b/src/mc/Channel.cpp @@ -0,0 +1,53 @@ +/* Copyright (c) 2015-2016. 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 "src/mc/Channel.hpp" + +XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_Channel, mc, "MC interprocess communication"); + +namespace simgrid { +namespace mc { + +Channel::~Channel() +{ + if (this->socket_ >=0) + close(this->socket_); +} + +int Channel::send(const void* message, size_t size) const +{ + XBT_DEBUG("Protocol [%s] send %s", + MC_mode_name(mc_mode), + MC_message_type_name(*(e_mc_message_type*) message)); + + while (::send(this->socket_, message, size, 0) == -1) + if (errno == EINTR) + continue; + else + return errno; + return 0; +} + +ssize_t Channel::receive(void* message, size_t size, bool block) const +{ + int res = recv(this->socket_, message, size, block ? 0 : MSG_DONTWAIT); + if (res != -1) + XBT_DEBUG("Protocol [%s] received %s", + MC_mode_name(mc_mode), + MC_message_type_name(*(e_mc_message_type*) message)); + return res; +} + +} +} diff --git a/src/mc/Channel.hpp b/src/mc/Channel.hpp new file mode 100644 index 0000000000..61514adc36 --- /dev/null +++ b/src/mc/Channel.hpp @@ -0,0 +1,81 @@ +/* Copyright (c) 2015-2016. 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_CHANNEL_HPP +#define SIMGRID_MC_CHANNEL_HPP + +#include + +#include + +#include "src/mc/mc_protocol.h" + +namespace simgrid { +namespace mc { + +class Channel { + int socket_ = -1; + template + static constexpr bool messageType() + { + return std::is_class::value && std::is_trivial::value; + } +public: + + Channel() {} + Channel(int sock) : socket_(sock) {} + ~Channel(); + + // No copy: + Channel(Channel const&) = delete; + Channel& operator=(Channel const&) = delete; + + // Move: + Channel(Channel&& that) : socket_(that.socket_) + { + that.socket_ = -1; + } + Channel& operator=(Channel&& that) + { + this->socket_ = that.socket_; + that.socket_ = -1; + return *this; + } + + // Send + int send(const void* message, size_t size) const; + int send(e_mc_message_type type) const + { + s_mc_message message = { type }; + return this->send(&message, sizeof(message)); + } + template + typename std::enable_if< messageType(), int >::type + send(M const& m) const + { + return this->send(&m, sizeof(M)); + } + + // Receive + ssize_t receive(void* message, size_t size, bool block = true) const; + template + typename std::enable_if< messageType(), ssize_t >::type + receive(M& m) const + { + return this->receive(&m, sizeof(M)); + } + + int getSocket() const + { + return socket_; + } + +}; + +} +} + +#endif diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp index a385dfc6e4..bc69fbe034 100644 --- a/src/mc/ModelChecker.cpp +++ b/src/mc/ModelChecker.cpp @@ -88,7 +88,7 @@ void ModelChecker::start() // Prepare data for poll: struct pollfd* socket_pollfd = &fds_[SOCKET_FD_INDEX]; - socket_pollfd->fd = process_->socket();; + socket_pollfd->fd = process_->getChannel().getSocket(); socket_pollfd->events = POLLIN; socket_pollfd->revents = 0; @@ -173,7 +173,7 @@ void ModelChecker::shutdown() void ModelChecker::resume(simgrid::mc::Process& process) { - int res = process.send_message(MC_MESSAGE_CONTINUE); + int res = process.getChannel().send(MC_MESSAGE_CONTINUE); if (res) throw simgrid::xbt::errno_error(res); process.cache_flags = (mc_process_cache_flags_t) 0; @@ -310,7 +310,7 @@ bool ModelChecker::handle_events() if (socket_pollfd->revents) { if (socket_pollfd->revents & POLLIN) { - ssize_t size = MC_receive_message(socket_pollfd->fd, buffer, sizeof(buffer), MSG_DONTWAIT); + ssize_t size = process_->getChannel().receive(buffer, sizeof(buffer), false); if (size == -1 && errno != EAGAIN) throw simgrid::xbt::errno_error(errno); return handle_message(buffer, size); @@ -433,7 +433,7 @@ void ModelChecker::simcall_handle(simgrid::mc::Process& process, unsigned long p m.type = MC_MESSAGE_SIMCALL_HANDLE; m.pid = pid; m.value = value; - process.send_message(m); + process.getChannel().send(m); process.cache_flags = (mc_process_cache_flags_t) 0; while (process.running()) if (!this->handle_events()) diff --git a/src/mc/Process.cpp b/src/mc/Process.cpp index f9099a26b2..3f06a40b42 100644 --- a/src/mc/Process.cpp +++ b/src/mc/Process.cpp @@ -201,7 +201,7 @@ int open_vm(pid_t pid, int flags) // ***** Process Process::Process(pid_t pid, int sockfd) : - AddressSpace(this),pid_(pid), socket_(sockfd), running_(true) + AddressSpace(this), pid_(pid), channel_(sockfd), running_(true) {} void Process::init() @@ -233,12 +233,6 @@ void Process::init() Process::~Process() { - if (this->socket_ >= 0 && close(this->socket_) < 0) - xbt_die("Could not close communication socket"); - - this->maestro_stack_start_ = nullptr; - this->maestro_stack_end_ = nullptr; - if (this->memory_file >= 0) close(this->memory_file); @@ -246,13 +240,8 @@ Process::~Process() unw_destroy_addr_space(this->unw_underlying_addr_space); _UPT_destroy(this->unw_underlying_context); } - this->unw_underlying_context = nullptr; - this->unw_underlying_addr_space = nullptr; unw_destroy_addr_space(this->unw_addr_space); - this->unw_addr_space = nullptr; - - this->cache_flags = MC_PROCESS_CACHE_FLAG_NONE; if (this->clear_refs_fd_ >= 0) close(this->clear_refs_fd_); diff --git a/src/mc/Process.hpp b/src/mc/Process.hpp index a2cef8542e..36ef9944e3 100644 --- a/src/mc/Process.hpp +++ b/src/mc/Process.hpp @@ -22,9 +22,8 @@ #include #include -#if HAVE_MC #include "src/xbt/mmalloc/mmprivate.h" -#endif +#include "src/mc/Channel.hpp" #include #include "src/simix/popping_private.h" @@ -147,6 +146,9 @@ public: return this->heap_info.data(); } + Channel const& getChannel() const { return channel_; } + Channel& getChannel() { return channel_; } + std::vector const& ignored_regions() const { return ignored_regions_; @@ -170,25 +172,6 @@ public: running_ = false; } - template - typename std::enable_if< std::is_class::value && std::is_trivial::value, int >::type - send_message(M const& m) - { - return MC_protocol_send(this->socket_, &m, sizeof(M)); - } - - int send_message(e_mc_message_type message_id) - { - return MC_protocol_send_simple_message(this->socket_, message_id); - } - - template - typename std::enable_if< std::is_class::value && std::is_trivial::value, ssize_t >::type - receive_message(M& m) - { - return MC_receive_message(this->socket_, &m, sizeof(M), 0); - } - void reset_soft_dirty(); void read_pagemap(uint64_t* pagemap, size_t start_page, size_t page_count); @@ -226,7 +209,6 @@ public: void unignore_heap(void *address, size_t size); void ignore_local_variable(const char *var_name, const char *frame_name); - int socket() { return socket_; } std::vector& simix_processes(); std::vector& old_simix_processes(); @@ -238,7 +220,7 @@ private: private: pid_t pid_ = -1; - int socket_ = -1; + Channel channel_; bool running_ = false; std::vector memory_map_; RemotePtr maestro_stack_start_, maestro_stack_end_; diff --git a/src/mc/mc_checkpoint.cpp b/src/mc/mc_checkpoint.cpp index 171db1830b..1c0c1cefad 100644 --- a/src/mc/mc_checkpoint.cpp +++ b/src/mc/mc_checkpoint.cpp @@ -603,7 +603,7 @@ void restore_snapshot_regions(mc_snapshot_t snapshot) s_mc_restore_message message; message.type = MC_MESSAGE_RESTORE; message.index = snapshot->privatization_index; - mc_model_checker->process().send_message(message); + mc_model_checker->process().getChannel().send(message); } #endif } diff --git a/src/mc/mc_client.cpp b/src/mc/mc_client.cpp index a173b8f884..7598472033 100644 --- a/src/mc/mc_client.cpp +++ b/src/mc/mc_client.cpp @@ -25,30 +25,35 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_client, mc, "MC client logic"); -extern "C" { +namespace simgrid { +namespace mc { -mc_client_t mc_client; +std::unique_ptr Client::client_; -void MC_client_init(void) +Client* Client::initialize() { - if (mc_mode != MC_MODE_NONE) - return; + // We are not in MC mode: + // TODO, handle this more gracefully. if (!getenv(MC_ENV_SOCKET_FD)) - return; - mc_mode = MC_MODE_CLIENT; + return nullptr; - if (mc_client) { - XBT_WARN("MC_client_init called more than once."); - return; - } + // Do not break if we are called multiple times: + if (client_) + return client_.get(); + // Check and set the mode: + if (mc_mode != MC_MODE_NONE) + abort(); + mc_mode = MC_MODE_CLIENT; + + // Fetch socket from MC_ENV_SOCKET_FD: char* fd_env = std::getenv(MC_ENV_SOCKET_FD); if (!fd_env) - xbt_die("MC socket not found"); - - int fd = xbt_str_parse_int(fd_env,bprintf("Variable %s should contain a number but contains '%%s'", MC_ENV_SOCKET_FD)); + xbt_die("No MC socket passed in the environment"); + int fd = xbt_str_parse_int(fd_env, bprintf("Variable %s should contain a number but contains '%%s'", MC_ENV_SOCKET_FD)); XBT_DEBUG("Model-checked application found socket FD %i", fd); + // Check the socket type/validity: int type; socklen_t socklen = sizeof(type); if (getsockopt(fd, SOL_SOCKET, SO_TYPE, &type, &socklen) != 0) @@ -57,36 +62,25 @@ void MC_client_init(void) xbt_die("Unexpected socket type %i", type); XBT_DEBUG("Model-checked application found expected socket type"); - mc_client = xbt_new0(s_mc_client_t, 1); - mc_client->fd = fd; - mc_client->active = 1; + client_ = std::unique_ptr(new simgrid::mc::Client(fd)); - // Waiting for the model-checker: + // Wait for the model-checker: if (ptrace(PTRACE_TRACEME, 0, nullptr, NULL) == -1 || raise(SIGSTOP) != 0) xbt_die("Could not wait for the model-checker"); - MC_client_handle_messages(); -} -void MC_client_send_message(void* message, size_t size) -{ - if (MC_protocol_send(mc_client->fd, message, size)) - xbt_die("Could not send message %i", (int) ((mc_message_t)message)->type); + client_->handleMessages(); + return client_.get(); } -void MC_client_send_simple_message(e_mc_message_type type) -{ - if (MC_protocol_send_simple_message(mc_client->fd, type)) - xbt_die("Could not send message %i", type); -} - -void MC_client_handle_messages(void) +void Client::handleMessages() { while (1) { XBT_DEBUG("Waiting messages from model-checker"); char message_buffer[MC_MESSAGE_LENGTH]; ssize_t s; - if ((s = MC_receive_message(mc_client->fd, &message_buffer, sizeof(message_buffer), 0)) < 0) + + if ((s = channel_.receive(&message_buffer, sizeof(message_buffer))) < 0) xbt_die("Could not receive commands from the model-checker"); s_mc_message_t message; @@ -101,7 +95,7 @@ void MC_client_handle_messages(void) s_mc_int_message_t answer; answer.type = MC_MESSAGE_DEADLOCK_CHECK_REPLY; answer.value = result; - if (MC_protocol_send(mc_client->fd, &answer, sizeof(answer))) + if (channel_.send(answer)) xbt_die("Could not send response"); } break; @@ -119,7 +113,8 @@ void MC_client_handle_messages(void) if (!process) xbt_die("Invalid pid %lu", (unsigned long) message.pid); SIMIX_simcall_handle(&process->simcall, message.value); - MC_protocol_send_simple_message(mc_client->fd, MC_MESSAGE_WAITING); + if (channel_.send(MC_MESSAGE_WAITING)) + xbt_die("Could not send MESSAGE_WAITING to model-checker"); } break; @@ -143,13 +138,15 @@ void MC_client_handle_messages(void) } } -void MC_client_main_loop(void) +void Client::mainLoop(void) { while (1) { - MC_protocol_send_simple_message(mc_client->fd, MC_MESSAGE_WAITING); - MC_client_handle_messages(); + if (channel_.send(MC_MESSAGE_WAITING)) + xbt_die("Could not send WAITING mesage to model-checker"); + this->handleMessages(); simgrid::mc::wait_for_requests(); } } } +} diff --git a/src/mc/mc_client.h b/src/mc/mc_client.h index 0f1fc22baa..8ed4907dfe 100644 --- a/src/mc/mc_client.h +++ b/src/mc/mc_client.h @@ -9,29 +9,47 @@ #include +#include + #include + #include "src/mc/mc_protocol.h" +#include "src/mc/Channel.hpp" + +namespace simgrid { +namespace mc { + +class XBT_PUBLIC() Client { +private: + bool active_ = false; + Channel channel_; + static std::unique_ptr client_; +public: + Client(); + Client(int fd) : active_(true), channel_(fd) {} + void handleMessages(); + Channel const& getChannel() const { return channel_; } + Channel& getChannel() { return channel_; } + void mainLoop(void); + + // Singleton :/ + // TODO, remove the singleton antipattern. + static Client* initialize(); + static Client* get() + { + return client_.get(); + } +}; + +} +} SG_BEGIN_DECL() -typedef struct s_mc_client { - int active; - int fd; -} s_mc_client_t, *mc_client_t; - -extern XBT_PRIVATE mc_client_t mc_client; - -XBT_PRIVATE void MC_client_init(void); -XBT_PRIVATE void MC_client_handle_messages(void); -XBT_PRIVATE void MC_client_send_message(void* message, std::size_t size); -XBT_PRIVATE void MC_client_send_simple_message(e_mc_message_type type); - #if HAVE_MC void MC_ignore(void* addr, std::size_t size); #endif -void MC_client_main_loop(void); - SG_END_DECL() #endif diff --git a/src/mc/mc_client_api.cpp b/src/mc/mc_client_api.cpp index da2fece992..f3b6538d88 100644 --- a/src/mc/mc_client_api.cpp +++ b/src/mc/mc_client_api.cpp @@ -30,8 +30,9 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_client_api, mc, void MC_assert(int prop) { if (MC_is_active() && !prop) { - MC_client_send_simple_message(MC_MESSAGE_ASSERTION_FAILED); - MC_client_handle_messages(); + if (simgrid::mc::Client::get()->getChannel().send(MC_MESSAGE_ASSERTION_FAILED)) + xbt_die("Could not send assertion to model-checker"); + simgrid::mc::Client::get()->handleMessages(); } } @@ -50,7 +51,8 @@ void MC_ignore(void* addr, size_t size) message.type = MC_MESSAGE_IGNORE_MEMORY; message.addr = (std::uintptr_t) addr; message.size = size; - MC_client_send_message(&message, sizeof(message)); + if (simgrid::mc::Client::get()->getChannel().send(message)) + xbt_die("Could not send IGNORE_MEMORY mesage to model-checker"); } void MC_automaton_new_propositional_symbol(const char *id, int(*fct)(void)) @@ -77,5 +79,6 @@ void MC_automaton_new_propositional_symbol_pointer(const char *name, int* value) strncpy(message.name, name, sizeof(message.name)); message.callback = nullptr; message.data = value; - MC_client_send_message(&message, sizeof(message)); + if (simgrid::mc::Client::get()->getChannel().send(message)) + xbt_die("Could send REGISTER_SYMBOL message to model-checker"); } diff --git a/src/mc/mc_comm_determinism.cpp b/src/mc/mc_comm_determinism.cpp index 08366263ff..7745aa591f 100644 --- a/src/mc/mc_comm_determinism.cpp +++ b/src/mc/mc_comm_determinism.cpp @@ -468,7 +468,7 @@ int MC_modelcheck_comm_determinism(void) if (mc_mode == MC_MODE_CLIENT) // This will move somehwere else: - MC_client_handle_messages(); + simgrid::mc::Client::get()->handleMessages(); /* Create exploration stack */ mc_stack = xbt_fifo_new(); diff --git a/src/mc/mc_global.cpp b/src/mc/mc_global.cpp index 128e8772f9..7c33396c9b 100644 --- a/src/mc/mc_global.cpp +++ b/src/mc/mc_global.cpp @@ -140,7 +140,7 @@ void MC_run() { mc_mode = MC_MODE_CLIENT; MC_init(); - MC_client_main_loop(); + simgrid::mc::Client::get()->mainLoop(); } void MC_exit(void) @@ -155,10 +155,10 @@ int MC_deadlock_check() { if (mc_mode == MC_MODE_SERVER) { int res; - if ((res = mc_model_checker->process().send_message(MC_MESSAGE_DEADLOCK_CHECK))) + if ((res = mc_model_checker->process().getChannel().send(MC_MESSAGE_DEADLOCK_CHECK))) xbt_die("Could not check deadlock state"); s_mc_int_message_t message; - ssize_t s = mc_model_checker->process().receive_message(message); + ssize_t s = mc_model_checker->process().getChannel().receive(message); if (s == -1) xbt_die("Could not receive message"); if (s != sizeof(message) || message.type != MC_MESSAGE_DEADLOCK_CHECK_REPLY) diff --git a/src/mc/mc_ignore.cpp b/src/mc/mc_ignore.cpp index 51d781c403..4ff5d5fcaa 100644 --- a/src/mc/mc_ignore.cpp +++ b/src/mc/mc_ignore.cpp @@ -43,7 +43,7 @@ void MC_ignore_heap(void *address, size_t size) heap->heapinfo[message.block].busy_frag.ignore[message.fragment]++; } - if (MC_protocol_send(mc_client->fd, &message, sizeof(message))) + if (simgrid::mc::Client::get()->getChannel().send(message)) xbt_die("Could not send ignored region to MCer"); } @@ -56,7 +56,8 @@ void MC_remove_ignore_heap(void *address, size_t size) message.type = MC_MESSAGE_UNIGNORE_HEAP; message.addr = (std::uintptr_t) address; message.size = size; - MC_client_send_message(&message, sizeof(message)); + if (simgrid::mc::Client::get()->getChannel().send(message)) + xbt_die("Could not send UNIGNORE_HEAP mesasge to model-checker"); } void MC_ignore_global_variable(const char *name) @@ -101,7 +102,8 @@ void MC_register_stack_area(void *stack, smx_process_t process, ucontext_t* cont s_mc_stack_region_message_t message; message.type = MC_MESSAGE_STACK_REGION; message.stack_region = region; - MC_client_send_message(&message, sizeof(message)); + if (simgrid::mc::Client::get()->getChannel().send(message)) + xbt_die("Coule not send STACK_REGION to model-checker"); } } diff --git a/src/mc/mc_protocol.cpp b/src/mc/mc_protocol.cpp index 55ab2954e6..3815d39b1e 100644 --- a/src/mc/mc_protocol.cpp +++ b/src/mc/mc_protocol.cpp @@ -19,39 +19,6 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_protocol, mc, "Generic MC protocol logic"); -extern "C" { - -int MC_protocol_send(int socket, const void* message, std::size_t size) -{ - XBT_DEBUG("Protocol [%s] send %s", - MC_mode_name(mc_mode), - MC_message_type_name(*(e_mc_message_type*) message)); - - while (send(socket, message, size, 0) == -1) - if (errno == EINTR) - continue; - else - return errno; - return 0; -} - -int MC_protocol_send_simple_message(int socket, e_mc_message_type type) -{ - s_mc_message_t message; - message.type = type; - return MC_protocol_send(socket, &message, sizeof(message)); -} - -ssize_t MC_receive_message(int socket, void* message, size_t size, int options) -{ - int res = recv(socket, message, size, options); - if (res != -1) - XBT_DEBUG("Protocol [%s] received %s", - MC_mode_name(mc_mode), - MC_message_type_name(*(e_mc_message_type*) message)); - return res; -} - const char* MC_message_type_name(e_mc_message_type type) { switch(type) { @@ -97,5 +64,3 @@ const char* MC_mode_name(e_mc_mode_t mode) return "?"; } } - -} diff --git a/src/mc/mc_protocol.h b/src/mc/mc_protocol.h index bd6fd13538..b48902b545 100644 --- a/src/mc/mc_protocol.h +++ b/src/mc/mc_protocol.h @@ -114,10 +114,6 @@ typedef struct s_mc_restore_message { int index; } s_mc_restore_message_t, *mc_restore_message_t; -XBT_PRIVATE int MC_protocol_send(int socket, const void* message, size_t size); -XBT_PRIVATE int MC_protocol_send_simple_message(int socket, e_mc_message_type type); -XBT_PRIVATE ssize_t MC_receive_message(int socket, void* message, size_t size, int options); - XBT_PRIVATE const char* MC_message_type_name(e_mc_message_type type); XBT_PRIVATE const char* MC_mode_name(e_mc_mode_t mode); diff --git a/src/simix/smx_global.cpp b/src/simix/smx_global.cpp index b48faf5a04..8a92857d2f 100644 --- a/src/simix/smx_global.cpp +++ b/src/simix/smx_global.cpp @@ -266,7 +266,7 @@ void SIMIX_global_init(int *argc, char **argv) #if HAVE_MC // The communication initialization is done ASAP. // We need to communicate initialization of the different layers to the model-checker. - MC_client_init(); + simgrid::mc::Client::initialize(); #endif if (_sg_cfg_exit_asap) diff --git a/tools/cmake/DefinePackages.cmake b/tools/cmake/DefinePackages.cmake index ef11ae1ad3..99b5aa578d 100644 --- a/tools/cmake/DefinePackages.cmake +++ b/tools/cmake/DefinePackages.cmake @@ -549,6 +549,8 @@ set(MC_SRC src/mc/RemotePtr.hpp src/mc/AddressSpace.hpp src/mc/AddressSpace.cpp + src/mc/Channel.cpp + src/mc/Channel.hpp src/mc/Frame.hpp src/mc/Frame.cpp src/mc/ModelChecker.hpp -- 2.20.1