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