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_stats->visited_states);
  95   XBT_INFO("Executed transitions = %lu", mc_stats->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_stats->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_stats->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   initial_global_state = nullptr;
 178   return SIMGRID_MC_EXIT_SUCCESS;
 179 }
 180
 181 int SafetyChecker::backtrack()
 182 {
 183   if (stack_.size() > (std::size_t) _sg_mc_max_depth
 184       || visitedState_ != nullptr) {
 185     if (visitedState_ == nullptr)
 186       XBT_WARN("/!\\ Max depth reached ! /!\\ ");
 187     else
 188       XBT_DEBUG("State already visited (equal to state %d),"
 189         " exploration stopped on this path.",
 190         visitedState_->other_num == -1 ? visitedState_->num : visitedState_->other_num);
 191   } else
 192     XBT_DEBUG("There are no more processes to interleave. (depth %zi)",
 193       stack_.size() + 1);
 194
 195   stack_.pop_back();
 196
 197   visitedState_ = nullptr;
 198
 199   /* Check for deadlocks */
 200   if (mc_model_checker->checkDeadlock()) {
 201     MC_show_deadlock();
 202     return SIMGRID_MC_EXIT_DEADLOCK;
 203   }
 204
 205   /* Traverse the stack backwards until a state with a non empty interleave
 206      set is found, deleting all the states that have it empty in the way.
 207      For each deleted state, check if the request that has generated it
 208      (from it's predecesor state), depends on any other previous request
 209      executed before it. If it does then add it to the interleave set of the
 210      state that executed that previous request. */
 211
 212   while (!stack_.empty()) {
 213     std::unique_ptr<simgrid::mc::State> state = std::move(stack_.back());
 214     stack_.pop_back();
 215     if (reductionMode_ == simgrid::mc::ReductionMode::dpor) {
 216       smx_simcall_t req = &state->internal_req;
 217       if (req->call == SIMCALL_MUTEX_LOCK || req->call == SIMCALL_MUTEX_TRYLOCK)
 218         xbt_die("Mutex is currently not supported with DPOR, "
 219           "use --cfg=model-check/reduction:none");
 220       const smx_process_t issuer = MC_smx_simcall_get_issuer(req);
 221       for (auto i = stack_.rbegin(); i != stack_.rend(); ++i) {
 222         simgrid::mc::State* prev_state = i->get();
 223         if (reductionMode_ != simgrid::mc::ReductionMode::none
 224             && simgrid::mc::request_depend(req, &prev_state->internal_req)) {
 225           if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
 226             XBT_DEBUG("Dependent Transitions:");
 227             int value = prev_state->transition.argument;
 228             smx_simcall_t prev_req = &prev_state->executed_req;
 229             XBT_DEBUG("%s (state=%d)",
 230               simgrid::mc::request_to_string(
 231                 prev_req, value, simgrid::mc::RequestType::internal).c_str(),
 232               prev_state->num);
 233             value = state->transition.argument;
 234             prev_req = &state->executed_req;
 235             XBT_DEBUG("%s (state=%d)",
 236               simgrid::mc::request_to_string(
 237                 prev_req, value, simgrid::mc::RequestType::executed).c_str(),
 238               state->num);
 239           }
 240
 241           if (!prev_state->processStates[issuer->pid].isDone())
 242             prev_state->interleave(issuer);
 243           else
 244             XBT_DEBUG("Process %p is in done set", req->issuer);
 245
 246           break;
 247
 248         } else if (req->issuer == prev_state->internal_req.issuer) {
 249
 250           XBT_DEBUG("Simcall %d and %d with same issuer", req->call, prev_state->internal_req.call);
 251           break;
 252
 253         } else {
 254
 255           const smx_process_t previous_issuer = MC_smx_simcall_get_issuer(&prev_state->internal_req);
 256           XBT_DEBUG("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant",
 257                     req->call, issuer->pid, state->num,
 258                     prev_state->internal_req.call,
 259                     previous_issuer->pid,
 260                     prev_state->num);
 261
 262         }
 263       }
 264     }
 265
 266     if (state->interleaveSize()
 267         && stack_.size() < (std::size_t) _sg_mc_max_depth) {
 268       /* We found a back-tracking point, let's loop */
 269       XBT_DEBUG("Back-tracking to state %d at depth %zi",
 270         state->num, stack_.size() + 1);
 271       stack_.push_back(std::move(state));
 272       simgrid::mc::replay(stack_);
 273       XBT_DEBUG("Back-tracking to state %d at depth %zi done",
 274         stack_.back()->num, stack_.size());
 275       break;
 276     } else {
 277       XBT_DEBUG("Delete state %d at depth %zi",
 278         state->num, stack_.size() + 1);
 279     }
 280   }
 281   return SIMGRID_MC_EXIT_SUCCESS;
 282 }
 283
 284 void SafetyChecker::init()
 285 {
 286   reductionMode_ = simgrid::mc::reduction_mode;
 287   if( _sg_mc_termination)
 288     reductionMode_ = simgrid::mc::ReductionMode::none;
 289   else if (reductionMode_ == simgrid::mc::ReductionMode::unset)
 290     reductionMode_ = simgrid::mc::ReductionMode::dpor;
 291
 292   if (_sg_mc_termination)
 293     XBT_INFO("Check non progressive cycles");
 294   else
 295     XBT_INFO("Check a safety property");
 296   mc_model_checker->wait_for_requests();
 297
 298   XBT_DEBUG("Starting the safety algorithm");
 299
 300   std::unique_ptr<simgrid::mc::State> initial_state =
 301     std::unique_ptr<simgrid::mc::State>(MC_state_new(++expandedStatesCount_));
 302
 303   XBT_DEBUG("**************************************************");
 304   XBT_DEBUG("Initial state");
 305
 306   /* Get an enabled process and insert it in the interleave set of the initial state */
 307   for (auto& p : mc_model_checker->process().simix_processes())
 308     if (simgrid::mc::process_is_enabled(&p.copy)) {
 309       initial_state->interleave(&p.copy);
 310       if (reductionMode_ != simgrid::mc::ReductionMode::none)
 311         break;
 312     }
 313
 314   stack_.push_back(std::move(initial_state));
 315
 316   /* Save the initial state */
 317   initial_global_state = std::unique_ptr<s_mc_global_t>(new s_mc_global_t());
 318   initial_global_state->snapshot = simgrid::mc::take_snapshot(0);
 319 }
 320
 321 SafetyChecker::SafetyChecker(Session& session) : Checker(session)
 322 {
 323 }
 324
 325 SafetyChecker::~SafetyChecker()
 326 {
 327 }
 328
 329 Checker* createSafetyChecker(Session& session)
 330 {
 331   return new SafetyChecker(session);
 332 }
 333
 334 }
 335 }