src/mc/mc_safety.c

   1 /* Copyright (c) 2008-2014. 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 "mc_state.h"
   8 #include "mc_request.h"
   9 #include "mc_safety.h"
  10 #include "mc_private.h"
  11 #include "mc_record.h"
  12
  13 #include "xbt/mmalloc/mmprivate.h"
  14
  15 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_safety, mc,
  16                                 "Logging specific to MC safety verification ");
  17
  18 /**
  19  *  \brief Initialize the DPOR exploration algorithm
  20  */
  21 void MC_pre_modelcheck_safety()
  22 {
  23
  24   int mc_mem_set = (mmalloc_get_current_heap() == mc_heap);
  25
  26   mc_state_t initial_state = NULL;
  27   smx_process_t process;
  28
  29   /* Create the initial state and push it into the exploration stack */
  30   if (!mc_mem_set)
  31     MC_SET_MC_HEAP;
  32
  33   if (_sg_mc_visited > 0)
  34     visited_states = xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp);
  35
  36   initial_state = MC_state_new();
  37
  38   MC_SET_STD_HEAP;
  39
  40   XBT_DEBUG("**************************************************");
  41   XBT_DEBUG("Initial state");
  42
  43   /* Wait for requests (schedules processes) */
  44   MC_wait_for_requests();
  45
  46   MC_SET_MC_HEAP;
  47
  48   /* Get an enabled process and insert it in the interleave set of the initial state */
  49   xbt_swag_foreach(process, simix_global->process_list) {
  50     if (MC_process_is_enabled(process)) {
  51       MC_state_interleave_process(initial_state, process);
  52       if (mc_reduce_kind != e_mc_reduce_none)
  53         break;
  54     }
  55   }
  56
  57   xbt_fifo_unshift(mc_stack, initial_state);
  58
  59   if (!mc_mem_set)
  60     MC_SET_STD_HEAP;
  61 }
  62
  63
  64 /** \brief Model-check the application using a DFS exploration
  65  *         with DPOR (Dynamic Partial Order Reductions)
  66  */
  67 void MC_modelcheck_safety(void)
  68 {
  69
  70   char *req_str = NULL;
  71   int value;
  72   smx_simcall_t req = NULL, prev_req = NULL;
  73   mc_state_t state = NULL, prev_state = NULL, next_state = NULL;
  74   smx_process_t process = NULL;
  75   xbt_fifo_item_t item = NULL;
  76   mc_visited_state_t visited_state = NULL;
  77
  78   while (xbt_fifo_size(mc_stack) > 0) {
  79
  80     /* Get current state */
  81     state = (mc_state_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
  82
  83     XBT_DEBUG("**************************************************");
  84     XBT_DEBUG
  85         ("Exploration depth=%d (state=%p, num %d)(%u interleave, user_max_depth %d)",
  86          xbt_fifo_size(mc_stack), state, state->num,
  87          MC_state_interleave_size(state), user_max_depth_reached);
  88
  89     /* Update statistics */
  90     mc_stats->visited_states++;
  91
  92     /* If there are processes to interleave and the maximum depth has not been reached
  93        then perform one step of the exploration algorithm */
  94     if (xbt_fifo_size(mc_stack) <= _sg_mc_max_depth && !user_max_depth_reached
  95         && (req = MC_state_get_request(state, &value)) && visited_state == NULL) {
  96
  97       char* req_str = MC_request_to_string(req, value);
  98       XBT_DEBUG("Execute: %s", req_str);
  99       xbt_free(req_str);
 100
 101       if (dot_output != NULL) {
 102         MC_SET_MC_HEAP;
 103         req_str = MC_request_get_dot_output(req, value);
 104         MC_SET_STD_HEAP;
 105       }
 106
 107       MC_state_set_executed_request(state, req, value);
 108       mc_stats->executed_transitions++;
 109
 110       /* Answer the request */
 111       SIMIX_simcall_handle(req, value);
 112
 113       /* Wait for requests (schedules processes) */
 114       MC_wait_for_requests();
 115
 116       /* Create the new expanded state */
 117       MC_SET_MC_HEAP;
 118
 119       next_state = MC_state_new();
 120
 121       if ((visited_state = is_visited_state(next_state)) == NULL) {
 122
 123         /* Get an enabled process and insert it in the interleave set of the next state */
 124         xbt_swag_foreach(process, simix_global->process_list) {
 125           if (MC_process_is_enabled(process)) {
 126             MC_state_interleave_process(next_state, process);
 127             if (mc_reduce_kind != e_mc_reduce_none)
 128               break;
 129           }
 130         }
 131
 132         if (dot_output != NULL)
 133           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str);
 134
 135       } else {
 136
 137         if (dot_output != NULL)
 138           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str);
 139
 140       }
 141
 142       xbt_fifo_unshift(mc_stack, next_state);
 143
 144       if (dot_output != NULL)
 145         xbt_free(req_str);
 146
 147       MC_SET_STD_HEAP;
 148
 149       /* Let's loop again */
 150
 151       /* The interleave set is empty or the maximum depth is reached, let's back-track */
 152     } else {
 153
 154       if ((xbt_fifo_size(mc_stack) > _sg_mc_max_depth) || user_max_depth_reached || visited_state != NULL) {
 155
 156         if (user_max_depth_reached && visited_state == NULL)
 157           XBT_DEBUG("User max depth reached !");
 158         else if (visited_state == NULL)
 159           XBT_WARN("/!\\ Max depth reached ! /!\\ ");
 160         else
 161           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);
 162
 163       } else {
 164
 165         XBT_DEBUG("There are no more processes to interleave. (depth %d)", xbt_fifo_size(mc_stack) + 1);
 166
 167       }
 168
 169       MC_SET_MC_HEAP;
 170
 171       /* Trash the current state, no longer needed */
 172       xbt_fifo_shift(mc_stack);
 173       MC_state_delete(state, !state->in_visited_states ? 1 : 0);
 174       XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
 175
 176       MC_SET_STD_HEAP;
 177
 178       visited_state = NULL;
 179
 180       /* Check for deadlocks */
 181       if (MC_deadlock_check()) {
 182         MC_show_deadlock(NULL);
 183         return;
 184       }
 185
 186       MC_SET_MC_HEAP;
 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 = xbt_fifo_shift(mc_stack)) != NULL) {
 195         if (mc_reduce_kind == e_mc_reduce_dpor) {
 196           req = MC_state_get_internal_request(state);
 197           xbt_fifo_foreach(mc_stack, item, prev_state, mc_state_t) {
 198             if (MC_request_depend(req, MC_state_get_internal_request(prev_state))) {
 199               if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
 200                 XBT_DEBUG("Dependent Transitions:");
 201                 prev_req = MC_state_get_executed_request(prev_state, &value);
 202                 req_str = MC_request_to_string(prev_req, value);
 203                 XBT_DEBUG("%s (state=%d)", req_str, prev_state->num);
 204                 xbt_free(req_str);
 205                 prev_req = MC_state_get_executed_request(state, &value);
 206                 req_str = MC_request_to_string(prev_req, value);
 207                 XBT_DEBUG("%s (state=%d)", req_str, state->num);
 208                 xbt_free(req_str);
 209               }
 210
 211               if (!MC_state_process_is_done(prev_state, req->issuer))
 212                 MC_state_interleave_process(prev_state, req->issuer);
 213               else
 214                 XBT_DEBUG("Process %p is in done set", req->issuer);
 215
 216               break;
 217
 218             } else if (req->issuer == MC_state_get_internal_request(prev_state)->issuer) {
 219
 220               XBT_DEBUG("Simcall %d and %d with same issuer", req->call, MC_state_get_internal_request(prev_state)->call);
 221               break;
 222
 223             } else {
 224
 225               XBT_DEBUG("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant",
 226                         req->call, req->issuer->pid, state->num,
 227                         MC_state_get_internal_request(prev_state)->call,
 228                         MC_state_get_internal_request(prev_state)->issuer->pid,
 229                         prev_state->num);
 230
 231             }
 232           }
 233         }
 234
 235         if (MC_state_interleave_size(state) && xbt_fifo_size(mc_stack) < _sg_mc_max_depth) {
 236           /* We found a back-tracking point, let's loop */
 237           XBT_DEBUG("Back-tracking to state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
 238           xbt_fifo_unshift(mc_stack, state);
 239           MC_replay(mc_stack);
 240           XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num, xbt_fifo_size(mc_stack));
 241           break;
 242         } else {
 243           XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
 244           MC_state_delete(state, !state->in_visited_states ? 1 : 0);
 245         }
 246       }
 247       MC_SET_STD_HEAP;
 248     }
 249   }
 250   MC_print_statistics(mc_stats);
 251   MC_SET_STD_HEAP;
 252
 253   return;
 254 }