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