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