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