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