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   MC_schedule_enabled_processes();
  31
  32   MC_SET_RAW_MEM;
  33   MC_trans_compute_enabled(initial_state->enabled_transitions,
  34                            initial_state->transitions);
  35
  36   /* Fill the interleave set of the initial state with an enabled process */
  37   trans = xbt_setset_set_choose(initial_state->enabled_transitions);
  38   if(trans){
  39     DEBUG1("Choosing process %s for next interleave", trans->process->name);
  40     xbt_setset_foreach(initial_state->enabled_transitions, cursor, trans_tmp){
  41       if(trans_tmp->process == trans->process)
  42         xbt_setset_set_insert(initial_state->interleave, trans_tmp);
  43     }
  44   }
  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, trans_tmp = 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       /* Update statistics */
  81       mc_stats->visited_states++;
  82       mc_stats->executed_transitions++;
  83
  84       /* Choose a transition to execute from the interleave set of the current
  85          state, and create the data structures for the new expanded state in the
  86          exploration stack. */
  87       MC_SET_RAW_MEM;
  88       trans = xbt_setset_set_extract(mc_current_state->interleave);
  89
  90       /* Add the transition in the done set of the current state */
  91       xbt_setset_set_insert(mc_current_state->done, trans);
  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       /* Calculate the enabled transitions set of the next state */
 109       MC_SET_RAW_MEM;
 110
 111       xbt_setset_foreach(mc_current_state->transitions, cursor, trans_tmp){
 112         if(trans_tmp->process != trans->process){
 113           xbt_setset_set_insert(next_state->transitions, trans_tmp);
 114         }
 115       }
 116
 117       MC_trans_compute_enabled(next_state->enabled_transitions, next_state->transitions);
 118
 119       /* Choose one transition to interleave from the enabled transition set */
 120       trans = xbt_setset_set_choose(next_state->enabled_transitions);
 121       if(trans){
 122         DEBUG1("Choosing process %s for next interleave", trans->process->name);
 123         xbt_setset_foreach(next_state->enabled_transitions, cursor, trans_tmp){
 124           if(trans_tmp->process == trans->process)
 125             xbt_setset_set_insert(next_state->interleave, trans_tmp);
 126         }
 127       }
 128       MC_UNSET_RAW_MEM;
 129
 130       /* Update Statistics */
 131       mc_stats->state_size += xbt_setset_set_size(next_state->enabled_transitions);
 132
 133       /* Let's loop again */
 134
 135     /* The interleave set is empty or the maximum depth is reached, let's back-track */
 136     }else{
 137       DEBUG0("There are no more transitions to interleave.");
 138
 139
 140       /* Check for deadlocks */
 141       xbt_setset_substract(mc_current_state->transitions, mc_current_state->done);
 142       if(xbt_setset_set_size(mc_current_state->transitions) > 0){
 143         INFO0("**************************");
 144         INFO0("*** DEAD-LOCK DETECTED ***");
 145         INFO0("**************************");
 146         INFO0("Locked transitions:");
 147         xbt_setset_foreach(mc_current_state->transitions, cursor, trans){
 148           INFO1("%s", trans->name);
 149         }
 150
 151         INFO0("Counter-example execution trace:");
 152         MC_dump_stack(mc_stack);
 153
 154         MC_print_statistics(mc_stats);
 155         xbt_abort();
 156       }
 157
 158       mc_transition_t q = NULL;
 159       xbt_fifo_item_t item = NULL;
 160       mc_state_t state = NULL;
 161
 162       //MC_show_stack(mc_stack);
 163
 164       /* Trash the current state, no longer needed */
 165       MC_SET_RAW_MEM;
 166       xbt_fifo_shift(mc_stack);
 167       MC_state_delete(mc_current_state);
 168
 169       /* Traverse the stack backwards until a state with a non empty interleave
 170          set is found, deleting all the states that have it empty in the way.
 171          For each deleted state, check if the transition that has generated it
 172          (from it's predecesor state), depends on any other previous transition
 173          executed before it. If it does then add it to the interleave set of the
 174          state that executed that previous transition. */
 175       while((mc_current_state = xbt_fifo_shift(mc_stack)) != NULL){
 176         q = mc_current_state->executed_transition;
 177         xbt_fifo_foreach(mc_stack, item, state, mc_state_t){
 178           if(MC_transition_depend(q, state->executed_transition)){
 179             DEBUG3("Dependence found at state %p (%p,%p)", state, state->executed_transition, q);
 180             xbt_setset_foreach(state->enabled_transitions, cursor, trans){
 181               if((trans->process == q->process) && !xbt_setset_set_belongs(state->done, trans)){
 182                 DEBUG2("Unexplored interleaving found at state %p (%p)", state, trans);
 183
 184                 xbt_setset_foreach(state->enabled_transitions, cursor, trans){
 185                   if(trans->process == q->process)
 186                     xbt_setset_set_insert(state->interleave, trans);
 187                 }
 188                 /* FIXME: hack to make it work*/
 189                 trans = q;
 190                 break;
 191               }
 192             }
 193             if(trans)
 194               break;
 195           }
 196         }
 197         if(xbt_setset_set_size(mc_current_state->interleave) > 0){
 198           /* We found a back-tracking point, let's loop */
 199           xbt_fifo_unshift(mc_stack, mc_current_state);
 200           DEBUG1("Back-tracking to depth %d", xbt_fifo_size(mc_stack));
 201           MC_replay(mc_stack);
 202           MC_UNSET_RAW_MEM;
 203           break;
 204         }else{
 205           MC_state_delete(mc_current_state);
 206         }
 207       }
 208     }
 209   }
 210   DEBUG0("We are done");
 211   /* We are done, show the statistics and return */
 212   MC_print_statistics(mc_stats);
 213 }