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