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