1 /* Copyright (c) 2015. The SimGrid Team.
2 * All rights reserved. */
4 /* This program is free software; you can redistribute it and/or modify it
5 * under the terms of the license (GNU LGPL) which comes with this package. */
20 #include <sys/types.h>
21 #include <sys/socket.h>
23 #include <sys/ptrace.h>
26 #include <sys/prctl.h>
31 #include "simgrid/sg_config.h"
32 #include "src/xbt_modinter.h"
34 #include "src/mc/mc_base.h"
35 #include "src/mc/mc_private.h"
36 #include "src/mc/mc_protocol.h"
37 #include "src/mc/mc_safety.h"
38 #include "src/mc/mc_comm_pattern.h"
39 #include "src/mc/mc_liveness.h"
40 #include "src/mc/mc_exit.h"
42 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_main, mc, "Entry point for simgrid-mc");
44 /** Execute some code in a forked process */
51 throw simgrid::mc::errno_error(errno, "Could not fork model-checked process");
58 std::exit(EXIT_SUCCESS);
61 // The callback should catch exceptions:
67 int exec_model_checked(int socket, char** argv)
69 XBT_DEBUG("Inside the child process PID=%i", (int) getpid());
72 // Make sure we do not outlive our parent:
75 if (sigprocmask(SIG_SETMASK, &mask, nullptr) < 0)
76 throw simgrid::mc::errno_error(errno, "Could not unblock signals");
77 if (prctl(PR_SET_PDEATHSIG, SIGHUP) != 0)
78 throw simgrid::mc::errno_error(errno, "Could not PR_SET_PDEATHSIG");
83 // Remove CLOEXEC in order to pass the socket to the exec-ed program:
84 int fdflags = fcntl(socket, F_GETFD, 0);
85 if (fdflags == -1 || fcntl(socket, F_SETFD, fdflags & ~FD_CLOEXEC) == -1)
86 throw simgrid::xbt::system_error(errno, "Could not remove CLOEXEC for socket");
89 setenv(MC_ENV_VARIABLE, "1", 1);
91 // Disable lazy relocation in the model-checked process.
92 // We don't want the model-checked process to modify its .got.plt during
94 setenv("LC_BIND_NOW", "1", 1);
97 res = std::snprintf(buffer, sizeof(buffer), "%i", socket);
98 if ((size_t) res >= sizeof(buffer) || res == -1)
100 setenv(MC_ENV_SOCKET_FD, buffer, 1);
102 execvp(argv[1], argv+1);
104 XBT_ERROR("Could not run the model-checked program");
105 // This is the value used by system() and popen() in this case:
110 std::pair<pid_t, int> create_model_checked(char** argv)
112 // Create a AF_LOCAL socketpair used for exchanging messages
113 // bewteen the model-checker process (ourselves) and the model-checked
117 res = socketpair(AF_LOCAL, SOCK_DGRAM | SOCK_CLOEXEC, 0, sockets);
119 throw simgrid::xbt::system_error(errno, "Could not create socketpair");
121 pid_t pid = do_fork([&] {
123 int res = exec_model_checked(sockets[0], argv);
124 XBT_DEBUG("Error in the child process creation");
128 // Parent (model-checker):
130 return std::make_pair(pid, sockets[1]);
134 char** argvdup(int argc, char** argv)
136 char** argv_copy = xbt_new(char*, argc+1);
137 std::memcpy(argv_copy, argv, sizeof(char*) * argc);
138 argv_copy[argc] = NULL;
142 int main(int argc, char** argv)
146 xbt_die("Missing arguments.\n");
148 _sg_do_model_check = 1;
150 // The initialisation function can touch argv.
151 // We need to keep the original parameters in order to pass them to the
152 // model-checked process so we make a copy of them:
153 int argc_copy = argc;
154 char** argv_copy = argvdup(argc, argv);
155 xbt_log_init(&argc_copy, argv_copy);
156 sg_config_init(&argc_copy, argv_copy);
159 pid_t model_checked_pid;
160 std::tie(model_checked_pid, sock) = create_model_checked(argv);
161 XBT_DEBUG("Inside the parent process");
162 if (mc_model_checker)
163 xbt_die("MC server already present");
165 mc_mode = MC_MODE_SERVER;
166 std::unique_ptr<simgrid::mc::Process> process(new simgrid::mc::Process(model_checked_pid, sock));
167 process->privatized(sg_cfg_get_boolean("smpi/privatize_global_variables"));
168 mc_model_checker = new simgrid::mc::ModelChecker(std::move(process));
169 mc_model_checker->start();
171 if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
172 res = MC_modelcheck_comm_determinism();
173 else if (!_sg_mc_property_file || _sg_mc_property_file[0] == '\0')
174 res = MC_modelcheck_safety();
176 res = MC_modelcheck_liveness();
177 mc_model_checker->shutdown();
180 catch(std::exception& e) {
181 XBT_ERROR("Exception: %s", e.what());
182 return SIMGRID_MC_EXIT_ERROR;
185 XBT_ERROR("Unknown exception");
186 return SIMGRID_MC_EXIT_ERROR;