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