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/dynar.h>
  14 #include <xbt/dynar.hpp>
  15 #include <xbt/fifo.h>
  16 #include <xbt/sysdep.h>
  17
  18 #include "src/mc/mc_state.h"
  19 #include "src/mc/mc_request.h"
  20 #include "src/mc/mc_safety.h"
  21 #include "src/mc/mc_private.h"
  22 #include "src/mc/mc_record.h"
  23 #include "src/mc/mc_smx.h"
  24 #include "src/mc/Client.hpp"
  25 #include "src/mc/mc_exit.h"
  26 #include "src/mc/Checker.hpp"
  27 #include "src/mc/SafetyChecker.hpp"
  28 #include "src/mc/VisitedState.hpp"
  29
  30 #include "src/xbt/mmalloc/mmprivate.h"
  31
  32 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_safety, mc,
  33                                 "Logging specific to MC safety verification ");
  34 namespace simgrid {
  35 namespace mc {
  36
  37 static void MC_show_non_termination(void)
  38 {
  39   XBT_INFO("******************************************");
  40   XBT_INFO("*** NON-PROGRESSIVE CYCLE DETECTED ***");
  41   XBT_INFO("******************************************");
  42   XBT_INFO("Counter-example execution trace:");
  43   for (auto& s : mc_model_checker->getChecker()->getTextualTrace())
  44     XBT_INFO("%s", s.c_str());
  45   MC_print_statistics(mc_stats);
  46 }
  47
  48 static int snapshot_compare(simgrid::mc::State* state1, simgrid::mc::State* state2)
  49 {
  50   simgrid::mc::Snapshot* s1 = state1->system_state.get();
  51   simgrid::mc::Snapshot* s2 = state2->system_state.get();
  52   int num1 = state1->num;
  53   int num2 = state2->num;
  54   return snapshot_compare(num1, s1, num2, s2);
  55 }
  56
  57 bool SafetyChecker::checkNonDeterminism(simgrid::mc::State* current_state)
  58 {
  59   for (auto i = stack_.rbegin(); i != stack_.rend(); ++i)
  60     if (snapshot_compare(i->get(), current_state) == 0){
  61       XBT_INFO("Non-progressive cycle : state %d -> state %d",
  62         (*i)->num, current_state->num);
  63       return true;
  64     }
  65   return false;
  66 }
  67
  68 RecordTrace SafetyChecker::getRecordTrace() // override
  69 {
  70   RecordTrace res;
  71   for (auto const& state : stack_) {
  72     int value = 0;
  73     smx_simcall_t saved_req = MC_state_get_executed_request(state.get(), &value);
  74     const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req);
  75     const int pid = issuer->pid;
  76     res.push_back(RecordTraceElement(pid, value));
  77   }
  78   return res;
  79 }
  80
  81 std::vector<std::string> SafetyChecker::getTextualTrace() // override
  82 {
  83   std::vector<std::string> trace;
  84   for (auto const& state : stack_) {
  85     int value;
  86     smx_simcall_t req = MC_state_get_executed_request(state.get(), &value);
  87     if (req) {
  88       char* req_str = simgrid::mc::request_to_string(
  89         req, value, simgrid::mc::RequestType::executed);
  90       trace.push_back(req_str);
  91       xbt_free(req_str);
  92     }
  93   }
  94   return trace;
  95 }
  96
  97 int SafetyChecker::run()
  98 {
  99   this->init();
 100
 101   int value;
 102   smx_simcall_t req = nullptr;
 103   std::unique_ptr<simgrid::mc::VisitedState> visited_state = nullptr;
 104
 105   while (!stack_.empty()) {
 106
 107     /* Get current state */
 108     simgrid::mc::State* state = stack_.back().get();
 109
 110     XBT_DEBUG("**************************************************");
 111     XBT_DEBUG(
 112       "Exploration depth=%zi (state=%p, num %d)(%u interleave, user_max_depth %d)",
 113       stack_.size(), state, state->num,
 114       MC_state_interleave_size(state), user_max_depth_reached);
 115
 116     /* Update statistics */
 117     mc_stats->visited_states++;
 118
 119     /* If there are processes to interleave and the maximum depth has not been reached
 120        then perform one step of the exploration algorithm */
 121     if (stack_.size() <= (std::size_t) _sg_mc_max_depth && !user_max_depth_reached
 122         && (req = MC_state_get_request(state, &value)) && visited_state == nullptr) {
 123
 124       char* req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::simix);
 125       XBT_DEBUG("Execute: %s", req_str);
 126       xbt_free(req_str);
 127
 128       if (dot_output != nullptr)
 129         req_str = simgrid::mc::request_get_dot_output(req, value);
 130
 131       MC_state_set_executed_request(state, req, value);
 132       mc_stats->executed_transitions++;
 133
 134       // TODO, bundle both operations in a single message
 135       //   MC_execute_transition(req, value)
 136
 137       /* Answer the request */
 138       simgrid::mc::handle_simcall(req, value);
 139       mc_model_checker->wait_for_requests();
 140
 141       /* Create the new expanded state */
 142       std::unique_ptr<simgrid::mc::State> next_state =
 143         std::unique_ptr<simgrid::mc::State>(MC_state_new());
 144
 145       if (_sg_mc_termination && this->checkNonDeterminism(next_state.get())){
 146           MC_show_non_termination();
 147           return SIMGRID_MC_EXIT_NON_TERMINATION;
 148       }
 149
 150       if (_sg_mc_visited == 0
 151           || (visited_state = visitedStates_.addVisitedState(next_state.get(), true)) == nullptr) {
 152
 153         /* Get an enabled process and insert it in the interleave set of the next state */
 154         for (auto& p : mc_model_checker->process().simix_processes())
 155           if (simgrid::mc::process_is_enabled(&p.copy)) {
 156             MC_state_interleave_process(next_state.get(), &p.copy);
 157             if (reductionMode_ != simgrid::mc::ReductionMode::none)
 158               break;
 159           }
 160
 161         if (dot_output != nullptr)
 162           std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str);
 163
 164       } else if (dot_output != nullptr)
 165         std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str);
 166
 167       stack_.push_back(std::move(next_state));
 168
 169       if (dot_output != nullptr)
 170         xbt_free(req_str);
 171
 172       /* Let's loop again */
 173
 174       /* The interleave set is empty or the maximum depth is reached, let's back-track */
 175     } else {
 176
 177       if (stack_.size() > (std::size_t) _sg_mc_max_depth
 178           || user_max_depth_reached
 179           || visited_state != nullptr) {
 180
 181         if (user_max_depth_reached && visited_state == nullptr)
 182           XBT_DEBUG("User max depth reached !");
 183         else if (visited_state == nullptr)
 184           XBT_WARN("/!\\ Max depth reached ! /!\\ ");
 185         else
 186           XBT_DEBUG("State already visited (equal to state %d), exploration stopped on this path.", visited_state->other_num == -1 ? visited_state->num : visited_state->other_num);
 187
 188       } else
 189         XBT_DEBUG("There are no more processes to interleave. (depth %zi)",
 190           stack_.size() + 1);
 191
 192       /* Trash the current state, no longer needed */
 193       XBT_DEBUG("Delete state %d at depth %zi", state->num, stack_.size());
 194       stack_.pop_back();
 195
 196       visited_state = nullptr;
 197
 198       /* Check for deadlocks */
 199       if (mc_model_checker->checkDeadlock()) {
 200         MC_show_deadlock();
 201         return SIMGRID_MC_EXIT_DEADLOCK;
 202       }
 203
 204       /* Traverse the stack backwards until a state with a non empty interleave
 205          set is found, deleting all the states that have it empty in the way.
 206          For each deleted state, check if the request that has generated it
 207          (from it's predecesor state), depends on any other previous request
 208          executed before it. If it does then add it to the interleave set of the
 209          state that executed that previous request. */
 210
 211       while (!stack_.empty()) {
 212         std::unique_ptr<simgrid::mc::State> state = std::move(stack_.back());
 213         stack_.pop_back();
 214         if (reductionMode_ == simgrid::mc::ReductionMode::dpor) {
 215           req = MC_state_get_internal_request(state.get());
 216           if (req->call == SIMCALL_MUTEX_LOCK || req->call == SIMCALL_MUTEX_TRYLOCK)
 217             xbt_die("Mutex is currently not supported with DPOR, "
 218               "use --cfg=model-check/reduction:none");
 219           const smx_process_t issuer = MC_smx_simcall_get_issuer(req);
 220           for (auto i = stack_.rbegin(); i != stack_.rend(); ++i) {
 221             simgrid::mc::State* prev_state = i->get();
 222             if (reductionMode_ != simgrid::mc::ReductionMode::none
 223                 && simgrid::mc::request_depend(req, MC_state_get_internal_request(prev_state))) {
 224               if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
 225                 XBT_DEBUG("Dependent Transitions:");
 226                 smx_simcall_t prev_req = MC_state_get_executed_request(prev_state, &value);
 227                 char* req_str = simgrid::mc::request_to_string(prev_req, value, simgrid::mc::RequestType::internal);
 228                 XBT_DEBUG("%s (state=%d)", req_str, prev_state->num);
 229                 xbt_free(req_str);
 230                 prev_req = MC_state_get_executed_request(state.get(), &value);
 231                 req_str = simgrid::mc::request_to_string(prev_req, value, simgrid::mc::RequestType::executed);
 232                 XBT_DEBUG("%s (state=%d)", req_str, state->num);
 233                 xbt_free(req_str);
 234               }
 235
 236               if (!MC_state_process_is_done(prev_state, issuer))
 237                 MC_state_interleave_process(prev_state, 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 (MC_state_interleave_size(state.get())
 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     }
 277   }
 278
 279   XBT_INFO("No property violation found.");
 280   MC_print_statistics(mc_stats);
 281   initial_global_state = nullptr;
 282   return SIMGRID_MC_EXIT_SUCCESS;
 283 }
 284
 285 void SafetyChecker::init()
 286 {
 287   reductionMode_ = simgrid::mc::reduction_mode;
 288   if( _sg_mc_termination)
 289     reductionMode_ = simgrid::mc::ReductionMode::none;
 290   else if (reductionMode_ == simgrid::mc::ReductionMode::unset)
 291     reductionMode_ = simgrid::mc::ReductionMode::dpor;
 292
 293   if (_sg_mc_termination)
 294     XBT_INFO("Check non progressive cycles");
 295   else
 296     XBT_INFO("Check a safety property");
 297   mc_model_checker->wait_for_requests();
 298
 299   XBT_DEBUG("Starting the safety algorithm");
 300
 301   std::unique_ptr<simgrid::mc::State> initial_state =
 302     std::unique_ptr<simgrid::mc::State>(MC_state_new());
 303
 304   XBT_DEBUG("**************************************************");
 305   XBT_DEBUG("Initial state");
 306
 307   /* Wait for requests (schedules processes) */
 308   mc_model_checker->wait_for_requests();
 309
 310   /* Get an enabled process and insert it in the interleave set of the initial state */
 311   for (auto& p : mc_model_checker->process().simix_processes())
 312     if (simgrid::mc::process_is_enabled(&p.copy)) {
 313       MC_state_interleave_process(initial_state.get(), &p.copy);
 314       if (reductionMode_ != simgrid::mc::ReductionMode::none)
 315         break;
 316     }
 317
 318   stack_.push_back(std::move(initial_state));
 319
 320   /* Save the initial state */
 321   initial_global_state = std::unique_ptr<s_mc_global_t>(new s_mc_global_t());
 322   initial_global_state->snapshot = simgrid::mc::take_snapshot(0);
 323 }
 324
 325 SafetyChecker::SafetyChecker(Session& session) : Checker(session)
 326 {
 327 }
 328
 329 SafetyChecker::~SafetyChecker()
 330 {
 331 }
 332
 333 }
 334 }