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
 119       MC_state_set_executed_request(state, req, value);
 120       mc_stats->executed_transitions++;
 121
 122       // TODO, bundle both operations in a single message
 123       //   MC_execute_transition(req, value)
 124
 125       /* Answer the request */
 126       MC_simcall_handle(req, value);
 127       mc_model_checker->wait_for_requests();
 128
 129       /* Create the new expanded state */
 130       next_state = MC_state_new();
 131
 132       if(_sg_mc_termination && is_exploration_stack_state(next_state)){
 133           MC_show_non_termination();
 134           return SIMGRID_MC_EXIT_NON_TERMINATION;
 135       }
 136
 137       if ((visited_state = is_visited_state(next_state)) == nullptr) {
 138
 139         /* Get an enabled process and insert it in the interleave set of the next state */
 140         for (auto& p : mc_model_checker->process().simix_processes())
 141           if (MC_process_is_enabled(&p.copy)) {
 142             MC_state_interleave_process(next_state, &p.copy);
 143             if (mc_reduce_kind != e_mc_reduce_none)
 144               break;
 145           }
 146
 147         if (dot_output != nullptr)
 148           std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str);
 149
 150       } else {
 151
 152         if (dot_output != nullptr)
 153           std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str);
 154
 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
 178         XBT_DEBUG("There are no more processes to interleave. (depth %d)", xbt_fifo_size(mc_stack) + 1);
 179
 180       }
 181
 182       /* Trash the current state, no longer needed */
 183       xbt_fifo_shift(mc_stack);
 184       XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
 185       MC_state_delete(state, !state->in_visited_states ? 1 : 0);
 186
 187       visited_state = nullptr;
 188
 189       /* Check for deadlocks */
 190       if (MC_deadlock_check()) {
 191         MC_show_deadlock(nullptr);
 192         return SIMGRID_MC_EXIT_DEADLOCK;
 193       }
 194
 195       /* Traverse the stack backwards until a state with a non empty interleave
 196          set is found, deleting all the states that have it empty in the way.
 197          For each deleted state, check if the request that has generated it
 198          (from it's predecesor state), depends on any other previous request
 199          executed before it. If it does then add it to the interleave set of the
 200          state that executed that previous request. */
 201
 202       while ((state = (mc_state_t) xbt_fifo_shift(mc_stack))) {
 203         if (mc_reduce_kind == e_mc_reduce_dpor) {
 204           req = MC_state_get_internal_request(state);
 205           if (req->call == SIMCALL_MUTEX_LOCK || req->call == SIMCALL_MUTEX_TRYLOCK)
 206             xbt_die("Mutex is currently not supported with DPOR, "
 207               "use --cfg=model-check/reduction:none");
 208           const smx_process_t issuer = MC_smx_simcall_get_issuer(req);
 209           xbt_fifo_foreach(mc_stack, item, prev_state, mc_state_t) {
 210             if (MC_request_depend(req, MC_state_get_internal_request(prev_state))) {
 211               if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
 212                 XBT_DEBUG("Dependent Transitions:");
 213                 smx_simcall_t prev_req = MC_state_get_executed_request(prev_state, &value);
 214                 req_str = MC_request_to_string(prev_req, value, MC_REQUEST_INTERNAL);
 215                 XBT_DEBUG("%s (state=%d)", req_str, prev_state->num);
 216                 xbt_free(req_str);
 217                 prev_req = MC_state_get_executed_request(state, &value);
 218                 req_str = MC_request_to_string(prev_req, value, MC_REQUEST_EXECUTED);
 219                 XBT_DEBUG("%s (state=%d)", req_str, state->num);
 220                 xbt_free(req_str);
 221               }
 222
 223               if (!MC_state_process_is_done(prev_state, issuer))
 224                 MC_state_interleave_process(prev_state, issuer);
 225               else
 226                 XBT_DEBUG("Process %p is in done set", req->issuer);
 227
 228               break;
 229
 230             } else if (req->issuer == MC_state_get_internal_request(prev_state)->issuer) {
 231
 232               XBT_DEBUG("Simcall %d and %d with same issuer", req->call, MC_state_get_internal_request(prev_state)->call);
 233               break;
 234
 235             } else {
 236
 237               const smx_process_t previous_issuer = MC_smx_simcall_get_issuer(MC_state_get_internal_request(prev_state));
 238               XBT_DEBUG("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant",
 239                         req->call, issuer->pid, state->num,
 240                         MC_state_get_internal_request(prev_state)->call,
 241                         previous_issuer->pid,
 242                         prev_state->num);
 243
 244             }
 245           }
 246         }
 247
 248         if (MC_state_interleave_size(state) && xbt_fifo_size(mc_stack) < _sg_mc_max_depth) {
 249           /* We found a back-tracking point, let's loop */
 250           XBT_DEBUG("Back-tracking to state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
 251           xbt_fifo_unshift(mc_stack, state);
 252           MC_replay(mc_stack);
 253           XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num, xbt_fifo_size(mc_stack));
 254           break;
 255         } else {
 256           XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
 257           MC_state_delete(state, !state->in_visited_states ? 1 : 0);
 258         }
 259       }
 260     }
 261   }
 262
 263   XBT_INFO("No property violation found.");
 264   MC_print_statistics(mc_stats);
 265   return SIMGRID_MC_EXIT_SUCCESS;
 266 }
 267
 268 static void MC_modelcheck_safety_init(void)
 269 {
 270   if(_sg_mc_termination)
 271     mc_reduce_kind = e_mc_reduce_none;
 272   else if (mc_reduce_kind == e_mc_reduce_unset)
 273     mc_reduce_kind = e_mc_reduce_dpor;
 274   _sg_mc_safety = 1;
 275   if (_sg_mc_termination)
 276     XBT_INFO("Check non progressive cycles");
 277   else
 278     XBT_INFO("Check a safety property");
 279   mc_model_checker->wait_for_requests();
 280
 281   XBT_DEBUG("Starting the safety algorithm");
 282
 283   _sg_mc_safety = 1;
 284
 285   /* Create exploration stack */
 286   mc_stack = xbt_fifo_new();
 287
 288   MC_pre_modelcheck_safety();
 289
 290   /* Save the initial state */
 291   initial_global_state = xbt_new0(s_mc_global_t, 1);
 292   initial_global_state->snapshot = simgrid::mc::take_snapshot(0);
 293 }