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& remoteActor : mc_model_checker->process().actors()) {
 166         auto actor = remoteActor.copy.getBuffer();
 167         if (simgrid::mc::actor_is_enabled(actor)) {
 168           next_state->addInterleavingSet(actor);
 169           if (reductionMode_ == simgrid::mc::ReductionMode::dpor)
 170             break; // With DPOR, we take the first enabled transition
 171         }
 172       }
 173
 174       if (dot_output != nullptr)
 175         std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
 176           state->num, next_state->num, req_str.c_str());
 177
 178     } else if (dot_output != nullptr)
 179       std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num,
 180                    visitedState_->original_num == -1 ? visitedState_->num : visitedState_->original_num,
 181                    req_str.c_str());
 182
 183     stack_.push_back(std::move(next_state));
 184   }
 185
 186   XBT_INFO("No property violation found.");
 187   simgrid::mc::session->logState();
 188 }
 189
 190 void SafetyChecker::backtrack()
 191 {
 192   stack_.pop_back();
 193
 194   /* Check for deadlocks */
 195   if (mc_model_checker->checkDeadlock()) {
 196     MC_show_deadlock();
 197     throw simgrid::mc::DeadlockError();
 198   }
 199
 200   /* Traverse the stack backwards until a state with a non empty interleave
 201      set is found, deleting all the states that have it empty in the way.
 202      For each deleted state, check if the request that has generated it
 203      (from it's predecessor state), depends on any other previous request
 204      executed before it. If it does then add it to the interleave set of the
 205      state that executed that previous request. */
 206
 207   while (not stack_.empty()) {
 208     std::unique_ptr<simgrid::mc::State> state = std::move(stack_.back());
 209     stack_.pop_back();
 210     if (reductionMode_ == simgrid::mc::ReductionMode::dpor) {
 211       smx_simcall_t req = &state->internal_req;
 212       if (req->call == SIMCALL_MUTEX_LOCK || req->call == SIMCALL_MUTEX_TRYLOCK)
 213         xbt_die("Mutex is currently not supported with DPOR,  use --cfg=model-check/reduction:none");
 214
 215       const smx_actor_t issuer = MC_smx_simcall_get_issuer(req);
 216       for (auto i = stack_.rbegin(); i != stack_.rend(); ++i) {
 217         simgrid::mc::State* prev_state = i->get();
 218         if (simgrid::mc::request_depend(req, &prev_state->internal_req)) {
 219           if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
 220             XBT_DEBUG("Dependent Transitions:");
 221             int value = prev_state->transition.argument;
 222             smx_simcall_t prev_req = &prev_state->executed_req;
 223             XBT_DEBUG("%s (state=%d)",
 224               simgrid::mc::request_to_string(
 225                 prev_req, value, simgrid::mc::RequestType::internal).c_str(),
 226               prev_state->num);
 227             value = state->transition.argument;
 228             prev_req = &state->executed_req;
 229             XBT_DEBUG("%s (state=%d)",
 230               simgrid::mc::request_to_string(
 231                 prev_req, value, simgrid::mc::RequestType::executed).c_str(),
 232               state->num);
 233           }
 234
 235           if (not prev_state->actorStates[issuer->pid].isDone())
 236             prev_state->addInterleavingSet(issuer);
 237           else
 238             XBT_DEBUG("Process %p is in done set", req->issuer);
 239
 240           break;
 241
 242         } else if (req->issuer == prev_state->internal_req.issuer) {
 243
 244           XBT_DEBUG("Simcall %d and %d with same issuer", req->call, prev_state->internal_req.call);
 245           break;
 246
 247         } else {
 248
 249           const smx_actor_t previous_issuer = MC_smx_simcall_get_issuer(&prev_state->internal_req);
 250           XBT_DEBUG("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independent",
 251                     req->call, issuer->pid, state->num,
 252                     prev_state->internal_req.call,
 253                     previous_issuer->pid,
 254                     prev_state->num);
 255
 256         }
 257       }
 258     }
 259
 260     if (state->interleaveSize()
 261         && stack_.size() < (std::size_t) _sg_mc_max_depth) {
 262       /* We found a back-tracking point, let's loop */
 263       XBT_DEBUG("Back-tracking to state %d at depth %zi", state->num, stack_.size() + 1);
 264       stack_.push_back(std::move(state));
 265       this->restoreState();
 266       XBT_DEBUG("Back-tracking to state %d at depth %zi done",
 267         stack_.back()->num, stack_.size());
 268       break;
 269     } else {
 270       XBT_DEBUG("Delete state %d at depth %zi",
 271         state->num, stack_.size() + 1);
 272     }
 273   }
 274 }
 275
 276 void SafetyChecker::restoreState()
 277 {
 278   /* Intermediate backtracking */
 279   simgrid::mc::State* state = stack_.back().get();
 280   if (state->system_state) {
 281     simgrid::mc::restore_snapshot(state->system_state);
 282     return;
 283   }
 284
 285   /* Restore the initial state */
 286   simgrid::mc::session->restoreInitialState();
 287
 288   /* Traverse the stack from the state at position start and re-execute the transitions */
 289   for (std::unique_ptr<simgrid::mc::State> const& state : stack_) {
 290     if (state == stack_.back())
 291       break;
 292     session->execute(state->transition);
 293     /* Update statistics */
 294     mc_model_checker->visited_states++;
 295     mc_model_checker->executed_transitions++;
 296   }
 297 }
 298
 299 SafetyChecker::SafetyChecker(Session& session) : Checker(session)
 300 {
 301   reductionMode_ = simgrid::mc::reduction_mode;
 302   if (_sg_mc_termination)
 303     reductionMode_ = simgrid::mc::ReductionMode::none;
 304   else if (reductionMode_ == simgrid::mc::ReductionMode::unset)
 305     reductionMode_ = simgrid::mc::ReductionMode::dpor;
 306
 307   if (_sg_mc_termination)
 308     XBT_INFO("Check non progressive cycles");
 309   else
 310     XBT_INFO("Check a safety property. Reduction is: %s.",
 311         (reductionMode_ == simgrid::mc::ReductionMode::none ? "none":
 312             (reductionMode_ == simgrid::mc::ReductionMode::dpor ? "dpor": "unknown")));
 313   simgrid::mc::session->initialize();
 314
 315   XBT_DEBUG("Starting the safety algorithm");
 316
 317   std::unique_ptr<simgrid::mc::State> initial_state =
 318       std::unique_ptr<simgrid::mc::State>(new simgrid::mc::State(++expandedStatesCount_));
 319
 320   XBT_DEBUG("**************************************************");
 321   XBT_DEBUG("Initial state");
 322
 323   /* Get an enabled actor and insert it in the interleave set of the initial state */
 324   for (auto& actor : mc_model_checker->process().actors())
 325     if (simgrid::mc::actor_is_enabled(actor.copy.getBuffer())) {
 326       initial_state->addInterleavingSet(actor.copy.getBuffer());
 327       if (reductionMode_ != simgrid::mc::ReductionMode::none)
 328         break;
 329     }
 330
 331   stack_.push_back(std::move(initial_state));
 332 }
 333
 334 Checker* createSafetyChecker(Session& session)
 335 {
 336   return new SafetyChecker(session);
 337 }
 338
 339 }
 340 }