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