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
  29 #include "src/xbt/mmalloc/mmprivate.h"
  30
  31 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_safety, mc,
  32                                 "Logging specific to MC safety verification ");
  33 namespace simgrid {
  34 namespace mc {
  35
  36 static void MC_show_non_termination(void)
  37 {
  38   XBT_INFO("******************************************");
  39   XBT_INFO("*** NON-PROGRESSIVE CYCLE DETECTED ***");
  40   XBT_INFO("******************************************");
  41   XBT_INFO("Counter-example execution trace:");
  42   for (auto& s : mc_model_checker->getChecker()->getTextualTrace())
  43     XBT_INFO("%s", s.c_str());
  44   MC_print_statistics(mc_stats);
  45 }
  46
  47 static int snapshot_compare(simgrid::mc::State* state1, simgrid::mc::State* state2)
  48 {
  49   simgrid::mc::Snapshot* s1 = state1->system_state.get();
  50   simgrid::mc::Snapshot* s2 = state2->system_state.get();
  51   int num1 = state1->num;
  52   int num2 = state2->num;
  53   return snapshot_compare(num1, s1, num2, s2);
  54 }
  55
  56 bool SafetyChecker::checkNonTermination(simgrid::mc::State* current_state)
  57 {
  58   for (auto i = stack_.rbegin(); i != stack_.rend(); ++i)
  59     if (snapshot_compare(i->get(), current_state) == 0){
  60       XBT_INFO("Non-progressive cycle : state %d -> state %d",
  61         (*i)->num, current_state->num);
  62       return true;
  63     }
  64   return false;
  65 }
  66
  67 RecordTrace SafetyChecker::getRecordTrace() // override
  68 {
  69   RecordTrace res;
  70   for (auto const& state : stack_) {
  71     int value = 0;
  72     smx_simcall_t saved_req = MC_state_get_executed_request(state.get(), &value);
  73     const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req);
  74     const int pid = issuer->pid;
  75     res.push_back(RecordTraceElement(pid, value));
  76   }
  77   return res;
  78 }
  79
  80 std::vector<std::string> SafetyChecker::getTextualTrace() // override
  81 {
  82   std::vector<std::string> trace;
  83   for (auto const& state : stack_) {
  84     int value;
  85     smx_simcall_t req = MC_state_get_executed_request(state.get(), &value);
  86     if (req)
  87       trace.push_back(simgrid::mc::request_to_string(
  88         req, value, simgrid::mc::RequestType::executed));
  89   }
  90   return trace;
  91 }
  92
  93 int SafetyChecker::run()
  94 {
  95   this->init();
  96
  97   int value;
  98
  99   while (!stack_.empty()) {
 100
 101     /* Get current state */
 102     simgrid::mc::State* state = stack_.back().get();
 103
 104     XBT_DEBUG("**************************************************");
 105     XBT_DEBUG(
 106       "Exploration depth=%zi (state=%p, num %d)(%zu interleave)",
 107       stack_.size(), state, state->num,
 108       state->interleaveSize());
 109
 110     mc_stats->visited_states++;
 111
 112     // The interleave set is empty or the maximum depth is reached,
 113     // let's back-track.
 114     smx_simcall_t req = nullptr;
 115     if (stack_.size() > (std::size_t) _sg_mc_max_depth
 116         || (req = MC_state_get_request(state, &value)) == nullptr
 117         || visitedState_ != nullptr) {
 118       int res = this->backtrack();
 119       if (res)
 120         return res;
 121       else
 122         continue;
 123     }
 124
 125     // If there are processes to interleave and the maximum depth has not been
 126     // reached then perform one step of the exploration algorithm.
 127     XBT_DEBUG("Execute: %s",
 128       simgrid::mc::request_to_string(
 129         req, value, simgrid::mc::RequestType::simix).c_str());
 130
 131     std::string req_str;
 132     if (dot_output != nullptr)
 133       req_str = simgrid::mc::request_get_dot_output(req, value);
 134
 135     MC_state_set_executed_request(state, req, value);
 136     mc_stats->executed_transitions++;
 137
 138     // TODO, bundle both operations in a single message
 139     //   MC_execute_transition(req, value)
 140
 141     /* Answer the request */
 142     simgrid::mc::handle_simcall(req, value);
 143     mc_model_checker->wait_for_requests();
 144
 145     /* Create the new expanded state */
 146     std::unique_ptr<simgrid::mc::State> next_state =
 147       std::unique_ptr<simgrid::mc::State>(MC_state_new());
 148
 149     if (_sg_mc_termination && this->checkNonTermination(next_state.get())) {
 150         MC_show_non_termination();
 151         return SIMGRID_MC_EXIT_NON_TERMINATION;
 152     }
 153
 154     if (_sg_mc_visited == 0
 155         || (visitedState_ = visitedStates_.addVisitedState(next_state.get(), true)) == nullptr) {
 156
 157       /* Get an enabled process and insert it in the interleave set of the next state */
 158       for (auto& p : mc_model_checker->process().simix_processes())
 159         if (simgrid::mc::process_is_enabled(&p.copy)) {
 160           MC_state_interleave_process(next_state.get(), &p.copy);
 161           if (reductionMode_ != simgrid::mc::ReductionMode::none)
 162             break;
 163         }
 164
 165       if (dot_output != nullptr)
 166         std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
 167           state->num, next_state->num, req_str.c_str());
 168
 169     } else if (dot_output != nullptr)
 170       std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
 171         state->num,
 172         visitedState_->other_num == -1 ? visitedState_->num : visitedState_->other_num, req_str.c_str());
 173
 174     stack_.push_back(std::move(next_state));
 175   }
 176
 177   XBT_INFO("No property violation found.");
 178   MC_print_statistics(mc_stats);
 179   initial_global_state = nullptr;
 180   return SIMGRID_MC_EXIT_SUCCESS;
 181 }
 182
 183 int SafetyChecker::backtrack()
 184 {
 185   if (stack_.size() > (std::size_t) _sg_mc_max_depth
 186       || visitedState_ != nullptr) {
 187     if (visitedState_ == nullptr)
 188       XBT_WARN("/!\\ Max depth reached ! /!\\ ");
 189     else
 190       XBT_DEBUG("State already visited (equal to state %d),"
 191         " exploration stopped on this path.",
 192         visitedState_->other_num == -1 ? visitedState_->num : visitedState_->other_num);
 193   } else
 194     XBT_DEBUG("There are no more processes to interleave. (depth %zi)",
 195       stack_.size() + 1);
 196
 197   stack_.pop_back();
 198
 199   visitedState_ = nullptr;
 200
 201   /* Check for deadlocks */
 202   if (mc_model_checker->checkDeadlock()) {
 203     MC_show_deadlock();
 204     return SIMGRID_MC_EXIT_DEADLOCK;
 205   }
 206
 207   /* Traverse the stack backwards until a state with a non empty interleave
 208      set is found, deleting all the states that have it empty in the way.
 209      For each deleted state, check if the request that has generated it
 210      (from it's predecesor state), depends on any other previous request
 211      executed before it. If it does then add it to the interleave set of the
 212      state that executed that previous request. */
 213
 214   while (!stack_.empty()) {
 215     std::unique_ptr<simgrid::mc::State> state = std::move(stack_.back());
 216     stack_.pop_back();
 217     if (reductionMode_ == simgrid::mc::ReductionMode::dpor) {
 218       smx_simcall_t req = MC_state_get_internal_request(state.get());
 219       if (req->call == SIMCALL_MUTEX_LOCK || req->call == SIMCALL_MUTEX_TRYLOCK)
 220         xbt_die("Mutex is currently not supported with DPOR, "
 221           "use --cfg=model-check/reduction:none");
 222       const smx_process_t issuer = MC_smx_simcall_get_issuer(req);
 223       for (auto i = stack_.rbegin(); i != stack_.rend(); ++i) {
 224         simgrid::mc::State* prev_state = i->get();
 225         if (reductionMode_ != simgrid::mc::ReductionMode::none
 226             && simgrid::mc::request_depend(req, MC_state_get_internal_request(prev_state))) {
 227           if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
 228             XBT_DEBUG("Dependent Transitions:");
 229             int value;
 230             smx_simcall_t prev_req = MC_state_get_executed_request(prev_state, &value);
 231             XBT_DEBUG("%s (state=%d)",
 232               simgrid::mc::request_to_string(
 233                 prev_req, value, simgrid::mc::RequestType::internal).c_str(),
 234               prev_state->num);
 235             prev_req = MC_state_get_executed_request(state.get(), &value);
 236             XBT_DEBUG("%s (state=%d)",
 237               simgrid::mc::request_to_string(
 238                 prev_req, value, simgrid::mc::RequestType::executed).c_str(),
 239               state->num);
 240           }
 241
 242           if (!prev_state->processStates[issuer->pid].done())
 243             MC_state_interleave_process(prev_state, issuer);
 244           else
 245             XBT_DEBUG("Process %p is in done set", req->issuer);
 246
 247           break;
 248
 249         } else if (req->issuer == MC_state_get_internal_request(prev_state)->issuer) {
 250
 251           XBT_DEBUG("Simcall %d and %d with same issuer", req->call, MC_state_get_internal_request(prev_state)->call);
 252           break;
 253
 254         } else {
 255
 256           const smx_process_t previous_issuer = MC_smx_simcall_get_issuer(MC_state_get_internal_request(prev_state));
 257           XBT_DEBUG("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant",
 258                     req->call, issuer->pid, state->num,
 259                     MC_state_get_internal_request(prev_state)->call,
 260                     previous_issuer->pid,
 261                     prev_state->num);
 262
 263         }
 264       }
 265     }
 266
 267     if (state->interleaveSize()
 268         && stack_.size() < (std::size_t) _sg_mc_max_depth) {
 269       /* We found a back-tracking point, let's loop */
 270       XBT_DEBUG("Back-tracking to state %d at depth %zi",
 271         state->num, stack_.size() + 1);
 272       stack_.push_back(std::move(state));
 273       simgrid::mc::replay(stack_);
 274       XBT_DEBUG("Back-tracking to state %d at depth %zi done",
 275         stack_.back()->num, stack_.size());
 276       break;
 277     } else {
 278       XBT_DEBUG("Delete state %d at depth %zi",
 279         state->num, stack_.size() + 1);
 280     }
 281   }
 282   return SIMGRID_MC_EXIT_SUCCESS;
 283 }
 284
 285 void SafetyChecker::init()
 286 {
 287   reductionMode_ = simgrid::mc::reduction_mode;
 288   if( _sg_mc_termination)
 289     reductionMode_ = simgrid::mc::ReductionMode::none;
 290   else if (reductionMode_ == simgrid::mc::ReductionMode::unset)
 291     reductionMode_ = simgrid::mc::ReductionMode::dpor;
 292
 293   if (_sg_mc_termination)
 294     XBT_INFO("Check non progressive cycles");
 295   else
 296     XBT_INFO("Check a safety property");
 297   mc_model_checker->wait_for_requests();
 298
 299   XBT_DEBUG("Starting the safety algorithm");
 300
 301   std::unique_ptr<simgrid::mc::State> initial_state =
 302     std::unique_ptr<simgrid::mc::State>(MC_state_new());
 303
 304   XBT_DEBUG("**************************************************");
 305   XBT_DEBUG("Initial state");
 306
 307   /* Wait for requests (schedules processes) */
 308   mc_model_checker->wait_for_requests();
 309
 310   /* Get an enabled process and insert it in the interleave set of the initial state */
 311   for (auto& p : mc_model_checker->process().simix_processes())
 312     if (simgrid::mc::process_is_enabled(&p.copy)) {
 313       MC_state_interleave_process(initial_state.get(), &p.copy);
 314       if (reductionMode_ != simgrid::mc::ReductionMode::none)
 315         break;
 316     }
 317
 318   stack_.push_back(std::move(initial_state));
 319
 320   /* Save the initial state */
 321   initial_global_state = std::unique_ptr<s_mc_global_t>(new s_mc_global_t());
 322   initial_global_state->snapshot = simgrid::mc::take_snapshot(0);
 323 }
 324
 325 SafetyChecker::SafetyChecker(Session& session) : Checker(session)
 326 {
 327 }
 328
 329 SafetyChecker::~SafetyChecker()
 330 {
 331 }
 332
 333 Checker* createSafetyChecker(Session& session)
 334 {
 335   return new SafetyChecker(session);
 336 }
 337
 338 }
 339 }