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();
  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();
 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
 154 void ModelChecker::shutdown()
 155 {
 156   XBT_DEBUG("Shuting down model-checker");
 157
 158   simgrid::mc::Process* process = &this->process();
 159   if (process->running()) {
 160     XBT_DEBUG("Killing process");
 161     kill(process->pid(), SIGTERM);
 162     process->terminate();
 163   }
 164 }
 165
 166 void ModelChecker::resume(simgrid::mc::Process& process)
 167 {
 168   int res = process.getChannel().send(MC_MESSAGE_CONTINUE);
 169   if (res)
 170     throw simgrid::xbt::errno_error();
 171   process.clear_cache();
 172 }
 173
 174 static
 175 void throw_socket_error(int fd)
 176 {
 177   int error = 0;
 178   socklen_t errlen = sizeof(error);
 179   if (getsockopt(fd, SOL_SOCKET, SO_ERROR, (void *)&error, &errlen) == -1)
 180     error = errno;
 181   throw simgrid::xbt::errno_error();
 182 }
 183
 184 static void MC_report_crash(int status)
 185 {
 186   XBT_INFO("**************************");
 187   XBT_INFO("** CRASH IN THE PROGRAM **");
 188   XBT_INFO("**************************");
 189   if (WIFSIGNALED(status))
 190     XBT_INFO("From signal: %s", strsignal(WTERMSIG(status)));
 191   else if (WIFEXITED(status))
 192     XBT_INFO("From exit: %i", WEXITSTATUS(status));
 193   if (WCOREDUMP(status))
 194     XBT_INFO("A core dump was generated by the system.");
 195   else
 196     XBT_INFO("No core dump was generated by the system.");
 197   XBT_INFO("Counter-example execution trace:");
 198   simgrid::mc::dumpRecordPath();
 199   for (auto& s : mc_model_checker->getChecker()->getTextualTrace())
 200     XBT_INFO("%s", s.c_str());
 201   simgrid::mc::session->logState();
 202   XBT_INFO("Stack trace:");
 203   mc_model_checker->process().dumpStack();
 204 }
 205
 206 static void MC_report_assertion_error(void)
 207 {
 208   XBT_INFO("**************************");
 209   XBT_INFO("*** PROPERTY NOT VALID ***");
 210   XBT_INFO("**************************");
 211   XBT_INFO("Counter-example execution trace:");
 212   simgrid::mc::dumpRecordPath();
 213   for (auto& s : mc_model_checker->getChecker()->getTextualTrace())
 214     XBT_INFO("%s", s.c_str());
 215   simgrid::mc::session->logState();
 216 }
 217
 218 bool ModelChecker::handle_message(char* buffer, ssize_t size)
 219 {
 220   s_mc_message_t base_message;
 221   if (size < (ssize_t) sizeof(base_message))
 222     xbt_die("Broken message");
 223   memcpy(&base_message, buffer, sizeof(base_message));
 224
 225   switch(base_message.type) {
 226
 227   case MC_MESSAGE_IGNORE_HEAP:
 228     {
 229       s_mc_ignore_heap_message_t message;
 230       if (size != sizeof(message))
 231         xbt_die("Broken messsage");
 232       memcpy(&message, buffer, sizeof(message));
 233
 234       IgnoredHeapRegion region;
 235       region.block = message.block;
 236       region.fragment = message.fragment;
 237       region.address = message.address;
 238       region.size = message.size;
 239       process().ignore_heap(region);
 240       break;
 241     }
 242
 243   case MC_MESSAGE_UNIGNORE_HEAP:
 244     {
 245       s_mc_ignore_memory_message_t message;
 246       if (size != sizeof(message))
 247         xbt_die("Broken messsage");
 248       memcpy(&message, buffer, sizeof(message));
 249       process().unignore_heap(
 250         (void *)(std::uintptr_t) message.addr, message.size);
 251       break;
 252     }
 253
 254   case MC_MESSAGE_IGNORE_MEMORY:
 255     {
 256       s_mc_ignore_memory_message_t message;
 257       if (size != sizeof(message))
 258         xbt_die("Broken messsage");
 259       memcpy(&message, buffer, sizeof(message));
 260       this->process().ignore_region(message.addr, message.size);
 261       break;
 262     }
 263
 264   case MC_MESSAGE_STACK_REGION:
 265     {
 266       s_mc_stack_region_message_t message;
 267       if (size != sizeof(message))
 268         xbt_die("Broken messsage");
 269       memcpy(&message, buffer, sizeof(message));
 270       this->process().stack_areas().push_back(message.stack_region);
 271     }
 272     break;
 273
 274   case MC_MESSAGE_REGISTER_SYMBOL:
 275     {
 276       s_mc_register_symbol_message_t message;
 277       if (size != sizeof(message))
 278         xbt_die("Broken message");
 279       memcpy(&message, buffer, sizeof(message));
 280       if (message.callback)
 281         xbt_die("Support for client-side function proposition is not implemented.");
 282       XBT_DEBUG("Received symbol: %s", message.name);
 283
 284       if (simgrid::mc::property_automaton == nullptr)
 285         simgrid::mc::property_automaton = xbt_automaton_new();
 286
 287       simgrid::mc::Process* process = &this->process();
 288       simgrid::mc::RemotePtr<int> address
 289         = simgrid::mc::remote((int*) message.data);
 290       simgrid::xbt::add_proposition(simgrid::mc::property_automaton,
 291         message.name,
 292         [process, address]() { return process->read(address); }
 293         );
 294
 295       break;
 296     }
 297
 298   case MC_MESSAGE_WAITING:
 299     return false;
 300
 301   case MC_MESSAGE_ASSERTION_FAILED:
 302     MC_report_assertion_error();
 303     this->exit(SIMGRID_MC_EXIT_SAFETY);
 304     break;
 305
 306   default:
 307     xbt_die("Unexpected message from model-checked application");
 308
 309   }
 310   return true;
 311 }
 312
 313 /** Terminate the model-checker aplication */
 314 void ModelChecker::exit(int status)
 315 {
 316   // TODO, terminate the model checker politely instead of exiting rudel
 317   if (process().running())
 318     kill(process().pid(), SIGKILL);
 319   ::exit(status);
 320 }
 321
 322 bool ModelChecker::handle_events()
 323 {
 324   char buffer[MC_MESSAGE_LENGTH];
 325   struct pollfd* socket_pollfd = &fds_[SOCKET_FD_INDEX];
 326   struct pollfd* signalfd_pollfd = &fds_[SIGNAL_FD_INDEX];
 327
 328   while(poll(fds_, 2, -1) == -1) {
 329     switch(errno) {
 330     case EINTR:
 331       continue;
 332     default:
 333       throw simgrid::xbt::errno_error();
 334     }
 335   }
 336
 337   if (socket_pollfd->revents) {
 338     if (socket_pollfd->revents & POLLIN) {
 339       ssize_t size = process_->getChannel().receive(buffer, sizeof(buffer), false);
 340       if (size == -1 && errno != EAGAIN)
 341         throw simgrid::xbt::errno_error();
 342       return handle_message(buffer, size);
 343     }
 344     if (socket_pollfd->revents & POLLERR)
 345       throw_socket_error(socket_pollfd->fd);
 346     if (socket_pollfd->revents & POLLHUP)
 347       xbt_die("Socket hang up?");
 348   }
 349
 350   if (signalfd_pollfd->revents) {
 351     if (signalfd_pollfd->revents & POLLIN) {
 352       this->handle_signals();
 353       return true;
 354     }
 355     if (signalfd_pollfd->revents & POLLERR)
 356       throw_socket_error(signalfd_pollfd->fd);
 357     if (signalfd_pollfd->revents & POLLHUP)
 358       xbt_die("Signalfd hang up?");
 359   }
 360
 361   return true;
 362 }
 363
 364 void ModelChecker::loop()
 365 {
 366   while (this->process().running())
 367     this->handle_events();
 368 }
 369
 370 void ModelChecker::handle_signals()
 371 {
 372   struct signalfd_siginfo info;
 373   struct pollfd* signalfd_pollfd = &fds_[SIGNAL_FD_INDEX];
 374   while (1) {
 375     ssize_t size = read(signalfd_pollfd->fd, &info, sizeof(info));
 376     if (size == -1) {
 377       if (errno == EINTR)
 378         continue;
 379       else
 380         throw simgrid::xbt::errno_error();
 381     } else if (size != sizeof(info))
 382         return throw std::runtime_error(
 383           "Bad communication with model-checked application");
 384     else
 385       break;
 386   }
 387   this->on_signal(&info);
 388 }
 389
 390 void ModelChecker::handle_waitpid()
 391 {
 392   XBT_DEBUG("Check for wait event");
 393   int status;
 394   pid_t pid;
 395   while ((pid = waitpid(-1, &status, WNOHANG)) != 0) {
 396     if (pid == -1) {
 397       if (errno == ECHILD) {
 398         // No more children:
 399         if (this->process().running())
 400           xbt_die("Inconsistent state");
 401         else
 402           break;
 403       } else {
 404         XBT_ERROR("Could not wait for pid");
 405         throw simgrid::xbt::errno_error();
 406       }
 407     }
 408
 409     if (pid == this->process().pid()) {
 410
 411       // From PTRACE_O_TRACEEXIT:
 412       if (status>>8 == (SIGTRAP | (PTRACE_EVENT_EXIT<<8))) {
 413         if (ptrace(PTRACE_GETEVENTMSG, this->process().pid(), 0, &status) == -1)
 414           xbt_die("Could not get exit status");
 415         if (WIFSIGNALED(status)) {
 416           MC_report_crash(status);
 417           mc_model_checker->exit(SIMGRID_MC_EXIT_PROGRAM_CRASH);
 418         }
 419       }
 420
 421       // We don't care about signals, just reinject them:
 422       if (WIFSTOPPED(status)) {
 423         XBT_DEBUG("Stopped with signal %i", (int) WSTOPSIG(status));
 424         if (ptrace(PTRACE_CONT, this->process().pid(), 0, WSTOPSIG(status)) == -1)
 425           xbt_die("Could not PTRACE_CONT");
 426       }
 427
 428       else if (WIFEXITED(status) || WIFSIGNALED(status)) {
 429         XBT_DEBUG("Child process is over");
 430         this->process().terminate();
 431       }
 432     }
 433   }
 434 }
 435
 436 void ModelChecker::on_signal(const struct signalfd_siginfo* info)
 437 {
 438   switch(info->ssi_signo) {
 439   case SIGCHLD:
 440     this->handle_waitpid();
 441     break;
 442   default:
 443     break;
 444   }
 445 }
 446
 447 void ModelChecker::wait_client(simgrid::mc::Process& process)
 448 {
 449   this->resume(process);
 450   while (this->process().running())
 451     if (!this->handle_events())
 452       return;
 453 }
 454
 455 void ModelChecker::handle_simcall(Transition const& transition)
 456 {
 457   s_mc_simcall_handle_message m;
 458   memset(&m, 0, sizeof(m));
 459   m.type  = MC_MESSAGE_SIMCALL_HANDLE;
 460   m.pid   = transition.pid;
 461   m.value = transition.argument;
 462   this->process_->getChannel().send(m);
 463   this->process_->clear_cache();
 464   while (this->process_->running())
 465     if (!this->handle_events())
 466       return;
 467 }
 468
 469 bool ModelChecker::checkDeadlock()
 470 {
 471   int res;
 472   if ((res = this->process().getChannel().send(MC_MESSAGE_DEADLOCK_CHECK)))
 473     xbt_die("Could not check deadlock state");
 474   s_mc_int_message_t message;
 475   ssize_t s = mc_model_checker->process().getChannel().receive(message);
 476   if (s == -1)
 477     xbt_die("Could not receive message");
 478   if (s != sizeof(message) || message.type != MC_MESSAGE_DEADLOCK_CHECK_REPLY)
 479     xbt_die("%s received unexpected message %s (%i, size=%i) "
 480       "expected MC_MESSAGE_DEADLOCK_CHECK_REPLY (%i, size=%i)",
 481       MC_mode_name(mc_mode),
 482       MC_message_type_name(message.type), (int) message.type, (int) s,
 483       (int) MC_MESSAGE_DEADLOCK_CHECK_REPLY, (int) sizeof(message)
 484       );
 485   return message.value != 0;
 486 }
 487
 488 }
 489 }