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_private.h"
   8
   9 #include "xbt/mmalloc/mmprivate.h"
  10
  11 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_safety, mc,
  12                                 "Logging specific to MC safety verification ");
  13
  14 xbt_dict_t first_enabled_state;
  15
  16 /**
  17  *  \brief Initialize the DPOR exploration algorithm
  18  */
  19 void MC_pre_modelcheck_safety()
  20 {
  21
  22   int mc_mem_set = (mmalloc_get_current_heap() == mc_heap);
  23
  24   mc_state_t initial_state = NULL;
  25   smx_process_t process;
  26
  27   /* Create the initial state and push it into the exploration stack */
  28   if (!mc_mem_set)
  29     MC_SET_MC_HEAP;
  30
  31   if (_sg_mc_visited > 0)
  32     visited_states =
  33         xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp);
  34
  35   if (mc_reduce_kind == e_mc_reduce_dpor)
  36     first_enabled_state = xbt_dict_new_homogeneous(&xbt_free_f);
  37
  38   initial_state = MC_state_new();
  39
  40   MC_SET_STD_HEAP;
  41
  42   XBT_DEBUG("**************************************************");
  43   XBT_DEBUG("Initial state");
  44
  45   /* Wait for requests (schedules processes) */
  46   MC_wait_for_requests();
  47
  48   if (_sg_mc_visited > 0) {
  49     MC_ignore_heap(simix_global->process_to_run->data, 0);
  50     MC_ignore_heap(simix_global->process_that_ran->data, 0);
  51   }
  52
  53   MC_SET_MC_HEAP;
  54
  55   /* Get an enabled process and insert it in the interleave set of the initial state */
  56   xbt_swag_foreach(process, simix_global->process_list) {
  57     if (MC_process_is_enabled(process)) {
  58       MC_state_interleave_process(initial_state, process);
  59       if (mc_reduce_kind != e_mc_reduce_none)
  60         break;
  61     }
  62   }
  63
  64   xbt_fifo_unshift(mc_stack, initial_state);
  65
  66   if (mc_reduce_kind == e_mc_reduce_dpor) {
  67     /* To ensure the soundness of DPOR, we have to keep a list of
  68        processes which are still enabled at each step of the exploration.
  69        If max depth is reached, we interleave them in the state in which they have
  70        been enabled for the first time. */
  71     xbt_swag_foreach(process, simix_global->process_list) {
  72       if (MC_process_is_enabled(process)) {
  73         char *key = bprintf("%lu", process->pid);
  74         char *data = bprintf("%d", xbt_fifo_size(mc_stack));
  75         xbt_dict_set(first_enabled_state, key, data, NULL);
  76         xbt_free(key);
  77       }
  78     }
  79   }
  80
  81   if (!mc_mem_set)
  82     MC_SET_STD_HEAP;
  83 }
  84
  85
  86 /** \brief Model-check the application using a DFS exploration
  87  *         with DPOR (Dynamic Partial Order Reductions)
  88  */
  89 void MC_modelcheck_safety(void)
  90 {
  91
  92   char *req_str = NULL;
  93   int value;
  94   smx_simcall_t req = NULL, prev_req = NULL;
  95   mc_state_t state = NULL, prev_state = NULL, next_state =
  96       NULL, restored_state = NULL;
  97   smx_process_t process = NULL;
  98   xbt_fifo_item_t item = NULL;
  99   mc_state_t state_test = NULL;
 100   int pos;
 101   int visited_state = -1;
 102   int enabled = 0;
 103
 104   while (xbt_fifo_size(mc_stack) > 0) {
 105
 106     /* Get current state */
 107     state = (mc_state_t)
 108         xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
 109
 110     XBT_DEBUG("**************************************************");
 111     XBT_DEBUG
 112         ("Exploration depth=%d (state=%p, num %d)(%u interleave, user_max_depth %d, first_enabled_state size : %d)",
 113          xbt_fifo_size(mc_stack), state, state->num,
 114          MC_state_interleave_size(state), user_max_depth_reached,
 115          xbt_dict_size(first_enabled_state));
 116
 117     /* Update statistics */
 118     mc_stats->visited_states++;
 119
 120     /* If there are processes to interleave and the maximum depth has not been reached
 121        then perform one step of the exploration algorithm */
 122     if (xbt_fifo_size(mc_stack) <= _sg_mc_max_depth && !user_max_depth_reached
 123         && (req = MC_state_get_request(state, &value)) && visited_state == -1) {
 124
 125       /* Debug information */
 126       if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
 127         req_str = MC_request_to_string(req, value);
 128         XBT_DEBUG("Execute: %s", req_str);
 129         xbt_free(req_str);
 130       }
 131
 132       MC_SET_MC_HEAP;
 133       if (dot_output != NULL)
 134         req_str = MC_request_get_dot_output(req, value);
 135       MC_SET_STD_HEAP;
 136
 137       MC_state_set_executed_request(state, req, value);
 138       mc_stats->executed_transitions++;
 139
 140       if (mc_reduce_kind == e_mc_reduce_dpor) {
 141         MC_SET_MC_HEAP;
 142         char *key = bprintf("%lu", req->issuer->pid);
 143         xbt_dict_remove(first_enabled_state, key);
 144         xbt_free(key);
 145         MC_SET_STD_HEAP;
 146       }
 147
 148       /* Answer the request */
 149       SIMIX_simcall_pre(req, value);
 150
 151       /* Wait for requests (schedules processes) */
 152       MC_wait_for_requests();
 153
 154       /* Create the new expanded state */
 155       MC_SET_MC_HEAP;
 156
 157       next_state = MC_state_new();
 158
 159       if ((visited_state = is_visited_state()) == -1) {
 160
 161         /* Get an enabled process and insert it in the interleave set of the next state */
 162         xbt_swag_foreach(process, simix_global->process_list) {
 163           if (MC_process_is_enabled(process)) {
 164             MC_state_interleave_process(next_state, process);
 165             if (mc_reduce_kind != e_mc_reduce_none)
 166               break;
 167           }
 168         }
 169
 170         if (_sg_mc_checkpoint
 171             && ((xbt_fifo_size(mc_stack) + 1) % _sg_mc_checkpoint == 0)) {
 172           next_state->system_state = MC_take_snapshot(next_state->num);
 173         }
 174
 175         if (dot_output != NULL)
 176           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num,
 177                   next_state->num, req_str);
 178
 179       } else {
 180
 181         if (dot_output != NULL)
 182           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num,
 183                   visited_state, req_str);
 184
 185       }
 186
 187       xbt_fifo_unshift(mc_stack, next_state);
 188
 189       if (mc_reduce_kind == e_mc_reduce_dpor) {
 190         /* Insert in dict all enabled processes, if not included yet */
 191         xbt_swag_foreach(process, simix_global->process_list) {
 192           if (MC_process_is_enabled(process)) {
 193             char *key = bprintf("%lu", process->pid);
 194             if (xbt_dict_get_or_null(first_enabled_state, key) == NULL) {
 195               char *data = bprintf("%d", xbt_fifo_size(mc_stack));
 196               xbt_dict_set(first_enabled_state, key, data, NULL);
 197             }
 198             xbt_free(key);
 199           }
 200         }
 201       }
 202
 203       if (dot_output != NULL)
 204         xbt_free(req_str);
 205
 206       MC_SET_STD_HEAP;
 207
 208       /* Let's loop again */
 209
 210       /* The interleave set is empty or the maximum depth is reached, let's back-track */
 211     } else {
 212
 213       if ((xbt_fifo_size(mc_stack) > _sg_mc_max_depth) || user_max_depth_reached
 214           || visited_state != -1) {
 215
 216         if (user_max_depth_reached && visited_state == -1)
 217           XBT_DEBUG("User max depth reached !");
 218         else if (visited_state == -1)
 219           XBT_WARN("/!\\ Max depth reached ! /!\\ ");
 220
 221         if (mc_reduce_kind == e_mc_reduce_dpor) {
 222           /* Interleave enabled processes in the state in which they have been enabled for the first time */
 223           xbt_swag_foreach(process, simix_global->process_list) {
 224             if (MC_process_is_enabled(process)) {
 225               char *key = bprintf("%lu", process->pid);
 226               enabled =
 227                   (int) strtoul(xbt_dict_get_or_null(first_enabled_state, key),
 228                                 0, 10);
 229               xbt_free(key);
 230               int cursor = xbt_fifo_size(mc_stack);
 231               xbt_fifo_foreach(mc_stack, item, state_test, mc_state_t) {
 232                 if (cursor-- == enabled) {
 233                   if (!MC_state_process_is_done(state_test, process)
 234                       && state_test->num != state->num) {
 235                     XBT_DEBUG("Interleave process %lu in state %d",
 236                               process->pid, state_test->num);
 237                     MC_state_interleave_process(state_test, process);
 238                     break;
 239                   }
 240                 }
 241               }
 242             }
 243           }
 244         }
 245
 246       } else {
 247
 248         XBT_DEBUG("There are no more processes to interleave. (depth %d)",
 249                   xbt_fifo_size(mc_stack) + 1);
 250
 251       }
 252
 253       MC_SET_MC_HEAP;
 254
 255       /* Trash the current state, no longer needed */
 256       xbt_fifo_shift(mc_stack);
 257       MC_state_delete(state);
 258       XBT_DEBUG("Delete state %d at depth %d", state->num,
 259                 xbt_fifo_size(mc_stack) + 1);
 260
 261       MC_SET_STD_HEAP;
 262
 263       visited_state = -1;
 264
 265       /* Check for deadlocks */
 266       if (MC_deadlock_check()) {
 267         MC_show_deadlock(NULL);
 268         return;
 269       }
 270
 271       MC_SET_MC_HEAP;
 272       /* Traverse the stack backwards until a state with a non empty interleave
 273          set is found, deleting all the states that have it empty in the way.
 274          For each deleted state, check if the request that has generated it
 275          (from it's predecesor state), depends on any other previous request
 276          executed before it. If it does then add it to the interleave set of the
 277          state that executed that previous request. */
 278
 279       while ((state = xbt_fifo_shift(mc_stack)) != NULL) {
 280         if (mc_reduce_kind == e_mc_reduce_dpor) {
 281           req = MC_state_get_internal_request(state);
 282           xbt_fifo_foreach(mc_stack, item, prev_state, mc_state_t) {
 283             if (MC_request_depend
 284                 (req, MC_state_get_internal_request(prev_state))) {
 285               if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
 286                 XBT_DEBUG("Dependent Transitions:");
 287                 prev_req = MC_state_get_executed_request(prev_state, &value);
 288                 req_str = MC_request_to_string(prev_req, value);
 289                 XBT_DEBUG("%s (state=%d)", req_str, prev_state->num);
 290                 xbt_free(req_str);
 291                 prev_req = MC_state_get_executed_request(state, &value);
 292                 req_str = MC_request_to_string(prev_req, value);
 293                 XBT_DEBUG("%s (state=%d)", req_str, state->num);
 294                 xbt_free(req_str);
 295               }
 296
 297               if (!MC_state_process_is_done(prev_state, req->issuer))
 298                 MC_state_interleave_process(prev_state, req->issuer);
 299               else
 300                 XBT_DEBUG("Process %p is in done set", req->issuer);
 301
 302               break;
 303
 304             } else if (req->issuer ==
 305                        MC_state_get_internal_request(prev_state)->issuer) {
 306
 307               XBT_DEBUG("Simcall %d and %d with same issuer", req->call,
 308                         MC_state_get_internal_request(prev_state)->call);
 309               break;
 310
 311             } else {
 312
 313               XBT_DEBUG
 314                   ("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant",
 315                    req->call, req->issuer->pid, state->num,
 316                    MC_state_get_internal_request(prev_state)->call,
 317                    MC_state_get_internal_request(prev_state)->issuer->pid,
 318                    prev_state->num);
 319
 320             }
 321           }
 322         }
 323
 324         if (MC_state_interleave_size(state)
 325             && xbt_fifo_size(mc_stack) < _sg_mc_max_depth) {
 326           /* We found a back-tracking point, let's loop */
 327           XBT_DEBUG("Back-tracking to state %d at depth %d", state->num,
 328                     xbt_fifo_size(mc_stack) + 1);
 329           if (_sg_mc_checkpoint) {
 330             if (state->system_state != NULL) {
 331               MC_restore_snapshot(state->system_state);
 332               xbt_fifo_unshift(mc_stack, state);
 333               MC_SET_STD_HEAP;
 334             } else {
 335               pos = xbt_fifo_size(mc_stack);
 336               item = xbt_fifo_get_first_item(mc_stack);
 337               while (pos > 0) {
 338                 restored_state = (mc_state_t) xbt_fifo_get_item_content(item);
 339                 if (restored_state->system_state != NULL) {
 340                   break;
 341                 } else {
 342                   item = xbt_fifo_get_next_item(item);
 343                   pos--;
 344                 }
 345               }
 346               MC_restore_snapshot(restored_state->system_state);
 347               xbt_fifo_unshift(mc_stack, state);
 348               MC_SET_STD_HEAP;
 349               MC_replay(mc_stack, pos);
 350             }
 351           } else {
 352             xbt_fifo_unshift(mc_stack, state);
 353             MC_SET_STD_HEAP;
 354             MC_replay(mc_stack, -1);
 355           }
 356           XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num,
 357                     xbt_fifo_size(mc_stack));
 358           break;
 359         } else {
 360           XBT_DEBUG("Delete state %d at depth %d", state->num,
 361                     xbt_fifo_size(mc_stack) + 1);
 362           MC_state_delete(state);
 363         }
 364       }
 365       MC_SET_STD_HEAP;
 366     }
 367   }
 368   MC_print_statistics(mc_stats);
 369   MC_SET_STD_HEAP;
 370
 371   return;
 372 }