1 /* Copyright (c) 2008-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. */
10 #include <sys/types.h>
12 #include <sys/socket.h>
13 #include <sys/signalfd.h>
14 #include <sys/ptrace.h>
17 #include <system_error>
20 #include <xbt/automaton.h>
21 #include <xbt/automaton.hpp>
23 #include "simgrid/sg_config.h"
25 #include "ModelChecker.hpp"
26 #include "PageStore.hpp"
27 #include "ModelChecker.hpp"
28 #include "mc_protocol.h"
29 #include "mc_private.h"
30 #include "mc_ignore.h"
32 #include "src/mc/mc_liveness.h"
36 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_ModelChecker, mc, "ModelChecker");
40 ::simgrid::mc::ModelChecker* mc_model_checker = nullptr;
42 using simgrid::mc::remote;
44 // Hardcoded index for now:
45 #define SOCKET_FD_INDEX 0
46 #define SIGNAL_FD_INDEX 1
51 ModelChecker::ModelChecker(pid_t pid, int socket) :
52 pid_(pid), socket_(socket),
53 hostnames_(xbt_dict_new()),
55 parent_snapshot_(nullptr)
59 ModelChecker::~ModelChecker()
61 xbt_dict_free(&this->hostnames_);
64 const char* ModelChecker::get_host_name(const char* hostname)
66 // Lookup the host name in the dictionary (or create it):
67 xbt_dictelm_t elt = xbt_dict_get_elm_or_null(this->hostnames_, hostname);
69 xbt_dict_set(this->hostnames_, hostname, nullptr, nullptr);
70 elt = xbt_dict_get_elm_or_null(this->hostnames_, hostname);
76 void ModelChecker::start()
78 // Block SIGCHLD (this will be handled with accept/signalfd):
81 sigaddset(&set, SIGCHLD);
82 if (sigprocmask(SIG_BLOCK, &set, nullptr) == -1)
83 throw std::system_error(errno, std::system_category());
86 sigfillset(&full_set);
88 // Prepare data for poll:
90 struct pollfd* socket_pollfd = &fds_[SOCKET_FD_INDEX];
91 socket_pollfd->fd = socket_;
92 socket_pollfd->events = POLLIN;
93 socket_pollfd->revents = 0;
95 int signal_fd = signalfd(-1, &set, 0);
97 throw std::system_error(errno, std::system_category());
99 struct pollfd* signalfd_pollfd = &fds_[SIGNAL_FD_INDEX];
100 signalfd_pollfd->fd = signal_fd;
101 signalfd_pollfd->events = POLLIN;
102 signalfd_pollfd->revents = 0;
104 XBT_DEBUG("Waiting for the model-checked process");
107 // The model-checked process SIGSTOP itself to signal it's ready:
108 pid_t res = waitpid(pid_, &status, __WALL);
109 if (res < 0 || !WIFSTOPPED(status) || WSTOPSIG(status) != SIGSTOP)
110 xbt_die("Could not wait model-checked process");
112 assert(process_ == nullptr);
113 process_ = std::unique_ptr<Process>(new Process(pid_, socket_));
114 // TODO, avoid direct dependency on sg_cfg
115 process_->privatized(sg_cfg_get_boolean("smpi/privatize_global_variables"));
117 /* Initialize statistics */
118 mc_stats = xbt_new0(s_mc_stats_t, 1);
119 mc_stats->state_size = 1;
121 if ((_sg_mc_dot_output_file != nullptr) && (_sg_mc_dot_output_file[0] != '\0'))
122 MC_init_dot_output();
125 //parmap = xbt_parmap_mc_new(xbt_os_get_numcores(), XBT_PARMAP_DEFAULT);
129 ptrace(PTRACE_SETOPTIONS, pid_, nullptr, PTRACE_O_TRACEEXIT);
130 ptrace(PTRACE_CONT, pid_, 0, 0);
133 void ModelChecker::setup_ignore()
135 /* Ignore some variables from xbt/ex.h used by exception e for stacks comparison */
136 MC_ignore_local_variable("e", "*");
137 MC_ignore_local_variable("__ex_cleanup", "*");
138 MC_ignore_local_variable("__ex_mctx_en", "*");
139 MC_ignore_local_variable("__ex_mctx_me", "*");
140 MC_ignore_local_variable("__xbt_ex_ctx_ptr", "*");
141 MC_ignore_local_variable("_log_ev", "*");
142 MC_ignore_local_variable("_throw_ctx", "*");
143 MC_ignore_local_variable("ctx", "*");
145 MC_ignore_local_variable("self", "simcall_BODY_mc_snapshot");
146 MC_ignore_local_variable("next_cont"
147 "ext", "smx_ctx_sysv_suspend_serial");
148 MC_ignore_local_variable("i", "smx_ctx_sysv_suspend_serial");
150 /* Ignore local variable about time used for tracing */
151 MC_ignore_local_variable("start_time", "*");
153 /* Static variable used for tracing */
154 this->process().ignore_global_variable("counter");
157 this->process().ignore_global_variable("smx_total_comms");
160 void ModelChecker::shutdown()
162 XBT_DEBUG("Shuting down model-checker");
164 simgrid::mc::Process* process = &this->process();
165 if (process->running()) {
166 XBT_DEBUG("Killing process");
167 kill(process->pid(), SIGTERM);
168 process->terminate();
172 void ModelChecker::resume(simgrid::mc::Process& process)
174 int res = process.send_message(MC_MESSAGE_CONTINUE);
176 throw std::system_error(res, std::system_category());
177 process.cache_flags = (mc_process_cache_flags_t) 0;
181 void throw_socket_error(int fd)
184 socklen_t errlen = sizeof(error);
185 if (getsockopt(fd, SOL_SOCKET, SO_ERROR, (void *)&error, &errlen) == -1)
187 throw std::system_error(error, std::system_category());
190 bool ModelChecker::handle_message(char* buffer, ssize_t size)
192 s_mc_message_t base_message;
193 if (size < (ssize_t) sizeof(base_message))
194 xbt_die("Broken message");
195 memcpy(&base_message, buffer, sizeof(base_message));
197 switch(base_message.type) {
199 case MC_MESSAGE_IGNORE_HEAP:
201 s_mc_ignore_heap_message_t message;
202 if (size != sizeof(message))
203 xbt_die("Broken messsage");
204 memcpy(&message, buffer, sizeof(message));
206 IgnoredHeapRegion region;
207 region.block = message.block;
208 region.fragment = message.fragment;
209 region.address = message.address;
210 region.size = message.size;
211 process().ignore_heap(region);
215 case MC_MESSAGE_UNIGNORE_HEAP:
217 s_mc_ignore_memory_message_t message;
218 if (size != sizeof(message))
219 xbt_die("Broken messsage");
220 memcpy(&message, buffer, sizeof(message));
221 process().unignore_heap(
222 (void *)(std::uintptr_t) message.addr, message.size);
226 case MC_MESSAGE_IGNORE_MEMORY:
228 s_mc_ignore_memory_message_t message;
229 if (size != sizeof(message))
230 xbt_die("Broken messsage");
231 memcpy(&message, buffer, sizeof(message));
232 this->process().ignore_region(message.addr, message.size);
236 case MC_MESSAGE_STACK_REGION:
238 s_mc_stack_region_message_t message;
239 if (size != sizeof(message))
240 xbt_die("Broken messsage");
241 memcpy(&message, buffer, sizeof(message));
242 this->process().stack_areas().push_back(message.stack_region);
246 case MC_MESSAGE_REGISTER_SYMBOL:
248 s_mc_register_symbol_message_t message;
249 if (size != sizeof(message))
250 xbt_die("Broken message");
251 memcpy(&message, buffer, sizeof(message));
252 if (message.callback)
253 xbt_die("Support for client-side function proposition is not implemented.");
254 XBT_DEBUG("Received symbol: %s", message.name);
256 if (_mc_property_automaton == nullptr)
257 _mc_property_automaton = xbt_automaton_new();
259 simgrid::mc::Process* process = &this->process();
260 simgrid::mc::remote_ptr<int> address
261 = simgrid::mc::remote((int*) message.data);
262 simgrid::xbt::add_proposition(_mc_property_automaton,
264 [process, address]() { return process->read(address); }
270 case MC_MESSAGE_WAITING:
273 case MC_MESSAGE_ASSERTION_FAILED:
274 MC_report_assertion_error();
275 ::exit(SIMGRID_MC_EXIT_SAFETY);
279 xbt_die("Unexpected message from model-checked application");
285 bool ModelChecker::handle_events()
287 char buffer[MC_MESSAGE_LENGTH];
288 struct pollfd* socket_pollfd = &fds_[SOCKET_FD_INDEX];
289 struct pollfd* signalfd_pollfd = &fds_[SIGNAL_FD_INDEX];
291 while(poll(fds_, 2, -1) == -1) {
296 throw std::system_error(errno, std::system_category());
300 if (socket_pollfd->revents) {
301 if (socket_pollfd->revents & POLLIN) {
302 ssize_t size = MC_receive_message(socket_pollfd->fd, buffer, sizeof(buffer), MSG_DONTWAIT);
303 if (size == -1 && errno != EAGAIN)
304 throw std::system_error(errno, std::system_category());
305 return handle_message(buffer, size);
307 if (socket_pollfd->revents & POLLERR) {
308 throw_socket_error(socket_pollfd->fd);
310 if (socket_pollfd->revents & POLLHUP)
311 xbt_die("Socket hang up?");
314 if (signalfd_pollfd->revents) {
315 if (signalfd_pollfd->revents & POLLIN) {
316 this->handle_signals();
319 if (signalfd_pollfd->revents & POLLERR) {
320 throw_socket_error(signalfd_pollfd->fd);
322 if (signalfd_pollfd->revents & POLLHUP)
323 xbt_die("Signalfd hang up?");
329 void ModelChecker::loop()
331 while (this->process().running())
332 this->handle_events();
335 void ModelChecker::handle_signals()
337 struct signalfd_siginfo info;
338 struct pollfd* signalfd_pollfd = &fds_[SIGNAL_FD_INDEX];
340 ssize_t size = read(signalfd_pollfd->fd, &info, sizeof(info));
345 throw std::system_error(errno, std::system_category());
346 } else if (size != sizeof(info))
347 return throw std::runtime_error(
348 "Bad communication with model-checked application");
352 this->on_signal(&info);
355 void ModelChecker::handle_waitpid()
357 XBT_DEBUG("Check for wait event");
360 while ((pid = waitpid(-1, &status, WNOHANG)) != 0) {
362 if (errno == ECHILD) {
364 if (this->process().running())
365 xbt_die("Inconsistent state");
369 XBT_ERROR("Could not wait for pid");
370 throw std::system_error(errno, std::system_category());
374 if (pid == this->process().pid()) {
376 // From PTRACE_O_TRACEEXIT:
377 if (status>>8 == (SIGTRAP | (PTRACE_EVENT_EXIT<<8))) {
378 if (ptrace(PTRACE_GETEVENTMSG, pid_, 0, &status) == -1)
379 xbt_die("Could not get exit status");
380 if (WIFSIGNALED(status)) {
381 MC_report_crash(status);
382 ::exit(SIMGRID_MC_EXIT_PROGRAM_CRASH);
386 // We don't care about signals, just reinject them:
387 if (WIFSTOPPED(status)) {
388 XBT_DEBUG("Stopped with signal %i", (int) WSTOPSIG(status));
389 if (ptrace(PTRACE_CONT, pid_, 0, WSTOPSIG(status)) == -1)
390 xbt_die("Could not PTRACE_CONT");
393 else if (WIFEXITED(status) || WIFSIGNALED(status)) {
394 XBT_DEBUG("Child process is over");
395 this->process().terminate();
401 void ModelChecker::on_signal(const struct signalfd_siginfo* info)
403 switch(info->ssi_signo) {
405 this->handle_waitpid();
412 void ModelChecker::wait_client(simgrid::mc::Process& process)
414 this->resume(process);
415 while (this->process().running()) {
416 if (!this->handle_events())
421 void ModelChecker::simcall_handle(simgrid::mc::Process& process, unsigned long pid, int value)
423 s_mc_simcall_handle_message m;
424 memset(&m, 0, sizeof(m));
425 m.type = MC_MESSAGE_SIMCALL_HANDLE;
428 process.send_message(m);
429 process.cache_flags = (mc_process_cache_flags_t) 0;
430 while (process.running()) {
431 if (!this->handle_events())