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         MC_state_set_executed_request(state, req);
  96
  97         SIMIX_request_pre(req); /* After this call req is no longer usefull */
  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       /* FIXME: use REQ_NO_REQ instead of NULL for comparison */
 130         if(&process->request && !SIMIX_request_is_enabled(&process->request)){
 131           MC_show_deadlock(&process->request);
 132           return;
 133         }
 134       }
 135
 136       /*
 137       INFO0("*********************************");
 138       MC_show_stack(mc_stack); */
 139
 140       /* Trash the current state, no longer needed */
 141       MC_SET_RAW_MEM;
 142       xbt_fifo_shift(mc_stack);
 143       MC_state_delete(state);
 144
 145       /* Traverse the stack backwards until a state with a non empty interleave
 146          set is found, deleting all the states that have it empty in the way.
 147          For each deleted state, check if the request that has generated it
 148          (from it's predecesor state), depends on any other previous request
 149          executed before it. If it does then add it to the interleave set of the
 150          state that executed that previous request. */
 151       while ((state = xbt_fifo_shift(mc_stack)) != NULL) {
 152         req = MC_state_get_executed_request(state);
 153         xbt_fifo_foreach(mc_stack, item, prev_state, mc_state_t) {
 154           if(MC_request_depend(req, MC_state_get_executed_request(prev_state))){
 155             if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
 156               DEBUG0("Dependent Transitions:");
 157               req_str = MC_request_to_string(MC_state_get_executed_request(prev_state));
 158               DEBUG1("%s", req_str);
 159               xbt_free(req_str);
 160               req_str = MC_request_to_string(req);
 161               DEBUG1("%s", req_str);
 162               xbt_free(req_str);
 163             }
 164             xbt_setset_set_insert(prev_state->interleave, req->issuer);
 165             break;
 166           }
 167         }
 168         if (xbt_setset_set_size(state->interleave) > 0) {
 169           /* We found a back-tracking point, let's loop */
 170           xbt_fifo_unshift(mc_stack, state);
 171           DEBUG1("Back-tracking to depth %d", xbt_fifo_size(mc_stack));
 172           MC_UNSET_RAW_MEM;
 173           MC_replay(mc_stack);
 174           break;
 175         } else {
 176           MC_state_delete(state);
 177         }
 178       }
 179       MC_UNSET_RAW_MEM;
 180     }
 181   }
 182   MC_UNSET_RAW_MEM;
 183   return;
 184 }