src/mc/mc_dfs.c

   1 #include "private.h"
   2
   3 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_dfs, mc,
   4                                 "Logging specific to MC DFS exploration");
   5
   6
   7 void MC_dfs_init()
   8 {
   9   mc_transition_t trans = NULL;
  10   mc_state_t initial_state = NULL;
  11   xbt_setset_cursor_t cursor = NULL;
  12
  13   MC_SET_RAW_MEM;
  14   initial_state = MC_state_new();
  15   /* Add the state data structure for the initial state */
  16   xbt_fifo_unshift(mc_stack, initial_state);
  17   MC_UNSET_RAW_MEM;
  18
  19   DEBUG0("**************************************************");
  20   DEBUG0("Initial state");
  21
  22   /* Schedule all the processes to detect the transitions from the initial state */
  23   MC_schedule_enabled_processes();
  24
  25   MC_SET_RAW_MEM;
  26   xbt_setset_add(initial_state->enabled_transitions,
  27                  initial_state->transitions);
  28   xbt_setset_foreach(initial_state->enabled_transitions, cursor, trans) {
  29     if (trans->type == mc_wait
  30         && (trans->wait.comm->src_proc == NULL
  31             || trans->wait.comm->dst_proc == NULL)) {
  32       xbt_setset_set_remove(initial_state->enabled_transitions, trans);
  33     }
  34   }
  35
  36   /* Fill the interleave set of the initial state with all enabled transitions */
  37   xbt_setset_add(initial_state->interleave,
  38                  initial_state->enabled_transitions);
  39
  40   /* Update Statistics */
  41   mc_stats->state_size +=
  42       xbt_setset_set_size(initial_state->enabled_transitions);
  43
  44   MC_UNSET_RAW_MEM;
  45 }
  46
  47 /**
  48  *      \brief Perform the model-checking operation using a depth-first search exploration
  49  *
  50  *      It performs the model-checking operation by executing all possible scheduling of the communication actions
  51  *      \return The time spent to execute the simulation or -1 if the simulation ended
  52  */
  53 void MC_dfs(void)
  54 {
  55   mc_transition_t trans = NULL;
  56   mc_state_t current_state = NULL;
  57   mc_state_t next_state = NULL;
  58   xbt_setset_cursor_t cursor = NULL;
  59
  60   while (xbt_fifo_size(mc_stack) > 0) {
  61     DEBUG0("**************************************************");
  62
  63     /* FIXME: Think about what happens if there are no transitions but there are
  64        some actions on the models. (ex. all the processes do a sleep(0) in a round). */
  65
  66     /* Get current state */
  67     current_state = (mc_state_t)
  68         xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
  69
  70     /* If there are transitions to execute and the maximun depth has not been reached
  71        then perform one step of the exploration algorithm */
  72     if (xbt_setset_set_size(current_state->interleave) > 0
  73         && xbt_fifo_size(mc_stack) < MAX_DEPTH) {
  74
  75       DEBUG3("Exploration detph=%d (state=%p)(%d transitions)",
  76              xbt_fifo_size(mc_stack), current_state,
  77              xbt_setset_set_size(current_state->interleave));
  78
  79       /* Update statistics */
  80       mc_stats->visited_states++;
  81       mc_stats->executed_transitions++;
  82
  83       /* Choose a transition to execute from the interleave set of the current state,
  84          and create the data structures for the new expanded state in the exploration
  85          stack. */
  86       MC_SET_RAW_MEM;
  87       trans = xbt_setset_set_extract(current_state->interleave);
  88
  89       /* Define it as the executed transition of this state */
  90       current_state->executed_transition = trans;
  91
  92       next_state = MC_state_new();
  93       xbt_fifo_unshift(mc_stack, next_state);
  94       MC_UNSET_RAW_MEM;
  95
  96       DEBUG1("Executing transition %s", trans->name);
  97       SIMIX_process_schedule(trans->process);
  98
  99       /* Do all surf's related black magic tricks to keep all working */
 100       MC_execute_surf_actions();
 101
 102       /* Schedule every process that got enabled due to the executed transition */
 103       MC_schedule_enabled_processes();
 104
 105       /* Calculate the enabled transitions set of the next state:
 106          -add the transition sets of the current state and the next state
 107          -remove the executed transition from that set
 108          -remove all the transitions that are disabled (mc_wait only)
 109          -use the resulting set as the enabled transitions of the next state */
 110       MC_SET_RAW_MEM;
 111       xbt_setset_add(next_state->transitions, current_state->transitions);
 112       xbt_setset_set_remove(next_state->transitions, trans);
 113       xbt_setset_add(next_state->enabled_transitions,
 114                      next_state->transitions);
 115       xbt_setset_foreach(next_state->enabled_transitions, cursor, trans) {
 116         if (trans->type == mc_wait
 117             && (trans->wait.comm->src_proc == NULL
 118                 || trans->wait.comm->dst_proc == NULL)) {
 119           xbt_setset_set_remove(next_state->enabled_transitions, trans);
 120         }
 121       }
 122
 123       /* Fill the interleave set of the new state with all enabled transitions */
 124       xbt_setset_add(next_state->interleave,
 125                      next_state->enabled_transitions);
 126       MC_UNSET_RAW_MEM;
 127
 128       /* Update Statistics */
 129       mc_stats->state_size +=
 130           xbt_setset_set_size(next_state->enabled_transitions);
 131
 132       /* Let's loop again */
 133
 134       /* The interleave set is empty or the maximum depth is reached, let's back-track */
 135     } else {
 136       DEBUG0("There are no more actions to run");
 137
 138       MC_SET_RAW_MEM;
 139       xbt_fifo_shift(mc_stack);
 140       MC_state_delete(current_state);
 141
 142       /* Go backwards in the stack until we find a state with transitions in the interleave set */
 143       while (xbt_fifo_size(mc_stack) > 0
 144              && (current_state = (mc_state_t) xbt_fifo_shift(mc_stack))) {
 145         if (xbt_setset_set_size(current_state->interleave) == 0) {
 146           MC_state_delete(current_state);
 147         } else {
 148           xbt_fifo_unshift(mc_stack, current_state);
 149           DEBUG1("Back-tracking to depth %d", xbt_fifo_size(mc_stack));
 150           MC_replay(mc_stack);
 151           MC_UNSET_RAW_MEM;
 152           /* Let's loop again */
 153           break;
 154         }
 155       }
 156     }
 157   }
 158   MC_UNSET_RAW_MEM;
 159   /* We are done, show the statistics and return */
 160   MC_print_statistics(mc_stats);
 161 }