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