src/mc/ModelChecker.cpp

   1 /* Copyright (c) 2008-2019. The SimGrid Team. All rights reserved.          */
   2
   3 /* This program is free software; you can redistribute it and/or modify it
   4  * under the terms of the license (GNU LGPL) which comes with this package. */
   5
   6 #include "src/mc/ModelChecker.hpp"
   7 #include "src/mc/Session.hpp"
   8 #include "src/mc/Transition.hpp"
   9 #include "src/mc/checker/Checker.hpp"
  10 #include "src/mc/mc_config.hpp"
  11 #include "src/mc/mc_exit.hpp"
  12 #include "src/mc/mc_private.hpp"
  13 #include "src/mc/remote/RemoteClient.hpp"
  14 #include "xbt/automaton.hpp"
  15 #include "xbt/system_error.hpp"
  16
  17 #include <sys/wait.h>
  18
  19 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_ModelChecker, mc, "ModelChecker");
  20
  21 ::simgrid::mc::ModelChecker* mc_model_checker = nullptr;
  22
  23 using simgrid::mc::remote;
  24
  25 #ifdef __linux__
  26 # define WAITPID_CHECKED_FLAGS __WALL
  27 #else
  28 # define WAITPID_CHECKED_FLAGS 0
  29 #endif
  30
  31 namespace simgrid {
  32 namespace mc {
  33
  34 ModelChecker::ModelChecker(std::unique_ptr<RemoteClient> process)
  35     : base_(nullptr)
  36     , socket_event_(nullptr)
  37     , signal_event_(nullptr)
  38     , page_store_(500)
  39     , process_(std::move(process))
  40 {
  41
  42 }
  43
  44 ModelChecker::~ModelChecker() {
  45   if (socket_event_ != nullptr)
  46     event_free(socket_event_);
  47   if (signal_event_ != nullptr)
  48     event_free(signal_event_);
  49   if (base_ != nullptr)
  50     event_base_free(base_);
  51 }
  52
  53 void ModelChecker::start()
  54 {
  55   base_ = event_base_new();
  56   event_callback_fn event_callback = [](evutil_socket_t fd, short events, void *arg)
  57   {
  58     ((ModelChecker *)arg)->handle_events(fd, events);
  59   };
  60   socket_event_ = event_new(base_, process_->get_channel().get_socket(), EV_READ | EV_PERSIST, event_callback, this);
  61   event_add(socket_event_, NULL);
  62   signal_event_ = event_new(base_,
  63                             SIGCHLD,
  64                             EV_SIGNAL|EV_PERSIST,
  65                             event_callback, this);
  66   event_add(signal_event_, NULL);
  67
  68   XBT_DEBUG("Waiting for the model-checked process");
  69   int status;
  70
  71   // The model-checked process SIGSTOP itself to signal it's ready:
  72   const pid_t pid = process_->pid();
  73
  74   pid_t res = waitpid(pid, &status, WUNTRACED | WAITPID_CHECKED_FLAGS);
  75   if (res < 0 || not WIFSTOPPED(status) || WSTOPSIG(status) != SIGSTOP)
  76     xbt_die("Could not wait model-checked process");
  77
  78   process_->init();
  79
  80   if (not _sg_mc_dot_output_file.get().empty())
  81     MC_init_dot_output();
  82
  83   setup_ignore();
  84
  85   if (kill(pid, SIGCONT) != 0)
  86     throw simgrid::xbt::errno_error("Could not wake up the model-checked process");
  87 }
  88
  89 static const std::pair<const char*, const char*> ignored_local_variables[] = {
  90   std::pair<const char*, const char*>{  "e", "*" },
  91   std::pair<const char*, const char*>{ "_log_ev", "*" },
  92
  93   /* Ignore local variable about time used for tracing */
  94   std::pair<const char*, const char*>{ "start_time", "*" },
  95 };
  96
  97 void ModelChecker::setup_ignore()
  98 {
  99   RemoteClient& process = this->process();
 100   for (std::pair<const char*, const char*> const& var :
 101       ignored_local_variables)
 102     process.ignore_local_variable(var.first, var.second);
 103
 104   /* Static variable used for tracing */
 105   process.ignore_global_variable("counter");
 106 }
 107
 108 void ModelChecker::shutdown()
 109 {
 110   XBT_DEBUG("Shuting down model-checker");
 111
 112   simgrid::mc::RemoteClient* process = &this->process();
 113   if (process->running()) {
 114     XBT_DEBUG("Killing process");
 115     kill(process->pid(), SIGKILL);
 116     process->terminate();
 117   }
 118 }
 119
 120 void ModelChecker::resume(simgrid::mc::RemoteClient& process)
 121 {
 122   int res = process.get_channel().send(MC_MESSAGE_CONTINUE);
 123   if (res)
 124     throw simgrid::xbt::errno_error();
 125   process.clear_cache();
 126 }
 127
 128 static void MC_report_crash(int status)
 129 {
 130   XBT_INFO("**************************");
 131   XBT_INFO("** CRASH IN THE PROGRAM **");
 132   XBT_INFO("**************************");
 133   if (WIFSIGNALED(status))
 134     XBT_INFO("From signal: %s", strsignal(WTERMSIG(status)));
 135   else if (WIFEXITED(status))
 136     XBT_INFO("From exit: %i", WEXITSTATUS(status));
 137   if (WCOREDUMP(status))
 138     XBT_INFO("A core dump was generated by the system.");
 139   else
 140     XBT_INFO("No core dump was generated by the system.");
 141   XBT_INFO("Counter-example execution trace:");
 142   for (auto const& s : mc_model_checker->getChecker()->get_textual_trace())
 143     XBT_INFO("  %s", s.c_str());
 144   simgrid::mc::dumpRecordPath();
 145   simgrid::mc::session->log_state();
 146   XBT_INFO("Stack trace:");
 147   mc_model_checker->process().dump_stack();
 148 }
 149
 150 static void MC_report_assertion_error()
 151 {
 152   XBT_INFO("**************************");
 153   XBT_INFO("*** PROPERTY NOT VALID ***");
 154   XBT_INFO("**************************");
 155   XBT_INFO("Counter-example execution trace:");
 156   for (auto const& s : mc_model_checker->getChecker()->get_textual_trace())
 157     XBT_INFO("  %s", s.c_str());
 158   simgrid::mc::dumpRecordPath();
 159   simgrid::mc::session->log_state();
 160 }
 161
 162 bool ModelChecker::handle_message(char* buffer, ssize_t size)
 163 {
 164   s_mc_message_t base_message;
 165   if (size < (ssize_t) sizeof(base_message))
 166     xbt_die("Broken message");
 167   memcpy(&base_message, buffer, sizeof(base_message));
 168
 169   switch(base_message.type) {
 170
 171   case MC_MESSAGE_IGNORE_HEAP:
 172     {
 173     s_mc_message_ignore_heap_t message;
 174     if (size != sizeof(message))
 175       xbt_die("Broken messsage");
 176     memcpy(&message, buffer, sizeof(message));
 177
 178     IgnoredHeapRegion region;
 179     region.block    = message.block;
 180     region.fragment = message.fragment;
 181     region.address  = message.address;
 182     region.size     = message.size;
 183     process().ignore_heap(region);
 184     break;
 185     }
 186
 187   case MC_MESSAGE_UNIGNORE_HEAP:
 188     {
 189     s_mc_message_ignore_memory_t message;
 190     if (size != sizeof(message))
 191       xbt_die("Broken messsage");
 192     memcpy(&message, buffer, sizeof(message));
 193     process().unignore_heap((void*)(std::uintptr_t)message.addr, message.size);
 194     break;
 195     }
 196
 197   case MC_MESSAGE_IGNORE_MEMORY:
 198     {
 199     s_mc_message_ignore_memory_t message;
 200     if (size != sizeof(message))
 201       xbt_die("Broken messsage");
 202     memcpy(&message, buffer, sizeof(message));
 203     this->process().ignore_region(message.addr, message.size);
 204     break;
 205     }
 206
 207   case MC_MESSAGE_STACK_REGION:
 208     {
 209     s_mc_message_stack_region_t message;
 210     if (size != sizeof(message))
 211       xbt_die("Broken messsage");
 212     memcpy(&message, buffer, sizeof(message));
 213     this->process().stack_areas().push_back(message.stack_region);
 214     }
 215     break;
 216
 217   case MC_MESSAGE_REGISTER_SYMBOL:
 218     {
 219     s_mc_message_register_symbol_t message;
 220     if (size != sizeof(message))
 221       xbt_die("Broken message");
 222     memcpy(&message, buffer, sizeof(message));
 223     if (message.callback)
 224       xbt_die("Support for client-side function proposition is not implemented.");
 225     XBT_DEBUG("Received symbol: %s", message.name);
 226
 227     if (simgrid::mc::property_automaton == nullptr)
 228       simgrid::mc::property_automaton = xbt_automaton_new();
 229
 230     simgrid::mc::RemoteClient* process  = &this->process();
 231     simgrid::mc::RemotePtr<int> address = simgrid::mc::remote((int*)message.data);
 232     simgrid::xbt::add_proposition(simgrid::mc::property_automaton, message.name,
 233                                   [process, address]() { return process->read(address); });
 234
 235     break;
 236     }
 237
 238   case MC_MESSAGE_WAITING:
 239     return false;
 240
 241   case MC_MESSAGE_ASSERTION_FAILED:
 242     MC_report_assertion_error();
 243     this->exit(SIMGRID_MC_EXIT_SAFETY);
 244
 245   default:
 246     xbt_die("Unexpected message from model-checked application");
 247
 248   }
 249   return true;
 250 }
 251
 252 /** Terminate the model-checker application */
 253 void ModelChecker::exit(int status)
 254 {
 255   // TODO, terminate the model checker politely instead of exiting rudely
 256   if (process().running())
 257     kill(process().pid(), SIGKILL);
 258   ::exit(status);
 259 }
 260
 261 void ModelChecker::handle_events(int fd, short events)
 262 {
 263   if (events == EV_READ) {
 264     char buffer[MC_MESSAGE_LENGTH];
 265     ssize_t size = process_->get_channel().receive(buffer, sizeof(buffer), false);
 266     if (size == -1 && errno != EAGAIN)
 267       throw simgrid::xbt::errno_error();
 268     if (not handle_message(buffer, size)) {
 269       event_base_loopbreak(base_);
 270     }
 271   }
 272   else if (events == EV_SIGNAL) {
 273     on_signal(fd);
 274   }
 275   else {
 276     xbt_die("Unexpected event");
 277   }
 278 }
 279
 280 void ModelChecker::loop()
 281 {
 282   if (this->process().running())
 283     event_base_dispatch(base_);
 284 }
 285
 286 void ModelChecker::handle_waitpid()
 287 {
 288   XBT_DEBUG("Check for wait event");
 289   int status;
 290   pid_t pid;
 291   while ((pid = waitpid(-1, &status, WNOHANG)) != 0) {
 292     if (pid == -1) {
 293       if (errno == ECHILD) {
 294         // No more children:
 295         if (this->process().running())
 296           xbt_die("Inconsistent state");
 297         else
 298           break;
 299       } else {
 300         XBT_ERROR("Could not wait for pid");
 301         throw simgrid::xbt::errno_error();
 302       }
 303     }
 304
 305     if (pid == this->process().pid()) {
 306       xbt_assert(WIFEXITED(status) || WIFSIGNALED(status));
 307       XBT_DEBUG("Child process is over");
 308       this->process().terminate();
 309     }
 310   }
 311 }
 312
 313 void ModelChecker::on_signal(int signo)
 314 {
 315   if (signo == SIGCHLD)
 316     this->handle_waitpid();
 317 }
 318
 319 void ModelChecker::wait_for_requests()
 320 {
 321   this->resume(process());
 322   if (this->process().running())
 323     event_base_dispatch(base_);
 324 }
 325
 326 void ModelChecker::handle_simcall(Transition const& transition)
 327 {
 328   s_mc_message_simcall_handle_t m;
 329   memset(&m, 0, sizeof(m));
 330   m.type  = MC_MESSAGE_SIMCALL_HANDLE;
 331   m.pid   = transition.pid;
 332   m.value = transition.argument;
 333   this->process_->get_channel().send(m);
 334   this->process_->clear_cache();
 335   if (this->process_->running())
 336     event_base_dispatch(base_);
 337 }
 338
 339 bool ModelChecker::checkDeadlock()
 340 {
 341   int res;
 342   if ((res = this->process().get_channel().send(MC_MESSAGE_DEADLOCK_CHECK)))
 343     xbt_die("Could not check deadlock state");
 344   s_mc_message_int_t message;
 345   ssize_t s = mc_model_checker->process().get_channel().receive(message);
 346   if (s == -1)
 347     xbt_die("Could not receive message");
 348   if (s != sizeof(message) || message.type != MC_MESSAGE_DEADLOCK_CHECK_REPLY)
 349     xbt_die("Received unexpected message %s (%i, size=%i) "
 350       "expected MC_MESSAGE_DEADLOCK_CHECK_REPLY (%i, size=%i)",
 351       MC_message_type_name(message.type), (int) message.type, (int) s,
 352       (int) MC_MESSAGE_DEADLOCK_CHECK_REPLY, (int) sizeof(message)
 353       );
 354   return message.value != 0;
 355 }
 356
 357 }
 358 }