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