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