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