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   smx_simcall_t req = nullptr;
 100
 101   while (!stack_.empty()) {
 102
 103     /* Get current state */
 104     simgrid::mc::State* state = stack_.back().get();
 105
 106     XBT_DEBUG("**************************************************");
 107     XBT_DEBUG(
 108       "Exploration depth=%zi (state=%p, num %d)(%u interleave)",
 109       stack_.size(), state, state->num,
 110       MC_state_interleave_size(state));
 111
 112     /* Update statistics */
 113     mc_stats->visited_states++;
 114
 115     /* If there are processes to interleave and the maximum depth has not been reached
 116        then perform one step of the exploration algorithm */
 117     if (stack_.size() <= (std::size_t) _sg_mc_max_depth
 118         && (req = MC_state_get_request(state, &value)) != nullptr
 119         && visitedState_ == 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->checkNonTermination(next_state.get())) {
 143           MC_show_non_termination();
 144           return SIMGRID_MC_EXIT_NON_TERMINATION;
 145       }
 146
 147       if (_sg_mc_visited == 0
 148           || (visitedState_ = 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, visitedState_->other_num == -1 ? visitedState_->num : visitedState_->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           || visitedState_ != nullptr) {
 176         if (visitedState_ == nullptr)
 177           XBT_WARN("/!\\ Max depth reached ! /!\\ ");
 178         else
 179           XBT_DEBUG("State already visited (equal to state %d),"
 180             " exploration stopped on this path.",
 181             visitedState_->other_num == -1 ? visitedState_->num : visitedState_->other_num);
 182       } else
 183         XBT_DEBUG("There are no more processes to interleave. (depth %zi)",
 184           stack_.size() + 1);
 185
 186       /* Trash the current state, no longer needed */
 187       XBT_DEBUG("Delete state %d at depth %zi", state->num, stack_.size());
 188       stack_.pop_back();
 189
 190       visitedState_ = nullptr;
 191
 192       /* Check for deadlocks */
 193       if (mc_model_checker->checkDeadlock()) {
 194         MC_show_deadlock();
 195         return SIMGRID_MC_EXIT_DEADLOCK;
 196       }
 197
 198       /* Traverse the stack backwards until a state with a non empty interleave
 199          set is found, deleting all the states that have it empty in the way.
 200          For each deleted state, check if the request that has generated it
 201          (from it's predecesor state), depends on any other previous request
 202          executed before it. If it does then add it to the interleave set of the
 203          state that executed that previous request. */
 204
 205       while (!stack_.empty()) {
 206         std::unique_ptr<simgrid::mc::State> state = std::move(stack_.back());
 207         stack_.pop_back();
 208         if (reductionMode_ == simgrid::mc::ReductionMode::dpor) {
 209           req = MC_state_get_internal_request(state.get());
 210           if (req->call == SIMCALL_MUTEX_LOCK || req->call == SIMCALL_MUTEX_TRYLOCK)
 211             xbt_die("Mutex is currently not supported with DPOR, "
 212               "use --cfg=model-check/reduction:none");
 213           const smx_process_t issuer = MC_smx_simcall_get_issuer(req);
 214           for (auto i = stack_.rbegin(); i != stack_.rend(); ++i) {
 215             simgrid::mc::State* prev_state = i->get();
 216             if (reductionMode_ != simgrid::mc::ReductionMode::none
 217                 && simgrid::mc::request_depend(req, MC_state_get_internal_request(prev_state))) {
 218               if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
 219                 XBT_DEBUG("Dependent Transitions:");
 220                 smx_simcall_t prev_req = MC_state_get_executed_request(prev_state, &value);
 221                 char* req_str = simgrid::mc::request_to_string(prev_req, value, simgrid::mc::RequestType::internal);
 222                 XBT_DEBUG("%s (state=%d)", req_str, prev_state->num);
 223                 xbt_free(req_str);
 224                 prev_req = MC_state_get_executed_request(state.get(), &value);
 225                 req_str = simgrid::mc::request_to_string(prev_req, value, simgrid::mc::RequestType::executed);
 226                 XBT_DEBUG("%s (state=%d)", req_str, state->num);
 227                 xbt_free(req_str);
 228               }
 229
 230               if (!MC_state_process_is_done(prev_state, issuer))
 231                 MC_state_interleave_process(prev_state, issuer);
 232               else
 233                 XBT_DEBUG("Process %p is in done set", req->issuer);
 234
 235               break;
 236
 237             } else if (req->issuer == MC_state_get_internal_request(prev_state)->issuer) {
 238
 239               XBT_DEBUG("Simcall %d and %d with same issuer", req->call, MC_state_get_internal_request(prev_state)->call);
 240               break;
 241
 242             } else {
 243
 244               const smx_process_t previous_issuer = MC_smx_simcall_get_issuer(MC_state_get_internal_request(prev_state));
 245               XBT_DEBUG("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant",
 246                         req->call, issuer->pid, state->num,
 247                         MC_state_get_internal_request(prev_state)->call,
 248                         previous_issuer->pid,
 249                         prev_state->num);
 250
 251             }
 252           }
 253         }
 254
 255         if (MC_state_interleave_size(state.get())
 256             && stack_.size() < (std::size_t) _sg_mc_max_depth) {
 257           /* We found a back-tracking point, let's loop */
 258           XBT_DEBUG("Back-tracking to state %d at depth %zi",
 259             state->num, stack_.size() + 1);
 260           stack_.push_back(std::move(state));
 261           simgrid::mc::replay(stack_);
 262           XBT_DEBUG("Back-tracking to state %d at depth %zi done",
 263             stack_.back()->num, stack_.size());
 264           break;
 265         } else {
 266           XBT_DEBUG("Delete state %d at depth %zi",
 267             state->num, stack_.size() + 1);
 268         }
 269       }
 270     }
 271   }
 272
 273   XBT_INFO("No property violation found.");
 274   MC_print_statistics(mc_stats);
 275   initial_global_state = nullptr;
 276   return SIMGRID_MC_EXIT_SUCCESS;
 277 }
 278
 279 void SafetyChecker::init()
 280 {
 281   reductionMode_ = simgrid::mc::reduction_mode;
 282   if( _sg_mc_termination)
 283     reductionMode_ = simgrid::mc::ReductionMode::none;
 284   else if (reductionMode_ == simgrid::mc::ReductionMode::unset)
 285     reductionMode_ = simgrid::mc::ReductionMode::dpor;
 286
 287   if (_sg_mc_termination)
 288     XBT_INFO("Check non progressive cycles");
 289   else
 290     XBT_INFO("Check a safety property");
 291   mc_model_checker->wait_for_requests();
 292
 293   XBT_DEBUG("Starting the safety algorithm");
 294
 295   std::unique_ptr<simgrid::mc::State> initial_state =
 296     std::unique_ptr<simgrid::mc::State>(MC_state_new());
 297
 298   XBT_DEBUG("**************************************************");
 299   XBT_DEBUG("Initial state");
 300
 301   /* Wait for requests (schedules processes) */
 302   mc_model_checker->wait_for_requests();
 303
 304   /* Get an enabled process and insert it in the interleave set of the initial state */
 305   for (auto& p : mc_model_checker->process().simix_processes())
 306     if (simgrid::mc::process_is_enabled(&p.copy)) {
 307       MC_state_interleave_process(initial_state.get(), &p.copy);
 308       if (reductionMode_ != simgrid::mc::ReductionMode::none)
 309         break;
 310     }
 311
 312   stack_.push_back(std::move(initial_state));
 313
 314   /* Save the initial state */
 315   initial_global_state = std::unique_ptr<s_mc_global_t>(new s_mc_global_t());
 316   initial_global_state->snapshot = simgrid::mc::take_snapshot(0);
 317 }
 318
 319 SafetyChecker::SafetyChecker(Session& session) : Checker(session)
 320 {
 321 }
 322
 323 SafetyChecker::~SafetyChecker()
 324 {
 325 }
 326
 327 Checker* createSafetyChecker(Session& session)
 328 {
 329   return new SafetyChecker(session);
 330 }
 331
 332 }
 333 }