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       /* Check for deadlocks */
 122       if(MC_deadlock_check()){
 123         MC_show_deadlock(&process->request);
 124         return;
 125       }
 126
 127       /* Trash the current state, no longer needed */
 128       MC_SET_RAW_MEM;
 129       xbt_fifo_shift(mc_stack);
 130       MC_state_delete(state);
 131
 132       /* Traverse the stack backwards until a state with a non empty interleave
 133          set is found, deleting all the states that have it empty in the way.
 134          For each deleted state, check if the request that has generated it
 135          (from it's predecesor state), depends on any other previous request
 136          executed before it. If it does then add it to the interleave set of the
 137          state that executed that previous request. */
 138       while ((state = xbt_fifo_shift(mc_stack)) != NULL) {
 139         req = MC_state_get_executed_request(state, &value);
 140         xbt_fifo_foreach(mc_stack, item, prev_state, mc_state_t) {
 141           if(MC_request_depend(req, MC_state_get_executed_request(prev_state, &value))){
 142             if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
 143               DEBUG0("Dependent Transitions:");
 144               req_str = MC_request_to_string(MC_state_get_executed_request(prev_state, &value));
 145               DEBUG2("%s (state=%p)", req_str, prev_state);
 146               xbt_free(req_str);
 147               req_str = MC_request_to_string(req);
 148               DEBUG2("%s (state=%p)", req_str, state);
 149               xbt_free(req_str);
 150             }
 151
 152             if(!MC_state_process_is_done(prev_state, req->issuer))
 153               MC_state_interleave_process(prev_state, req->issuer);
 154             else
 155               DEBUG1("Process %p is in done set", req->issuer);
 156
 157             break;
 158           }
 159         }
 160         if (MC_state_interleave_size(state)) {
 161           /* We found a back-tracking point, let's loop */
 162           xbt_fifo_unshift(mc_stack, state);
 163           DEBUG1("Back-tracking to depth %d", xbt_fifo_size(mc_stack));
 164           MC_UNSET_RAW_MEM;
 165           MC_replay(mc_stack);
 166           break;
 167         } else {
 168           MC_state_delete(state);
 169         }
 170       }
 171       MC_UNSET_RAW_MEM;
 172     }
 173   }
 174   MC_UNSET_RAW_MEM;
 175   return;
 176 }