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