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 int snapshot_compare(simgrid::mc::State* state1, simgrid::mc::State* state2)
  38 {
  39   simgrid::mc::Snapshot* s1 = state1->system_state.get();
  40   simgrid::mc::Snapshot* s2 = state2->system_state.get();
  41   int num1 = state1->num;
  42   int num2 = state2->num;
  43   return snapshot_compare(num1, s1, num2, s2);
  44 }
  45
  46 void SafetyChecker::checkNonTermination(simgrid::mc::State* current_state)
  47 {
  48   for (auto state = stack_.rbegin(); state != stack_.rend(); ++state)
  49     if (snapshot_compare(state->get(), current_state) == 0) {
  50       XBT_INFO("Non-progressive cycle: state %d -> state %d", (*state)->num, current_state->num);
  51       XBT_INFO("******************************************");
  52       XBT_INFO("*** NON-PROGRESSIVE CYCLE DETECTED ***");
  53       XBT_INFO("******************************************");
  54       XBT_INFO("Counter-example execution trace:");
  55       for (auto& s : mc_model_checker->getChecker()->getTextualTrace())
  56         XBT_INFO("%s", s.c_str());
  57       simgrid::mc::session->logState();
  58
  59       throw simgrid::mc::TerminationError();
  60     }
  61 }
  62
  63 RecordTrace SafetyChecker::getRecordTrace() // override
  64 {
  65   RecordTrace res;
  66   for (auto const& state : stack_)
  67     res.push_back(state->getTransition());
  68   return res;
  69 }
  70
  71 std::vector<std::string> SafetyChecker::getTextualTrace() // override
  72 {
  73   std::vector<std::string> trace;
  74   for (auto const& state : stack_) {
  75     int value = state->transition.argument;
  76     smx_simcall_t req = &state->executed_req;
  77     if (req)
  78       trace.push_back(simgrid::mc::request_to_string(
  79         req, value, simgrid::mc::RequestType::executed));
  80   }
  81   return trace;
  82 }
  83
  84 void SafetyChecker::logState() // override
  85 {
  86   Checker::logState();
  87   XBT_INFO("Expanded states = %lu", expandedStatesCount_);
  88   XBT_INFO("Visited states = %lu", mc_model_checker->visited_states);
  89   XBT_INFO("Executed transitions = %lu", mc_model_checker->executed_transitions);
  90 }
  91
  92 void SafetyChecker::run()
  93 {
  94   /* This function runs the DFS algorithm the state space.
  95    * We do so iteratively instead of recursively, dealing with the call stack manually.
  96    * This allows to explore the call stack when we want to. */
  97
  98   while (!stack_.empty()) {
  99
 100     /* Get current state */
 101     simgrid::mc::State* state = stack_.back().get();
 102
 103     XBT_DEBUG("**************************************************");
 104     XBT_DEBUG("Exploration depth=%zi (state=%p, num %d)(%zu interleave)",
 105       stack_.size(), state, state->num, state->interleaveSize());
 106
 107     mc_model_checker->visited_states++;
 108
 109     // Backtrack if we reached the maximum depth
 110     if (stack_.size() > (std::size_t)_sg_mc_max_depth) {
 111       XBT_WARN("/!\\ Max depth reached ! /!\\ ");
 112       this->backtrack();
 113       continue;
 114     }
 115
 116     // Backtrack if we are revisiting a state we saw previously
 117     if (visitedState_ != nullptr) {
 118       XBT_DEBUG("State already visited (equal to state %d), exploration stopped on this path.",
 119                 visitedState_->other_num == -1 ? visitedState_->num : visitedState_->other_num);
 120
 121       visitedState_ = nullptr;
 122       this->backtrack();
 123       continue;
 124     }
 125
 126     // Search an enabled transition in the current state; backtrack if the interleave set is empty
 127     smx_simcall_t req = MC_state_get_request(state);
 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     /* Answer the request */
 148     this->getSession().execute(state->transition);
 149
 150     /* Create the new expanded state */
 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_visited == true)
 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",
 178         state->num,
 179         visitedState_->other_num == -1 ? visitedState_->num : visitedState_->other_num, 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 (!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, "
 212           "use --cfg=model-check/reduction:none");
 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 (!prev_state->processStates[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 independant",
 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",
 262         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 %zi done",
 266         stack_.back()->num, stack_.size());
 267       break;
 268     } else {
 269       XBT_DEBUG("Delete state %d at depth %zi",
 270         state->num, stack_.size() + 1);
 271     }
 272   }
 273 }
 274
 275 void SafetyChecker::restoreState()
 276 {
 277   /* Intermediate backtracking */
 278   simgrid::mc::State* state = stack_.back().get();
 279   if (state->system_state) {
 280     simgrid::mc::restore_snapshot(state->system_state);
 281     return;
 282   }
 283
 284   /* Restore the initial state */
 285   simgrid::mc::session->restoreInitialState();
 286
 287   /* Traverse the stack from the state at position start and re-execute the transitions */
 288   for (std::unique_ptr<simgrid::mc::State> const& state : stack_) {
 289     if (state == stack_.back())
 290       break;
 291     session->execute(state->transition);
 292     /* Update statistics */
 293     mc_model_checker->visited_states++;
 294     mc_model_checker->executed_transitions++;
 295   }
 296 }
 297
 298 SafetyChecker::SafetyChecker(Session& session) : Checker(session)
 299 {
 300   reductionMode_ = simgrid::mc::reduction_mode;
 301   if (_sg_mc_termination)
 302     reductionMode_ = simgrid::mc::ReductionMode::none;
 303   else if (reductionMode_ == simgrid::mc::ReductionMode::unset)
 304     reductionMode_ = simgrid::mc::ReductionMode::dpor;
 305
 306   if (_sg_mc_termination)
 307     XBT_INFO("Check non progressive cycles");
 308   else
 309     XBT_INFO("Check a safety property");
 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->interleave(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 SafetyChecker::~SafetyChecker()
 332 {
 333 }
 334
 335 Checker* createSafetyChecker(Session& session)
 336 {
 337   return new SafetyChecker(session);
 338 }
 339
 340 }
 341 }