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