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)) {
 158           next_state->interleave(&p.copy);
 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       simgrid::mc::restoreState(stack_);
 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::init()
 284 {
 285   reductionMode_ = simgrid::mc::reduction_mode;
 286   if( _sg_mc_termination)
 287     reductionMode_ = simgrid::mc::ReductionMode::none;
 288   else if (reductionMode_ == simgrid::mc::ReductionMode::unset)
 289     reductionMode_ = simgrid::mc::ReductionMode::dpor;
 290
 291   if (_sg_mc_termination)
 292     XBT_INFO("Check non progressive cycles");
 293   else
 294     XBT_INFO("Check a safety property");
 295   simgrid::mc::session->initialize();
 296
 297   XBT_DEBUG("Starting the safety algorithm");
 298
 299   std::unique_ptr<simgrid::mc::State> initial_state =
 300     std::unique_ptr<simgrid::mc::State>(MC_state_new(++expandedStatesCount_));
 301
 302   XBT_DEBUG("**************************************************");
 303   XBT_DEBUG("Initial state");
 304
 305   /* Get an enabled process and insert it in the interleave set of the initial state */
 306   for (auto& p : mc_model_checker->process().simix_processes())
 307     if (simgrid::mc::process_is_enabled(&p.copy)) {
 308       initial_state->interleave(&p.copy);
 309       if (reductionMode_ != simgrid::mc::ReductionMode::none)
 310         break;
 311     }
 312
 313   stack_.push_back(std::move(initial_state));
 314 }
 315
 316 SafetyChecker::SafetyChecker(Session& session) : Checker(session)
 317 {
 318 }
 319
 320 SafetyChecker::~SafetyChecker()
 321 {
 322 }
 323
 324 Checker* createSafetyChecker(Session& session)
 325 {
 326   return new SafetyChecker(session);
 327 }
 328
 329 }
 330 }