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   smx_process_t process;
  19
  20   /* Create the initial state and push it into the exploration stack */
  21   MC_SET_RAW_MEM;
  22   initial_state = MC_state_new();
  23   xbt_fifo_unshift(mc_stack, initial_state);
  24   MC_UNSET_RAW_MEM;
  25
  26   DEBUG0("**************************************************");
  27   DEBUG0("Initial state");
  28
  29   /* Wait for requests (schedules processes) */
  30   MC_wait_for_requests();
  31
  32   MC_SET_RAW_MEM;
  33   /* Get an enabled process and insert it in the interleave set of the initial state */
  34   xbt_swag_foreach(process, simix_global->process_list){
  35     if(SIMIX_process_is_enabled(process)){
  36       xbt_setset_set_insert(initial_state->interleave, process);
  37       break;
  38     }
  39   }
  40   MC_UNSET_RAW_MEM;
  41
  42   /* FIXME: Update Statistics
  43   mc_stats->state_size +=
  44       xbt_setset_set_size(initial_state->enabled_transitions); */
  45 }
  46
  47
  48 /**
  49  *      \brief Perform the model-checking operation using a depth-first search exploration
  50  *         with Dynamic Partial Order Reductions
  51  */
  52 void MC_dpor(void)
  53 {
  54   char *req_str;
  55   smx_req_t req = NULL;
  56   mc_state_t state = NULL, prev_state = NULL, next_state = NULL;
  57   smx_process_t process = NULL;
  58   xbt_fifo_item_t item = NULL;
  59
  60   while (xbt_fifo_size(mc_stack) > 0) {
  61
  62     DEBUG0("**************************************************");
  63
  64     /* Get current state */
  65     state = (mc_state_t)
  66       xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
  67
  68     /* If there are processes to interleave and the maximun depth has not been reached
  69        then perform one step of the exploration algorithm */
  70     if (xbt_setset_set_size(state->interleave) > 0
  71         && xbt_fifo_size(mc_stack) < MAX_DEPTH) {
  72
  73       DEBUG3("Exploration detph=%d (state=%p)(%d interleave)",
  74              xbt_fifo_size(mc_stack), state,
  75              xbt_setset_set_size(state->interleave));
  76
  77       /* Update statistics */
  78       mc_stats->visited_states++;
  79       mc_stats->executed_transitions++;
  80
  81       MC_SET_RAW_MEM;
  82       /* Choose a request to execute from the the current state */
  83       req = MC_state_get_request(state);
  84       MC_UNSET_RAW_MEM;
  85
  86       if(req){
  87         /* Answer the request */
  88         /* Debug information */
  89         if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
  90           req_str = MC_request_to_string(req);
  91           DEBUG1("Execute: %s", req_str);
  92           xbt_free(req_str);
  93         }
  94
  95         SIMIX_request_pre(req);
  96
  97         MC_state_set_executed_request(state, req);
  98
  99         /* Wait for requests (schedules processes) */
 100         MC_wait_for_requests();
 101
 102         /* Create the new expanded state */
 103         MC_SET_RAW_MEM;
 104         next_state = MC_state_new();
 105         xbt_fifo_unshift(mc_stack, next_state);
 106
 107
 108         /* Get an enabled process and insert it in the interleave set of the next state */
 109         xbt_swag_foreach(process, simix_global->process_list){
 110           if(SIMIX_process_is_enabled(process)){
 111             xbt_setset_set_insert(next_state->interleave, process);
 112             break;
 113           }
 114         }
 115         MC_UNSET_RAW_MEM;
 116
 117         /* FIXME: Update Statistics
 118         mc_stats->state_size +=
 119             xbt_setset_set_size(next_state->enabled_transitions);*/
 120       }
 121       /* Let's loop again */
 122
 123       /* The interleave set is empty or the maximum depth is reached, let's back-track */
 124     } else {
 125       DEBUG0("There are no more processes to interleave.");
 126
 127       /* Check for deadlocks */
 128       xbt_swag_foreach(process, simix_global->process_list){
 129         if(process->request && !SIMIX_request_is_enabled(process->request)){
 130           *mc_exp_ctl = MC_DEADLOCK;
 131           return;
 132         }
 133       }
 134
 135       /*
 136       INFO0("*********************************");
 137       MC_show_stack(mc_stack); */
 138
 139       /* Trash the current state, no longer needed */
 140       MC_SET_RAW_MEM;
 141       xbt_fifo_shift(mc_stack);
 142       MC_state_delete(state);
 143
 144       /* Traverse the stack backwards until a state with a non empty interleave
 145          set is found, deleting all the states that have it empty in the way.
 146          For each deleted state, check if the request that has generated it
 147          (from it's predecesor state), depends on any other previous request
 148          executed before it. If it does then add it to the interleave set of the
 149          state that executed that previous request. */
 150       while ((state = xbt_fifo_shift(mc_stack)) != NULL) {
 151         req = MC_state_get_executed_request(state);
 152         xbt_fifo_foreach(mc_stack, item, prev_state, mc_state_t) {
 153           if(MC_request_depend(req, MC_state_get_executed_request(prev_state))){
 154             if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
 155               DEBUG0("Dependent Transitions:");
 156               req_str = MC_request_to_string(MC_state_get_executed_request(prev_state));
 157               DEBUG1("%s", req_str);
 158               xbt_free(req_str);
 159               req_str = MC_request_to_string(req);
 160               DEBUG1("%s", req_str);
 161               xbt_free(req_str);
 162             }
 163             xbt_setset_set_insert(prev_state->interleave, req->issuer);
 164             break;
 165           }
 166         }
 167         if (xbt_setset_set_size(state->interleave) > 0) {
 168           /* We found a back-tracking point, let's loop */
 169           xbt_fifo_unshift(mc_stack, state);
 170           DEBUG1("Back-tracking to depth %d", xbt_fifo_size(mc_stack));
 171           *mc_exp_ctl = MC_EXPLORE;
 172           MC_UNSET_RAW_MEM;
 173           return;
 174           break;
 175         } else {
 176           MC_state_delete(state);
 177         }
 178       }
 179     }
 180   }
 181   MC_UNSET_RAW_MEM;
 182   *mc_exp_ctl = MC_STOP;
 183   return;
 184 }