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 new std::system_error(errno, std::generic_category());
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 new std::system_error(errno, std::generic_category(), "sigprocmask");
77 if (prctl(PR_SET_PDEATHSIG, SIGHUP) != 0)
78 throw new std::system_error(errno, std::generic_category(), "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);
86 throw new std::system_error(errno, std::generic_category(), "F_GETFD");
87 if (fcntl(socket, F_SETFD, fdflags & ~FD_CLOEXEC) == -1)
88 throw new std::system_error(errno, std::generic_category(), "Remove FD_CLOEXEC");
91 setenv(MC_ENV_VARIABLE, "1", 1);
93 // Disable lazy relocation in the model-checked process.
94 // We don't want the model-checked process to modify its .got.plt during
96 setenv("LC_BIND_NOW", "1", 1);
99 res = std::snprintf(buffer, sizeof(buffer), "%i", socket);
100 if ((size_t) res >= sizeof(buffer) || res == -1)
102 setenv(MC_ENV_SOCKET_FD, buffer, 1);
104 execvp(argv[1], argv+1);
106 XBT_ERROR("Could not run the model-checked program");
107 // This is the value used by system() and popen() in this case:
112 std::pair<pid_t, int> create_model_checked(char** argv)
114 // Create a AF_LOCAL socketpair used for exchanging messages
115 // bewteen the model-checker process (ourselves) and the model-checked
119 res = socketpair(AF_LOCAL, SOCK_DGRAM | SOCK_CLOEXEC, 0, sockets);
121 throw new std::system_error(errno, std::generic_category(), "socketpair");
123 pid_t pid = do_fork([&] {
125 int res = exec_model_checked(sockets[0], argv);
126 XBT_DEBUG("Error in the child process creation");
130 // Parent (model-checker):
132 return std::make_pair(pid, sockets[1]);
136 char** argvdup(int argc, char** argv)
138 char** argv_copy = xbt_new(char*, argc+1);
139 std::memcpy(argv_copy, argv, sizeof(char*) * argc);
140 argv_copy[argc] = NULL;
144 int main(int argc, char** argv)
148 xbt_die("Missing arguments.\n");
150 _sg_do_model_check = 1;
152 // The initialisation function can touch argv.
153 // We need to keep the original parameters in order to pass them to the
154 // model-checked process so we make a copy of them:
155 int argc_copy = argc;
156 char** argv_copy = argvdup(argc, argv);
157 xbt_log_init(&argc_copy, argv_copy);
158 sg_config_init(&argc_copy, argv_copy);
161 pid_t model_checked_pid;
162 std::tie(model_checked_pid, sock) = create_model_checked(argv);
163 XBT_DEBUG("Inside the parent process");
164 if (mc_model_checker)
165 xbt_die("MC server already present");
167 mc_mode = MC_MODE_SERVER;
168 std::unique_ptr<simgrid::mc::Process> process(new simgrid::mc::Process(model_checked_pid, sock));
169 process->privatized(sg_cfg_get_boolean("smpi/privatize_global_variables"));
170 mc_model_checker = new simgrid::mc::ModelChecker(std::move(process));
171 mc_model_checker->start();
173 if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
174 res = MC_modelcheck_comm_determinism();
175 else if (!_sg_mc_property_file || _sg_mc_property_file[0] == '\0')
176 res = MC_modelcheck_safety();
178 res = MC_modelcheck_liveness();
179 mc_model_checker->shutdown();
182 catch(std::exception& e) {
183 XBT_ERROR("Exception: %s", e.what());
184 return SIMGRID_MC_EXIT_ERROR;
187 XBT_ERROR("Unknown exception");
188 return SIMGRID_MC_EXIT_ERROR;