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