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 one to explore the call stack at will. */
  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_choose_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 %s and %s with same issuer", SIMIX_simcall_name(req->call_),
 233                     SIMIX_simcall_name(prev_state->internal_req.call_));
 234           break;
 235
 236         } else {
 237
 238           const smx_actor_t previous_issuer = MC_smx_simcall_get_issuer(&prev_state->internal_req);
 239           XBT_DEBUG("Simcall %s, process %ld (state %d) and simcall %s, process %ld (state %d) are independent",
 240                     SIMIX_simcall_name(req->call_), issuer->get_pid(), state->num_,
 241                     SIMIX_simcall_name(prev_state->internal_req.call_), previous_issuer->get_pid(), prev_state->num_);
 242         }
 243       }
 244     }
 245
 246     if (state->interleave_size() && stack_.size() < (std::size_t)_sg_mc_max_depth) {
 247       /* We found a back-tracking point, let's loop */
 248       XBT_DEBUG("Back-tracking to state %d at depth %zu", state->num_, stack_.size() + 1);
 249       stack_.push_back(std::move(state));
 250       this->restore_state();
 251       XBT_DEBUG("Back-tracking to state %d at depth %zu done", stack_.back()->num_, stack_.size());
 252       break;
 253     } else {
 254       XBT_DEBUG("Delete state %d at depth %zu", state->num_, stack_.size() + 1);
 255     }
 256   }
 257 }
 258
 259 void SafetyChecker::restore_state()
 260 {
 261   /* Intermediate backtracking */
 262   simgrid::mc::State* last_state = stack_.back().get();
 263   if (last_state->system_state) {
 264     last_state->system_state->restore(&mc_model_checker->process());
 265     return;
 266   }
 267
 268   /* Restore the initial state */
 269   simgrid::mc::session->restore_initial_state();
 270
 271   /* Traverse the stack from the state at position start and re-execute the transitions */
 272   for (std::unique_ptr<simgrid::mc::State> const& state : stack_) {
 273     if (state == stack_.back())
 274       break;
 275     session->execute(state->transition_);
 276     /* Update statistics */
 277     mc_model_checker->visited_states++;
 278     mc_model_checker->executed_transitions++;
 279   }
 280 }
 281
 282 SafetyChecker::SafetyChecker(Session& s) : Checker(s)
 283 {
 284   reductionMode_ = simgrid::mc::reduction_mode;
 285   if (_sg_mc_termination)
 286     reductionMode_ = simgrid::mc::ReductionMode::none;
 287   else if (reductionMode_ == simgrid::mc::ReductionMode::unset)
 288     reductionMode_ = simgrid::mc::ReductionMode::dpor;
 289
 290   if (_sg_mc_termination)
 291     XBT_INFO("Check non progressive cycles");
 292   else
 293     XBT_INFO("Check a safety property. Reduction is: %s.",
 294         (reductionMode_ == simgrid::mc::ReductionMode::none ? "none":
 295             (reductionMode_ == simgrid::mc::ReductionMode::dpor ? "dpor": "unknown")));
 296   simgrid::mc::session->initialize();
 297
 298   XBT_DEBUG("Starting the safety algorithm");
 299
 300   std::unique_ptr<simgrid::mc::State> initial_state =
 301       std::unique_ptr<simgrid::mc::State>(new simgrid::mc::State(++expanded_states_count_));
 302
 303   XBT_DEBUG("**************************************************");
 304   XBT_DEBUG("Initial state");
 305
 306   /* Get an enabled actor and insert it in the interleave set of the initial state */
 307   for (auto& actor : mc_model_checker->process().actors())
 308     if (simgrid::mc::actor_is_enabled(actor.copy.get_buffer())) {
 309       initial_state->add_interleaving_set(actor.copy.get_buffer());
 310       if (reductionMode_ != simgrid::mc::ReductionMode::none)
 311         break;
 312     }
 313
 314   stack_.push_back(std::move(initial_state));
 315 }
 316
 317 Checker* createSafetyChecker(Session& s)
 318 {
 319   return new SafetyChecker(s);
 320 }
 321
 322 }
 323 }