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       MC_state_interleave_process(initial_state, 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   int value;
  56   smx_req_t req = NULL;
  57   mc_state_t state = NULL, prev_state = NULL, next_state = NULL;
  58   smx_process_t process = NULL;
  59   xbt_fifo_item_t item = NULL;
  60
  61   while (xbt_fifo_size(mc_stack) > 0) {
  62
  63     /* Get current state */
  64     state = (mc_state_t)
  65       xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
  66
  67     DEBUG0("**************************************************");
  68     DEBUG3("Exploration detph=%d (state=%p)(%u interleave)",
  69            xbt_fifo_size(mc_stack), state,
  70            MC_state_interleave_size(state));
  71
  72     /* Update statistics */
  73     mc_stats->visited_states++;
  74
  75     /* If there are processes to interleave and the maximum depth has not been reached
  76        then perform one step of the exploration algorithm */
  77     if (xbt_fifo_size(mc_stack) < MAX_DEPTH &&
  78         (req = MC_state_get_request(state, &value))) {
  79
  80       /* Debug information */
  81       if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
  82         req_str = MC_request_to_string(req);
  83         DEBUG2("Execute: %s (%u)", req_str, value);
  84         xbt_free(req_str);
  85       }
  86
  87       MC_state_set_executed_request(state, req, value);
  88       mc_stats->executed_transitions++;
  89
  90       /* Answer the request */
  91       SIMIX_request_pre(req, value); /* After this call req is no longer usefull */
  92
  93       /* Wait for requests (schedules processes) */
  94       MC_wait_for_requests();
  95
  96       /* Create the new expanded state */
  97       MC_SET_RAW_MEM;
  98       next_state = MC_state_new();
  99       xbt_fifo_unshift(mc_stack, next_state);
 100
 101       /* Get an enabled process and insert it in the interleave set of the next state */
 102       xbt_swag_foreach(process, simix_global->process_list){
 103         if(SIMIX_process_is_enabled(process)){
 104           MC_state_interleave_process(next_state, process);
 105           break;
 106         }
 107       }
 108       MC_UNSET_RAW_MEM;
 109
 110       /* FIXME: Update Statistics
 111       mc_stats->state_size +=
 112           xbt_setset_set_size(next_state->enabled_transitions);*/
 113
 114       /* Let's loop again */
 115
 116       /* The interleave set is empty or the maximum depth is reached, let's back-track */
 117     } else {
 118       DEBUG0("There are no more processes to interleave.");
 119
 120       /* Trash the current state, no longer needed */
 121       MC_SET_RAW_MEM;
 122       xbt_fifo_shift(mc_stack);
 123       MC_state_delete(state);
 124       MC_UNSET_RAW_MEM;
 125
 126       /* Check for deadlocks */
 127       if(MC_deadlock_check()){
 128         MC_show_deadlock(NULL);
 129         return;
 130       }
 131
 132       MC_SET_RAW_MEM;
 133       /* Traverse the stack backwards until a state with a non empty interleave
 134          set is found, deleting all the states that have it empty in the way.
 135          For each deleted state, check if the request that has generated it
 136          (from it's predecesor state), depends on any other previous request
 137          executed before it. If it does then add it to the interleave set of the
 138          state that executed that previous request. */
 139       while ((state = xbt_fifo_shift(mc_stack)) != NULL) {
 140         req = MC_state_get_internal_request(state);
 141         xbt_fifo_foreach(mc_stack, item, prev_state, mc_state_t) {
 142           if(MC_request_depend(req, MC_state_get_internal_request(prev_state))){
 143             if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
 144               DEBUG0("Dependent Transitions:");
 145               req_str = MC_request_to_string(MC_state_get_executed_request(prev_state, &value));
 146               DEBUG2("%s (state=%p)", req_str, prev_state);
 147               xbt_free(req_str);
 148               req_str = MC_request_to_string(MC_state_get_executed_request(state, &value));
 149               DEBUG2("%s (state=%p)", req_str, state);
 150               xbt_free(req_str);
 151             }
 152
 153             if(!MC_state_process_is_done(prev_state, req->issuer))
 154               MC_state_interleave_process(prev_state, req->issuer);
 155             else
 156               DEBUG1("Process %p is in done set", req->issuer);
 157
 158             break;
 159           }
 160         }
 161         if (MC_state_interleave_size(state)) {
 162           /* We found a back-tracking point, let's loop */
 163           xbt_fifo_unshift(mc_stack, state);
 164           DEBUG1("Back-tracking to depth %d", xbt_fifo_size(mc_stack));
 165           MC_UNSET_RAW_MEM;
 166           MC_replay(mc_stack);
 167           break;
 168         } else {
 169           MC_state_delete(state);
 170         }
 171       }
 172       MC_UNSET_RAW_MEM;
 173     }
 174   }
 175   MC_UNSET_RAW_MEM;
 176   return;
 177 }