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 }