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",
  63         (*i)->num, current_state->num);
  64       return true;
  65     }
  66   return false;
  67 }
  68
  69 RecordTrace SafetyChecker::getRecordTrace() // override
  70 {
  71   RecordTrace res;
  72   for (auto const& state : stack_)
  73     res.push_back(state->getTransition());
  74   return res;
  75 }
  76
  77 std::vector<std::string> SafetyChecker::getTextualTrace() // override
  78 {
  79   std::vector<std::string> trace;
  80   for (auto const& state : stack_) {
  81     int value = state->transition.argument;
  82     smx_simcall_t req = &state->executed_req;
  83     if (req)
  84       trace.push_back(simgrid::mc::request_to_string(
  85         req, value, simgrid::mc::RequestType::executed));
  86   }
  87   return trace;
  88 }
  89
  90 void SafetyChecker::logState() // override
  91 {
  92   Checker::logState();
  93   XBT_INFO("Expanded states = %lu", expandedStatesCount_);
  94   XBT_INFO("Visited states = %lu", mc_model_checker->visited_states);
  95   XBT_INFO("Executed transitions = %lu", mc_model_checker->executed_transitions);
  96 }
  97
  98 int SafetyChecker::run()
  99 {
 100   while (!stack_.empty()) {
 101
 102     /* Get current state */
 103     simgrid::mc::State* state = stack_.back().get();
 104
 105     XBT_DEBUG("**************************************************");
 106     XBT_DEBUG(
 107       "Exploration depth=%zi (state=%p, num %d)(%zu interleave)",
 108       stack_.size(), state, state->num,
 109       state->interleaveSize());
 110
 111     mc_model_checker->visited_states++;
 112
 113     // The interleave set is empty or the maximum depth is reached,
 114     // let's back-track.
 115     smx_simcall_t req = nullptr;
 116     if (stack_.size() > (std::size_t) _sg_mc_max_depth
 117         || (req = MC_state_get_request(state)) == nullptr
 118         || visitedState_ != nullptr) {
 119       int res = this->backtrack();
 120       if (res)
 121         return res;
 122       else
 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("Execute: %s",
 129       simgrid::mc::request_to_string(
 130         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     /* Answer the request */
 139     this->getSession().execute(state->transition);
 140
 141     /* Create the new expanded state */
 142     std::unique_ptr<simgrid::mc::State> next_state =
 143       std::unique_ptr<simgrid::mc::State>(MC_state_new(++expandedStatesCount_));
 144
 145     if (_sg_mc_termination && this->checkNonTermination(next_state.get())) {
 146         MC_show_non_termination();
 147         return SIMGRID_MC_EXIT_NON_TERMINATION;
 148     }
 149
 150     if (_sg_mc_visited == 0
 151         || (visitedState_ = visitedStates_.addVisitedState(expandedStatesCount_, next_state.get(), true)) == nullptr) {
 152
 153       /* Get an enabled process and insert it in the interleave set of the next state */
 154       for (auto& p : mc_model_checker->process().simix_processes())
 155         if (simgrid::mc::process_is_enabled(p.copy.getBuffer())) {
 156           next_state->interleave(p.copy.getBuffer());
 157           if (reductionMode_ != simgrid::mc::ReductionMode::none)
 158             break;
 159         }
 160
 161       if (dot_output != nullptr)
 162         std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
 163           state->num, next_state->num, req_str.c_str());
 164
 165     } else if (dot_output != nullptr)
 166       std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
 167         state->num,
 168         visitedState_->other_num == -1 ? visitedState_->num : visitedState_->other_num, req_str.c_str());
 169
 170     stack_.push_back(std::move(next_state));
 171   }
 172
 173   XBT_INFO("No property violation found.");
 174   simgrid::mc::session->logState();
 175   return SIMGRID_MC_EXIT_SUCCESS;
 176 }
 177
 178 int SafetyChecker::backtrack()
 179 {
 180   if (stack_.size() > (std::size_t) _sg_mc_max_depth
 181       || visitedState_ != nullptr) {
 182     if (visitedState_ == nullptr)
 183       XBT_WARN("/!\\ Max depth reached ! /!\\ ");
 184     else
 185       XBT_DEBUG("State already visited (equal to state %d),"
 186         " exploration stopped on this path.",
 187         visitedState_->other_num == -1 ? visitedState_->num : visitedState_->other_num);
 188   } else
 189     XBT_DEBUG("There are no more processes to interleave. (depth %zi)",
 190       stack_.size() + 1);
 191
 192   stack_.pop_back();
 193
 194   visitedState_ = nullptr;
 195
 196   /* Check for deadlocks */
 197   if (mc_model_checker->checkDeadlock()) {
 198     MC_show_deadlock();
 199     return SIMGRID_MC_EXIT_DEADLOCK;
 200   }
 201
 202   /* Traverse the stack backwards until a state with a non empty interleave
 203      set is found, deleting all the states that have it empty in the way.
 204      For each deleted state, check if the request that has generated it
 205      (from it's predecesor state), depends on any other previous request
 206      executed before it. If it does then add it to the interleave set of the
 207      state that executed that previous request. */
 208
 209   while (!stack_.empty()) {
 210     std::unique_ptr<simgrid::mc::State> state = std::move(stack_.back());
 211     stack_.pop_back();
 212     if (reductionMode_ == simgrid::mc::ReductionMode::dpor) {
 213       smx_simcall_t req = &state->internal_req;
 214       if (req->call == SIMCALL_MUTEX_LOCK || req->call == SIMCALL_MUTEX_TRYLOCK)
 215         xbt_die("Mutex is currently not supported with DPOR, "
 216           "use --cfg=model-check/reduction:none");
 217       const smx_actor_t issuer = MC_smx_simcall_get_issuer(req);
 218       for (auto i = stack_.rbegin(); i != stack_.rend(); ++i) {
 219         simgrid::mc::State* prev_state = i->get();
 220         if (simgrid::mc::request_depend(req, &prev_state->internal_req)) {
 221           if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
 222             XBT_DEBUG("Dependent Transitions:");
 223             int value = prev_state->transition.argument;
 224             smx_simcall_t prev_req = &prev_state->executed_req;
 225             XBT_DEBUG("%s (state=%d)",
 226               simgrid::mc::request_to_string(
 227                 prev_req, value, simgrid::mc::RequestType::internal).c_str(),
 228               prev_state->num);
 229             value = state->transition.argument;
 230             prev_req = &state->executed_req;
 231             XBT_DEBUG("%s (state=%d)",
 232               simgrid::mc::request_to_string(
 233                 prev_req, value, simgrid::mc::RequestType::executed).c_str(),
 234               state->num);
 235           }
 236
 237           if (!prev_state->processStates[issuer->pid].isDone())
 238             prev_state->interleave(issuer);
 239           else
 240             XBT_DEBUG("Process %p is in done set", req->issuer);
 241
 242           break;
 243
 244         } else if (req->issuer == prev_state->internal_req.issuer) {
 245
 246           XBT_DEBUG("Simcall %d and %d with same issuer", req->call, prev_state->internal_req.call);
 247           break;
 248
 249         } else {
 250
 251           const smx_actor_t previous_issuer = MC_smx_simcall_get_issuer(&prev_state->internal_req);
 252           XBT_DEBUG("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant",
 253                     req->call, issuer->pid, state->num,
 254                     prev_state->internal_req.call,
 255                     previous_issuer->pid,
 256                     prev_state->num);
 257
 258         }
 259       }
 260     }
 261
 262     if (state->interleaveSize()
 263         && stack_.size() < (std::size_t) _sg_mc_max_depth) {
 264       /* We found a back-tracking point, let's loop */
 265       XBT_DEBUG("Back-tracking to state %d at depth %zi",
 266         state->num, stack_.size() + 1);
 267       stack_.push_back(std::move(state));
 268       this->restoreState();
 269       XBT_DEBUG("Back-tracking to state %d at depth %zi done",
 270         stack_.back()->num, stack_.size());
 271       break;
 272     } else {
 273       XBT_DEBUG("Delete state %d at depth %zi",
 274         state->num, stack_.size() + 1);
 275     }
 276   }
 277   return SIMGRID_MC_EXIT_SUCCESS;
 278 }
 279
 280 void SafetyChecker::restoreState()
 281 {
 282   /* Intermediate backtracking */
 283   {
 284     simgrid::mc::State* state = stack_.back().get();
 285     if (state->system_state) {
 286       simgrid::mc::restore_snapshot(state->system_state);
 287       return;
 288     }
 289   }
 290
 291   /* Restore the initial state */
 292   simgrid::mc::session->restoreInitialState();
 293
 294   /* Traverse the stack from the state at position start and re-execute the transitions */
 295   for (std::unique_ptr<simgrid::mc::State> const& state : stack_) {
 296     if (state == stack_.back())
 297       break;
 298     session->execute(state->transition);
 299     /* Update statistics */
 300     mc_model_checker->visited_states++;
 301     mc_model_checker->executed_transitions++;
 302   }
 303 }
 304
 305 SafetyChecker::SafetyChecker(Session& session) : Checker(session)
 306 {
 307   reductionMode_ = simgrid::mc::reduction_mode;
 308   if (_sg_mc_termination)
 309     reductionMode_ = simgrid::mc::ReductionMode::none;
 310   else if (reductionMode_ == simgrid::mc::ReductionMode::unset)
 311     reductionMode_ = simgrid::mc::ReductionMode::dpor;
 312
 313   if (_sg_mc_termination)
 314     XBT_INFO("Check non progressive cycles");
 315   else
 316     XBT_INFO("Check a safety property");
 317   simgrid::mc::session->initialize();
 318
 319   XBT_DEBUG("Starting the safety algorithm");
 320
 321   std::unique_ptr<simgrid::mc::State> initial_state =
 322     std::unique_ptr<simgrid::mc::State>(MC_state_new(++expandedStatesCount_));
 323
 324   XBT_DEBUG("**************************************************");
 325   XBT_DEBUG("Initial state");
 326
 327   /* Get an enabled process and insert it in the interleave set of the initial state */
 328   for (auto& p : mc_model_checker->process().simix_processes())
 329     if (simgrid::mc::process_is_enabled(p.copy.getBuffer())) {
 330       initial_state->interleave(p.copy.getBuffer());
 331       if (reductionMode_ != simgrid::mc::ReductionMode::none)
 332         break;
 333     }
 334
 335   stack_.push_back(std::move(initial_state));
 336 }
 337
 338 SafetyChecker::~SafetyChecker()
 339 {
 340 }
 341
 342 Checker* createSafetyChecker(Session& session)
 343 {
 344   return new SafetyChecker(session);
 345 }
 346
 347 }
 348 }