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