Logo AND Algorithmique Numérique Distribuée

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