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