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 <memory>
  11 #include <string>
  12 #include <vector>
  13
  14 #include <xbt/log.h>
  15 #include <xbt/sysdep.h>
  16
  17 #include "src/mc/mc_state.h"
  18 #include "src/mc/mc_request.h"
  19 #include "src/mc/mc_safety.h"
  20 #include "src/mc/mc_private.h"
  21 #include "src/mc/mc_record.h"
  22 #include "src/mc/mc_smx.h"
  23 #include "src/mc/Client.hpp"
  24 #include "src/mc/mc_exit.h"
  25 #include "src/mc/Checker.hpp"
  26 #include "src/mc/SafetyChecker.hpp"
  27 #include "src/mc/VisitedState.hpp"
  28
  29 #include "src/xbt/mmalloc/mmprivate.h"
  30
  31 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_safety, mc,
  32                                 "Logging specific to MC safety verification ");
  33 namespace simgrid {
  34 namespace mc {
  35
  36 static void MC_show_non_termination(void)
  37 {
  38   XBT_INFO("******************************************");
  39   XBT_INFO("*** NON-PROGRESSIVE CYCLE DETECTED ***");
  40   XBT_INFO("******************************************");
  41   XBT_INFO("Counter-example execution trace:");
  42   for (auto& s : mc_model_checker->getChecker()->getTextualTrace())
  43     XBT_INFO("%s", s.c_str());
  44   MC_print_statistics(mc_stats);
  45 }
  46
  47 static int snapshot_compare(simgrid::mc::State* state1, simgrid::mc::State* state2)
  48 {
  49   simgrid::mc::Snapshot* s1 = state1->system_state.get();
  50   simgrid::mc::Snapshot* s2 = state2->system_state.get();
  51   int num1 = state1->num;
  52   int num2 = state2->num;
  53   return snapshot_compare(num1, s1, num2, s2);
  54 }
  55
  56 bool SafetyChecker::checkNonTermination(simgrid::mc::State* current_state)
  57 {
  58   for (auto i = stack_.rbegin(); i != stack_.rend(); ++i)
  59     if (snapshot_compare(i->get(), current_state) == 0){
  60       XBT_INFO("Non-progressive cycle : state %d -> state %d",
  61         (*i)->num, current_state->num);
  62       return true;
  63     }
  64   return false;
  65 }
  66
  67 RecordTrace SafetyChecker::getRecordTrace() // override
  68 {
  69   RecordTrace res;
  70   for (auto const& state : stack_)
  71     res.push_back(state->getRecordElement());
  72   return res;
  73 }
  74
  75 std::vector<std::string> SafetyChecker::getTextualTrace() // override
  76 {
  77   std::vector<std::string> trace;
  78   for (auto const& state : stack_) {
  79     int value = state->req_num;
  80     smx_simcall_t req = &state->executed_req;
  81     if (req)
  82       trace.push_back(simgrid::mc::request_to_string(
  83         req, value, simgrid::mc::RequestType::executed));
  84   }
  85   return trace;
  86 }
  87
  88 int SafetyChecker::run()
  89 {
  90   this->init();
  91
  92   int value;
  93
  94   while (!stack_.empty()) {
  95
  96     /* Get current state */
  97     simgrid::mc::State* state = stack_.back().get();
  98
  99     XBT_DEBUG("**************************************************");
 100     XBT_DEBUG(
 101       "Exploration depth=%zi (state=%p, num %d)(%zu interleave)",
 102       stack_.size(), state, state->num,
 103       state->interleaveSize());
 104
 105     mc_stats->visited_states++;
 106
 107     // The interleave set is empty or the maximum depth is reached,
 108     // let's back-track.
 109     smx_simcall_t req = nullptr;
 110     if (stack_.size() > (std::size_t) _sg_mc_max_depth
 111         || (req = MC_state_get_request(state, &value)) == nullptr
 112         || visitedState_ != nullptr) {
 113       int res = this->backtrack();
 114       if (res)
 115         return res;
 116       else
 117         continue;
 118     }
 119
 120     // If there are processes to interleave and the maximum depth has not been
 121     // reached then perform one step of the exploration algorithm.
 122     XBT_DEBUG("Execute: %s",
 123       simgrid::mc::request_to_string(
 124         req, value, simgrid::mc::RequestType::simix).c_str());
 125
 126     std::string req_str;
 127     if (dot_output != nullptr)
 128       req_str = simgrid::mc::request_get_dot_output(req, value);
 129
 130     mc_stats->executed_transitions++;
 131
 132     // TODO, bundle both operations in a single message
 133     //   MC_execute_transition(req, value)
 134
 135     /* Answer the request */
 136     simgrid::mc::handle_simcall(req, value);
 137     mc_model_checker->wait_for_requests();
 138
 139     /* Create the new expanded state */
 140     std::unique_ptr<simgrid::mc::State> next_state =
 141       std::unique_ptr<simgrid::mc::State>(MC_state_new());
 142
 143     if (_sg_mc_termination && this->checkNonTermination(next_state.get())) {
 144         MC_show_non_termination();
 145         return SIMGRID_MC_EXIT_NON_TERMINATION;
 146     }
 147
 148     if (_sg_mc_visited == 0
 149         || (visitedState_ = visitedStates_.addVisitedState(next_state.get(), true)) == nullptr) {
 150
 151       /* Get an enabled process and insert it in the interleave set of the next state */
 152       for (auto& p : mc_model_checker->process().simix_processes())
 153         if (simgrid::mc::process_is_enabled(&p.copy)) {
 154           next_state->interleave(&p.copy);
 155           if (reductionMode_ != simgrid::mc::ReductionMode::none)
 156             break;
 157         }
 158
 159       if (dot_output != nullptr)
 160         std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
 161           state->num, next_state->num, req_str.c_str());
 162
 163     } else if (dot_output != nullptr)
 164       std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
 165         state->num,
 166         visitedState_->other_num == -1 ? visitedState_->num : visitedState_->other_num, req_str.c_str());
 167
 168     stack_.push_back(std::move(next_state));
 169   }
 170
 171   XBT_INFO("No property violation found.");
 172   MC_print_statistics(mc_stats);
 173   initial_global_state = nullptr;
 174   return SIMGRID_MC_EXIT_SUCCESS;
 175 }
 176
 177 int SafetyChecker::backtrack()
 178 {
 179   if (stack_.size() > (std::size_t) _sg_mc_max_depth
 180       || visitedState_ != nullptr) {
 181     if (visitedState_ == nullptr)
 182       XBT_WARN("/!\\ Max depth reached ! /!\\ ");
 183     else
 184       XBT_DEBUG("State already visited (equal to state %d),"
 185         " exploration stopped on this path.",
 186         visitedState_->other_num == -1 ? visitedState_->num : visitedState_->other_num);
 187   } else
 188     XBT_DEBUG("There are no more processes to interleave. (depth %zi)",
 189       stack_.size() + 1);
 190
 191   stack_.pop_back();
 192
 193   visitedState_ = 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       smx_simcall_t 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             int value = prev_state->req_num;
 224             smx_simcall_t prev_req = &prev_state->executed_req;
 225             XBT_DEBUG("%s (state=%d)",
 226               simgrid::mc::request_to_string(
 227                 prev_req, value, simgrid::mc::RequestType::internal).c_str(),
 228               prev_state->num);
 229             value = state->req_num;
 230             prev_req = &state->executed_req;
 231             XBT_DEBUG("%s (state=%d)",
 232               simgrid::mc::request_to_string(
 233                 prev_req, value, simgrid::mc::RequestType::executed).c_str(),
 234               state->num);
 235           }
 236
 237           if (!prev_state->processStates[issuer->pid].isDone())
 238             prev_state->interleave(issuer);
 239           else
 240             XBT_DEBUG("Process %p is in done set", req->issuer);
 241
 242           break;
 243
 244         } else if (req->issuer == MC_state_get_internal_request(prev_state)->issuer) {
 245
 246           XBT_DEBUG("Simcall %d and %d with same issuer", req->call, MC_state_get_internal_request(prev_state)->call);
 247           break;
 248
 249         } else {
 250
 251           const smx_process_t previous_issuer = MC_smx_simcall_get_issuer(MC_state_get_internal_request(prev_state));
 252           XBT_DEBUG("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant",
 253                     req->call, issuer->pid, state->num,
 254                     MC_state_get_internal_request(prev_state)->call,
 255                     previous_issuer->pid,
 256                     prev_state->num);
 257
 258         }
 259       }
 260     }
 261
 262     if (state->interleaveSize()
 263         && stack_.size() < (std::size_t) _sg_mc_max_depth) {
 264       /* We found a back-tracking point, let's loop */
 265       XBT_DEBUG("Back-tracking to state %d at depth %zi",
 266         state->num, stack_.size() + 1);
 267       stack_.push_back(std::move(state));
 268       simgrid::mc::replay(stack_);
 269       XBT_DEBUG("Back-tracking to state %d at depth %zi done",
 270         stack_.back()->num, stack_.size());
 271       break;
 272     } else {
 273       XBT_DEBUG("Delete state %d at depth %zi",
 274         state->num, stack_.size() + 1);
 275     }
 276   }
 277   return SIMGRID_MC_EXIT_SUCCESS;
 278 }
 279
 280 void SafetyChecker::init()
 281 {
 282   reductionMode_ = simgrid::mc::reduction_mode;
 283   if( _sg_mc_termination)
 284     reductionMode_ = simgrid::mc::ReductionMode::none;
 285   else if (reductionMode_ == simgrid::mc::ReductionMode::unset)
 286     reductionMode_ = simgrid::mc::ReductionMode::dpor;
 287
 288   if (_sg_mc_termination)
 289     XBT_INFO("Check non progressive cycles");
 290   else
 291     XBT_INFO("Check a safety property");
 292   mc_model_checker->wait_for_requests();
 293
 294   XBT_DEBUG("Starting the safety algorithm");
 295
 296   std::unique_ptr<simgrid::mc::State> initial_state =
 297     std::unique_ptr<simgrid::mc::State>(MC_state_new());
 298
 299   XBT_DEBUG("**************************************************");
 300   XBT_DEBUG("Initial state");
 301
 302   /* Wait for requests (schedules processes) */
 303   mc_model_checker->wait_for_requests();
 304
 305   /* Get an enabled process and insert it in the interleave set of the initial state */
 306   for (auto& p : mc_model_checker->process().simix_processes())
 307     if (simgrid::mc::process_is_enabled(&p.copy)) {
 308       initial_state->interleave(&p.copy);
 309       if (reductionMode_ != simgrid::mc::ReductionMode::none)
 310         break;
 311     }
 312
 313   stack_.push_back(std::move(initial_state));
 314
 315   /* Save the initial state */
 316   initial_global_state = std::unique_ptr<s_mc_global_t>(new s_mc_global_t());
 317   initial_global_state->snapshot = simgrid::mc::take_snapshot(0);
 318 }
 319
 320 SafetyChecker::SafetyChecker(Session& session) : Checker(session)
 321 {
 322 }
 323
 324 SafetyChecker::~SafetyChecker()
 325 {
 326 }
 327
 328 Checker* createSafetyChecker(Session& session)
 329 {
 330   return new SafetyChecker(session);
 331 }
 332
 333 }
 334 }