Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
[mc] Fix MC cross-process memory access
[simgrid.git] / src / mc / ModelChecker.cpp
1 /* Copyright (c) 2008-2015. The SimGrid Team.
2  * All rights reserved.                                                     */
3
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. */
6
7 #include <cassert>
8
9 #include <poll.h>
10 #include <sys/types.h>
11 #include <sys/wait.h>
12 #include <sys/socket.h>
13 #include <sys/signalfd.h>
14 #include <sys/ptrace.h>
15
16 #include <memory>
17 #include <system_error>
18
19 #include <xbt/log.h>
20 #include <xbt/automaton.h>
21 #include <xbt/automaton.hpp>
22
23 #include "simgrid/sg_config.h"
24
25 #include "src/mc/ModelChecker.hpp"
26 #include "src/mc/PageStore.hpp"
27 #include "src/mc/ModelChecker.hpp"
28 #include "src/mc/mc_protocol.h"
29 #include "src/mc/mc_private.h"
30 #include "src/mc/mc_ignore.h"
31 #include "src/mc/mc_exit.h"
32 #include "src/mc/mc_liveness.h"
33
34 extern "C" {
35
36 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_ModelChecker, mc, "ModelChecker");
37
38 }
39
40 ::simgrid::mc::ModelChecker* mc_model_checker = nullptr;
41
42 using simgrid::mc::remote;
43
44 // Hardcoded index for now:
45 #define SOCKET_FD_INDEX 0
46 #define SIGNAL_FD_INDEX 1
47
48 namespace simgrid {
49 namespace mc {
50
51 ModelChecker::ModelChecker(pid_t pid, int socket) :
52   pid_(pid), socket_(socket),
53   hostnames_(xbt_dict_new()),
54   page_store_(500),
55   parent_snapshot_(nullptr)
56 {
57
58 }
59
60 ModelChecker::~ModelChecker()
61 {
62   xbt_dict_free(&this->hostnames_);
63 }
64
65 const char* ModelChecker::get_host_name(const char* hostname)
66 {
67   // Lookup the host name in the dictionary (or create it):
68   xbt_dictelm_t elt = xbt_dict_get_elm_or_null(this->hostnames_, hostname);
69   if (!elt) {
70     xbt_dict_set(this->hostnames_, hostname, nullptr, nullptr);
71     elt = xbt_dict_get_elm_or_null(this->hostnames_, hostname);
72     assert(elt);
73   }
74   return elt->key;
75 }
76
77 // HACK, for the unit test only
78 void ModelChecker::init_process()
79 {
80   // TODO, avoid direct dependency on sg_cfg
81   process_ = std::unique_ptr<Process>(new Process(pid_, socket_));
82   process_->privatized(sg_cfg_get_boolean("smpi/privatize_global_variables"));
83 }
84
85 void ModelChecker::start()
86 {
87   // Block SIGCHLD (this will be handled with accept/signalfd):
88   sigset_t set;
89   sigemptyset(&set);
90   sigaddset(&set, SIGCHLD);
91   if (sigprocmask(SIG_BLOCK, &set, nullptr) == -1)
92     throw std::system_error(errno, std::system_category());
93
94   sigset_t full_set;
95   sigfillset(&full_set);
96
97   // Prepare data for poll:
98
99   struct pollfd* socket_pollfd = &fds_[SOCKET_FD_INDEX];
100   socket_pollfd->fd = socket_;
101   socket_pollfd->events = POLLIN;
102   socket_pollfd->revents = 0;
103
104   int signal_fd = signalfd(-1, &set, 0);
105   if (signal_fd == -1)
106     throw std::system_error(errno, std::system_category());
107
108   struct pollfd* signalfd_pollfd = &fds_[SIGNAL_FD_INDEX];
109   signalfd_pollfd->fd = signal_fd;
110   signalfd_pollfd->events = POLLIN;
111   signalfd_pollfd->revents = 0;
112
113   XBT_DEBUG("Waiting for the model-checked process");
114   int status;
115
116   // The model-checked process SIGSTOP itself to signal it's ready:
117   pid_t res = waitpid(pid_, &status, __WALL);
118   if (res < 0 || !WIFSTOPPED(status) || WSTOPSIG(status) != SIGSTOP)
119     xbt_die("Could not wait model-checked process");
120
121   this->init_process();
122
123   /* Initialize statistics */
124   mc_stats = xbt_new0(s_mc_stats_t, 1);
125   mc_stats->state_size = 1;
126
127   if ((_sg_mc_dot_output_file != nullptr) && (_sg_mc_dot_output_file[0] != '\0'))
128     MC_init_dot_output();
129
130   /* Init parmap */
131   //parmap = xbt_parmap_mc_new(xbt_os_get_numcores(), XBT_PARMAP_DEFAULT);
132
133   setup_ignore();
134
135   ptrace(PTRACE_SETOPTIONS, pid_, nullptr, PTRACE_O_TRACEEXIT);
136   ptrace(PTRACE_CONT, pid_, 0, 0);
137 }
138
139 static const std::pair<const char*, const char*> ignored_local_variables[] = {
140   std::pair<const char*, const char*>{  "e", "*" },
141   std::pair<const char*, const char*>{ "__ex_cleanup", "*" },
142   std::pair<const char*, const char*>{ "__ex_mctx_en", "*" },
143   std::pair<const char*, const char*>{ "__ex_mctx_me", "*" },
144   std::pair<const char*, const char*>{ "__xbt_ex_ctx_ptr", "*" },
145   std::pair<const char*, const char*>{ "_log_ev", "*" },
146   std::pair<const char*, const char*>{ "_throw_ctx", "*" },
147   std::pair<const char*, const char*>{ "ctx", "*" },
148
149   std::pair<const char*, const char*>{ "self", "simcall_BODY_mc_snapshot" },
150   std::pair<const char*, const char*>{ "next_context", "smx_ctx_sysv_suspend_serial" },
151   std::pair<const char*, const char*>{ "i", "smx_ctx_sysv_suspend_serial" },
152
153   /* Ignore local variable about time used for tracing */
154   std::pair<const char*, const char*>{ "start_time", "*" },
155 };
156
157 void ModelChecker::setup_ignore()
158 {
159   Process& process = this->process();
160   for (std::pair<const char*, const char*> const& var :
161       ignored_local_variables)
162     process.ignore_local_variable(var.first, var.second);
163
164   /* Static variable used for tracing */
165   process.ignore_global_variable("counter");
166
167   /* SIMIX */
168   process.ignore_global_variable("smx_total_comms");
169 }
170
171 void ModelChecker::shutdown()
172 {
173   XBT_DEBUG("Shuting down model-checker");
174
175   simgrid::mc::Process* process = &this->process();
176   if (process->running()) {
177     XBT_DEBUG("Killing process");
178     kill(process->pid(), SIGTERM);
179     process->terminate();
180   }
181 }
182
183 void ModelChecker::resume(simgrid::mc::Process& process)
184 {
185   int res = process.send_message(MC_MESSAGE_CONTINUE);
186   if (res)
187     throw std::system_error(res, std::system_category());
188   process.cache_flags = (mc_process_cache_flags_t) 0;
189 }
190
191 static
192 void throw_socket_error(int fd)
193 {
194   int error = 0;
195   socklen_t errlen = sizeof(error);
196   if (getsockopt(fd, SOL_SOCKET, SO_ERROR, (void *)&error, &errlen) == -1)
197     error = errno;
198   throw std::system_error(error, std::system_category());
199 }
200
201 bool ModelChecker::handle_message(char* buffer, ssize_t size)
202 {
203   s_mc_message_t base_message;
204   if (size < (ssize_t) sizeof(base_message))
205     xbt_die("Broken message");
206   memcpy(&base_message, buffer, sizeof(base_message));
207
208   switch(base_message.type) {
209
210   case MC_MESSAGE_IGNORE_HEAP:
211     {
212       s_mc_ignore_heap_message_t message;
213       if (size != sizeof(message))
214         xbt_die("Broken messsage");
215       memcpy(&message, buffer, sizeof(message));
216
217       IgnoredHeapRegion region;
218       region.block = message.block;
219       region.fragment = message.fragment;
220       region.address = message.address;
221       region.size = message.size;
222       process().ignore_heap(region);
223       break;
224     }
225
226   case MC_MESSAGE_UNIGNORE_HEAP:
227     {
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       process().unignore_heap(
233         (void *)(std::uintptr_t) message.addr, message.size);
234       break;
235     }
236
237   case MC_MESSAGE_IGNORE_MEMORY:
238     {
239       s_mc_ignore_memory_message_t message;
240       if (size != sizeof(message))
241         xbt_die("Broken messsage");
242       memcpy(&message, buffer, sizeof(message));
243       this->process().ignore_region(message.addr, message.size);
244       break;
245     }
246
247   case MC_MESSAGE_STACK_REGION:
248     {
249       s_mc_stack_region_message_t message;
250       if (size != sizeof(message))
251         xbt_die("Broken messsage");
252       memcpy(&message, buffer, sizeof(message));
253       this->process().stack_areas().push_back(message.stack_region);
254     }
255     break;
256
257   case MC_MESSAGE_REGISTER_SYMBOL:
258     {
259       s_mc_register_symbol_message_t message;
260       if (size != sizeof(message))
261         xbt_die("Broken message");
262       memcpy(&message, buffer, sizeof(message));
263       if (message.callback)
264         xbt_die("Support for client-side function proposition is not implemented.");
265       XBT_DEBUG("Received symbol: %s", message.name);
266
267       if (_mc_property_automaton == nullptr)
268         _mc_property_automaton = xbt_automaton_new();
269
270       simgrid::mc::Process* process = &this->process();
271       simgrid::mc::remote_ptr<int> address
272         = simgrid::mc::remote((int*) message.data);
273       simgrid::xbt::add_proposition(_mc_property_automaton,
274         message.name,
275         [process, address]() { return process->read(address); }
276         );
277
278       break;
279     }
280
281   case MC_MESSAGE_WAITING:
282     return false;
283
284   case MC_MESSAGE_ASSERTION_FAILED:
285     MC_report_assertion_error();
286     ::exit(SIMGRID_MC_EXIT_SAFETY);
287     break;
288
289   default:
290     xbt_die("Unexpected message from model-checked application");
291
292   }
293   return true;
294 }
295
296 bool ModelChecker::handle_events()
297 {
298   char buffer[MC_MESSAGE_LENGTH];
299   struct pollfd* socket_pollfd = &fds_[SOCKET_FD_INDEX];
300   struct pollfd* signalfd_pollfd = &fds_[SIGNAL_FD_INDEX];
301
302   while(poll(fds_, 2, -1) == -1) {
303     switch(errno) {
304     case EINTR:
305       continue;
306     default:
307       throw std::system_error(errno, std::system_category());
308     }
309   }
310
311   if (socket_pollfd->revents) {
312     if (socket_pollfd->revents & POLLIN) {
313       ssize_t size = MC_receive_message(socket_pollfd->fd, buffer, sizeof(buffer), MSG_DONTWAIT);
314       if (size == -1 && errno != EAGAIN)
315         throw std::system_error(errno, std::system_category());
316       return handle_message(buffer, size);
317     }
318     if (socket_pollfd->revents & POLLERR) {
319       throw_socket_error(socket_pollfd->fd);
320     }
321     if (socket_pollfd->revents & POLLHUP)
322       xbt_die("Socket hang up?");
323   }
324
325   if (signalfd_pollfd->revents) {
326     if (signalfd_pollfd->revents & POLLIN) {
327       this->handle_signals();
328       return true;
329     }
330     if (signalfd_pollfd->revents & POLLERR) {
331       throw_socket_error(signalfd_pollfd->fd);
332     }
333     if (signalfd_pollfd->revents & POLLHUP)
334       xbt_die("Signalfd hang up?");
335   }
336
337   return true;
338 }
339
340 void ModelChecker::loop()
341 {
342   while (this->process().running())
343     this->handle_events();
344 }
345
346 void ModelChecker::handle_signals()
347 {
348   struct signalfd_siginfo info;
349   struct pollfd* signalfd_pollfd = &fds_[SIGNAL_FD_INDEX];
350   while (1) {
351     ssize_t size = read(signalfd_pollfd->fd, &info, sizeof(info));
352     if (size == -1) {
353       if (errno == EINTR)
354         continue;
355       else
356         throw std::system_error(errno, std::system_category());
357     } else if (size != sizeof(info))
358         return throw std::runtime_error(
359           "Bad communication with model-checked application");
360     else
361       break;
362   }
363   this->on_signal(&info);
364 }
365
366 void ModelChecker::handle_waitpid()
367 {
368   XBT_DEBUG("Check for wait event");
369   int status;
370   pid_t pid;
371   while ((pid = waitpid(-1, &status, WNOHANG)) != 0) {
372     if (pid == -1) {
373       if (errno == ECHILD) {
374         // No more children:
375         if (this->process().running())
376           xbt_die("Inconsistent state");
377         else
378           break;
379       } else {
380         XBT_ERROR("Could not wait for pid");
381         throw std::system_error(errno, std::system_category());
382       }
383     }
384
385     if (pid == this->process().pid()) {
386
387       // From PTRACE_O_TRACEEXIT:
388       if (status>>8 == (SIGTRAP | (PTRACE_EVENT_EXIT<<8))) {
389         if (ptrace(PTRACE_GETEVENTMSG, pid_, 0, &status) == -1)
390           xbt_die("Could not get exit status");
391         if (WIFSIGNALED(status)) {
392           MC_report_crash(status);
393           ::exit(SIMGRID_MC_EXIT_PROGRAM_CRASH);
394         }
395       }
396
397       // We don't care about signals, just reinject them:
398       if (WIFSTOPPED(status)) {
399         XBT_DEBUG("Stopped with signal %i", (int) WSTOPSIG(status));
400         if (ptrace(PTRACE_CONT, pid_, 0, WSTOPSIG(status)) == -1)
401           xbt_die("Could not PTRACE_CONT");
402       }
403
404       else if (WIFEXITED(status) || WIFSIGNALED(status)) {
405         XBT_DEBUG("Child process is over");
406         this->process().terminate();
407       }
408     }
409   }
410 }
411
412 void ModelChecker::on_signal(const struct signalfd_siginfo* info)
413 {
414   switch(info->ssi_signo) {
415   case SIGCHLD:
416     this->handle_waitpid();
417     break;
418   default:
419     break;
420   }
421 }
422
423 void ModelChecker::wait_client(simgrid::mc::Process& process)
424 {
425   this->resume(process);
426   while (this->process().running()) {
427     if (!this->handle_events())
428       return;
429   }
430 }
431
432 void ModelChecker::simcall_handle(simgrid::mc::Process& process, unsigned long pid, int value)
433 {
434   s_mc_simcall_handle_message m;
435   memset(&m, 0, sizeof(m));
436   m.type  = MC_MESSAGE_SIMCALL_HANDLE;
437   m.pid   = pid;
438   m.value = value;
439   process.send_message(m);
440   process.cache_flags = (mc_process_cache_flags_t) 0;
441   while (process.running()) {
442     if (!this->handle_events())
443       return;
444   }
445 }
446
447 }
448 }