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>
30 #include <xbt/system_error.hpp>
32 #include "simgrid/sg_config.h"
33 #include "src/xbt_modinter.h"
35 #include "src/mc/mc_base.h"
36 #include "src/mc/mc_private.h"
37 #include "src/mc/mc_protocol.h"
38 #include "src/mc/mc_safety.h"
39 #include "src/mc/mc_comm_pattern.h"
40 #include "src/mc/mc_liveness.h"
41 #include "src/mc/mc_exit.h"
43 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_main, mc, "Entry point for simgrid-mc");
45 /** Execute some code in a forked process */
52 throw simgrid::xbt::errno_error(errno, "Could not fork model-checked process");
59 std::exit(EXIT_SUCCESS);
62 // The callback should catch exceptions:
68 int exec_model_checked(int socket, char** argv)
70 XBT_DEBUG("Inside the child process PID=%i", (int) getpid());
73 // Make sure we do not outlive our parent:
76 if (sigprocmask(SIG_SETMASK, &mask, nullptr) < 0)
77 throw simgrid::xbt::errno_error(errno, "Could not unblock signals");
78 if (prctl(PR_SET_PDEATHSIG, SIGHUP) != 0)
79 throw simgrid::xbt::errno_error(errno, "Could not PR_SET_PDEATHSIG");
84 // Remove CLOEXEC in order to pass the socket to the exec-ed program:
85 int fdflags = fcntl(socket, F_GETFD, 0);
86 if (fdflags == -1 || fcntl(socket, F_SETFD, fdflags & ~FD_CLOEXEC) == -1)
87 throw simgrid::xbt::errno_error(errno, "Could not remove CLOEXEC for socket");
90 setenv(MC_ENV_VARIABLE, "1", 1);
92 // Disable lazy relocation in the model-checked process.
93 // We don't want the model-checked process to modify its .got.plt during
95 setenv("LC_BIND_NOW", "1", 1);
98 res = std::snprintf(buffer, sizeof(buffer), "%i", socket);
99 if ((size_t) res >= sizeof(buffer) || res == -1)
101 setenv(MC_ENV_SOCKET_FD, buffer, 1);
103 execvp(argv[1], argv+1);
105 XBT_ERROR("Could not run the model-checked program");
106 // This is the value used by system() and popen() in this case:
111 std::pair<pid_t, int> create_model_checked(char** argv)
113 // Create a AF_LOCAL socketpair used for exchanging messages
114 // bewteen the model-checker process (ourselves) and the model-checked
118 res = socketpair(AF_LOCAL, SOCK_DGRAM | SOCK_CLOEXEC, 0, sockets);
120 throw simgrid::xbt::errno_error(errno, "Could not create socketpair");
122 pid_t pid = do_fork([&] {
124 int res = exec_model_checked(sockets[0], argv);
125 XBT_DEBUG("Error in the child process creation");
129 // Parent (model-checker):
131 return std::make_pair(pid, sockets[1]);
135 char** argvdup(int argc, char** argv)
137 char** argv_copy = xbt_new(char*, argc+1);
138 std::memcpy(argv_copy, argv, sizeof(char*) * argc);
139 argv_copy[argc] = NULL;
143 int main(int argc, char** argv)
147 xbt_die("Missing arguments.\n");
149 _sg_do_model_check = 1;
151 // The initialisation function can touch argv.
152 // We need to keep the original parameters in order to pass them to the
153 // model-checked process so we make a copy of them:
154 int argc_copy = argc;
155 char** argv_copy = argvdup(argc, argv);
156 xbt_log_init(&argc_copy, argv_copy);
157 sg_config_init(&argc_copy, argv_copy);
160 pid_t model_checked_pid;
161 std::tie(model_checked_pid, sock) = create_model_checked(argv);
162 XBT_DEBUG("Inside the parent process");
163 if (mc_model_checker)
164 xbt_die("MC server already present");
166 mc_mode = MC_MODE_SERVER;
167 std::unique_ptr<simgrid::mc::Process> process(new simgrid::mc::Process(model_checked_pid, sock));
168 process->privatized(sg_cfg_get_boolean("smpi/privatize_global_variables"));
169 mc_model_checker = new simgrid::mc::ModelChecker(std::move(process));
170 mc_model_checker->start();
172 if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
173 res = MC_modelcheck_comm_determinism();
174 else if (!_sg_mc_property_file || _sg_mc_property_file[0] == '\0')
175 res = MC_modelcheck_safety();
177 res = MC_modelcheck_liveness();
178 mc_model_checker->shutdown();
181 catch(std::exception& e) {
182 XBT_ERROR("Exception: %s", e.what());
183 return SIMGRID_MC_EXIT_ERROR;
186 XBT_ERROR("Unknown exception");
187 return SIMGRID_MC_EXIT_ERROR;