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 static int is_exploration_stack_state(mc_state_t current_state){
  19
  20   xbt_fifo_item_t item;
  21   mc_state_t stack_state;
  22   for(item = xbt_fifo_get_first_item(mc_stack); item != NULL; item = xbt_fifo_get_next_item(item)) {
  23     stack_state = (mc_state_t) xbt_fifo_get_item_content(item);
  24     if(snapshot_compare(stack_state, current_state) == 0){
  25       XBT_INFO("Non-progressive cycle : state %d -> state %d", stack_state->num, current_state->num);
  26       return 1;
  27     }
  28   }
  29   return 0;
  30 }
  31
  32 /**
  33  *  \brief Initialize the DPOR exploration algorithm
  34  */
  35 void MC_pre_modelcheck_safety()
  36 {
  37
  38   int mc_mem_set = (mmalloc_get_current_heap() == mc_heap);
  39
  40   mc_state_t initial_state = NULL;
  41   smx_process_t process;
  42
  43   /* Create the initial state and push it into the exploration stack */
  44   if (!mc_mem_set)
  45     MC_SET_MC_HEAP;
  46
  47   if (_sg_mc_visited > 0)
  48     visited_states = xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp);
  49
  50   initial_state = MC_state_new();
  51
  52   MC_SET_STD_HEAP;
  53
  54   XBT_DEBUG("**************************************************");
  55   XBT_DEBUG("Initial state");
  56
  57   /* Wait for requests (schedules processes) */
  58   MC_wait_for_requests();
  59
  60   MC_SET_MC_HEAP;
  61
  62   /* Get an enabled process and insert it in the interleave set of the initial state */
  63   xbt_swag_foreach(process, simix_global->process_list) {
  64     if (MC_process_is_enabled(process)) {
  65       MC_state_interleave_process(initial_state, process);
  66       if (mc_reduce_kind != e_mc_reduce_none)
  67         break;
  68     }
  69   }
  70
  71   xbt_fifo_unshift(mc_stack, initial_state);
  72
  73   if (!mc_mem_set)
  74     MC_SET_STD_HEAP;
  75 }
  76
  77
  78 /** \brief Model-check the application using a DFS exploration
  79  *         with DPOR (Dynamic Partial Order Reductions)
  80  */
  81 void MC_modelcheck_safety(void)
  82 {
  83
  84   char *req_str = NULL;
  85   int value;
  86   smx_simcall_t req = NULL, prev_req = NULL;
  87   mc_state_t state = NULL, prev_state = NULL, next_state = NULL;
  88   smx_process_t process = NULL;
  89   xbt_fifo_item_t item = NULL;
  90   mc_visited_state_t visited_state = NULL;
  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 == NULL) {
 110
 111       char* req_str = MC_request_to_string(req, value);
 112       XBT_DEBUG("Execute: %s", req_str);
 113       xbt_free(req_str);
 114
 115       if (dot_output != NULL) {
 116         MC_SET_MC_HEAP;
 117         req_str = MC_request_get_dot_output(req, value);
 118         MC_SET_STD_HEAP;
 119       }
 120
 121       MC_state_set_executed_request(state, req, value);
 122       mc_stats->executed_transitions++;
 123
 124       /* Answer the request */
 125       SIMIX_simcall_handle(req, value);
 126
 127       /* Wait for requests (schedules processes) */
 128       MC_wait_for_requests();
 129
 130       /* Create the new expanded state */
 131       MC_SET_MC_HEAP;
 132
 133       next_state = MC_state_new();
 134
 135       if(_sg_mc_termination && is_exploration_stack_state(next_state)){
 136           MC_show_non_termination();
 137           return;
 138       }
 139
 140       if ((visited_state = is_visited_state(next_state)) == NULL) {
 141
 142         /* Get an enabled process and insert it in the interleave set of the next state */
 143         xbt_swag_foreach(process, simix_global->process_list) {
 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 != NULL)
 152           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str);
 153
 154       } else {
 155
 156         if (dot_output != NULL)
 157           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 != NULL)
 164         xbt_free(req_str);
 165
 166       MC_SET_STD_HEAP;
 167
 168       /* Let's loop again */
 169
 170       /* The interleave set is empty or the maximum depth is reached, let's back-track */
 171     } else {
 172
 173       if ((xbt_fifo_size(mc_stack) > _sg_mc_max_depth) || user_max_depth_reached || visited_state != NULL) {
 174
 175         if (user_max_depth_reached && visited_state == NULL)
 176           XBT_DEBUG("User max depth reached !");
 177         else if (visited_state == NULL)
 178           XBT_WARN("/!\\ Max depth reached ! /!\\ ");
 179         else
 180           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);
 181
 182       } else {
 183
 184         XBT_DEBUG("There are no more processes to interleave. (depth %d)", xbt_fifo_size(mc_stack) + 1);
 185
 186       }
 187
 188       MC_SET_MC_HEAP;
 189
 190       /* Trash the current state, no longer needed */
 191       xbt_fifo_shift(mc_stack);
 192       MC_state_delete(state, !state->in_visited_states ? 1 : 0);
 193       XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
 194
 195       MC_SET_STD_HEAP;
 196
 197       visited_state = NULL;
 198
 199       /* Check for deadlocks */
 200       if (MC_deadlock_check()) {
 201         MC_show_deadlock(NULL);
 202         return;
 203       }
 204
 205       MC_SET_MC_HEAP;
 206       /* Traverse the stack backwards until a state with a non empty interleave
 207          set is found, deleting all the states that have it empty in the way.
 208          For each deleted state, check if the request that has generated it
 209          (from it's predecesor state), depends on any other previous request
 210          executed before it. If it does then add it to the interleave set of the
 211          state that executed that previous request. */
 212
 213       while ((state = xbt_fifo_shift(mc_stack)) != NULL) {
 214         if (mc_reduce_kind == e_mc_reduce_dpor) {
 215           req = MC_state_get_internal_request(state);
 216           xbt_fifo_foreach(mc_stack, item, prev_state, mc_state_t) {
 217             if (MC_request_depend(req, MC_state_get_internal_request(prev_state))) {
 218               if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
 219                 XBT_DEBUG("Dependent Transitions:");
 220                 prev_req = MC_state_get_executed_request(prev_state, &value);
 221                 req_str = MC_request_to_string(prev_req, value);
 222                 XBT_DEBUG("%s (state=%d)", req_str, prev_state->num);
 223                 xbt_free(req_str);
 224                 prev_req = MC_state_get_executed_request(state, &value);
 225                 req_str = MC_request_to_string(prev_req, value);
 226                 XBT_DEBUG("%s (state=%d)", req_str, state->num);
 227                 xbt_free(req_str);
 228               }
 229
 230               if (!MC_state_process_is_done(prev_state, req->issuer))
 231                 MC_state_interleave_process(prev_state, req->issuer);
 232               else
 233                 XBT_DEBUG("Process %p is in done set", req->issuer);
 234
 235               break;
 236
 237             } else if (req->issuer == MC_state_get_internal_request(prev_state)->issuer) {
 238
 239               XBT_DEBUG("Simcall %d and %d with same issuer", req->call, MC_state_get_internal_request(prev_state)->call);
 240               break;
 241
 242             } else {
 243
 244               XBT_DEBUG("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant",
 245                         req->call, req->issuer->pid, state->num,
 246                         MC_state_get_internal_request(prev_state)->call,
 247                         MC_state_get_internal_request(prev_state)->issuer->pid,
 248                         prev_state->num);
 249
 250             }
 251           }
 252         }
 253
 254         if (MC_state_interleave_size(state) && xbt_fifo_size(mc_stack) < _sg_mc_max_depth) {
 255           /* We found a back-tracking point, let's loop */
 256           XBT_DEBUG("Back-tracking to state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
 257           xbt_fifo_unshift(mc_stack, state);
 258           MC_replay(mc_stack);
 259           XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num, xbt_fifo_size(mc_stack));
 260           break;
 261         } else {
 262           XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
 263           MC_state_delete(state, !state->in_visited_states ? 1 : 0);
 264         }
 265       }
 266       MC_SET_STD_HEAP;
 267     }
 268   }
 269   MC_print_statistics(mc_stats);
 270   MC_SET_STD_HEAP;
 271
 272   return;
 273 }