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