src/mc/mc_dpor.c

   1 /* Copyright (c) 2008-2012. Da SimGrid Team. All rights reserved.           */
   2
   3 /* This program is free software; you can redistribute it and/or modify it
   4  * under the terms of the license (GNU LGPL) which comes with this package. */
   5
   6 #include "mc_private.h"
   7
   8 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_dpor, mc,
   9                                 "Logging specific to MC DPOR exploration");
  10
  11 /**
  12  *  \brief Initialize the DPOR exploration algorithm
  13  */
  14 void MC_dpor_init()
  15 {
  16
  17   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
  18
  19   mc_state_t initial_state = NULL;
  20   smx_process_t process;
  21
  22   /* Create the initial state and push it into the exploration stack */
  23   MC_SET_RAW_MEM;
  24   initial_state = MC_state_new();
  25   MC_UNSET_RAW_MEM;
  26
  27   XBT_DEBUG("**************************************************");
  28   XBT_DEBUG("Initial state");
  29
  30   /* Wait for requests (schedules processes) */
  31   MC_wait_for_requests();
  32
  33   MC_SET_RAW_MEM;
  34   /* Get an enabled process and insert it in the interleave set of the initial state */
  35   xbt_swag_foreach(process, simix_global->process_list){
  36     if(MC_process_is_enabled(process)){
  37       MC_state_interleave_process(initial_state, process);
  38       break;
  39     }
  40   }
  41
  42   xbt_fifo_unshift(mc_stack_safety, initial_state);
  43
  44   MC_UNSET_RAW_MEM;
  45
  46   if(raw_mem_set)
  47     MC_SET_RAW_MEM;
  48   else
  49     MC_UNSET_RAW_MEM;
  50
  51
  52   /* FIXME: Update Statistics
  53      mc_stats->state_size +=
  54      xbt_setset_set_size(initial_state->enabled_transitions); */
  55 }
  56
  57
  58 /**
  59  *   \brief Perform the model-checking operation using a depth-first search exploration
  60  *         with Dynamic Partial Order Reductions
  61  */
  62 void MC_dpor(void)
  63 {
  64
  65   char *req_str;
  66   int value;
  67   smx_simcall_t req = NULL, prev_req = NULL;
  68   mc_state_t state = NULL, prev_state = NULL, next_state = NULL, restore_state=NULL;
  69   smx_process_t process = NULL;
  70   xbt_fifo_item_t item = NULL;
  71   int pos;
  72
  73   while (xbt_fifo_size(mc_stack_safety) > 0) {
  74
  75     /* Get current state */
  76     state = (mc_state_t)
  77       xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_safety));
  78
  79     XBT_DEBUG("**************************************************");
  80     XBT_DEBUG("Exploration depth=%d (state=%p)(%u interleave)",
  81               xbt_fifo_size(mc_stack_safety), state,
  82               MC_state_interleave_size(state));
  83
  84     /* Update statistics */
  85     mc_stats->visited_states++;
  86
  87     /* If there are processes to interleave and the maximum depth has not been reached
  88        then perform one step of the exploration algorithm */
  89     if (xbt_fifo_size(mc_stack_safety) < _surf_mc_max_depth &&
  90         (req = MC_state_get_request(state, &value))) {
  91
  92       /* Debug information */
  93       if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
  94         req_str = MC_request_to_string(req, value);
  95         XBT_DEBUG("Execute: %s", req_str);
  96         xbt_free(req_str);
  97       }
  98
  99       MC_state_set_executed_request(state, req, value);
 100       mc_stats->executed_transitions++;
 101
 102       /* Answer the request */
 103       SIMIX_simcall_pre(req, value); /* After this call req is no longer usefull */
 104
 105       /* Wait for requests (schedules processes) */
 106       MC_wait_for_requests();
 107
 108       /* Create the new expanded state */
 109       MC_SET_RAW_MEM;
 110
 111       next_state = MC_state_new();
 112
 113       /* Get an enabled process and insert it in the interleave set of the next state */
 114       xbt_swag_foreach(process, simix_global->process_list){
 115         if(MC_process_is_enabled(process)){
 116           MC_state_interleave_process(next_state, process);
 117           break;
 118         }
 119       }
 120
 121       if(_surf_mc_checkpoint && ((xbt_fifo_size(mc_stack_safety) + 1) % _surf_mc_checkpoint == 0)){
 122         next_state->system_state = xbt_new0(s_mc_snapshot_t, 1);
 123         MC_take_snapshot(next_state->system_state);
 124       }
 125
 126       xbt_fifo_unshift(mc_stack_safety, next_state);
 127       MC_UNSET_RAW_MEM;
 128
 129       /* FIXME: Update Statistics
 130          mc_stats->state_size +=
 131          xbt_setset_set_size(next_state->enabled_transitions);*/
 132
 133       /* Let's loop again */
 134
 135       /* The interleave set is empty or the maximum depth is reached, let's back-track */
 136     } else {
 137       XBT_DEBUG("There are no more processes to interleave.");
 138
 139       /* Trash the current state, no longer needed */
 140       MC_SET_RAW_MEM;
 141       xbt_fifo_shift(mc_stack_safety);
 142       MC_state_delete(state);
 143       MC_UNSET_RAW_MEM;
 144
 145       /* Check for deadlocks */
 146       if(MC_deadlock_check()){
 147         MC_show_deadlock(NULL);
 148         return;
 149       }
 150
 151       MC_SET_RAW_MEM;
 152       /* Traverse the stack backwards until a state with a non empty interleave
 153          set is found, deleting all the states that have it empty in the way.
 154          For each deleted state, check if the request that has generated it
 155          (from it's predecesor state), depends on any other previous request
 156          executed before it. If it does then add it to the interleave set of the
 157          state that executed that previous request. */
 158       while ((state = xbt_fifo_shift(mc_stack_safety)) != NULL) {
 159         req = MC_state_get_internal_request(state);
 160         xbt_fifo_foreach(mc_stack_safety, item, prev_state, mc_state_t) {
 161           if(MC_request_depend(req, MC_state_get_internal_request(prev_state))){
 162             if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
 163               XBT_DEBUG("Dependent Transitions:");
 164               prev_req = MC_state_get_executed_request(prev_state, &value);
 165               req_str = MC_request_to_string(prev_req, value);
 166               XBT_DEBUG("%s (state=%p)", req_str, prev_state);
 167               xbt_free(req_str);
 168               prev_req = MC_state_get_executed_request(state, &value);
 169               req_str = MC_request_to_string(prev_req, value);
 170               XBT_DEBUG("%s (state=%p)", req_str, state);
 171               xbt_free(req_str);
 172             }
 173
 174             if(!MC_state_process_is_done(prev_state, req->issuer))
 175               MC_state_interleave_process(prev_state, req->issuer);
 176             else
 177               XBT_DEBUG("Process %p is in done set", req->issuer);
 178
 179             break;
 180           }
 181         }
 182         if (MC_state_interleave_size(state)) {
 183           /* We found a back-tracking point, let's loop */
 184           if(_surf_mc_checkpoint){
 185             if(state->system_state != NULL){
 186               MC_restore_snapshot(state->system_state);
 187               xbt_fifo_unshift(mc_stack_safety, state);
 188               XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety));
 189               MC_UNSET_RAW_MEM;
 190             }else{
 191               pos = xbt_fifo_size(mc_stack_safety);
 192               item = xbt_fifo_get_first_item(mc_stack_safety);
 193               while(pos>0){
 194                 restore_state = (mc_state_t) xbt_fifo_get_item_content(item);
 195                 if(restore_state->system_state != NULL){
 196                   break;
 197                 }else{
 198                   item = xbt_fifo_get_next_item(item);
 199                   pos--;
 200                 }
 201               }
 202               MC_restore_snapshot(restore_state->system_state);
 203               xbt_fifo_unshift(mc_stack_safety, state);
 204               XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety));
 205               MC_UNSET_RAW_MEM;
 206               MC_replay(mc_stack_safety, pos);
 207             }
 208           }else{
 209             xbt_fifo_unshift(mc_stack_safety, state);
 210             XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety));
 211             MC_UNSET_RAW_MEM;
 212             MC_replay(mc_stack_safety, -1);
 213           }
 214           break;
 215         } else {
 216           MC_state_delete(state);
 217         }
 218       }
 219       MC_UNSET_RAW_MEM;
 220     }
 221   }
 222   MC_print_statistics(mc_stats);
 223   MC_UNSET_RAW_MEM;
 224
 225   return;
 226 }
 227
 228
 229
 230