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
  30 #include "src/xbt/mmalloc/mmprivate.h"
  31
  32 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_safety, mc,
  33                                 "Logging specific to MC safety verification ");
  34 namespace simgrid {
  35 namespace mc {
  36
  37 static void MC_show_non_termination(void)
  38 {
  39   XBT_INFO("******************************************");
  40   XBT_INFO("*** NON-PROGRESSIVE CYCLE DETECTED ***");
  41   XBT_INFO("******************************************");
  42   XBT_INFO("Counter-example execution trace:");
  43   for (auto& s : mc_model_checker->getChecker()->getTextualTrace())
  44     XBT_INFO("%s", s.c_str());
  45   MC_print_statistics(mc_stats);
  46 }
  47
  48 static int snapshot_compare(simgrid::mc::State* state1, simgrid::mc::State* state2)
  49 {
  50   simgrid::mc::Snapshot* s1 = state1->system_state.get();
  51   simgrid::mc::Snapshot* s2 = state2->system_state.get();
  52   int num1 = state1->num;
  53   int num2 = state2->num;
  54   return snapshot_compare(num1, s1, num2, s2);
  55 }
  56
  57 bool SafetyChecker::checkNonTermination(simgrid::mc::State* current_state)
  58 {
  59   for (auto i = stack_.rbegin(); i != stack_.rend(); ++i)
  60     if (snapshot_compare(i->get(), current_state) == 0){
  61       XBT_INFO("Non-progressive cycle : state %d -> state %d",
  62         (*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->getRecordElement());
  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 int SafetyChecker::run()
  90 {
  91   this->init();
  92
  93   while (!stack_.empty()) {
  94
  95     /* Get current state */
  96     simgrid::mc::State* state = stack_.back().get();
  97
  98     XBT_DEBUG("**************************************************");
  99     XBT_DEBUG(
 100       "Exploration depth=%zi (state=%p, num %d)(%zu interleave)",
 101       stack_.size(), state, state->num,
 102       state->interleaveSize());
 103
 104     mc_stats->visited_states++;
 105
 106     // The interleave set is empty or the maximum depth is reached,
 107     // let's back-track.
 108     smx_simcall_t req = nullptr;
 109     if (stack_.size() > (std::size_t) _sg_mc_max_depth
 110         || (req = MC_state_get_request(state)) == nullptr
 111         || visitedState_ != nullptr) {
 112       int res = this->backtrack();
 113       if (res)
 114         return res;
 115       else
 116         continue;
 117     }
 118
 119     int req_num = state->transition.argument;
 120
 121     // If there are processes to interleave and the maximum depth has not been
 122     // reached then perform one step of the exploration algorithm.
 123     XBT_DEBUG("Execute: %s",
 124       simgrid::mc::request_to_string(
 125         req, req_num, simgrid::mc::RequestType::simix).c_str());
 126
 127     std::string req_str;
 128     if (dot_output != nullptr)
 129       req_str = simgrid::mc::request_get_dot_output(req, req_num);
 130
 131     mc_stats->executed_transitions++;
 132
 133     // TODO, bundle both operations in a single message
 134     //   MC_execute_transition(req, req_num)
 135
 136     /* Answer the request */
 137     mc_model_checker->handle_simcall(state->transition);
 138     mc_model_checker->wait_for_requests();
 139
 140     /* Create the new expanded state */
 141     std::unique_ptr<simgrid::mc::State> next_state =
 142       std::unique_ptr<simgrid::mc::State>(MC_state_new());
 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(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().simix_processes())
 154         if (simgrid::mc::process_is_enabled(&p.copy)) {
 155           next_state->interleave(&p.copy);
 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   MC_print_statistics(mc_stats);
 174   initial_global_state = nullptr;
 175   return SIMGRID_MC_EXIT_SUCCESS;
 176 }
 177
 178 int SafetyChecker::backtrack()
 179 {
 180   if (stack_.size() > (std::size_t) _sg_mc_max_depth
 181       || visitedState_ != nullptr) {
 182     if (visitedState_ == nullptr)
 183       XBT_WARN("/!\\ Max depth reached ! /!\\ ");
 184     else
 185       XBT_DEBUG("State already visited (equal to state %d),"
 186         " exploration stopped on this path.",
 187         visitedState_->other_num == -1 ? visitedState_->num : visitedState_->other_num);
 188   } else
 189     XBT_DEBUG("There are no more processes to interleave. (depth %zi)",
 190       stack_.size() + 1);
 191
 192   stack_.pop_back();
 193
 194   visitedState_ = nullptr;
 195
 196   /* Check for deadlocks */
 197   if (mc_model_checker->checkDeadlock()) {
 198     MC_show_deadlock();
 199     return SIMGRID_MC_EXIT_DEADLOCK;
 200   }
 201
 202   /* Traverse the stack backwards until a state with a non empty interleave
 203      set is found, deleting all the states that have it empty in the way.
 204      For each deleted state, check if the request that has generated it
 205      (from it's predecesor state), depends on any other previous request
 206      executed before it. If it does then add it to the interleave set of the
 207      state that executed that previous request. */
 208
 209   while (!stack_.empty()) {
 210     std::unique_ptr<simgrid::mc::State> state = std::move(stack_.back());
 211     stack_.pop_back();
 212     if (reductionMode_ == simgrid::mc::ReductionMode::dpor) {
 213       smx_simcall_t req = &state->internal_req;
 214       if (req->call == SIMCALL_MUTEX_LOCK || req->call == SIMCALL_MUTEX_TRYLOCK)
 215         xbt_die("Mutex is currently not supported with DPOR, "
 216           "use --cfg=model-check/reduction:none");
 217       const smx_process_t issuer = MC_smx_simcall_get_issuer(req);
 218       for (auto i = stack_.rbegin(); i != stack_.rend(); ++i) {
 219         simgrid::mc::State* prev_state = i->get();
 220         if (reductionMode_ != simgrid::mc::ReductionMode::none
 221             && simgrid::mc::request_depend(req, &prev_state->internal_req)) {
 222           if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
 223             XBT_DEBUG("Dependent Transitions:");
 224             int value = prev_state->transition.argument;
 225             smx_simcall_t prev_req = &prev_state->executed_req;
 226             XBT_DEBUG("%s (state=%d)",
 227               simgrid::mc::request_to_string(
 228                 prev_req, value, simgrid::mc::RequestType::internal).c_str(),
 229               prev_state->num);
 230             value = state->transition.argument;
 231             prev_req = &state->executed_req;
 232             XBT_DEBUG("%s (state=%d)",
 233               simgrid::mc::request_to_string(
 234                 prev_req, value, simgrid::mc::RequestType::executed).c_str(),
 235               state->num);
 236           }
 237
 238           if (!prev_state->processStates[issuer->pid].isDone())
 239             prev_state->interleave(issuer);
 240           else
 241             XBT_DEBUG("Process %p is in done set", req->issuer);
 242
 243           break;
 244
 245         } else if (req->issuer == prev_state->internal_req.issuer) {
 246
 247           XBT_DEBUG("Simcall %d and %d with same issuer", req->call, prev_state->internal_req.call);
 248           break;
 249
 250         } else {
 251
 252           const smx_process_t previous_issuer = MC_smx_simcall_get_issuer(&prev_state->internal_req);
 253           XBT_DEBUG("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant",
 254                     req->call, issuer->pid, state->num,
 255                     prev_state->internal_req.call,
 256                     previous_issuer->pid,
 257                     prev_state->num);
 258
 259         }
 260       }
 261     }
 262
 263     if (state->interleaveSize()
 264         && stack_.size() < (std::size_t) _sg_mc_max_depth) {
 265       /* We found a back-tracking point, let's loop */
 266       XBT_DEBUG("Back-tracking to state %d at depth %zi",
 267         state->num, stack_.size() + 1);
 268       stack_.push_back(std::move(state));
 269       simgrid::mc::replay(stack_);
 270       XBT_DEBUG("Back-tracking to state %d at depth %zi done",
 271         stack_.back()->num, stack_.size());
 272       break;
 273     } else {
 274       XBT_DEBUG("Delete state %d at depth %zi",
 275         state->num, stack_.size() + 1);
 276     }
 277   }
 278   return SIMGRID_MC_EXIT_SUCCESS;
 279 }
 280
 281 void SafetyChecker::init()
 282 {
 283   reductionMode_ = simgrid::mc::reduction_mode;
 284   if( _sg_mc_termination)
 285     reductionMode_ = simgrid::mc::ReductionMode::none;
 286   else if (reductionMode_ == simgrid::mc::ReductionMode::unset)
 287     reductionMode_ = simgrid::mc::ReductionMode::dpor;
 288
 289   if (_sg_mc_termination)
 290     XBT_INFO("Check non progressive cycles");
 291   else
 292     XBT_INFO("Check a safety property");
 293   mc_model_checker->wait_for_requests();
 294
 295   XBT_DEBUG("Starting the safety algorithm");
 296
 297   std::unique_ptr<simgrid::mc::State> initial_state =
 298     std::unique_ptr<simgrid::mc::State>(MC_state_new());
 299
 300   XBT_DEBUG("**************************************************");
 301   XBT_DEBUG("Initial state");
 302
 303   /* Wait for requests (schedules processes) */
 304   mc_model_checker->wait_for_requests();
 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 }