Logo AND Algorithmique Numérique Distribuée

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