src/mc/mc_dpor.c

   1 /* Copyright (c) 2008 Martin Quinson, Cristian Rosa.
   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 "private.h"
   8
   9 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_dpor, mc,
  10                                 "Logging specific to MC DPOR exploration");
  11
  12 /**
  13  *  \brief Initialize the DPOR exploration algorithm
  14  */
  15 void MC_dpor_init()
  16 {
  17   mc_state_t initial_state = NULL;
  18   mc_transition_t trans = NULL;
  19   xbt_setset_cursor_t cursor = NULL;
  20
  21   /* Create the initial state and push it into the exploration stack */
  22   MC_SET_RAW_MEM;
  23   initial_state = MC_state_new();
  24   xbt_fifo_unshift(mc_stack, initial_state);
  25   MC_UNSET_RAW_MEM;
  26
  27   /* Schedule all the processes to detect the transitions of the initial state */
  28   DEBUG0("**************************************************");
  29   DEBUG0("Initial state");
  30   MC_schedule_enabled_processes();
  31
  32   MC_SET_RAW_MEM;
  33   xbt_setset_add(initial_state->enabled_transitions, initial_state->transitions);
  34   xbt_setset_foreach(initial_state->enabled_transitions, cursor, trans){
  35     if(trans->type == mc_wait
  36        && (trans->comm->src_proc == NULL || trans->comm->dst_proc == NULL)){
  37       xbt_setset_set_remove(initial_state->enabled_transitions, trans);
  38     }
  39   }
  40
  41   /* Fill the interleave set of the initial state with an enabled process */
  42   trans = xbt_setset_set_choose(initial_state->enabled_transitions);
  43   if(trans)
  44     xbt_setset_set_insert(initial_state->interleave, trans);
  45   MC_UNSET_RAW_MEM;
  46
  47   /* Update Statistics */
  48   mc_stats->state_size += xbt_setset_set_size(initial_state->enabled_transitions);
  49 }
  50
  51
  52 /**
  53  *      \brief Perform the model-checking operation using a depth-first search exploration
  54  *         with Dynamic Partial Order Reductions
  55  */
  56 void MC_dpor(void)
  57 {
  58   mc_transition_t trans = NULL;
  59   mc_state_t next_state = NULL;
  60   xbt_setset_cursor_t cursor = NULL;
  61
  62   while(xbt_fifo_size(mc_stack) > 0){
  63
  64     DEBUG0("**************************************************");
  65
  66     /* FIXME: Think about what happen if there are no transitions but there are
  67        some actions on the models. (ex. all the processes do a sleep(0) in a round). */
  68
  69     /* Get current state */
  70     mc_current_state = (mc_state_t) xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
  71
  72     /* If there are transitions to execute and the maximun depth has not been reached
  73        then perform one step of the exploration algorithm */
  74     if(xbt_setset_set_size(mc_current_state->interleave) > 0 && xbt_fifo_size(mc_stack) < MAX_DEPTH){
  75
  76       DEBUG4("Exploration detph=%d (state=%p)(%d interleave) (%d enabled)", xbt_fifo_size(mc_stack),
  77         mc_current_state, xbt_setset_set_size(mc_current_state->interleave),
  78         xbt_setset_set_size(mc_current_state->enabled_transitions));
  79
  80       xbt_setset_foreach(mc_current_state->enabled_transitions, cursor, trans){
  81         DEBUG1("\t %s", trans->name);
  82       }
  83
  84       /* Update statistics */
  85       mc_stats->visited_states++;
  86       mc_stats->executed_transitions++;
  87
  88       /* Choose a transition to execute from the interleave set of the current
  89          state, and create the data structures for the new expanded state in the
  90          exploration stack. */
  91       MC_SET_RAW_MEM;
  92       trans = xbt_setset_set_choose(mc_current_state->interleave);
  93       if(!trans->type == mc_random){
  94         xbt_setset_set_remove(mc_current_state->interleave, trans);
  95         /* Add the transition in the done set of the current state */
  96         xbt_setset_set_insert(mc_current_state->done, trans);
  97       }
  98
  99       next_state = MC_state_new();
 100       xbt_fifo_unshift(mc_stack, next_state);
 101
 102       /* Set it as the executed transition of the current state */
 103       mc_current_state->executed_transition = trans;
 104       MC_UNSET_RAW_MEM;
 105
 106       /* Execute the selected transition by scheduling it's associated process.
 107          Then schedule every process that got ready to run due to the execution
 108          of the transition */
 109       DEBUG1("Executing transition %s", trans->name);
 110       SIMIX_process_schedule(trans->process);
 111       MC_execute_surf_actions();        /* Do surf's related black magic */
 112       MC_schedule_enabled_processes();
 113
 114       if(trans->type == mc_random && trans->current_value < trans->max ){
 115         trans->current_value++;
 116       }else{
 117         trans->current_value = trans->min;
 118         xbt_setset_set_remove(mc_current_state->interleave, trans);
 119         xbt_setset_set_insert(mc_current_state->done, trans);
 120       }
 121
 122       /* Calculate the enabled transitions set of the next state:
 123           -add the transition sets of the current state and the next state
 124           -remove the executed transition from that set
 125           -remove all the transitions that are disabled (mc_wait only)
 126           -use the resulting set as the enabled transitions of the next state */
 127       MC_SET_RAW_MEM;
 128       xbt_setset_add(next_state->transitions, mc_current_state->transitions);
 129       xbt_setset_set_remove(next_state->transitions, trans);
 130       xbt_setset_add(next_state->enabled_transitions, next_state->transitions);
 131       xbt_setset_foreach(next_state->enabled_transitions, cursor, trans){
 132         if(trans->type == mc_wait
 133            && (trans->comm->src_proc == NULL || trans->comm->dst_proc == NULL)){
 134           xbt_setset_set_remove(next_state->enabled_transitions, trans);
 135         }
 136       }
 137
 138       /* Choose one transition to interleave from the enabled transition set */
 139       trans = xbt_setset_set_choose(next_state->enabled_transitions);
 140       if(trans)
 141         xbt_setset_set_insert(next_state->interleave, trans);
 142       MC_UNSET_RAW_MEM;
 143
 144       /* Update Statistics */
 145       mc_stats->state_size += xbt_setset_set_size(next_state->enabled_transitions);
 146
 147       /* Let's loop again */
 148
 149     /* The interleave set is empty or the maximum depth is reached, let's back-track */
 150     }else{
 151       DEBUG0("There are no more transitions to interleave.");
 152
 153       mc_transition_t q = NULL;
 154       xbt_fifo_item_t item = NULL;
 155       mc_state_t state = NULL;
 156
 157       //MC_show_stack(mc_stack);
 158
 159       /* Trash the current state, no longer needed */
 160       MC_SET_RAW_MEM;
 161       xbt_fifo_shift(mc_stack);
 162       MC_state_delete(mc_current_state);
 163
 164       /* Traverse the stack backwards until a state with a non empty interleave
 165          set is found, deleting all the states that have it empty in the way.
 166          For each deleted state, check if the transition that has generated it
 167          (from it's predecesor state), depends on any other previous transition
 168          executed before it. If it does then add it to the interleave set of the
 169          state that executed that previous transition. */
 170       while((mc_current_state = xbt_fifo_shift(mc_stack)) != NULL){
 171         q = mc_current_state->executed_transition;
 172         xbt_fifo_foreach(mc_stack, item, state, mc_state_t){
 173           if(MC_transition_depend(q, state->executed_transition)){
 174             DEBUG3("Dependence found at state %p (%p,%p)", state, state->executed_transition, q);
 175             xbt_setset_foreach(state->enabled_transitions, cursor, trans){
 176               if((trans->process == q->process) && !xbt_setset_set_belongs(state->done, trans)){
 177                 DEBUG2("Unexplored interleaving found at state %p (%p)", state, trans);
 178                 xbt_setset_set_insert(state->interleave, trans);
 179                 break;
 180               }
 181             }
 182             if(trans)
 183               break;
 184           }
 185         }
 186         if(xbt_setset_set_size(mc_current_state->interleave) > 0){
 187           /* We found a back-tracking point, let's loop */
 188           xbt_fifo_unshift(mc_stack, mc_current_state);
 189           DEBUG1("Back-tracking to depth %d", xbt_fifo_size(mc_stack));
 190           MC_replay(mc_stack);
 191           MC_UNSET_RAW_MEM;
 192           break;
 193         }else{
 194           MC_state_delete(mc_current_state);
 195         }
 196       }
 197     }
 198   }
 199   DEBUG0("We are done");
 200   /* We are done, show the statistics and return */
 201   MC_print_statistics(mc_stats);
 202 }