src/mc/SafetyChecker.cpp

   1 /* Copyright (c) 2016. 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 #include <cstdio>
   9
  10 #include <memory>
  11 #include <string>
  12 #include <vector>
  13
  14 #include <xbt/log.h>
  15 #include <xbt/sysdep.h>
  16
  17 #include "src/mc/mc_state.h"
  18 #include "src/mc/mc_request.h"
  19 #include "src/mc/mc_safety.h"
  20 #include "src/mc/mc_private.h"
  21 #include "src/mc/mc_record.h"
  22 #include "src/mc/mc_smx.h"
  23 #include "src/mc/Client.hpp"
  24 #include "src/mc/mc_exit.h"
  25 #include "src/mc/Checker.hpp"
  26 #include "src/mc/SafetyChecker.hpp"
  27 #include "src/mc/VisitedState.hpp"
  28 #include "src/mc/Transition.hpp"
  29 #include "src/mc/Session.hpp"
  30
  31 #include "src/xbt/mmalloc/mmprivate.h"
  32
  33 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_safety, mc,
  34                                 "Logging specific to MC safety verification ");
  35 namespace simgrid {
  36 namespace mc {
  37
  38 static void MC_show_non_termination(void)
  39 {
  40   XBT_INFO("******************************************");
  41   XBT_INFO("*** NON-PROGRESSIVE CYCLE DETECTED ***");
  42   XBT_INFO("******************************************");
  43   XBT_INFO("Counter-example execution trace:");
  44   for (auto& s : mc_model_checker->getChecker()->getTextualTrace())
  45     XBT_INFO("%s", s.c_str());
  46   simgrid::mc::session->logState();
  47 }
  48
  49 static int snapshot_compare(simgrid::mc::State* state1, simgrid::mc::State* state2)
  50 {
  51   simgrid::mc::Snapshot* s1 = state1->system_state.get();
  52   simgrid::mc::Snapshot* s2 = state2->system_state.get();
  53   int num1 = state1->num;
  54   int num2 = state2->num;
  55   return snapshot_compare(num1, s1, num2, s2);
  56 }
  57
  58 bool SafetyChecker::checkNonTermination(simgrid::mc::State* current_state)
  59 {
  60   for (auto i = stack_.rbegin(); i != stack_.rend(); ++i)
  61     if (snapshot_compare(i->get(), current_state) == 0){
  62       XBT_INFO("Non-progressive cycle : state %d -> state %d",
  63         (*i)->num, current_state->num);
  64       return true;
  65     }
  66   return false;
  67 }
  68
  69 RecordTrace SafetyChecker::getRecordTrace() // override
  70 {
  71   RecordTrace res;
  72   for (auto const& state : stack_)
  73     res.push_back(state->getTransition());
  74   return res;
  75 }
  76
  77 std::vector<std::string> SafetyChecker::getTextualTrace() // override
  78 {
  79   std::vector<std::string> trace;
  80   for (auto const& state : stack_) {
  81     int value = state->transition.argument;
  82     smx_simcall_t req = &state->executed_req;
  83     if (req)
  84       trace.push_back(simgrid::mc::request_to_string(
  85         req, value, simgrid::mc::RequestType::executed));
  86   }
  87   return trace;
  88 }
  89
  90 void SafetyChecker::logState() // override
  91 {
  92   Checker::logState();
  93   XBT_INFO("Expanded states = %lu", expandedStatesCount_);
  94   XBT_INFO("Visited states = %lu", mc_model_checker->visited_states);
  95   XBT_INFO("Executed transitions = %lu", mc_model_checker->executed_transitions);
  96 }
  97
  98 int SafetyChecker::run()
  99 {
 100   this->init();
 101
 102   while (!stack_.empty()) {
 103
 104     /* Get current state */
 105     simgrid::mc::State* state = stack_.back().get();
 106
 107     XBT_DEBUG("**************************************************");
 108     XBT_DEBUG(
 109       "Exploration depth=%zi (state=%p, num %d)(%zu interleave)",
 110       stack_.size(), state, state->num,
 111       state->interleaveSize());
 112
 113     mc_model_checker->visited_states++;
 114
 115     // The interleave set is empty or the maximum depth is reached,
 116     // let's back-track.
 117     smx_simcall_t req = nullptr;
 118     if (stack_.size() > (std::size_t) _sg_mc_max_depth
 119         || (req = MC_state_get_request(state)) == nullptr
 120         || visitedState_ != nullptr) {
 121       int res = this->backtrack();
 122       if (res)
 123         return res;
 124       else
 125         continue;
 126     }
 127
 128     // If there are processes to interleave and the maximum depth has not been
 129     // reached then perform one step of the exploration algorithm.
 130     XBT_DEBUG("Execute: %s",
 131       simgrid::mc::request_to_string(
 132         req, state->transition.argument, simgrid::mc::RequestType::simix).c_str());
 133
 134     std::string req_str;
 135     if (dot_output != nullptr)
 136       req_str = simgrid::mc::request_get_dot_output(req, state->transition.argument);
 137
 138     mc_model_checker->executed_transitions++;
 139
 140     /* Answer the request */
 141     this->getSession().execute(state->transition);
 142
 143     /* Create the new expanded state */
 144     std::unique_ptr<simgrid::mc::State> next_state =
 145       std::unique_ptr<simgrid::mc::State>(MC_state_new(++expandedStatesCount_));
 146
 147     if (_sg_mc_termination && this->checkNonTermination(next_state.get())) {
 148         MC_show_non_termination();
 149         return SIMGRID_MC_EXIT_NON_TERMINATION;
 150     }
 151
 152     if (_sg_mc_visited == 0
 153         || (visitedState_ = visitedStates_.addVisitedState(expandedStatesCount_, next_state.get(), true)) == nullptr) {
 154
 155       /* Get an enabled process and insert it in the interleave set of the next state */
 156       for (auto& p : mc_model_checker->process().simix_processes())
 157         if (simgrid::mc::process_is_enabled(p.copy.getBuffer())) {
 158           next_state->interleave(p.copy.getBuffer());
 159           if (reductionMode_ != simgrid::mc::ReductionMode::none)
 160             break;
 161         }
 162
 163       if (dot_output != nullptr)
 164         std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
 165           state->num, next_state->num, req_str.c_str());
 166
 167     } else if (dot_output != nullptr)
 168       std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
 169         state->num,
 170         visitedState_->other_num == -1 ? visitedState_->num : visitedState_->other_num, req_str.c_str());
 171
 172     stack_.push_back(std::move(next_state));
 173   }
 174
 175   XBT_INFO("No property violation found.");
 176   simgrid::mc::session->logState();
 177   return SIMGRID_MC_EXIT_SUCCESS;
 178 }
 179
 180 int SafetyChecker::backtrack()
 181 {
 182   if (stack_.size() > (std::size_t) _sg_mc_max_depth
 183       || visitedState_ != nullptr) {
 184     if (visitedState_ == nullptr)
 185       XBT_WARN("/!\\ Max depth reached ! /!\\ ");
 186     else
 187       XBT_DEBUG("State already visited (equal to state %d),"
 188         " exploration stopped on this path.",
 189         visitedState_->other_num == -1 ? visitedState_->num : visitedState_->other_num);
 190   } else
 191     XBT_DEBUG("There are no more processes to interleave. (depth %zi)",
 192       stack_.size() + 1);
 193
 194   stack_.pop_back();
 195
 196   visitedState_ = nullptr;
 197
 198   /* Check for deadlocks */
 199   if (mc_model_checker->checkDeadlock()) {
 200     MC_show_deadlock();
 201     return SIMGRID_MC_EXIT_DEADLOCK;
 202   }
 203
 204   /* Traverse the stack backwards until a state with a non empty interleave
 205      set is found, deleting all the states that have it empty in the way.
 206      For each deleted state, check if the request that has generated it
 207      (from it's predecesor state), depends on any other previous request
 208      executed before it. If it does then add it to the interleave set of the
 209      state that executed that previous request. */
 210
 211   while (!stack_.empty()) {
 212     std::unique_ptr<simgrid::mc::State> state = std::move(stack_.back());
 213     stack_.pop_back();
 214     if (reductionMode_ == simgrid::mc::ReductionMode::dpor) {
 215       smx_simcall_t req = &state->internal_req;
 216       if (req->call == SIMCALL_MUTEX_LOCK || req->call == SIMCALL_MUTEX_TRYLOCK)
 217         xbt_die("Mutex is currently not supported with DPOR, "
 218           "use --cfg=model-check/reduction:none");
 219       const smx_actor_t issuer = MC_smx_simcall_get_issuer(req);
 220       for (auto i = stack_.rbegin(); i != stack_.rend(); ++i) {
 221         simgrid::mc::State* prev_state = i->get();
 222         if (simgrid::mc::request_depend(req, &prev_state->internal_req)) {
 223           if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
 224             XBT_DEBUG("Dependent Transitions:");
 225             int value = prev_state->transition.argument;
 226             smx_simcall_t prev_req = &prev_state->executed_req;
 227             XBT_DEBUG("%s (state=%d)",
 228               simgrid::mc::request_to_string(
 229                 prev_req, value, simgrid::mc::RequestType::internal).c_str(),
 230               prev_state->num);
 231             value = state->transition.argument;
 232             prev_req = &state->executed_req;
 233             XBT_DEBUG("%s (state=%d)",
 234               simgrid::mc::request_to_string(
 235                 prev_req, value, simgrid::mc::RequestType::executed).c_str(),
 236               state->num);
 237           }
 238
 239           if (!prev_state->processStates[issuer->pid].isDone())
 240             prev_state->interleave(issuer);
 241           else
 242             XBT_DEBUG("Process %p is in done set", req->issuer);
 243
 244           break;
 245
 246         } else if (req->issuer == prev_state->internal_req.issuer) {
 247
 248           XBT_DEBUG("Simcall %d and %d with same issuer", req->call, prev_state->internal_req.call);
 249           break;
 250
 251         } else {
 252
 253           const smx_actor_t previous_issuer = MC_smx_simcall_get_issuer(&prev_state->internal_req);
 254           XBT_DEBUG("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant",
 255                     req->call, issuer->pid, state->num,
 256                     prev_state->internal_req.call,
 257                     previous_issuer->pid,
 258                     prev_state->num);
 259
 260         }
 261       }
 262     }
 263
 264     if (state->interleaveSize()
 265         && stack_.size() < (std::size_t) _sg_mc_max_depth) {
 266       /* We found a back-tracking point, let's loop */
 267       XBT_DEBUG("Back-tracking to state %d at depth %zi",
 268         state->num, stack_.size() + 1);
 269       stack_.push_back(std::move(state));
 270       this->restoreState();
 271       XBT_DEBUG("Back-tracking to state %d at depth %zi done",
 272         stack_.back()->num, stack_.size());
 273       break;
 274     } else {
 275       XBT_DEBUG("Delete state %d at depth %zi",
 276         state->num, stack_.size() + 1);
 277     }
 278   }
 279   return SIMGRID_MC_EXIT_SUCCESS;
 280 }
 281
 282 void SafetyChecker::restoreState()
 283 {
 284   /* Intermediate backtracking */
 285   {
 286     simgrid::mc::State* state = stack_.back().get();
 287     if (state->system_state) {
 288       simgrid::mc::restore_snapshot(state->system_state);
 289       return;
 290     }
 291   }
 292
 293   /* Restore the initial state */
 294   simgrid::mc::session->restoreInitialState();
 295
 296   /* Traverse the stack from the state at position start and re-execute the transitions */
 297   for (std::unique_ptr<simgrid::mc::State> const& state : stack_) {
 298     if (state == stack_.back())
 299       break;
 300     session->execute(state->transition);
 301     /* Update statistics */
 302     mc_model_checker->visited_states++;
 303     mc_model_checker->executed_transitions++;
 304   }
 305 }
 306
 307 void SafetyChecker::init()
 308 {
 309   reductionMode_ = simgrid::mc::reduction_mode;
 310   if( _sg_mc_termination)
 311     reductionMode_ = simgrid::mc::ReductionMode::none;
 312   else if (reductionMode_ == simgrid::mc::ReductionMode::unset)
 313     reductionMode_ = simgrid::mc::ReductionMode::dpor;
 314
 315   if (_sg_mc_termination)
 316     XBT_INFO("Check non progressive cycles");
 317   else
 318     XBT_INFO("Check a safety property");
 319   simgrid::mc::session->initialize();
 320
 321   XBT_DEBUG("Starting the safety algorithm");
 322
 323   std::unique_ptr<simgrid::mc::State> initial_state =
 324     std::unique_ptr<simgrid::mc::State>(MC_state_new(++expandedStatesCount_));
 325
 326   XBT_DEBUG("**************************************************");
 327   XBT_DEBUG("Initial state");
 328
 329   /* Get an enabled process and insert it in the interleave set of the initial state */
 330   for (auto& p : mc_model_checker->process().simix_processes())
 331     if (simgrid::mc::process_is_enabled(p.copy.getBuffer())) {
 332       initial_state->interleave(p.copy.getBuffer());
 333       if (reductionMode_ != simgrid::mc::ReductionMode::none)
 334         break;
 335     }
 336
 337   stack_.push_back(std::move(initial_state));
 338 }
 339
 340 SafetyChecker::SafetyChecker(Session& session) : Checker(session)
 341 {
 342 }
 343
 344 SafetyChecker::~SafetyChecker()
 345 {
 346 }
 347
 348 Checker* createSafetyChecker(Session& session)
 349 {
 350   return new SafetyChecker(session);
 351 }
 352
 353 }
 354 }