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