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