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