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       MC_LOG_REQUEST(mc_safety, req, value);
 121
 122       if (dot_output != NULL) {
 123         MC_SET_MC_HEAP;
 124         req_str = MC_request_get_dot_output(req, value);
 125         MC_SET_STD_HEAP;
 126       }
 127
 128       MC_state_set_executed_request(state, req, value);
 129       mc_stats->executed_transitions++;
 130
 131       if (mc_reduce_kind == e_mc_reduce_dpor) {
 132         MC_SET_MC_HEAP;
 133         char *key = bprintf("%lu", req->issuer->pid);
 134         xbt_dict_remove(first_enabled_state, key);
 135         xbt_free(key);
 136         MC_SET_STD_HEAP;
 137       }
 138
 139       /* Answer the request */
 140       SIMIX_simcall_handle(req, value);
 141
 142       /* Wait for requests (schedules processes) */
 143       MC_wait_for_requests();
 144
 145       /* Create the new expanded state */
 146       MC_SET_MC_HEAP;
 147
 148       next_state = MC_state_new();
 149
 150       if ((visited_state = is_visited_state()) == NULL) {
 151
 152         /* Get an enabled process and insert it in the interleave set of the next state */
 153         xbt_swag_foreach(process, simix_global->process_list) {
 154           if (MC_process_is_enabled(process)) {
 155             MC_state_interleave_process(next_state, process);
 156             if (mc_reduce_kind != e_mc_reduce_none)
 157               break;
 158           }
 159         }
 160
 161         if (_sg_mc_checkpoint
 162             && ((xbt_fifo_size(mc_stack) + 1) % _sg_mc_checkpoint == 0)) {
 163           next_state->system_state = MC_take_snapshot(next_state->num);
 164         }
 165
 166         if (dot_output != NULL)
 167           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num,
 168                   next_state->num, req_str);
 169
 170       } else {
 171
 172         if (dot_output != NULL)
 173           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num,
 174                   visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str);
 175
 176       }
 177
 178       xbt_fifo_unshift(mc_stack, next_state);
 179
 180       if (mc_reduce_kind == e_mc_reduce_dpor) {
 181         /* Insert in dict all enabled processes, if not included yet */
 182         xbt_swag_foreach(process, simix_global->process_list) {
 183           if (MC_process_is_enabled(process)) {
 184             char *key = bprintf("%lu", process->pid);
 185             if (xbt_dict_get_or_null(first_enabled_state, key) == NULL) {
 186               char *data = bprintf("%d", xbt_fifo_size(mc_stack));
 187               xbt_dict_set(first_enabled_state, key, data, NULL);
 188             }
 189             xbt_free(key);
 190           }
 191         }
 192       }
 193
 194       if (dot_output != NULL)
 195         xbt_free(req_str);
 196
 197       MC_SET_STD_HEAP;
 198
 199       /* Let's loop again */
 200
 201       /* The interleave set is empty or the maximum depth is reached, let's back-track */
 202     } else {
 203
 204       if ((xbt_fifo_size(mc_stack) > _sg_mc_max_depth) || user_max_depth_reached
 205           || visited_state != NULL) {
 206
 207         if (user_max_depth_reached && visited_state == NULL)
 208           XBT_DEBUG("User max depth reached !");
 209         else if (visited_state == NULL)
 210           XBT_WARN("/!\\ Max depth reached ! /!\\ ");
 211         else
 212           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);
 213
 214         if (mc_reduce_kind == e_mc_reduce_dpor) {
 215           /* Interleave enabled processes in the state in which they have been enabled for the first time */
 216           xbt_swag_foreach(process, simix_global->process_list) {
 217             if (MC_process_is_enabled(process)) {
 218               char *key = bprintf("%lu", process->pid);
 219               enabled =
 220                   (int) strtoul(xbt_dict_get_or_null(first_enabled_state, key),
 221                                 0, 10);
 222               xbt_free(key);
 223               int cursor = xbt_fifo_size(mc_stack);
 224               xbt_fifo_foreach(mc_stack, item, state_test, mc_state_t) {
 225                 if (cursor-- == enabled) {
 226                   if (!MC_state_process_is_done(state_test, process)
 227                       && state_test->num != state->num) {
 228                     XBT_DEBUG("Interleave process %lu in state %d",
 229                               process->pid, state_test->num);
 230                     MC_state_interleave_process(state_test, process);
 231                     break;
 232                   }
 233                 }
 234               }
 235             }
 236           }
 237         }
 238
 239       } else {
 240
 241         XBT_DEBUG("There are no more processes to interleave. (depth %d)",
 242                   xbt_fifo_size(mc_stack) + 1);
 243
 244       }
 245
 246       MC_SET_MC_HEAP;
 247
 248       /* Trash the current state, no longer needed */
 249       xbt_fifo_shift(mc_stack);
 250       MC_state_delete(state);
 251       XBT_DEBUG("Delete state %d at depth %d", state->num,
 252                 xbt_fifo_size(mc_stack) + 1);
 253
 254       MC_SET_STD_HEAP;
 255
 256       visited_state = NULL;
 257
 258       /* Check for deadlocks */
 259       if (MC_deadlock_check()) {
 260         MC_show_deadlock(NULL);
 261         return;
 262       }
 263
 264       MC_SET_MC_HEAP;
 265       /* Traverse the stack backwards until a state with a non empty interleave
 266          set is found, deleting all the states that have it empty in the way.
 267          For each deleted state, check if the request that has generated it
 268          (from it's predecesor state), depends on any other previous request
 269          executed before it. If it does then add it to the interleave set of the
 270          state that executed that previous request. */
 271
 272       while ((state = xbt_fifo_shift(mc_stack)) != NULL) {
 273         if (mc_reduce_kind == e_mc_reduce_dpor) {
 274           req = MC_state_get_internal_request(state);
 275           xbt_fifo_foreach(mc_stack, item, prev_state, mc_state_t) {
 276             if (MC_request_depend
 277                 (req, MC_state_get_internal_request(prev_state))) {
 278               if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
 279                 XBT_DEBUG("Dependent Transitions:");
 280                 prev_req = MC_state_get_executed_request(prev_state, &value);
 281                 req_str = MC_request_to_string(prev_req, value);
 282                 XBT_DEBUG("%s (state=%d)", req_str, prev_state->num);
 283                 xbt_free(req_str);
 284                 prev_req = MC_state_get_executed_request(state, &value);
 285                 req_str = MC_request_to_string(prev_req, value);
 286                 XBT_DEBUG("%s (state=%d)", req_str, state->num);
 287                 xbt_free(req_str);
 288               }
 289
 290               if (!MC_state_process_is_done(prev_state, req->issuer))
 291                 MC_state_interleave_process(prev_state, req->issuer);
 292               else
 293                 XBT_DEBUG("Process %p is in done set", req->issuer);
 294
 295               break;
 296
 297             } else if (req->issuer ==
 298                        MC_state_get_internal_request(prev_state)->issuer) {
 299
 300               XBT_DEBUG("Simcall %d and %d with same issuer", req->call,
 301                         MC_state_get_internal_request(prev_state)->call);
 302               break;
 303
 304             } else {
 305
 306               XBT_DEBUG
 307                   ("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant",
 308                    req->call, req->issuer->pid, state->num,
 309                    MC_state_get_internal_request(prev_state)->call,
 310                    MC_state_get_internal_request(prev_state)->issuer->pid,
 311                    prev_state->num);
 312
 313             }
 314           }
 315         }
 316
 317         if (MC_state_interleave_size(state)
 318             && xbt_fifo_size(mc_stack) < _sg_mc_max_depth) {
 319           /* We found a back-tracking point, let's loop */
 320           XBT_DEBUG("Back-tracking to state %d at depth %d", state->num,
 321                     xbt_fifo_size(mc_stack) + 1);
 322           if (_sg_mc_checkpoint) {
 323             if (state->system_state != NULL) {
 324               MC_restore_snapshot(state->system_state);
 325               xbt_fifo_unshift(mc_stack, state);
 326               MC_SET_STD_HEAP;
 327             } else {
 328               pos = xbt_fifo_size(mc_stack);
 329               item = xbt_fifo_get_first_item(mc_stack);
 330               while (pos > 0) {
 331                 restored_state = (mc_state_t) xbt_fifo_get_item_content(item);
 332                 if (restored_state->system_state != NULL) {
 333                   break;
 334                 } else {
 335                   item = xbt_fifo_get_next_item(item);
 336                   pos--;
 337                 }
 338               }
 339               MC_restore_snapshot(restored_state->system_state);
 340               xbt_fifo_unshift(mc_stack, state);
 341               MC_SET_STD_HEAP;
 342               MC_replay(mc_stack, pos);
 343             }
 344           } else {
 345             xbt_fifo_unshift(mc_stack, state);
 346             MC_SET_STD_HEAP;
 347             MC_replay(mc_stack, -1);
 348           }
 349           XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num,
 350                     xbt_fifo_size(mc_stack));
 351           break;
 352         } else {
 353           XBT_DEBUG("Delete state %d at depth %d", state->num,
 354                     xbt_fifo_size(mc_stack) + 1);
 355           MC_state_delete(state);
 356         }
 357       }
 358       MC_SET_STD_HEAP;
 359     }
 360   }
 361   MC_print_statistics(mc_stats);
 362   MC_SET_STD_HEAP;
 363
 364   return;
 365 }