X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/d51a876f765fc68b3e1e667f867b91a1b4987a85..28e3d706d2b879fc7e84f569cd8cd72a86e0c550:/src/mc/simgrid_mc.cpp diff --git a/src/mc/simgrid_mc.cpp b/src/mc/simgrid_mc.cpp index e0f61709de..b8b4b08e76 100644 --- a/src/mc/simgrid_mc.cpp +++ b/src/mc/simgrid_mc.cpp @@ -10,20 +10,10 @@ #include #include -#include -#include +#include #include -#include -#include -#include -#include - -#ifdef __linux__ -#include -#endif - #include #include "simgrid/sg_config.h" @@ -36,136 +26,77 @@ #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" +#include "src/mc/SafetyChecker.hpp" XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_main, mc, "Entry point for simgrid-mc"); -static int do_child(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) { - std::perror ("sigprocmask"); - return SIMGRID_MC_EXIT_ERROR; - } - - if (prctl(PR_SET_PDEATHSIG, SIGHUP) != 0) { - std::perror("simgrid-mc"); - return SIMGRID_MC_EXIT_ERROR; - } -#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) { - std::perror("simgrid-mc"); - return SIMGRID_MC_EXIT_ERROR; - } - if (fcntl(socket, F_SETFD, fdflags & ~FD_CLOEXEC) == -1) { - std::perror("simgrid-mc"); - return SIMGRID_MC_EXIT_ERROR; - } - - XBT_DEBUG("CLOEXEC removed on socket %i", socket); - - // Set environment: - setenv(MC_ENV_VARIABLE, "1", 1); - - // Disable lazy relocation in the model-ched 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) - return SIMGRID_MC_EXIT_ERROR; - setenv(MC_ENV_SOCKET_FD, buffer, 1); - - execvp(argv[1], argv+1); - XBT_ERROR("Could not execute the child process"); - return SIMGRID_MC_EXIT_ERROR; -} - -static int do_parent(int socket, pid_t child) -{ - XBT_DEBUG("Inside the parent process"); - if (mc_model_checker) - xbt_die("MC server already present"); - try { - mc_mode = MC_MODE_SERVER; - std::unique_ptr process(new simgrid::mc::Process(child, socket)); - 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 = MC_modelcheck_safety(); - else - res = MC_modelcheck_liveness(); - mc_model_checker->shutdown(); - return res; - } - catch(std::exception& e) { - XBT_ERROR("Exception: %s", e.what()); - return SIMGRID_MC_EXIT_ERROR; - } -} - -static char** argvdup(int argc, char** argv) +static inline +char** argvdup(int argc, char** argv) { char** argv_copy = xbt_new(char*, argc+1); std::memcpy(argv_copy, argv, sizeof(char*) * argc); - argv_copy[argc] = NULL; + argv_copy[argc] = nullptr; return argv_copy; } -int main(int argc, char** argv) +static +std::unique_ptr createChecker(simgrid::mc::Session& session) { - _sg_do_model_check = 1; + 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') + return std::unique_ptr( + new simgrid::mc::SafetyChecker(session)); + else + code = [](Session& session) { + return simgrid::mc::modelcheck_liveness(); }; + + return std::unique_ptr( + new FunctionalChecker(session, std::move(code))); +} - // We need to keep the original parameters in order to pass them to the - // model-checked process: - int argc_copy = argc; - char** argv_copy = argvdup(argc, argv); - xbt_log_init(&argc_copy, argv_copy); - sg_config_init(&argc_copy, argv_copy); +int main(int argc, char** argv) +{ + using simgrid::mc::Session; - if (argc < 2) - xbt_die("Missing arguments.\n"); + try { + if (argc < 2) + xbt_die("Missing arguments.\n"); - // Create a AF_LOCAL socketpair: - int res; + // Currently, we need this before sg_config_init: + _sg_do_model_check = 1; + mc_mode = MC_MODE_SERVER; - int sockets[2]; - res = socketpair(AF_LOCAL, SOCK_DGRAM | SOCK_CLOEXEC, 0, sockets); - if (res == -1) { - perror("simgrid-mc"); + // The initialisation function can touch argv. + // We make a copy of argv before modifying it in order to pass the original + // value to the model-checked: + char** argv_copy = argvdup(argc, 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)); + free(argv_copy); + + simgrid::mc::session = session.get(); + std::unique_ptr checker = createChecker(*session); + int res = checker->run(); + session->close(); + return res; + } + catch(std::exception& e) { + XBT_ERROR("Exception: %s", e.what()); return SIMGRID_MC_EXIT_ERROR; } - - XBT_DEBUG("Created socketpair"); - - pid_t pid = fork(); - if (pid < 0) { - perror("simgrid-mc"); + catch(...) { + XBT_ERROR("Unknown exception"); return SIMGRID_MC_EXIT_ERROR; - } else if (pid == 0) { - close(sockets[1]); - int res = do_child(sockets[0], argv); - XBT_DEBUG("Error in the child process creation"); - return res; - } else { - close(sockets[0]); - return do_parent(sockets[1], pid); } - - return 0; }