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