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   mc_visited_state_t visited_state = NULL;
  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 == NULL) {
 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_enter(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()) == NULL) {
 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->other_num == -1 ? visited_state->num : visited_state->other_num, 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 != NULL) {
 210
 211         if (user_max_depth_reached && visited_state == NULL)
 212           XBT_DEBUG("User max depth reached !");
 213         else if (visited_state == NULL)
 214           XBT_WARN("/!\\ Max depth reached ! /!\\ ");
 215         else
 216           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);
 217
 218         if (mc_reduce_kind == e_mc_reduce_dpor) {
 219           /* Interleave enabled processes in the state in which they have been enabled for the first time */
 220           xbt_swag_foreach(process, simix_global->process_list) {
 221             if (MC_process_is_enabled(process)) {
 222               char *key = bprintf("%lu", process->pid);
 223               enabled =
 224                   (int) strtoul(xbt_dict_get_or_null(first_enabled_state, key),
 225                                 0, 10);
 226               xbt_free(key);
 227               int cursor = xbt_fifo_size(mc_stack);
 228               xbt_fifo_foreach(mc_stack, item, state_test, mc_state_t) {
 229                 if (cursor-- == enabled) {
 230                   if (!MC_state_process_is_done(state_test, process)
 231                       && state_test->num != state->num) {
 232                     XBT_DEBUG("Interleave process %lu in state %d",
 233                               process->pid, state_test->num);
 234                     MC_state_interleave_process(state_test, process);
 235                     break;
 236                   }
 237                 }
 238               }
 239             }
 240           }
 241         }
 242
 243       } else {
 244
 245         XBT_DEBUG("There are no more processes to interleave. (depth %d)",
 246                   xbt_fifo_size(mc_stack) + 1);
 247
 248       }
 249
 250       MC_SET_MC_HEAP;
 251
 252       /* Trash the current state, no longer needed */
 253       xbt_fifo_shift(mc_stack);
 254       MC_state_delete(state);
 255       XBT_DEBUG("Delete state %d at depth %d", state->num,
 256                 xbt_fifo_size(mc_stack) + 1);
 257
 258       MC_SET_STD_HEAP;
 259
 260       visited_state = NULL;
 261
 262       /* Check for deadlocks */
 263       if (MC_deadlock_check()) {
 264         MC_show_deadlock(NULL);
 265         return;
 266       }
 267
 268       MC_SET_MC_HEAP;
 269       /* Traverse the stack backwards until a state with a non empty interleave
 270          set is found, deleting all the states that have it empty in the way.
 271          For each deleted state, check if the request that has generated it
 272          (from it's predecesor state), depends on any other previous request
 273          executed before it. If it does then add it to the interleave set of the
 274          state that executed that previous request. */
 275
 276       while ((state = xbt_fifo_shift(mc_stack)) != NULL) {
 277         if (mc_reduce_kind == e_mc_reduce_dpor) {
 278           req = MC_state_get_internal_request(state);
 279           xbt_fifo_foreach(mc_stack, item, prev_state, mc_state_t) {
 280             if (MC_request_depend
 281                 (req, MC_state_get_internal_request(prev_state))) {
 282               if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
 283                 XBT_DEBUG("Dependent Transitions:");
 284                 prev_req = MC_state_get_executed_request(prev_state, &value);
 285                 req_str = MC_request_to_string(prev_req, value);
 286                 XBT_DEBUG("%s (state=%d)", req_str, prev_state->num);
 287                 xbt_free(req_str);
 288                 prev_req = MC_state_get_executed_request(state, &value);
 289                 req_str = MC_request_to_string(prev_req, value);
 290                 XBT_DEBUG("%s (state=%d)", req_str, state->num);
 291                 xbt_free(req_str);
 292               }
 293
 294               if (!MC_state_process_is_done(prev_state, req->issuer))
 295                 MC_state_interleave_process(prev_state, req->issuer);
 296               else
 297                 XBT_DEBUG("Process %p is in done set", req->issuer);
 298
 299               break;
 300
 301             } else if (req->issuer ==
 302                        MC_state_get_internal_request(prev_state)->issuer) {
 303
 304               XBT_DEBUG("Simcall %d and %d with same issuer", req->call,
 305                         MC_state_get_internal_request(prev_state)->call);
 306               break;
 307
 308             } else {
 309
 310               XBT_DEBUG
 311                   ("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant",
 312                    req->call, req->issuer->pid, state->num,
 313                    MC_state_get_internal_request(prev_state)->call,
 314                    MC_state_get_internal_request(prev_state)->issuer->pid,
 315                    prev_state->num);
 316
 317             }
 318           }
 319         }
 320
 321         if (MC_state_interleave_size(state)
 322             && xbt_fifo_size(mc_stack) < _sg_mc_max_depth) {
 323           /* We found a back-tracking point, let's loop */
 324           XBT_DEBUG("Back-tracking to state %d at depth %d", state->num,
 325                     xbt_fifo_size(mc_stack) + 1);
 326           if (_sg_mc_checkpoint) {
 327             if (state->system_state != NULL) {
 328               MC_restore_snapshot(state->system_state);
 329               xbt_fifo_unshift(mc_stack, state);
 330               MC_SET_STD_HEAP;
 331             } else {
 332               pos = xbt_fifo_size(mc_stack);
 333               item = xbt_fifo_get_first_item(mc_stack);
 334               while (pos > 0) {
 335                 restored_state = (mc_state_t) xbt_fifo_get_item_content(item);
 336                 if (restored_state->system_state != NULL) {
 337                   break;
 338                 } else {
 339                   item = xbt_fifo_get_next_item(item);
 340                   pos--;
 341                 }
 342               }
 343               MC_restore_snapshot(restored_state->system_state);
 344               xbt_fifo_unshift(mc_stack, state);
 345               MC_SET_STD_HEAP;
 346               MC_replay(mc_stack, pos);
 347             }
 348           } else {
 349             xbt_fifo_unshift(mc_stack, state);
 350             MC_SET_STD_HEAP;
 351             MC_replay(mc_stack, -1);
 352           }
 353           XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num,
 354                     xbt_fifo_size(mc_stack));
 355           break;
 356         } else {
 357           XBT_DEBUG("Delete state %d at depth %d", state->num,
 358                     xbt_fifo_size(mc_stack) + 1);
 359           MC_state_delete(state);
 360         }
 361       }
 362       MC_SET_STD_HEAP;
 363     }
 364   }
 365   MC_print_statistics(mc_stats);
 366   MC_SET_STD_HEAP;
 367
 368   return;
 369 }