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.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   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 const& 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   XBT_INFO("Expanded states = %lu", expandedStatesCount_);
  83   XBT_INFO("Visited states = %lu", mc_model_checker->visited_states);
  84   XBT_INFO("Executed transitions = %lu", mc_model_checker->executed_transitions);
  85 }
  86
  87 void SafetyChecker::run()
  88 {
  89   /* This function runs the DFS algorithm the state space.
  90    * We do so iteratively instead of recursively, dealing with the call stack manually.
  91    * This allows to explore the call stack at wish. */
  92
  93   while (not stack_.empty()) {
  94
  95     /* Get current state */
  96     simgrid::mc::State* state = stack_.back().get();
  97
  98     XBT_DEBUG("**************************************************");
  99     XBT_DEBUG("Exploration depth=%zu (state=%p, num %d)(%zu interleave)", stack_.size(), state, state->num,
 100               state->interleaveSize());
 101
 102     mc_model_checker->visited_states++;
 103
 104     // Backtrack if we reached the maximum depth
 105     if (stack_.size() > (std::size_t)_sg_mc_max_depth) {
 106       XBT_WARN("/!\\ Max depth reached ! /!\\ ");
 107       this->backtrack();
 108       continue;
 109     }
 110
 111     // Backtrack if we are revisiting a state we saw previously
 112     if (visitedState_ != nullptr) {
 113       XBT_DEBUG("State already visited (equal to state %d), exploration stopped on this path.",
 114                 visitedState_->original_num == -1 ? visitedState_->num : visitedState_->original_num);
 115
 116       visitedState_ = nullptr;
 117       this->backtrack();
 118       continue;
 119     }
 120
 121     // Search an enabled transition in the current state; backtrack if the interleave set is empty
 122     // get_request also sets state.transition to be the one corresponding to the returned req
 123     smx_simcall_t req = MC_state_get_request(state);
 124     // req is now the transition of the process that was selected to be executed
 125
 126     if (req == nullptr) {
 127       XBT_DEBUG("There are no more processes to interleave. (depth %zu)", stack_.size() + 1);
 128
 129       this->backtrack();
 130       continue;
 131     }
 132
 133     // If there are processes to interleave and the maximum depth has not been
 134     // reached then perform one step of the exploration algorithm.
 135     XBT_DEBUG("Execute: %s",
 136       simgrid::mc::request_to_string(
 137         req, state->transition.argument, simgrid::mc::RequestType::simix).c_str());
 138
 139     std::string req_str;
 140     if (dot_output != nullptr)
 141       req_str = simgrid::mc::request_get_dot_output(req, state->transition.argument);
 142
 143     mc_model_checker->executed_transitions++;
 144
 145     /* Actually answer the request: let execute the selected request (MCed does one step) */
 146     this->getSession().execute(state->transition);
 147
 148     /* Create the new expanded state (copy the state of MCed into our MCer data) */
 149     std::unique_ptr<simgrid::mc::State> next_state =
 150         std::unique_ptr<simgrid::mc::State>(new simgrid::mc::State(++expandedStatesCount_));
 151
 152     if (_sg_mc_termination)
 153       this->checkNonTermination(next_state.get());
 154
 155     /* Check whether we already explored next_state in the past (but only if interested in state-equality reduction) */
 156     if (_sg_mc_max_visited_states > 0)
 157       visitedState_ = visitedStates_.addVisitedState(expandedStatesCount_, next_state.get(), true);
 158
 159     /* If this is a new state (or if we don't care about state-equality reduction) */
 160     if (visitedState_ == nullptr) {
 161
 162       /* Get an enabled process and insert it in the interleave set of the next state */
 163       for (auto& remoteActor : mc_model_checker->process().actors()) {
 164         auto actor = remoteActor.copy.getBuffer();
 165         if (simgrid::mc::actor_is_enabled(actor)) {
 166           next_state->addInterleavingSet(actor);
 167           if (reductionMode_ == simgrid::mc::ReductionMode::dpor)
 168             break; // With DPOR, we take the first enabled transition
 169         }
 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->addInterleavingSet(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 %zu", 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 %zu done", stack_.back()->num, stack_.size());
 265       break;
 266     } else {
 267       XBT_DEBUG("Delete state %d at depth %zu", state->num, stack_.size() + 1);
 268     }
 269   }
 270 }
 271
 272 void SafetyChecker::restoreState()
 273 {
 274   /* Intermediate backtracking */
 275   simgrid::mc::State* state = stack_.back().get();
 276   if (state->system_state) {
 277     simgrid::mc::restore_snapshot(state->system_state);
 278     return;
 279   }
 280
 281   /* Restore the initial state */
 282   simgrid::mc::session->restoreInitialState();
 283
 284   /* Traverse the stack from the state at position start and re-execute the transitions */
 285   for (std::unique_ptr<simgrid::mc::State> const& state : stack_) {
 286     if (state == stack_.back())
 287       break;
 288     session->execute(state->transition);
 289     /* Update statistics */
 290     mc_model_checker->visited_states++;
 291     mc_model_checker->executed_transitions++;
 292   }
 293 }
 294
 295 SafetyChecker::SafetyChecker(Session& session) : Checker(session)
 296 {
 297   reductionMode_ = simgrid::mc::reduction_mode;
 298   if (_sg_mc_termination)
 299     reductionMode_ = simgrid::mc::ReductionMode::none;
 300   else if (reductionMode_ == simgrid::mc::ReductionMode::unset)
 301     reductionMode_ = simgrid::mc::ReductionMode::dpor;
 302
 303   if (_sg_mc_termination)
 304     XBT_INFO("Check non progressive cycles");
 305   else
 306     XBT_INFO("Check a safety property. Reduction is: %s.",
 307         (reductionMode_ == simgrid::mc::ReductionMode::none ? "none":
 308             (reductionMode_ == simgrid::mc::ReductionMode::dpor ? "dpor": "unknown")));
 309   simgrid::mc::session->initialize();
 310
 311   XBT_DEBUG("Starting the safety algorithm");
 312
 313   std::unique_ptr<simgrid::mc::State> initial_state =
 314       std::unique_ptr<simgrid::mc::State>(new simgrid::mc::State(++expandedStatesCount_));
 315
 316   XBT_DEBUG("**************************************************");
 317   XBT_DEBUG("Initial state");
 318
 319   /* Get an enabled actor and insert it in the interleave set of the initial state */
 320   for (auto& actor : mc_model_checker->process().actors())
 321     if (simgrid::mc::actor_is_enabled(actor.copy.getBuffer())) {
 322       initial_state->addInterleavingSet(actor.copy.getBuffer());
 323       if (reductionMode_ != simgrid::mc::ReductionMode::none)
 324         break;
 325     }
 326
 327   stack_.push_back(std::move(initial_state));
 328 }
 329
 330 Checker* createSafetyChecker(Session& session)
 331 {
 332   return new SafetyChecker(session);
 333 }
 334
 335 }
 336 }