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