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       trace.push_back(simgrid::mc::request_to_string(
  86         req, value, simgrid::mc::RequestType::executed));
  87   }
  88   return trace;
  89 }
  90
  91 int SafetyChecker::run()
  92 {
  93   this->init();
  94
  95   int value;
  96
  97   while (!stack_.empty()) {
  98
  99     /* Get current state */
 100     simgrid::mc::State* state = stack_.back().get();
 101
 102     XBT_DEBUG("**************************************************");
 103     XBT_DEBUG(
 104       "Exploration depth=%zi (state=%p, num %d)(%zu interleave)",
 105       stack_.size(), state, state->num,
 106       state->interleaveSize());
 107
 108     mc_stats->visited_states++;
 109
 110     // The interleave set is empty or the maximum depth is reached,
 111     // let's back-track.
 112     smx_simcall_t req = nullptr;
 113     if (stack_.size() > (std::size_t) _sg_mc_max_depth
 114         || (req = MC_state_get_request(state, &value)) == nullptr
 115         || visitedState_ != nullptr) {
 116       int res = this->backtrack();
 117       if (res)
 118         return res;
 119       else
 120         continue;
 121     }
 122
 123     // If there are processes to interleave and the maximum depth has not been
 124     // reached then perform one step of the exploration algorithm.
 125     XBT_DEBUG("Execute: %s",
 126       simgrid::mc::request_to_string(
 127         req, value, simgrid::mc::RequestType::simix).c_str());
 128
 129     char* req_str = nullptr;
 130     if (dot_output != nullptr)
 131       req_str = simgrid::mc::request_get_dot_output(req, value);
 132
 133     MC_state_set_executed_request(state, req, value);
 134     mc_stats->executed_transitions++;
 135
 136     // TODO, bundle both operations in a single message
 137     //   MC_execute_transition(req, value)
 138
 139     /* Answer the request */
 140     simgrid::mc::handle_simcall(req, value);
 141     mc_model_checker->wait_for_requests();
 142
 143     /* Create the new expanded state */
 144     std::unique_ptr<simgrid::mc::State> next_state =
 145       std::unique_ptr<simgrid::mc::State>(MC_state_new());
 146
 147     if (_sg_mc_termination && this->checkNonTermination(next_state.get())) {
 148         MC_show_non_termination();
 149         return SIMGRID_MC_EXIT_NON_TERMINATION;
 150     }
 151
 152     if (_sg_mc_visited == 0
 153         || (visitedState_ = visitedStates_.addVisitedState(next_state.get(), true)) == nullptr) {
 154
 155       /* Get an enabled process and insert it in the interleave set of the next state */
 156       for (auto& p : mc_model_checker->process().simix_processes())
 157         if (simgrid::mc::process_is_enabled(&p.copy)) {
 158           MC_state_interleave_process(next_state.get(), &p.copy);
 159           if (reductionMode_ != simgrid::mc::ReductionMode::none)
 160             break;
 161         }
 162
 163       if (dot_output != nullptr)
 164         std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str);
 165
 166     } else if (dot_output != nullptr)
 167       std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visitedState_->other_num == -1 ? visitedState_->num : visitedState_->other_num, req_str);
 168
 169     stack_.push_back(std::move(next_state));
 170
 171     if (dot_output != nullptr)
 172       xbt_free(req_str);
 173   }
 174
 175   XBT_INFO("No property violation found.");
 176   MC_print_statistics(mc_stats);
 177   initial_global_state = nullptr;
 178   return SIMGRID_MC_EXIT_SUCCESS;
 179 }
 180
 181 int SafetyChecker::backtrack()
 182 {
 183   if (stack_.size() > (std::size_t) _sg_mc_max_depth
 184       || visitedState_ != nullptr) {
 185     if (visitedState_ == nullptr)
 186       XBT_WARN("/!\\ Max depth reached ! /!\\ ");
 187     else
 188       XBT_DEBUG("State already visited (equal to state %d),"
 189         " exploration stopped on this path.",
 190         visitedState_->other_num == -1 ? visitedState_->num : visitedState_->other_num);
 191   } else
 192     XBT_DEBUG("There are no more processes to interleave. (depth %zi)",
 193       stack_.size() + 1);
 194
 195   stack_.pop_back();
 196
 197   visitedState_ = nullptr;
 198
 199   /* Check for deadlocks */
 200   if (mc_model_checker->checkDeadlock()) {
 201     MC_show_deadlock();
 202     return SIMGRID_MC_EXIT_DEADLOCK;
 203   }
 204
 205   /* Traverse the stack backwards until a state with a non empty interleave
 206      set is found, deleting all the states that have it empty in the way.
 207      For each deleted state, check if the request that has generated it
 208      (from it's predecesor state), depends on any other previous request
 209      executed before it. If it does then add it to the interleave set of the
 210      state that executed that previous request. */
 211
 212   while (!stack_.empty()) {
 213     std::unique_ptr<simgrid::mc::State> state = std::move(stack_.back());
 214     stack_.pop_back();
 215     if (reductionMode_ == simgrid::mc::ReductionMode::dpor) {
 216       smx_simcall_t req = MC_state_get_internal_request(state.get());
 217       if (req->call == SIMCALL_MUTEX_LOCK || req->call == SIMCALL_MUTEX_TRYLOCK)
 218         xbt_die("Mutex is currently not supported with DPOR, "
 219           "use --cfg=model-check/reduction:none");
 220       const smx_process_t issuer = MC_smx_simcall_get_issuer(req);
 221       for (auto i = stack_.rbegin(); i != stack_.rend(); ++i) {
 222         simgrid::mc::State* prev_state = i->get();
 223         if (reductionMode_ != simgrid::mc::ReductionMode::none
 224             && simgrid::mc::request_depend(req, MC_state_get_internal_request(prev_state))) {
 225           if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
 226             XBT_DEBUG("Dependent Transitions:");
 227             int value;
 228             smx_simcall_t prev_req = MC_state_get_executed_request(prev_state, &value);
 229             XBT_DEBUG("%s (state=%d)",
 230               simgrid::mc::request_to_string(
 231                 prev_req, value, simgrid::mc::RequestType::internal).c_str(),
 232               prev_state->num);
 233             prev_req = MC_state_get_executed_request(state.get(), &value);
 234             XBT_DEBUG("%s (state=%d)",
 235               simgrid::mc::request_to_string(
 236                 prev_req, value, simgrid::mc::RequestType::executed).c_str(),
 237               state->num);
 238           }
 239
 240           if (!prev_state->processStates[issuer->pid].done())
 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 (state->interleaveSize()
 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 }