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