src/mc/checker/SafetyChecker.cpp

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