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