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