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 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 static int is_exploration_stack_state(simgrid::mc::State* current_state){
  57
  58   xbt_fifo_item_t item;
  59   simgrid::mc::State* stack_state;
  60   for(item = xbt_fifo_get_first_item(mc_stack); item != nullptr; item = xbt_fifo_get_next_item(item)) {
  61     stack_state = (simgrid::mc::State*) xbt_fifo_get_item_content(item);
  62     if(snapshot_compare(stack_state, current_state) == 0){
  63       XBT_INFO("Non-progressive cycle : state %d -> state %d", stack_state->num, current_state->num);
  64       return 1;
  65     }
  66   }
  67   return 0;
  68 }
  69
  70 RecordTrace SafetyChecker::getRecordTrace() // override
  71 {
  72   RecordTrace res;
  73
  74   xbt_fifo_item_t start = xbt_fifo_get_last_item(mc_stack);
  75   for (xbt_fifo_item_t item = start; item; item = xbt_fifo_get_prev_item(item)) {
  76
  77     // Find (pid, value):
  78     simgrid::mc::State* state = (simgrid::mc::State*) xbt_fifo_get_item_content(item);
  79     int value = 0;
  80     smx_simcall_t saved_req = MC_state_get_executed_request(state, &value);
  81     const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req);
  82     const int pid = issuer->pid;
  83
  84     res.push_back(RecordTraceElement(pid, value));
  85   }
  86
  87   return res;
  88 }
  89
  90 std::vector<std::string> SafetyChecker::getTextualTrace() // override
  91 {
  92   std::vector<std::string> trace;
  93   for (xbt_fifo_item_t item = xbt_fifo_get_last_item(mc_stack);
  94        item; item = xbt_fifo_get_prev_item(item)) {
  95     simgrid::mc::State* state = (simgrid::mc::State*)xbt_fifo_get_item_content(item);
  96     int value;
  97     smx_simcall_t req = MC_state_get_executed_request(state, &value);
  98     if (req) {
  99       char* req_str = simgrid::mc::request_to_string(
 100         req, value, simgrid::mc::RequestType::executed);
 101       trace.push_back(req_str);
 102       xbt_free(req_str);
 103     }
 104   }
 105   return trace;
 106 }
 107
 108 int SafetyChecker::run()
 109 {
 110   this->init();
 111
 112   char *req_str = nullptr;
 113   int value;
 114   smx_simcall_t req = nullptr;
 115   simgrid::mc::State* state = nullptr;
 116   simgrid::mc::State* prev_state = nullptr;
 117   simgrid::mc::State* next_state = nullptr;
 118   xbt_fifo_item_t item = nullptr;
 119   std::unique_ptr<simgrid::mc::VisitedState> visited_state = nullptr;
 120
 121   while (xbt_fifo_size(mc_stack) > 0) {
 122
 123     /* Get current state */
 124     state = (simgrid::mc::State*)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
 125
 126     XBT_DEBUG("**************************************************");
 127     XBT_DEBUG
 128         ("Exploration depth=%d (state=%p, num %d)(%u interleave, user_max_depth %d)",
 129          xbt_fifo_size(mc_stack), state, state->num,
 130          MC_state_interleave_size(state), user_max_depth_reached);
 131
 132     /* Update statistics */
 133     mc_stats->visited_states++;
 134
 135     /* If there are processes to interleave and the maximum depth has not been reached
 136        then perform one step of the exploration algorithm */
 137     if (xbt_fifo_size(mc_stack) <= _sg_mc_max_depth && !user_max_depth_reached
 138         && (req = MC_state_get_request(state, &value)) && visited_state == nullptr) {
 139
 140       req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::simix);
 141       XBT_DEBUG("Execute: %s", req_str);
 142       xbt_free(req_str);
 143
 144       if (dot_output != nullptr)
 145         req_str = simgrid::mc::request_get_dot_output(req, value);
 146
 147       MC_state_set_executed_request(state, req, value);
 148       mc_stats->executed_transitions++;
 149
 150       // TODO, bundle both operations in a single message
 151       //   MC_execute_transition(req, value)
 152
 153       /* Answer the request */
 154       simgrid::mc::handle_simcall(req, value);
 155       mc_model_checker->wait_for_requests();
 156
 157       /* Create the new expanded state */
 158       next_state = MC_state_new();
 159
 160       if(_sg_mc_termination && is_exploration_stack_state(next_state)){
 161           MC_show_non_termination();
 162           return SIMGRID_MC_EXIT_NON_TERMINATION;
 163       }
 164
 165       if (_sg_mc_visited == 0 || (visited_state = simgrid::mc::is_visited_state(next_state, true)) == nullptr) {
 166
 167         /* Get an enabled process and insert it in the interleave set of the next state */
 168         for (auto& p : mc_model_checker->process().simix_processes())
 169           if (simgrid::mc::process_is_enabled(&p.copy)) {
 170             MC_state_interleave_process(next_state, &p.copy);
 171             if (reductionMode_ != simgrid::mc::ReductionMode::none)
 172               break;
 173           }
 174
 175         if (dot_output != nullptr)
 176           std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str);
 177
 178       } else if (dot_output != nullptr)
 179         std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str);
 180
 181
 182       xbt_fifo_unshift(mc_stack, next_state);
 183
 184       if (dot_output != nullptr)
 185         xbt_free(req_str);
 186
 187       /* Let's loop again */
 188
 189       /* The interleave set is empty or the maximum depth is reached, let's back-track */
 190     } else {
 191
 192       if ((xbt_fifo_size(mc_stack) > _sg_mc_max_depth) || user_max_depth_reached || visited_state != nullptr) {
 193
 194         if (user_max_depth_reached && visited_state == nullptr)
 195           XBT_DEBUG("User max depth reached !");
 196         else if (visited_state == nullptr)
 197           XBT_WARN("/!\\ Max depth reached ! /!\\ ");
 198         else
 199           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);
 200
 201       } else
 202         XBT_DEBUG("There are no more processes to interleave. (depth %d)", xbt_fifo_size(mc_stack) + 1);
 203
 204       /* Trash the current state, no longer needed */
 205       xbt_fifo_shift(mc_stack);
 206       XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
 207       MC_state_delete(state, !state->in_visited_states ? 1 : 0);
 208
 209       visited_state = nullptr;
 210
 211       /* Check for deadlocks */
 212       if (mc_model_checker->checkDeadlock()) {
 213         MC_show_deadlock();
 214         return SIMGRID_MC_EXIT_DEADLOCK;
 215       }
 216
 217       /* Traverse the stack backwards until a state with a non empty interleave
 218          set is found, deleting all the states that have it empty in the way.
 219          For each deleted state, check if the request that has generated it
 220          (from it's predecesor state), depends on any other previous request
 221          executed before it. If it does then add it to the interleave set of the
 222          state that executed that previous request. */
 223
 224       while ((state = (simgrid::mc::State*) xbt_fifo_shift(mc_stack))) {
 225         if (reductionMode_ == simgrid::mc::ReductionMode::dpor) {
 226           req = MC_state_get_internal_request(state);
 227           if (req->call == SIMCALL_MUTEX_LOCK || req->call == SIMCALL_MUTEX_TRYLOCK)
 228             xbt_die("Mutex is currently not supported with DPOR, "
 229               "use --cfg=model-check/reduction:none");
 230           const smx_process_t issuer = MC_smx_simcall_get_issuer(req);
 231           xbt_fifo_foreach(mc_stack, item, prev_state, simgrid::mc::State*) {
 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) && xbt_fifo_size(mc_stack) < _sg_mc_max_depth) {
 272           /* We found a back-tracking point, let's loop */
 273           XBT_DEBUG("Back-tracking to state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
 274           xbt_fifo_unshift(mc_stack, state);
 275           MC_replay(mc_stack);
 276           XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num, xbt_fifo_size(mc_stack));
 277           break;
 278         } else {
 279           XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
 280           MC_state_delete(state, !state->in_visited_states ? 1 : 0);
 281         }
 282       }
 283     }
 284   }
 285
 286   XBT_INFO("No property violation found.");
 287   MC_print_statistics(mc_stats);
 288   initial_global_state = nullptr;
 289   return SIMGRID_MC_EXIT_SUCCESS;
 290 }
 291
 292 void SafetyChecker::init()
 293 {
 294   reductionMode_ = simgrid::mc::reduction_mode;
 295   if( _sg_mc_termination)
 296     reductionMode_ = simgrid::mc::ReductionMode::none;
 297   else if (reductionMode_ == simgrid::mc::ReductionMode::unset)
 298     reductionMode_ = simgrid::mc::ReductionMode::dpor;
 299
 300   if (_sg_mc_termination)
 301     XBT_INFO("Check non progressive cycles");
 302   else
 303     XBT_INFO("Check a safety property");
 304   mc_model_checker->wait_for_requests();
 305
 306   XBT_DEBUG("Starting the safety algorithm");
 307
 308   /* Create exploration stack */
 309   mc_stack = xbt_fifo_new();
 310
 311   simgrid::mc::visited_states.clear();
 312
 313   simgrid::mc::State* initial_state = MC_state_new();
 314
 315   XBT_DEBUG("**************************************************");
 316   XBT_DEBUG("Initial state");
 317
 318   /* Wait for requests (schedules processes) */
 319   mc_model_checker->wait_for_requests();
 320
 321   /* Get an enabled process and insert it in the interleave set of the initial state */
 322   for (auto& p : mc_model_checker->process().simix_processes())
 323     if (simgrid::mc::process_is_enabled(&p.copy)) {
 324       MC_state_interleave_process(initial_state, &p.copy);
 325       if (reductionMode_ != simgrid::mc::ReductionMode::none)
 326         break;
 327     }
 328
 329   xbt_fifo_unshift(mc_stack, initial_state);
 330
 331   /* Save the initial state */
 332   initial_global_state = std::unique_ptr<s_mc_global_t>(new s_mc_global_t());
 333   initial_global_state->snapshot = simgrid::mc::take_snapshot(0);
 334 }
 335
 336 SafetyChecker::SafetyChecker(Session& session) : Checker(session)
 337 {
 338 }
 339
 340 SafetyChecker::~SafetyChecker()
 341 {
 342 }
 343
 344 }
 345 }