X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/30a925489c6e4d4a92042ef80de375c56ccb562b..96d281781f5a45598b4c1fa42fa2059d15d53c73:/src/mc/simgrid_mc.cpp diff --git a/src/mc/simgrid_mc.cpp b/src/mc/simgrid_mc.cpp index c05d0ae4ee..949ed65cd0 100644 --- a/src/mc/simgrid_mc.cpp +++ b/src/mc/simgrid_mc.cpp @@ -12,23 +12,9 @@ #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" @@ -38,101 +24,16 @@ #include "src/mc/mc_protocol.h" #include "src/mc/mc_safety.h" #include "src/mc/mc_comm_pattern.h" -#include "src/mc/mc_liveness.h" +#include "src/mc/LivenessChecker.hpp" #include "src/mc/mc_exit.h" +#include "src/mc/Session.hpp" +#include "src/mc/Checker.hpp" +#include "src/mc/CommunicationDeterminismChecker.hpp" +#include "src/mc/SafetyChecker.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(); - std::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) { char** argv_copy = xbt_new(char*, argc+1); @@ -141,42 +42,54 @@ 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) + return std::unique_ptr( + new simgrid::mc::CommunicationDeterminismChecker(session)); + else if (!_sg_mc_property_file || _sg_mc_property_file[0] == '\0') + return std::unique_ptr( + new simgrid::mc::SafetyChecker(session)); + else + return std::unique_ptr( + new simgrid::mc::LivenessChecker(session)); + + 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 - // model-checked process so we make a copy of them: - int argc_copy = argc; + // 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_copy, argv_copy); - sg_config_init(&argc_copy, argv_copy); + xbt_log_init(&argc, argv); + sg_config_init(&argc, argv); - 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"); + std::unique_ptr session = + std::unique_ptr(Session::spawnvp(argv_copy[1], argv_copy+1)); + free(argv_copy); - 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(); + simgrid::mc::session = session.get(); + std::unique_ptr checker = createChecker(*session); + int res = checker->run(); + session->close(); return res; } catch(std::exception& e) {