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