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(_sg_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) == _sg_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     }
 110   }
 111
 112   xbt_fifo_unshift(mc_stack_safety, initial_state);
 113
 114   MC_UNSET_RAW_MEM;
 115
 116   if(raw_mem_set)
 117     MC_SET_RAW_MEM;
 118   else
 119     MC_UNSET_RAW_MEM;
 120
 121 }
 122
 123
 124 /**
 125  *   \brief Perform the model-checking operation using a depth-first search exploration
 126  *         with Dynamic Partial Order Reductions
 127  */
 128 void MC_dpor(void)
 129 {
 130
 131   char *req_str;
 132   int value;
 133   smx_simcall_t req = NULL, prev_req = NULL;
 134   mc_state_t state = NULL, prev_state = NULL, next_state = NULL, restore_state=NULL;
 135   smx_process_t process = NULL;
 136   xbt_fifo_item_t item = NULL;
 137   int pos, i;
 138   int proc_eval[simix_process_maxpid];
 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) < _sg_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           }
 187         }
 188
 189         if(_sg_mc_checkpoint && ((xbt_fifo_size(mc_stack_safety) + 1) % _sg_mc_checkpoint == 0)){
 190           next_state->system_state = MC_take_snapshot();
 191         }
 192
 193       }else{
 194
 195         XBT_DEBUG("State already visited !");
 196
 197       }
 198
 199       xbt_fifo_unshift(mc_stack_safety, next_state);
 200       MC_UNSET_RAW_MEM;
 201
 202       /* FIXME: Update Statistics
 203          mc_stats->state_size +=
 204          xbt_setset_set_size(next_state->enabled_transitions);*/
 205
 206       /* Let's loop again */
 207
 208       /* The interleave set is empty or the maximum depth is reached, let's back-track */
 209     } else {
 210
 211       if(xbt_fifo_size(mc_stack_safety) == _sg_mc_max_depth)
 212         XBT_WARN("/!\\ Max depth reached ! /!\\ ");
 213       else
 214         XBT_DEBUG("There are no more processes to interleave.");
 215
 216       /* Trash the current state, no longer needed */
 217       MC_SET_RAW_MEM;
 218       xbt_fifo_shift(mc_stack_safety);
 219       MC_state_delete(state);
 220       MC_UNSET_RAW_MEM;
 221
 222       /* Check for deadlocks */
 223       if(MC_deadlock_check()){
 224         MC_show_deadlock(NULL);
 225         return;
 226       }
 227
 228       MC_SET_RAW_MEM;
 229       /* Traverse the stack backwards until a state with a non empty interleave
 230          set is found, deleting all the states that have it empty in the way.
 231          For each deleted state, check if the request that has generated it
 232          (from it's predecesor state), depends on any other previous request
 233          executed before it. If it does then add it to the interleave set of the
 234          state that executed that previous request. */
 235
 236       while ((state = xbt_fifo_shift(mc_stack_safety)) != NULL) {
 237
 238         for(i=0; i<simix_process_maxpid; i++)
 239           proc_eval[i] = 0;
 240
 241         if(MC_state_interleave_size(state) == 0){
 242           req = MC_state_get_internal_request(state);
 243           xbt_fifo_foreach(mc_stack_safety, item, prev_state, mc_state_t) {
 244             if(MC_request_depend(req, MC_state_get_internal_request(prev_state))){
 245               if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
 246                 XBT_DEBUG("Dependent Transitions:");
 247                 prev_req = MC_state_get_executed_request(prev_state, &value);
 248                 req_str = MC_request_to_string(prev_req, value);
 249                 XBT_DEBUG("%s (state=%p)", req_str, prev_state);
 250                 xbt_free(req_str);
 251                 prev_req = MC_state_get_executed_request(state, &value);
 252                 req_str = MC_request_to_string(prev_req, value);
 253                 XBT_DEBUG("%s (state=%p)", req_str, state);
 254                 xbt_free(req_str);
 255               }
 256
 257               break;
 258
 259             }else if(req->issuer == MC_state_get_executed_request(prev_state, &value)->issuer){
 260
 261               break;
 262
 263             }else if(proc_eval[MC_state_get_executed_request(prev_state, &value)->issuer->pid] == 0){
 264
 265               MC_state_remove_interleave_process(prev_state, MC_state_get_executed_request(prev_state, &value)->issuer);
 266
 267             }
 268
 269             proc_eval[MC_state_get_executed_request(prev_state, &value)->issuer->pid] = 1;
 270
 271           }
 272         }
 273
 274         if (MC_state_interleave_size(state)) {
 275           /* We found a back-tracking point, let's loop */
 276           if(_sg_mc_checkpoint){
 277             if(state->system_state != NULL){
 278               MC_restore_snapshot(state->system_state);
 279               xbt_fifo_unshift(mc_stack_safety, state);
 280               XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety));
 281               MC_UNSET_RAW_MEM;
 282             }else{
 283               pos = xbt_fifo_size(mc_stack_safety);
 284               item = xbt_fifo_get_first_item(mc_stack_safety);
 285               while(pos>0){
 286                 restore_state = (mc_state_t) xbt_fifo_get_item_content(item);
 287                 if(restore_state->system_state != NULL){
 288                   break;
 289                 }else{
 290                   item = xbt_fifo_get_next_item(item);
 291                   pos--;
 292                 }
 293               }
 294               MC_restore_snapshot(restore_state->system_state);
 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, pos);
 299             }
 300           }else{
 301             xbt_fifo_unshift(mc_stack_safety, state);
 302             XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety));
 303             MC_UNSET_RAW_MEM;
 304             MC_replay(mc_stack_safety, -1);
 305           }
 306           break;
 307         } else {
 308           MC_state_delete(state);
 309         }
 310       }
 311       MC_UNSET_RAW_MEM;
 312     }
 313   }
 314   MC_print_statistics(mc_stats);
 315   MC_UNSET_RAW_MEM;
 316
 317   return;
 318 }
 319
 320
 321
 322