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