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