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     // The interleave set is empty or the maximum depth is reached,
 113     // let's back-track.
 114     smx_simcall_t req = nullptr;
 115     if (stack_.size() > (std::size_t) _sg_mc_max_depth
 116         || (req = MC_state_get_request(state)) == nullptr
 117         || visitedState_ != nullptr) {
 118       int res = this->backtrack();
 119       if (res)
 120         return res;
 121       else
 122         continue;
 123     }
 124
 125     // If there are processes to interleave and the maximum depth has not been
 126     // reached then perform one step of the exploration algorithm.
 127     XBT_DEBUG("Execute: %s",
 128       simgrid::mc::request_to_string(
 129         req, state->transition.argument, simgrid::mc::RequestType::simix).c_str());
 130
 131     std::string req_str;
 132     if (dot_output != nullptr)
 133       req_str = simgrid::mc::request_get_dot_output(req, state->transition.argument);
 134
 135     mc_model_checker->executed_transitions++;
 136
 137     /* Answer the request */
 138     this->getSession().execute(state->transition);
 139
 140     /* Create the new expanded state */
 141     std::unique_ptr<simgrid::mc::State> next_state =
 142         std::unique_ptr<simgrid::mc::State>(new simgrid::mc::State(++expandedStatesCount_));
 143
 144     if (_sg_mc_termination && this->checkNonTermination(next_state.get())) {
 145         MC_show_non_termination();
 146         return SIMGRID_MC_EXIT_NON_TERMINATION;
 147     }
 148
 149     if (_sg_mc_visited == 0
 150         || (visitedState_ = visitedStates_.addVisitedState(expandedStatesCount_, next_state.get(), true)) == nullptr) {
 151
 152       /* Get an enabled process and insert it in the interleave set of the next state */
 153       for (auto& p : mc_model_checker->process().actors())
 154         if (simgrid::mc::actor_is_enabled(p.copy.getBuffer())) {
 155           next_state->interleave(p.copy.getBuffer());
 156           if (reductionMode_ != simgrid::mc::ReductionMode::none)
 157             break;
 158         }
 159
 160       if (dot_output != nullptr)
 161         std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
 162           state->num, next_state->num, req_str.c_str());
 163
 164     } else if (dot_output != nullptr)
 165       std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
 166         state->num,
 167         visitedState_->other_num == -1 ? visitedState_->num : visitedState_->other_num, req_str.c_str());
 168
 169     stack_.push_back(std::move(next_state));
 170   }
 171
 172   XBT_INFO("No property violation found.");
 173   simgrid::mc::session->logState();
 174   return SIMGRID_MC_EXIT_SUCCESS;
 175 }
 176
 177 int SafetyChecker::backtrack()
 178 {
 179   if (stack_.size() > (std::size_t) _sg_mc_max_depth
 180       || visitedState_ != nullptr) {
 181     if (visitedState_ == nullptr)
 182       XBT_WARN("/!\\ Max depth reached ! /!\\ ");
 183     else
 184       XBT_DEBUG("State already visited (equal to state %d),"
 185         " exploration stopped on this path.",
 186         visitedState_->other_num == -1 ? visitedState_->num : visitedState_->other_num);
 187   } else
 188     XBT_DEBUG("There are no more processes to interleave. (depth %zi)",
 189       stack_.size() + 1);
 190
 191   stack_.pop_back();
 192
 193   visitedState_ = nullptr;
 194
 195   /* Check for deadlocks */
 196   if (mc_model_checker->checkDeadlock()) {
 197     MC_show_deadlock();
 198     return SIMGRID_MC_EXIT_DEADLOCK;
 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 predecesor 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 (!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, "
 215           "use --cfg=model-check/reduction:none");
 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 (!prev_state->processStates[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 independant",
 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",
 265         state->num, stack_.size() + 1);
 266       stack_.push_back(std::move(state));
 267       this->restoreState();
 268       XBT_DEBUG("Back-tracking to state %d at depth %zi done",
 269         stack_.back()->num, stack_.size());
 270       break;
 271     } else {
 272       XBT_DEBUG("Delete state %d at depth %zi",
 273         state->num, stack_.size() + 1);
 274     }
 275   }
 276   return SIMGRID_MC_EXIT_SUCCESS;
 277 }
 278
 279 void SafetyChecker::restoreState()
 280 {
 281   /* Intermediate backtracking */
 282   {
 283     simgrid::mc::State* state = stack_.back().get();
 284     if (state->system_state) {
 285       simgrid::mc::restore_snapshot(state->system_state);
 286       return;
 287     }
 288   }
 289
 290   /* Restore the initial state */
 291   simgrid::mc::session->restoreInitialState();
 292
 293   /* Traverse the stack from the state at position start and re-execute the transitions */
 294   for (std::unique_ptr<simgrid::mc::State> const& state : stack_) {
 295     if (state == stack_.back())
 296       break;
 297     session->execute(state->transition);
 298     /* Update statistics */
 299     mc_model_checker->visited_states++;
 300     mc_model_checker->executed_transitions++;
 301   }
 302 }
 303
 304 SafetyChecker::SafetyChecker(Session& session) : Checker(session)
 305 {
 306   reductionMode_ = simgrid::mc::reduction_mode;
 307   if (_sg_mc_termination)
 308     reductionMode_ = simgrid::mc::ReductionMode::none;
 309   else if (reductionMode_ == simgrid::mc::ReductionMode::unset)
 310     reductionMode_ = simgrid::mc::ReductionMode::dpor;
 311
 312   if (_sg_mc_termination)
 313     XBT_INFO("Check non progressive cycles");
 314   else
 315     XBT_INFO("Check a safety property");
 316   simgrid::mc::session->initialize();
 317
 318   XBT_DEBUG("Starting the safety algorithm");
 319
 320   std::unique_ptr<simgrid::mc::State> initial_state =
 321       std::unique_ptr<simgrid::mc::State>(new simgrid::mc::State(++expandedStatesCount_));
 322
 323   XBT_DEBUG("**************************************************");
 324   XBT_DEBUG("Initial state");
 325
 326   /* Get an enabled actor and insert it in the interleave set of the initial state */
 327   for (auto& actor : mc_model_checker->process().actors())
 328     if (simgrid::mc::actor_is_enabled(actor.copy.getBuffer())) {
 329       initial_state->interleave(actor.copy.getBuffer());
 330       if (reductionMode_ != simgrid::mc::ReductionMode::none)
 331         break;
 332     }
 333
 334   stack_.push_back(std::move(initial_state));
 335 }
 336
 337 SafetyChecker::~SafetyChecker()
 338 {
 339 }
 340
 341 Checker* createSafetyChecker(Session& session)
 342 {
 343   return new SafetyChecker(session);
 344 }
 345
 346 }
 347 }