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