src/mc/checker/SafetyChecker.cpp

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