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
  20   /* Create the initial state and push it into the exploration stack */
  21   MC_SET_RAW_MEM;
  22   initial_state = MC_state_new();
  23   xbt_fifo_unshift(mc_stack, initial_state);
  24   MC_UNSET_RAW_MEM;
  25
  26   /* Schedule all the processes to detect the transitions of the initial state */
  27   DEBUG0("**************************************************");
  28   DEBUG0("Initial state");
  29   MC_schedule_enabled_processes();
  30
  31   MC_SET_RAW_MEM;
  32   MC_trans_compute_enabled(initial_state->enabled_transitions,
  33                            initial_state->transitions);
  34
  35   /* Fill the interleave set of the initial state with an enabled process */
  36   trans = xbt_setset_set_choose(initial_state->enabled_transitions);
  37   if(trans)
  38     xbt_setset_set_insert(initial_state->interleave, trans);
  39   MC_UNSET_RAW_MEM;
  40
  41   /* Update Statistics */
  42   mc_stats->state_size += xbt_setset_set_size(initial_state->enabled_transitions);
  43 }
  44
  45
  46 /**
  47  *      \brief Perform the model-checking operation using a depth-first search exploration
  48  *         with Dynamic Partial Order Reductions
  49  */
  50 void MC_dpor(void)
  51 {
  52   mc_transition_t trans, trans_tmp = 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
  58     DEBUG0("**************************************************");
  59
  60     /* FIXME: Think about what happen if there are no transitions but there are
  61        some actions on the models. (ex. all the processes do a sleep(0) in a round). */
  62
  63     /* Get current state */
  64     mc_current_state = (mc_state_t) 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(mc_current_state->interleave) > 0 && xbt_fifo_size(mc_stack) < MAX_DEPTH){
  69
  70       DEBUG4("Exploration detph=%d (state=%p)(%d interleave) (%d enabled)", xbt_fifo_size(mc_stack),
  71         mc_current_state, xbt_setset_set_size(mc_current_state->interleave),
  72         xbt_setset_set_size(mc_current_state->enabled_transitions));
  73
  74       xbt_setset_foreach(mc_current_state->enabled_transitions, cursor, trans){
  75         DEBUG1("\t %s", trans->name);
  76       }
  77
  78       /* Update statistics */
  79       mc_stats->visited_states++;
  80       mc_stats->executed_transitions++;
  81
  82       /* Choose a transition to execute from the interleave set of the current
  83          state, and create the data structures for the new expanded state in the
  84          exploration stack. */
  85       MC_SET_RAW_MEM;
  86       trans = xbt_setset_set_choose(mc_current_state->interleave);
  87       if(trans->type != mc_random){
  88         xbt_setset_set_remove(mc_current_state->interleave, trans);
  89         /* Add the transition in the done set of the current state */
  90         xbt_setset_set_insert(mc_current_state->done, trans);
  91       }
  92
  93       next_state = MC_state_new();
  94       xbt_fifo_unshift(mc_stack, next_state);
  95
  96       /* Set it as the executed transition of the current state */
  97       mc_current_state->executed_transition = trans;
  98       MC_UNSET_RAW_MEM;
  99
 100       /* Execute the selected transition by scheduling it's associated process.
 101          Then schedule every process that got ready to run due to the execution
 102          of the transition */
 103       DEBUG1("Executing transition %s", trans->name);
 104       SIMIX_process_schedule(trans->process);
 105       MC_execute_surf_actions();        /* Do surf's related black magic */
 106       MC_schedule_enabled_processes();
 107
 108       if(trans->type == mc_random && trans->random.current_value < trans->random.max){
 109         trans->random.current_value++;
 110       }else{
 111         //trans->random.current_value = trans->random.min;
 112         xbt_setset_set_remove(mc_current_state->interleave, trans);
 113         xbt_setset_set_insert(mc_current_state->done, trans);
 114       }
 115
 116       /* Calculate the enabled transitions set of the next state */
 117       MC_SET_RAW_MEM;
 118
 119       xbt_setset_foreach(mc_current_state->transitions, cursor, trans_tmp){
 120         DEBUG1("Checking transition %s", trans_tmp->name);
 121         if(trans_tmp->process != trans->process){
 122           DEBUG2("Inherit transition %p (%lu)", trans_tmp, trans_tmp->ID);
 123           xbt_setset_set_insert(next_state->transitions, trans_tmp);
 124         }
 125       }
 126
 127       MC_trans_compute_enabled(next_state->enabled_transitions, next_state->transitions);
 128
 129       /* Choose one transition to interleave from the enabled transition set */
 130       trans = xbt_setset_set_choose(next_state->enabled_transitions);
 131       if(trans){
 132         DEBUG1("Choosing transition %p", trans);
 133         xbt_setset_foreach(next_state->enabled_transitions, cursor, trans_tmp){
 134           if(trans_tmp->process == trans->process)
 135             xbt_setset_set_insert(next_state->interleave, trans_tmp);
 136         }
 137       }
 138       MC_UNSET_RAW_MEM;
 139
 140       /* Update Statistics */
 141       mc_stats->state_size += xbt_setset_set_size(next_state->enabled_transitions);
 142
 143       /* Let's loop again */
 144
 145     /* The interleave set is empty or the maximum depth is reached, let's back-track */
 146     }else{
 147       DEBUG0("There are no more transitions to interleave.");
 148
 149
 150       /* Check for deadlocks */
 151       xbt_setset_substract(mc_current_state->transitions, mc_current_state->done);
 152       if(xbt_setset_set_size(mc_current_state->transitions) > 0){
 153         INFO0("**************************");
 154         INFO0("*** DEAD-LOCK DETECTED ***");
 155         INFO0("**************************");
 156         INFO0("Locked transitions:");
 157         xbt_setset_foreach(mc_current_state->transitions, cursor, trans){
 158           INFO1("%s", trans->name);
 159         }
 160
 161         INFO0("Counter-example execution trace:");
 162         MC_dump_stack(mc_stack);
 163
 164         MC_print_statistics(mc_stats);
 165         xbt_abort();
 166       }
 167
 168       mc_transition_t q = NULL;
 169       xbt_fifo_item_t item = NULL;
 170       mc_state_t state = NULL;
 171
 172       //MC_show_stack(mc_stack);
 173
 174       /* Trash the current state, no longer needed */
 175       MC_SET_RAW_MEM;
 176       xbt_fifo_shift(mc_stack);
 177       MC_state_delete(mc_current_state);
 178
 179       /* Traverse the stack backwards until a state with a non empty interleave
 180          set is found, deleting all the states that have it empty in the way.
 181          For each deleted state, check if the transition that has generated it
 182          (from it's predecesor state), depends on any other previous transition
 183          executed before it. If it does then add it to the interleave set of the
 184          state that executed that previous transition. */
 185       while((mc_current_state = xbt_fifo_shift(mc_stack)) != NULL){
 186         q = mc_current_state->executed_transition;
 187         xbt_fifo_foreach(mc_stack, item, state, mc_state_t){
 188           if(MC_transition_depend(q, state->executed_transition)){
 189             DEBUG3("Dependence found at state %p (%p,%p)", state, state->executed_transition, q);
 190             xbt_setset_foreach(state->enabled_transitions, cursor, trans){
 191               if((trans->process == q->process) && !xbt_setset_set_belongs(state->done, trans)){
 192                 DEBUG2("Unexplored interleaving found at state %p (%p)", state, trans);
 193
 194                 xbt_setset_foreach(state->enabled_transitions, cursor, trans){
 195                   if(trans->process == q->process)
 196                     xbt_setset_set_insert(state->interleave, trans);
 197                 }
 198                 /* FIXME: hack to make it work*/
 199                 trans = q;
 200                 break;
 201               }
 202             }
 203             if(trans)
 204               break;
 205           }
 206         }
 207         if(xbt_setset_set_size(mc_current_state->interleave) > 0){
 208           /* We found a back-tracking point, let's loop */
 209           xbt_fifo_unshift(mc_stack, mc_current_state);
 210           DEBUG1("Back-tracking to depth %d", xbt_fifo_size(mc_stack));
 211           MC_replay(mc_stack);
 212           MC_UNSET_RAW_MEM;
 213           break;
 214         }else{
 215           MC_state_delete(mc_current_state);
 216         }
 217       }
 218     }
 219   }
 220   DEBUG0("We are done");
 221   /* We are done, show the statistics and return */
 222   MC_print_statistics(mc_stats);
 223 }