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