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