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;
  80     smx_simcall_t req = MC_state_get_executed_request(state.get(), &value);
  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;
 224             smx_simcall_t prev_req = MC_state_get_executed_request(prev_state, &value);
 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             prev_req = MC_state_get_executed_request(state.get(), &value);
 230             XBT_DEBUG("%s (state=%d)",
 231               simgrid::mc::request_to_string(
 232                 prev_req, value, simgrid::mc::RequestType::executed).c_str(),
 233               state->num);
 234           }
 235
 236           if (!prev_state->processStates[issuer->pid].isDone())
 237             prev_state->interleave(issuer);
 238           else
 239             XBT_DEBUG("Process %p is in done set", req->issuer);
 240
 241           break;
 242
 243         } else if (req->issuer == MC_state_get_internal_request(prev_state)->issuer) {
 244
 245           XBT_DEBUG("Simcall %d and %d with same issuer", req->call, MC_state_get_internal_request(prev_state)->call);
 246           break;
 247
 248         } else {
 249
 250           const smx_process_t previous_issuer = MC_smx_simcall_get_issuer(MC_state_get_internal_request(prev_state));
 251           XBT_DEBUG("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant",
 252                     req->call, issuer->pid, state->num,
 253                     MC_state_get_internal_request(prev_state)->call,
 254                     previous_issuer->pid,
 255                     prev_state->num);
 256
 257         }
 258       }
 259     }
 260
 261     if (state->interleaveSize()
 262         && stack_.size() < (std::size_t) _sg_mc_max_depth) {
 263       /* We found a back-tracking point, let's loop */
 264       XBT_DEBUG("Back-tracking to state %d at depth %zi",
 265         state->num, stack_.size() + 1);
 266       stack_.push_back(std::move(state));
 267       simgrid::mc::replay(stack_);
 268       XBT_DEBUG("Back-tracking to state %d at depth %zi done",
 269         stack_.back()->num, stack_.size());
 270       break;
 271     } else {
 272       XBT_DEBUG("Delete state %d at depth %zi",
 273         state->num, stack_.size() + 1);
 274     }
 275   }
 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       initial_state->interleave(&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 }