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 <list>
  11
  12 #include <xbt/log.h>
  13 #include <xbt/sysdep.h>
  14
  15 #include "src/mc/mc_state.h"
  16 #include "src/mc/mc_request.h"
  17 #include "src/mc/mc_safety.h"
  18 #include "src/mc/mc_private.h"
  19 #include "src/mc/mc_record.h"
  20 #include "src/mc/mc_smx.h"
  21 #include "src/mc/Client.hpp"
  22 #include "src/mc/mc_exit.h"
  23 #include "src/mc/Checker.hpp"
  24 #include "src/mc/SafetyChecker.hpp"
  25 #include "src/mc/VisitedState.hpp"
  26
  27 #include "src/xbt/mmalloc/mmprivate.h"
  28
  29 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_safety, mc,
  30                                 "Logging specific to MC safety verification ");
  31 namespace simgrid {
  32 namespace mc {
  33
  34 static void MC_show_non_termination(void)
  35 {
  36   XBT_INFO("******************************************");
  37   XBT_INFO("*** NON-PROGRESSIVE CYCLE DETECTED ***");
  38   XBT_INFO("******************************************");
  39   XBT_INFO("Counter-example execution trace:");
  40   for (auto& s : mc_model_checker->getChecker()->getTextualTrace())
  41     XBT_INFO("%s", s.c_str());
  42   MC_print_statistics(mc_stats);
  43 }
  44
  45 static int snapshot_compare(simgrid::mc::State* state1, simgrid::mc::State* state2)
  46 {
  47   simgrid::mc::Snapshot* s1 = state1->system_state.get();
  48   simgrid::mc::Snapshot* s2 = state2->system_state.get();
  49   int num1 = state1->num;
  50   int num2 = state2->num;
  51   return snapshot_compare(num1, s1, num2, s2);
  52 }
  53
  54 bool SafetyChecker::checkNonTermination(simgrid::mc::State* current_state)
  55 {
  56   for (auto i = stack_.rbegin(); i != stack_.rend(); ++i)
  57     if (snapshot_compare(i->get(), current_state) == 0){
  58       XBT_INFO("Non-progressive cycle : state %d -> state %d",
  59         (*i)->num, current_state->num);
  60       return true;
  61     }
  62   return false;
  63 }
  64
  65 RecordTrace SafetyChecker::getRecordTrace() // override
  66 {
  67   RecordTrace res;
  68   for (auto const& state : stack_) {
  69     int value = 0;
  70     smx_simcall_t saved_req = MC_state_get_executed_request(state.get(), &value);
  71     const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req);
  72     const int pid = issuer->pid;
  73     res.push_back(RecordTraceElement(pid, value));
  74   }
  75   return res;
  76 }
  77
  78 std::vector<std::string> SafetyChecker::getTextualTrace() // override
  79 {
  80   std::vector<std::string> trace;
  81   for (auto const& state : stack_) {
  82     int value;
  83     smx_simcall_t req = MC_state_get_executed_request(state.get(), &value);
  84     if (req) {
  85       char* req_str = simgrid::mc::request_to_string(
  86         req, value, simgrid::mc::RequestType::executed);
  87       trace.push_back(req_str);
  88       xbt_free(req_str);
  89     }
  90   }
  91   return trace;
  92 }
  93
  94 int SafetyChecker::run()
  95 {
  96   this->init();
  97
  98   int value;
  99
 100   while (!stack_.empty()) {
 101
 102     /* Get current state */
 103     simgrid::mc::State* state = stack_.back().get();
 104
 105     XBT_DEBUG("**************************************************");
 106     XBT_DEBUG(
 107       "Exploration depth=%zi (state=%p, num %d)(%u interleave)",
 108       stack_.size(), state, state->num,
 109       MC_state_interleave_size(state));
 110
 111     mc_stats->visited_states++;
 112
 113     // The interleave set is empty or the maximum depth is reached,
 114     // let's back-track.
 115     smx_simcall_t req = nullptr;
 116     if (stack_.size() > (std::size_t) _sg_mc_max_depth
 117         || (req = MC_state_get_request(state, &value)) == nullptr
 118         || visitedState_ != nullptr) {
 119       int res = this->backtrack();
 120       if (res)
 121         return res;
 122       else
 123         continue;
 124     }
 125
 126     // If there are processes to interleave and the maximum depth has not been
 127     // reached then perform one step of the exploration algorithm.
 128     char* req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::simix);
 129     XBT_DEBUG("Execute: %s", req_str);
 130     xbt_free(req_str);
 131
 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", state->num, next_state->num, req_str);
 167
 168     } else if (dot_output != nullptr)
 169       std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visitedState_->other_num == -1 ? visitedState_->num : visitedState_->other_num, req_str);
 170
 171     stack_.push_back(std::move(next_state));
 172
 173     if (dot_output != nullptr)
 174       xbt_free(req_str);
 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             char* req_str = simgrid::mc::request_to_string(prev_req, value, simgrid::mc::RequestType::internal);
 232             XBT_DEBUG("%s (state=%d)", req_str, prev_state->num);
 233             xbt_free(req_str);
 234             prev_req = MC_state_get_executed_request(state.get(), &value);
 235             req_str = simgrid::mc::request_to_string(prev_req, value, simgrid::mc::RequestType::executed);
 236             XBT_DEBUG("%s (state=%d)", req_str, state->num);
 237             xbt_free(req_str);
 238           }
 239
 240           if (!MC_state_process_is_done(prev_state, issuer))
 241             MC_state_interleave_process(prev_state, issuer);
 242           else
 243             XBT_DEBUG("Process %p is in done set", req->issuer);
 244
 245           break;
 246
 247         } else if (req->issuer == MC_state_get_internal_request(prev_state)->issuer) {
 248
 249           XBT_DEBUG("Simcall %d and %d with same issuer", req->call, MC_state_get_internal_request(prev_state)->call);
 250           break;
 251
 252         } else {
 253
 254           const smx_process_t previous_issuer = MC_smx_simcall_get_issuer(MC_state_get_internal_request(prev_state));
 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                     MC_state_get_internal_request(prev_state)->call,
 258                     previous_issuer->pid,
 259                     prev_state->num);
 260
 261         }
 262       }
 263     }
 264
 265     if (MC_state_interleave_size(state.get())
 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::replay(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   mc_model_checker->wait_for_requests();
 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());
 301
 302   XBT_DEBUG("**************************************************");
 303   XBT_DEBUG("Initial state");
 304
 305   /* Wait for requests (schedules processes) */
 306   mc_model_checker->wait_for_requests();
 307
 308   /* Get an enabled process and insert it in the interleave set of the initial state */
 309   for (auto& p : mc_model_checker->process().simix_processes())
 310     if (simgrid::mc::process_is_enabled(&p.copy)) {
 311       MC_state_interleave_process(initial_state.get(), &p.copy);
 312       if (reductionMode_ != simgrid::mc::ReductionMode::none)
 313         break;
 314     }
 315
 316   stack_.push_back(std::move(initial_state));
 317
 318   /* Save the initial state */
 319   initial_global_state = std::unique_ptr<s_mc_global_t>(new s_mc_global_t());
 320   initial_global_state->snapshot = simgrid::mc::take_snapshot(0);
 321 }
 322
 323 SafetyChecker::SafetyChecker(Session& session) : Checker(session)
 324 {
 325 }
 326
 327 SafetyChecker::~SafetyChecker()
 328 {
 329 }
 330
 331 Checker* createSafetyChecker(Session& session)
 332 {
 333   return new SafetyChecker(session);
 334 }
 335
 336 }
 337 }