src/mc/checker/SafetyChecker.cpp

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