From: Martin Quinson Date: Mon, 10 Jun 2019 20:54:41 +0000 (+0200) Subject: code simplification in MC start sequence X-Git-Tag: v3.23~52 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/7f5e78a43b4bed7bae8304ad12de6e2e555b34db code simplification in MC start sequence --- diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp index f50fac1a16..4250bffe34 100644 --- a/src/mc/ModelChecker.cpp +++ b/src/mc/ModelChecker.cpp @@ -53,8 +53,6 @@ ModelChecker::~ModelChecker() { void ModelChecker::start() { - const pid_t pid = process_->pid(); - base_ = event_base_new(); event_callback_fn event_callback = [](evutil_socket_t fd, short events, void *arg) { @@ -72,6 +70,8 @@ void ModelChecker::start() int status; // The model-checked process SIGSTOP itself to signal it's ready: + const pid_t pid = process_->pid(); + pid_t res = waitpid(pid, &status, WAITPID_CHECKED_FLAGS); if (res < 0 || not WIFSTOPPED(status) || WSTOPSIG(status) != SIGSTOP) xbt_die("Could not wait model-checked process"); diff --git a/src/mc/Session.cpp b/src/mc/Session.cpp index 87ed0f5073..4d73338e5f 100644 --- a/src/mc/Session.cpp +++ b/src/mc/Session.cpp @@ -77,16 +77,35 @@ pid_t do_fork(F code) } } -Session::Session(pid_t pid, int socket) +Session::Session(const std::function& code) { - std::unique_ptr process(new simgrid::mc::RemoteClient(pid, socket)); - #if HAVE_SMPI xbt_assert(smpi_privatize_global_variables != SmpiPrivStrategies::MMAP, "Please use the dlopen privatization schema when model-checking SMPI code"); #endif + // Create a AF_LOCAL socketpair used for exchanging messages + // between the model-checker process (ourselves) and the model-checked + // process: + int res; + int sockets[2]; + res = socketpair(AF_LOCAL, SOCK_SEQPACKET | SOCK_CLOEXEC, 0, sockets); + if (res == -1) + throw simgrid::xbt::errno_error("Could not create socketpair"); + + pid_t pid = do_fork([sockets, &code] { + ::close(sockets[1]); + setup_child_environment(sockets[0]); + code(); + xbt_die("The model-checked process failed to exec()"); + }); + + // Parent (model-checker): + ::close(sockets[0]); + + std::unique_ptr process(new simgrid::mc::RemoteClient(pid, sockets[1])); model_checker_.reset(new simgrid::mc::ModelChecker(std::move(process))); + xbt_assert(mc_model_checker == nullptr); mc_model_checker = model_checker_.get(); mc_model_checker->start(); @@ -129,47 +148,6 @@ void Session::log_state() } } -// static -Session* Session::fork(const std::function& code) -{ - // Create a AF_LOCAL socketpair used for exchanging messages - // between the model-checker process (ourselves) and the model-checked - // process: - int res; - int sockets[2]; - res = socketpair(AF_LOCAL, SOCK_SEQPACKET | SOCK_CLOEXEC, 0, sockets); - if (res == -1) - throw simgrid::xbt::errno_error("Could not create socketpair"); - - pid_t pid = do_fork([sockets, &code] { - ::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([path, argv] { - execv(path, argv); - }); -} - -// static -Session* Session::spawnvp(const char *file, char *const argv[]) -{ - return Session::fork([file, argv] { - execvp(file, argv); - }); -} - void Session::close() { initial_snapshot_ = nullptr; diff --git a/src/mc/Session.hpp b/src/mc/Session.hpp index 283366cda8..3a79387222 100644 --- a/src/mc/Session.hpp +++ b/src/mc/Session.hpp @@ -26,13 +26,20 @@ private: std::unique_ptr model_checker_; std::shared_ptr initial_snapshot_; - Session(pid_t pid, int socket); - // No copy: Session(Session const&) = delete; Session& operator=(Session const&) = delete; public: + /** Create a new session by executing the provided code in a fork() + * + * This sets up the environment for the model-checked process + * (environment variables, sockets, etc.). + * + * The code is expected to `exec` the model-checked application. + */ + Session(const std::function& code); + ~Session(); void close(); @@ -41,31 +48,6 @@ public: void log_state(); void restore_initial_state(); - - // static constructors - - /** Create a new session by forking - * - * This sets up the environment for the model-checked process - * (environment variables, sockets, etc.). - * - * The code is expected to `exec` the model-checker program. - */ - static Session* fork(const std::function& code); - - /** Spawn a model-checked process - * - * @param path full path of the executable - * @param argv arguments for the model-checked process (NULL-terminated) - */ - static Session* spawnv(const char *path, char *const argv[]); - - /** Spawn a model-checked process (using PATH) - * - * @param file file name of the executable (found using `PATH`) - * @param argv arguments for the model-checked process (NULL-terminated) - */ - static Session* spawnvp(const char *file, char *const argv[]); }; // Temporary :) diff --git a/src/mc/checker/simgrid_mc.cpp b/src/mc/checker/simgrid_mc.cpp index 0a713b8550..0c59749710 100644 --- a/src/mc/checker/simgrid_mc.cpp +++ b/src/mc/checker/simgrid_mc.cpp @@ -12,6 +12,7 @@ #include #include +#include XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_main, mc, "Entry point for simgrid-mc"); @@ -52,12 +53,12 @@ int main(int argc, char** argv) xbt_log_init(&argc, argv); sg_config_init(&argc, argv); - std::unique_ptr session = - std::unique_ptr(Session::spawnvp(argv_copy[1], argv_copy+1)); + simgrid::mc::session = new Session([argv_copy] { + execvp(argv_copy[1], argv_copy+1); + }); delete[] argv_copy; - simgrid::mc::session = session.get(); - std::unique_ptr checker = createChecker(*session); + std::unique_ptr checker = createChecker(*simgrid::mc::session); int res = SIMGRID_MC_EXIT_SUCCESS; try { checker->run(); @@ -69,7 +70,7 @@ int main(int argc, char** argv) res = SIMGRID_MC_EXIT_LIVENESS; } checker = nullptr; - session->close(); + simgrid::mc::session->close(); return res; } catch(std::exception& e) {