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 xbt_dynar_t visited_states;
  12
  13 static int is_visited_state(void);
  14
  15 static int is_visited_state(){
  16
  17   if(_surf_mc_visited == 0)
  18     return 0;
  19
  20   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
  21
  22   MC_SET_RAW_MEM;
  23
  24   mc_snapshot_t new_state = NULL;
  25   new_state = MC_take_snapshot();
  26
  27   MC_UNSET_RAW_MEM;
  28
  29   if(xbt_dynar_is_empty(visited_states)){
  30
  31     MC_SET_RAW_MEM;
  32     xbt_dynar_push(visited_states, &new_state);
  33     MC_UNSET_RAW_MEM;
  34
  35     if(raw_mem_set)
  36       MC_SET_RAW_MEM;
  37
  38     return 0;
  39
  40   }else{
  41
  42     MC_SET_RAW_MEM;
  43
  44     unsigned int cursor = 0;
  45     mc_snapshot_t state_test = NULL;
  46
  47     xbt_dynar_foreach(visited_states, cursor, state_test){
  48       if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug))
  49         XBT_DEBUG("****** Pair visited #%d ******", cursor + 1);
  50       if(snapshot_compare(new_state, state_test, NULL, NULL) == 0){
  51         if(raw_mem_set)
  52           MC_SET_RAW_MEM;
  53         else
  54           MC_UNSET_RAW_MEM;
  55
  56         return 1;
  57       }
  58     }
  59
  60     if(xbt_dynar_length(visited_states) == _surf_mc_visited){
  61       mc_snapshot_t state_to_remove = NULL;
  62       xbt_dynar_shift(visited_states, &state_to_remove);
  63       MC_free_snapshot(state_to_remove);
  64     }
  65
  66     xbt_dynar_push(visited_states, &new_state);
  67
  68     MC_UNSET_RAW_MEM;
  69
  70     if(raw_mem_set)
  71       MC_SET_RAW_MEM;
  72
  73     return 0;
  74
  75   }
  76 }
  77
  78 /**
  79  *  \brief Initialize the DPOR exploration algorithm
  80  */
  81 void MC_dpor_init()
  82 {
  83
  84   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
  85
  86   mc_state_t initial_state = NULL;
  87   smx_process_t process;
  88
  89   /* Create the initial state and push it into the exploration stack */
  90   MC_SET_RAW_MEM;
  91
  92   initial_state = MC_state_new();
  93   visited_states = xbt_dynar_new(sizeof(mc_snapshot_t), NULL);
  94
  95   MC_UNSET_RAW_MEM;
  96
  97   XBT_DEBUG("**************************************************");
  98   XBT_DEBUG("Initial state");
  99
 100   /* Wait for requests (schedules processes) */
 101   MC_wait_for_requests();
 102
 103   MC_SET_RAW_MEM;
 104
 105   /* Get an enabled process and insert it in the interleave set of the initial state */
 106   xbt_swag_foreach(process, simix_global->process_list){
 107     if(MC_process_is_enabled(process)){
 108       MC_state_interleave_process(initial_state, process);
 109       break;
 110     }
 111   }
 112
 113   xbt_fifo_unshift(mc_stack_safety, initial_state);
 114
 115   MC_UNSET_RAW_MEM;
 116
 117   if(raw_mem_set)
 118     MC_SET_RAW_MEM;
 119   else
 120     MC_UNSET_RAW_MEM;
 121
 122 }
 123
 124
 125 /**
 126  *   \brief Perform the model-checking operation using a depth-first search exploration
 127  *         with Dynamic Partial Order Reductions
 128  */
 129 void MC_dpor(void)
 130 {
 131
 132   char *req_str;
 133   int value;
 134   smx_simcall_t req = NULL, prev_req = NULL;
 135   mc_state_t state = NULL, prev_state = NULL, next_state = NULL, restore_state=NULL;
 136   smx_process_t process = NULL;
 137   xbt_fifo_item_t item = NULL;
 138   int pos;
 139
 140   while (xbt_fifo_size(mc_stack_safety) > 0) {
 141
 142     /* Get current state */
 143     state = (mc_state_t)
 144       xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_safety));
 145
 146     XBT_DEBUG("**************************************************");
 147     XBT_DEBUG("Exploration depth=%d (state=%p)(%u interleave)",
 148               xbt_fifo_size(mc_stack_safety), state,
 149               MC_state_interleave_size(state));
 150
 151     /* Update statistics */
 152     mc_stats->visited_states++;
 153
 154     /* If there are processes to interleave and the maximum depth has not been reached
 155        then perform one step of the exploration algorithm */
 156     if (xbt_fifo_size(mc_stack_safety) < _surf_mc_max_depth &&
 157         (req = MC_state_get_request(state, &value))) {
 158
 159       /* Debug information */
 160       if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
 161         req_str = MC_request_to_string(req, value);
 162         XBT_DEBUG("Execute: %s", req_str);
 163         xbt_free(req_str);
 164       }
 165
 166       MC_state_set_executed_request(state, req, value);
 167       mc_stats->executed_transitions++;
 168
 169       /* Answer the request */
 170       SIMIX_simcall_pre(req, value); /* After this call req is no longer usefull */
 171
 172       /* Wait for requests (schedules processes) */
 173       MC_wait_for_requests();
 174
 175       /* Create the new expanded state */
 176       MC_SET_RAW_MEM;
 177
 178       next_state = MC_state_new();
 179
 180       if(!is_visited_state()){
 181
 182         /* Get an enabled process and insert it in the interleave set of the next state */
 183         xbt_swag_foreach(process, simix_global->process_list){
 184           if(MC_process_is_enabled(process)){
 185             MC_state_interleave_process(next_state, process);
 186             if((xbt_fifo_size(mc_stack_safety) + 1) != (_surf_mc_max_depth - 1))
 187               break;
 188           }
 189         }
 190
 191         if(_surf_mc_checkpoint && ((xbt_fifo_size(mc_stack_safety) + 1) % _surf_mc_checkpoint == 0)){
 192           next_state->system_state = MC_take_snapshot();
 193         }
 194
 195       }else{
 196
 197         XBT_DEBUG("State already visited !");
 198
 199       }
 200
 201       xbt_fifo_unshift(mc_stack_safety, next_state);
 202       MC_UNSET_RAW_MEM;
 203
 204       /* FIXME: Update Statistics
 205          mc_stats->state_size +=
 206          xbt_setset_set_size(next_state->enabled_transitions);*/
 207
 208       /* Let's loop again */
 209
 210       /* The interleave set is empty or the maximum depth is reached, let's back-track */
 211     } else {
 212
 213       if(xbt_fifo_size(mc_stack_safety) == _surf_mc_max_depth)
 214         XBT_WARN("/!\\ Max depth reached ! /!\\ ");
 215       else
 216         XBT_DEBUG("There are no more processes to interleave.");
 217
 218       /* Trash the current state, no longer needed */
 219       MC_SET_RAW_MEM;
 220       xbt_fifo_shift(mc_stack_safety);
 221       MC_state_delete(state);
 222       MC_UNSET_RAW_MEM;
 223
 224       /* Check for deadlocks */
 225       if(MC_deadlock_check()){
 226         MC_show_deadlock(NULL);
 227         return;
 228       }
 229
 230       MC_SET_RAW_MEM;
 231       /* Traverse the stack backwards until a state with a non empty interleave
 232          set is found, deleting all the states that have it empty in the way.
 233          For each deleted state, check if the request that has generated it
 234          (from it's predecesor state), depends on any other previous request
 235          executed before it. If it does then add it to the interleave set of the
 236          state that executed that previous request. */
 237
 238       while ((state = xbt_fifo_shift(mc_stack_safety)) != NULL) {
 239         req = MC_state_get_internal_request(state);
 240         xbt_fifo_foreach(mc_stack_safety, item, prev_state, mc_state_t) {
 241           if(MC_request_depend(req, MC_state_get_internal_request(prev_state))){
 242             if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
 243               XBT_DEBUG("Dependent Transitions:");
 244               prev_req = MC_state_get_executed_request(prev_state, &value);
 245               req_str = MC_request_to_string(prev_req, value);
 246               XBT_DEBUG("%s (state=%p)", req_str, prev_state);
 247               xbt_free(req_str);
 248               prev_req = MC_state_get_executed_request(state, &value);
 249               req_str = MC_request_to_string(prev_req, value);
 250               XBT_DEBUG("%s (state=%p)", req_str, state);
 251               xbt_free(req_str);
 252             }
 253
 254             if(!MC_state_process_is_done(prev_state, req->issuer))
 255               MC_state_interleave_process(prev_state, req->issuer);
 256             else
 257               XBT_DEBUG("Process %p is in done set", req->issuer);
 258
 259             break;
 260
 261           }else if(req->issuer == MC_state_get_executed_request(prev_state, &value)->issuer){
 262
 263             break;
 264
 265           }
 266         }
 267
 268         if (MC_state_interleave_size(state)) {
 269           /* We found a back-tracking point, let's loop */
 270           if(_surf_mc_checkpoint){
 271             if(state->system_state != NULL){
 272               MC_restore_snapshot(state->system_state);
 273               xbt_fifo_unshift(mc_stack_safety, state);
 274               XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety));
 275               MC_UNSET_RAW_MEM;
 276             }else{
 277               pos = xbt_fifo_size(mc_stack_safety);
 278               item = xbt_fifo_get_first_item(mc_stack_safety);
 279               while(pos>0){
 280                 restore_state = (mc_state_t) xbt_fifo_get_item_content(item);
 281                 if(restore_state->system_state != NULL){
 282                   break;
 283                 }else{
 284                   item = xbt_fifo_get_next_item(item);
 285                   pos--;
 286                 }
 287               }
 288               MC_restore_snapshot(restore_state->system_state);
 289               xbt_fifo_unshift(mc_stack_safety, state);
 290               XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety));
 291               MC_UNSET_RAW_MEM;
 292               MC_replay(mc_stack_safety, pos);
 293             }
 294           }else{
 295             xbt_fifo_unshift(mc_stack_safety, state);
 296             XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety));
 297             MC_UNSET_RAW_MEM;
 298             MC_replay(mc_stack_safety, -1);
 299           }
 300           break;
 301         } else {
 302           MC_state_delete(state);
 303         }
 304       }
 305       MC_UNSET_RAW_MEM;
 306     }
 307   }
 308   MC_print_statistics(mc_stats);
 309   MC_UNSET_RAW_MEM;
 310
 311   return;
 312 }
 313
 314
 315
 316