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