From 33aec8491c4c337352f570c24f8a76298e3a319c Mon Sep 17 00:00:00 2001 From: Gabriel Corona Date: Fri, 18 Mar 2016 17:00:55 +0100 Subject: [PATCH] [mc] Working on an interface between a model-checking session and a model-checking algorithm --- include/xbt/system_error.hpp | 5 + src/mc/Checker.cpp | 26 ++++++ src/mc/Checker.hpp | 58 ++++++++++++ src/mc/Session.cpp | 148 +++++++++++++++++++++++++++++ src/mc/Session.hpp | 70 ++++++++++++++ src/mc/mc_forward.hpp | 4 + src/mc/simgrid_mc.cpp | 156 +++++++------------------------ tools/cmake/DefinePackages.cmake | 4 + 8 files changed, 347 insertions(+), 124 deletions(-) create mode 100644 src/mc/Checker.cpp create mode 100644 src/mc/Checker.hpp create mode 100644 src/mc/Session.cpp create mode 100644 src/mc/Session.hpp diff --git a/include/xbt/system_error.hpp b/include/xbt/system_error.hpp index f2aabe7f83..f580e750ce 100644 --- a/include/xbt/system_error.hpp +++ b/include/xbt/system_error.hpp @@ -8,6 +8,9 @@ #include +#ifndef SIMGRID_MC_SYSTEM_ERROR_HPP +#define SIMGRID_MC_SYSTEM_ERROR_HPP + namespace simgrid { namespace xbt { @@ -31,3 +34,5 @@ std::system_error errno_error(int errnum, const char* what) } } + +#endif diff --git a/src/mc/Checker.cpp b/src/mc/Checker.cpp new file mode 100644 index 0000000000..159e3d5780 --- /dev/null +++ b/src/mc/Checker.cpp @@ -0,0 +1,26 @@ +/* Copyright (c) 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 "src/mc/Checker.hpp" + +namespace simgrid { +namespace mc { + +Checker::~Checker() +{ +} + +FunctionalChecker::~FunctionalChecker() +{ +} + +int FunctionalChecker::run() +{ + return function_(*session_); +} + +} +} diff --git a/src/mc/Checker.hpp b/src/mc/Checker.hpp new file mode 100644 index 0000000000..478665a8f9 --- /dev/null +++ b/src/mc/Checker.hpp @@ -0,0 +1,58 @@ +/* Copyright (c) 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_CHECKER_HPP +#define SIMGRID_MC_CHECKER_HPP + +#include +#include + +#include "src/mc/mc_forward.hpp" + +namespace simgrid { +namespace mc { + +/** A model-checking algorithm + * + * The goal is to move the data/state/configuration of a model-checking + * algorihms in subclasses. Implementing this interface will probably + * not be really mandatory, you might be able to write your + * model-checking algorithm as plain imperative code instead. + * + * It works by manipulating a model-checking Session. + */ +// abstract +class Checker { + Session* session_; +public: + Checker(Session& session) : session_(&session) {} + + // No copy: + Checker(Checker const&) = delete; + Checker& operator=(Checker const&) = delete; + + virtual ~Checker(); + virtual int run() = 0; + +protected: + Session& getSession() { return *session_; } +}; + +/** Adapt a std::function to a checker */ +class FunctionalChecker : public Checker { + Session* session_; + std::function function_; +public: + FunctionalChecker(Session& session, std::function f) + : Checker(session), function_(std::move(f)) {} + ~FunctionalChecker(); + int run() override; +}; + +} +} + +#endif diff --git a/src/mc/Session.cpp b/src/mc/Session.cpp new file mode 100644 index 0000000000..961a9abff9 --- /dev/null +++ b/src/mc/Session.cpp @@ -0,0 +1,148 @@ +/* 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 + +#include "src/mc/Session.hpp" + +XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_Session, mc, "Model-checker session"); + +namespace simgrid { +namespace mc { + +static void setup_child_environment(int socket) +{ +#ifdef __linux__ + // Make sure we do not outlive our parent: + sigset_t mask; + sigemptyset (&mask); + if (sigprocmask(SIG_SETMASK, &mask, nullptr) < 0) + throw simgrid::xbt::errno_error(errno, "Could not unblock signals"); + if (prctl(PR_SET_PDEATHSIG, SIGHUP) != 0) + throw simgrid::xbt::errno_error(errno, "Could not PR_SET_PDEATHSIG"); +#endif + + int res; + + // Remove CLOEXEC in order to pass the socket to the exec-ed program: + int fdflags = fcntl(socket, F_GETFD, 0); + if (fdflags == -1 || fcntl(socket, F_SETFD, fdflags & ~FD_CLOEXEC) == -1) + throw simgrid::xbt::errno_error(errno, "Could not remove CLOEXEC for socket"); + + // Set environment: + setenv(MC_ENV_VARIABLE, "1", 1); + + // Disable lazy relocation in the model-checked process. + // We don't want the model-checked process to modify its .got.plt during + // snapshot. + setenv("LC_BIND_NOW", "1", 1); + + char buffer[64]; + res = std::snprintf(buffer, sizeof(buffer), "%i", socket); + if ((size_t) res >= sizeof(buffer) || res == -1) + std::abort(); + setenv(MC_ENV_SOCKET_FD, buffer, 1); +} + +/** Execute some code in a forked process */ +template +static inline +pid_t do_fork(F code) +{ + pid_t pid = fork(); + if (pid < 0) + throw simgrid::xbt::errno_error(errno, "Could not fork model-checked process"); + if (pid != 0) + return pid; + + // Child-process: + try { + code(); + _exit(EXIT_SUCCESS); + } + catch(...) { + // The callback should catch exceptions: + std::terminate(); + } +} + +Session::Session(pid_t pid, int socket) +{ + std::unique_ptr process(new simgrid::mc::Process(pid, socket)); + // TODO, automatic detection of the config from the process + process->privatized( + sg_cfg_get_boolean("smpi/privatize_global_variables")); + modelChecker_ = std::unique_ptr( + new simgrid::mc::ModelChecker(std::move(process))); + xbt_assert(mc_model_checker == nullptr); + mc_model_checker = modelChecker_.get(); + mc_model_checker->start(); +} + +Session::~Session() +{ + this->close(); +} + +// static +Session* Session::fork(std::function code) +{ + // Create a AF_LOCAL socketpair used for exchanging messages + // bewteen the model-checker process (ourselves) and the model-checked + // process: + int res; + int sockets[2]; + res = socketpair(AF_LOCAL, SOCK_DGRAM | SOCK_CLOEXEC, 0, sockets); + if (res == -1) + throw simgrid::xbt::errno_error(errno, "Could not create socketpair"); + + pid_t pid = do_fork([&] { + ::close(sockets[1]); + setup_child_environment(sockets[0]); + code(); + xbt_die("The model-checked process failed to exec()"); + }); + + // Parent (model-checker): + ::close(sockets[0]); + + return new Session(pid, sockets[1]); +} + +// static +Session* Session::spawnv(const char *path, char *const argv[]) +{ + return Session::fork([&] { + execv(path, argv); + }); +} + +// static +Session* Session::spawnvp(const char *path, char *const argv[]) +{ + return Session::fork([&] { + execvp(path, argv); + }); +} + +void Session::close() +{ + if (modelChecker_) { + modelChecker_->shutdown(); + modelChecker_ = nullptr; + mc_model_checker = nullptr; + } +} + +} +} \ No newline at end of file diff --git a/src/mc/Session.hpp b/src/mc/Session.hpp new file mode 100644 index 0000000000..47c10e7c17 --- /dev/null +++ b/src/mc/Session.hpp @@ -0,0 +1,70 @@ +/* Copyright (c) 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_SESSION_HPP +#define SIMGRID_MC_SESSION_HPP + +#ifdef __linux__ +#include +#endif + +#include +#include +#include +#include + +#include + +#include + +#include "src/mc/mc_forward.hpp" +#include "src/mc/ModelChecker.hpp" + +namespace simgrid { +namespace mc { + +/** A model-checking session + * + * This is expected to become the interface used by model-checking + * algorithms to control the execution of the model-checked process + * and the exploration of the execution graph. Model-checking + * algorithms should be able to be written in high-level languages + * (e.g. Python) using bindings on this interface. + */ +class Session { +private: + std::unique_ptr modelChecker_; + +private: // + Session(pid_t pid, int socket); + + // No copy: + Session(Session const&) = delete; + Session& operator=(Session const&) = delete; + +public: + ~Session(); + void close(); + +public: // static constructors + + /** Create a new session by forking + * + * The code is expected to `exec` the model-checker program. + */ + static Session* fork(std::function code); + + /** Create a session using `execv` */ + static Session* spawnv(const char *path, char *const argv[]); + + /** Create a session using `execvp` */ + static Session* spawnvp(const char *path, char *const argv[]); +}; + +} +} + +#endif diff --git a/src/mc/mc_forward.hpp b/src/mc/mc_forward.hpp index b71caabc3f..5b0cc70278 100644 --- a/src/mc/mc_forward.hpp +++ b/src/mc/mc_forward.hpp @@ -28,6 +28,10 @@ class Variable; class Frame; class SimixProcessInformation; +class Session; +class Checker; +class FunctionalChecker; + } } diff --git a/src/mc/simgrid_mc.cpp b/src/mc/simgrid_mc.cpp index 0c3a6f481e..e153b0c9a2 100644 --- a/src/mc/simgrid_mc.cpp +++ b/src/mc/simgrid_mc.cpp @@ -12,24 +12,9 @@ #include -#include -#include -#include - #include -#include -#include -#include -#include - -#ifdef __linux__ -#include -#endif - #include -#include -#include #include "simgrid/sg_config.h" #include "src/xbt_modinter.h" @@ -41,98 +26,11 @@ #include "src/mc/mc_comm_pattern.h" #include "src/mc/mc_liveness.h" #include "src/mc/mc_exit.h" +#include "src/mc/Session.hpp" +#include "src/mc/Checker.hpp" XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_main, mc, "Entry point for simgrid-mc"); -/** Execute some code in a forked process */ -template -static inline -pid_t do_fork(F f) -{ - pid_t pid = fork(); - if (pid < 0) - throw simgrid::xbt::errno_error(errno, "Could not fork model-checked process"); - if (pid != 0) - return pid; - - // Child-process: - try { - f(); - _exit(EXIT_SUCCESS); - } - catch(...) { - // The callback should catch exceptions: - abort(); - } -} - -static -int exec_model_checked(int socket, char** argv) -{ - XBT_DEBUG("Inside the child process PID=%i", (int) getpid()); - -#ifdef __linux__ - // Make sure we do not outlive our parent: - sigset_t mask; - sigemptyset (&mask); - if (sigprocmask(SIG_SETMASK, &mask, nullptr) < 0) - throw simgrid::xbt::errno_error(errno, "Could not unblock signals"); - if (prctl(PR_SET_PDEATHSIG, SIGHUP) != 0) - throw simgrid::xbt::errno_error(errno, "Could not PR_SET_PDEATHSIG"); -#endif - - int res; - - // Remove CLOEXEC in order to pass the socket to the exec-ed program: - int fdflags = fcntl(socket, F_GETFD, 0); - if (fdflags == -1 || fcntl(socket, F_SETFD, fdflags & ~FD_CLOEXEC) == -1) - throw simgrid::xbt::errno_error(errno, "Could not remove CLOEXEC for socket"); - - // Set environment: - setenv(MC_ENV_VARIABLE, "1", 1); - - // Disable lazy relocation in the model-checked process. - // We don't want the model-checked process to modify its .got.plt during - // snapshot. - setenv("LC_BIND_NOW", "1", 1); - - char buffer[64]; - res = std::snprintf(buffer, sizeof(buffer), "%i", socket); - if ((size_t) res >= sizeof(buffer) || res == -1) - std::abort(); - setenv(MC_ENV_SOCKET_FD, buffer, 1); - - execvp(argv[1], argv+1); - - XBT_ERROR("Could not run the model-checked program"); - // This is the value used by system() and popen() in this case: - return 127; -} - -static -std::pair create_model_checked(char** argv) -{ - // Create a AF_LOCAL socketpair used for exchanging messages - // bewteen the model-checker process (ourselves) and the model-checked - // process: - int res; - int sockets[2]; - res = socketpair(AF_LOCAL, SOCK_DGRAM | SOCK_CLOEXEC, 0, sockets); - if (res == -1) - throw simgrid::xbt::errno_error(errno, "Could not create socketpair"); - - pid_t pid = do_fork([&] { - close(sockets[1]); - int res = exec_model_checked(sockets[0], argv); - XBT_DEBUG("Error in the child process creation"); - _exit(res); - }); - - // Parent (model-checker): - close(sockets[0]); - return std::make_pair(pid, sockets[1]); -} - static char** argvdup(int argc, char** argv) { @@ -142,13 +40,38 @@ char** argvdup(int argc, char** argv) return argv_copy; } +static +std::unique_ptr createChecker(simgrid::mc::Session& session) +{ + using simgrid::mc::Session; + using simgrid::mc::FunctionalChecker; + + std::function code; + if (_sg_mc_comms_determinism || _sg_mc_send_determinism) + code = [](Session& session) { + return MC_modelcheck_comm_determinism(); }; + else if (!_sg_mc_property_file || _sg_mc_property_file[0] == '\0') + code = [](Session& session) { + return simgrid::mc::modelcheck_safety(); }; + else + code = [](Session& session) { + return simgrid::mc::modelcheck_liveness(); }; + + return std::unique_ptr( + new FunctionalChecker(session, std::move(code))); +} + int main(int argc, char** argv) { + using simgrid::mc::Session; + try { if (argc < 2) xbt_die("Missing arguments.\n"); + // Currently, we need this before sg_config_init: _sg_do_model_check = 1; + mc_mode = MC_MODE_SERVER; // The initialisation function can touch argv. // We need to keep the original parameters in order to pass them to the @@ -158,26 +81,11 @@ int main(int argc, char** argv) xbt_log_init(&argc_copy, argv_copy); sg_config_init(&argc_copy, argv_copy); - int sock; - pid_t model_checked_pid; - std::tie(model_checked_pid, sock) = create_model_checked(argv); - XBT_DEBUG("Inside the parent process"); - if (mc_model_checker) - xbt_die("MC server already present"); - - mc_mode = MC_MODE_SERVER; - std::unique_ptr process(new simgrid::mc::Process(model_checked_pid, sock)); - process->privatized(sg_cfg_get_boolean("smpi/privatize_global_variables")); - mc_model_checker = new simgrid::mc::ModelChecker(std::move(process)); - mc_model_checker->start(); - int res = 0; - if (_sg_mc_comms_determinism || _sg_mc_send_determinism) - res = MC_modelcheck_comm_determinism(); - else if (!_sg_mc_property_file || _sg_mc_property_file[0] == '\0') - res = simgrid::mc::modelcheck_safety(); - else - res = simgrid::mc::modelcheck_liveness(); - mc_model_checker->shutdown(); + std::unique_ptr session = + std::unique_ptr(Session::spawnvp(argv[1], argv+1)); + std::unique_ptr checker = createChecker(*session); + int res = checker->run(); + session->close(); return res; } catch(std::exception& e) { diff --git a/tools/cmake/DefinePackages.cmake b/tools/cmake/DefinePackages.cmake index 3e41773ce9..989aa3cc14 100644 --- a/tools/cmake/DefinePackages.cmake +++ b/tools/cmake/DefinePackages.cmake @@ -550,6 +550,8 @@ set(MC_SRC src/mc/AddressSpace.cpp src/mc/Channel.cpp src/mc/Channel.hpp + src/mc/Checker.cpp + src/mc/Checker.hpp src/mc/Client.cpp src/mc/Client.hpp src/mc/Frame.hpp @@ -570,6 +572,8 @@ set(MC_SRC src/mc/mc_forward.hpp src/mc/Process.hpp src/mc/Process.cpp + src/mc/Session.cpp + src/mc/Session.hpp src/mc/mc_unw.h src/mc/mc_unw.cpp src/mc/mc_unw_vmread.cpp -- 2.20.1