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 static int snapshot_compare(simgrid::mc::State* state1, simgrid::mc::State* state2)
  35 {
  36   simgrid::mc::Snapshot* s1 = state1->system_state.get();
  37   simgrid::mc::Snapshot* s2 = state2->system_state.get();
  38   return snapshot_compare(s1, s2);
  39 }
  40
  41 void SafetyChecker::check_non_termination(simgrid::mc::State* current_state)
  42 {
  43   for (auto state = stack_.rbegin(); state != stack_.rend(); ++state)
  44     if (snapshot_compare(state->get(), current_state) == 0) {
  45       XBT_INFO("Non-progressive cycle: state %d -> state %d", (*state)->num, current_state->num);
  46       XBT_INFO("******************************************");
  47       XBT_INFO("*** NON-PROGRESSIVE CYCLE DETECTED ***");
  48       XBT_INFO("******************************************");
  49       XBT_INFO("Counter-example execution trace:");
  50       for (auto const& s : mc_model_checker->getChecker()->get_textual_trace())
  51         XBT_INFO("  %s", s.c_str());
  52       simgrid::mc::dumpRecordPath();
  53       simgrid::mc::session->log_state();
  54
  55       throw simgrid::mc::TerminationError();
  56     }
  57 }
  58
  59 RecordTrace SafetyChecker::get_record_trace() // override
  60 {
  61   RecordTrace res;
  62   for (auto const& state : stack_)
  63     res.push_back(state->getTransition());
  64   return res;
  65 }
  66
  67 std::vector<std::string> SafetyChecker::get_textual_trace() // override
  68 {
  69   std::vector<std::string> trace;
  70   for (auto const& state : stack_) {
  71     int value = state->transition.argument;
  72     smx_simcall_t req = &state->executed_req;
  73     if (req)
  74       trace.push_back(simgrid::mc::request_to_string(
  75         req, value, simgrid::mc::RequestType::executed));
  76   }
  77   return trace;
  78 }
  79
  80 void SafetyChecker::log_state() // override
  81 {
  82   XBT_INFO("Expanded states = %lu", expanded_states_count_);
  83   XBT_INFO("Visited states = %lu", mc_model_checker->visited_states);
  84   XBT_INFO("Executed transitions = %lu", mc_model_checker->executed_transitions);
  85 }
  86
  87 void SafetyChecker::run()
  88 {
  89   /* This function runs the DFS algorithm the state space.
  90    * We do so iteratively instead of recursively, dealing with the call stack manually.
  91    * This allows to explore the call stack at wish. */
  92
  93   while (not stack_.empty()) {
  94
  95     /* Get current state */
  96     simgrid::mc::State* state = stack_.back().get();
  97
  98     XBT_DEBUG("**************************************************");
  99     XBT_DEBUG("Exploration depth=%zu (state=%p, num %d)(%zu interleave)", stack_.size(), state, state->num,
 100               state->interleaveSize());
 101
 102     mc_model_checker->visited_states++;
 103
 104     // Backtrack if we reached the maximum depth
 105     if (stack_.size() > (std::size_t)_sg_mc_max_depth) {
 106       XBT_WARN("/!\\ Max depth reached ! /!\\ ");
 107       this->backtrack();
 108       continue;
 109     }
 110
 111     // Backtrack if we are revisiting a state we saw previously
 112     if (visited_state_ != nullptr) {
 113       XBT_DEBUG("State already visited (equal to state %d), exploration stopped on this path.",
 114                 visited_state_->original_num == -1 ? visited_state_->num : visited_state_->original_num);
 115
 116       visited_state_ = nullptr;
 117       this->backtrack();
 118       continue;
 119     }
 120
 121     // Search an enabled transition in the current state; backtrack if the interleave set is empty
 122     // get_request also sets state.transition to be the one corresponding to the returned req
 123     smx_simcall_t req = MC_state_get_request(state);
 124     // req is now the transition of the process that was selected to be executed
 125
 126     if (req == nullptr) {
 127       XBT_DEBUG("There are no more processes to interleave. (depth %zu)", stack_.size() + 1);
 128
 129       this->backtrack();
 130       continue;
 131     }
 132
 133     // If there are processes to interleave and the maximum depth has not been
 134     // reached then perform one step of the exploration algorithm.
 135     XBT_DEBUG("Execute: %s",
 136       simgrid::mc::request_to_string(
 137         req, state->transition.argument, simgrid::mc::RequestType::simix).c_str());
 138
 139     std::string req_str;
 140     if (dot_output != nullptr)
 141       req_str = simgrid::mc::request_get_dot_output(req, state->transition.argument);
 142
 143     mc_model_checker->executed_transitions++;
 144
 145     /* Actually answer the request: let execute the selected request (MCed does one step) */
 146     this->get_session().execute(state->transition);
 147
 148     /* Create the new expanded state (copy the state of MCed into our MCer data) */
 149     std::unique_ptr<simgrid::mc::State> next_state =
 150         std::unique_ptr<simgrid::mc::State>(new simgrid::mc::State(++expanded_states_count_));
 151
 152     if (_sg_mc_termination)
 153       this->check_non_termination(next_state.get());
 154
 155     /* Check whether we already explored next_state in the past (but only if interested in state-equality reduction) */
 156     if (_sg_mc_max_visited_states > 0)
 157       visited_state_ = visited_states_.addVisitedState(expanded_states_count_, next_state.get(), true);
 158
 159     /* If this is a new state (or if we don't care about state-equality reduction) */
 160     if (visited_state_ == nullptr) {
 161
 162       /* Get an enabled process and insert it in the interleave set of the next state */
 163       for (auto& remoteActor : mc_model_checker->process().actors()) {
 164         auto actor = remoteActor.copy.get_buffer();
 165         if (simgrid::mc::actor_is_enabled(actor)) {
 166           next_state->addInterleavingSet(actor);
 167           if (reductionMode_ == simgrid::mc::ReductionMode::dpor)
 168             break; // With DPOR, we take the first enabled transition
 169         }
 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", state->num,
 178                    visited_state_->original_num == -1 ? visited_state_->num : visited_state_->original_num,
 179                    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->log_state();
 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 (not 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,  use --cfg=model-check/reduction:none");
 212
 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 (not prev_state->actorStates[issuer->get_pid()].isDone())
 234             prev_state->addInterleavingSet(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 %ld (state %d) and simcall %d, process %ld (state %d) are independent",
 249                     req->call, issuer->get_pid(), state->num, prev_state->internal_req.call, previous_issuer->get_pid(),
 250                     prev_state->num);
 251         }
 252       }
 253     }
 254
 255     if (state->interleaveSize()
 256         && stack_.size() < (std::size_t) _sg_mc_max_depth) {
 257       /* We found a back-tracking point, let's loop */
 258       XBT_DEBUG("Back-tracking to state %d at depth %zu", state->num, stack_.size() + 1);
 259       stack_.push_back(std::move(state));
 260       this->restore_state();
 261       XBT_DEBUG("Back-tracking to state %d at depth %zu done", stack_.back()->num, stack_.size());
 262       break;
 263     } else {
 264       XBT_DEBUG("Delete state %d at depth %zu", state->num, stack_.size() + 1);
 265     }
 266   }
 267 }
 268
 269 void SafetyChecker::restore_state()
 270 {
 271   /* Intermediate backtracking */
 272   simgrid::mc::State* last_state = stack_.back().get();
 273   if (last_state->system_state) {
 274     last_state->system_state->restore(&mc_model_checker->process());
 275     return;
 276   }
 277
 278   /* Restore the initial state */
 279   simgrid::mc::session->restore_initial_state();
 280
 281   /* Traverse the stack from the state at position start and re-execute the transitions */
 282   for (std::unique_ptr<simgrid::mc::State> const& state : stack_) {
 283     if (state == stack_.back())
 284       break;
 285     session->execute(state->transition);
 286     /* Update statistics */
 287     mc_model_checker->visited_states++;
 288     mc_model_checker->executed_transitions++;
 289   }
 290 }
 291
 292 SafetyChecker::SafetyChecker(Session& s) : Checker(s)
 293 {
 294   reductionMode_ = simgrid::mc::reduction_mode;
 295   if (_sg_mc_termination)
 296     reductionMode_ = simgrid::mc::ReductionMode::none;
 297   else if (reductionMode_ == simgrid::mc::ReductionMode::unset)
 298     reductionMode_ = simgrid::mc::ReductionMode::dpor;
 299
 300   if (_sg_mc_termination)
 301     XBT_INFO("Check non progressive cycles");
 302   else
 303     XBT_INFO("Check a safety property. Reduction is: %s.",
 304         (reductionMode_ == simgrid::mc::ReductionMode::none ? "none":
 305             (reductionMode_ == simgrid::mc::ReductionMode::dpor ? "dpor": "unknown")));
 306   simgrid::mc::session->initialize();
 307
 308   XBT_DEBUG("Starting the safety algorithm");
 309
 310   std::unique_ptr<simgrid::mc::State> initial_state =
 311       std::unique_ptr<simgrid::mc::State>(new simgrid::mc::State(++expanded_states_count_));
 312
 313   XBT_DEBUG("**************************************************");
 314   XBT_DEBUG("Initial state");
 315
 316   /* Get an enabled actor and insert it in the interleave set of the initial state */
 317   for (auto& actor : mc_model_checker->process().actors())
 318     if (simgrid::mc::actor_is_enabled(actor.copy.get_buffer())) {
 319       initial_state->addInterleavingSet(actor.copy.get_buffer());
 320       if (reductionMode_ != simgrid::mc::ReductionMode::none)
 321         break;
 322     }
 323
 324   stack_.push_back(std::move(initial_state));
 325 }
 326
 327 Checker* createSafetyChecker(Session& s)
 328 {
 329   return new SafetyChecker(s);
 330 }
 331
 332 }
 333 }