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 }