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   unsigned 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
 102       /* Get an enabled process and insert it in the interleave set of the next state */
 103       xbt_swag_foreach(process, simix_global->process_list){
 104         if(SIMIX_process_is_enabled(process)){
 105           MC_state_interleave_process(next_state, process);
 106           break;
 107         }
 108       }
 109       MC_UNSET_RAW_MEM;
 110
 111       /* FIXME: Update Statistics
 112       mc_stats->state_size +=
 113           xbt_setset_set_size(next_state->enabled_transitions);*/
 114
 115       /* Let's loop again */
 116
 117       /* The interleave set is empty or the maximum depth is reached, let's back-track */
 118     } else {
 119       DEBUG0("There are no more processes to interleave.");
 120
 121       /* Trash the current state, no longer needed */
 122       MC_SET_RAW_MEM;
 123       xbt_fifo_shift(mc_stack);
 124       MC_state_delete(state);
 125       MC_UNSET_RAW_MEM;
 126
 127       /* Check for deadlocks */
 128       if(MC_deadlock_check()){
 129         MC_show_deadlock(NULL);
 130         return;
 131       }
 132
 133       MC_SET_RAW_MEM;
 134       /* Traverse the stack backwards until a state with a non empty interleave
 135          set is found, deleting all the states that have it empty in the way.
 136          For each deleted state, check if the request that has generated it
 137          (from it's predecesor state), depends on any other previous request
 138          executed before it. If it does then add it to the interleave set of the
 139          state that executed that previous request. */
 140       while ((state = xbt_fifo_shift(mc_stack)) != NULL) {
 141         req = MC_state_get_executed_request(state, &value);
 142         xbt_fifo_foreach(mc_stack, item, prev_state, mc_state_t) {
 143           if(MC_request_depend(req, MC_state_get_executed_request(prev_state, &value))){
 144             if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
 145               DEBUG0("Dependent Transitions:");
 146               req_str = MC_request_to_string(MC_state_get_executed_request(prev_state, &value));
 147               DEBUG2("%s (state=%p)", req_str, prev_state);
 148               xbt_free(req_str);
 149               req_str = MC_request_to_string(req);
 150               DEBUG2("%s (state=%p)", req_str, state);
 151               xbt_free(req_str);
 152             }
 153
 154             if(!MC_state_process_is_done(prev_state, req->issuer))
 155               MC_state_interleave_process(prev_state, req->issuer);
 156             else
 157               DEBUG1("Process %p is in done set", req->issuer);
 158
 159             break;
 160           }
 161         }
 162         if (MC_state_interleave_size(state)) {
 163           /* We found a back-tracking point, let's loop */
 164           xbt_fifo_unshift(mc_stack, state);
 165           DEBUG1("Back-tracking to depth %d", xbt_fifo_size(mc_stack));
 166           MC_UNSET_RAW_MEM;
 167           MC_replay(mc_stack);
 168           break;
 169         } else {
 170           MC_state_delete(state);
 171         }
 172       }
 173       MC_UNSET_RAW_MEM;
 174     }
 175   }
 176   MC_UNSET_RAW_MEM;
 177   return;
 178 }