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