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