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