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