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