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(MC_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, prev_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, value);
  83         if(req->call == REQ_COMM_WAITANY)
  84           DEBUG3("Execute: %s (%u of %lu)", req_str, value, xbt_dynar_length(req->comm_waitany.comms));
  85         else if(req->call == REQ_COMM_TESTANY)
  86           DEBUG3("Execute: %s (%u of %lu)", req_str, value, xbt_dynar_length(req->comm_testany.comms));
  87         else
  88           DEBUG1("Execute: %s", req_str);
  89         xbt_free(req_str);
  90       }
  91
  92       MC_state_set_executed_request(state, req, value);
  93       mc_stats->executed_transitions++;
  94
  95       /* Answer the request */
  96       SIMIX_request_pre(req, value); /* After this call req is no longer usefull */
  97
  98       /* Wait for requests (schedules processes) */
  99       MC_wait_for_requests();
 100
 101       /* Create the new expanded state */
 102       MC_SET_RAW_MEM;
 103       next_state = MC_state_new();
 104       xbt_fifo_unshift(mc_stack, next_state);
 105
 106       /* Get an enabled process and insert it in the interleave set of the next state */
 107       xbt_swag_foreach(process, simix_global->process_list){
 108         if(MC_process_is_enabled(process)){
 109           MC_state_interleave_process(next_state, process);
 110           break;
 111         }
 112       }
 113       MC_UNSET_RAW_MEM;
 114
 115       /* FIXME: Update Statistics
 116       mc_stats->state_size +=
 117           xbt_setset_set_size(next_state->enabled_transitions);*/
 118
 119       /* Let's loop again */
 120
 121       /* The interleave set is empty or the maximum depth is reached, let's back-track */
 122     } else {
 123       DEBUG0("There are no more processes to interleave.");
 124
 125       /* Trash the current state, no longer needed */
 126       MC_SET_RAW_MEM;
 127       xbt_fifo_shift(mc_stack);
 128       MC_state_delete(state);
 129       MC_UNSET_RAW_MEM;
 130
 131       /* Check for deadlocks */
 132       if(MC_deadlock_check()){
 133         MC_show_deadlock(NULL);
 134         return;
 135       }
 136
 137       MC_SET_RAW_MEM;
 138       /* Traverse the stack backwards until a state with a non empty interleave
 139          set is found, deleting all the states that have it empty in the way.
 140          For each deleted state, check if the request that has generated it
 141          (from it's predecesor state), depends on any other previous request
 142          executed before it. If it does then add it to the interleave set of the
 143          state that executed that previous request. */
 144       while ((state = xbt_fifo_shift(mc_stack)) != NULL) {
 145         req = MC_state_get_internal_request(state);
 146         xbt_fifo_foreach(mc_stack, item, prev_state, mc_state_t) {
 147           if(MC_request_depend(req, MC_state_get_internal_request(prev_state))){
 148             if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
 149               DEBUG0("Dependent Transitions:");
 150               prev_req = MC_state_get_executed_request(prev_state, &value);
 151               req_str = MC_request_to_string(prev_req, value);
 152               DEBUG2("%s (state=%p)", req_str, prev_state);
 153               xbt_free(req_str);
 154               prev_req = MC_state_get_executed_request(state, &value);
 155               req_str = MC_request_to_string(prev_req, value);
 156               DEBUG2("%s (state=%p)", req_str, state);
 157               xbt_free(req_str);
 158             }
 159
 160             if(!MC_state_process_is_done(prev_state, req->issuer))
 161               MC_state_interleave_process(prev_state, req->issuer);
 162             else
 163               DEBUG1("Process %p is in done set", req->issuer);
 164
 165             break;
 166           }
 167         }
 168         if (MC_state_interleave_size(state)) {
 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 }