src/mc/mc_safety.cpp

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