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