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;
 138
 139   while (xbt_fifo_size(mc_stack_safety) > 0) {
 140
 141     /* Get current state */
 142     state = (mc_state_t)
 143       xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_safety));
 144
 145     XBT_DEBUG("**************************************************");
 146     XBT_DEBUG("Exploration depth=%d (state=%p)(%u interleave)",
 147               xbt_fifo_size(mc_stack_safety), state,
 148               MC_state_interleave_size(state));
 149
 150     /* Update statistics */
 151     mc_stats->visited_states++;
 152
 153     /* If there are processes to interleave and the maximum depth has not been reached
 154        then perform one step of the exploration algorithm */
 155     if (xbt_fifo_size(mc_stack_safety) < _sg_mc_max_depth &&
 156         (req = MC_state_get_request(state, &value))) {
 157
 158       /* Debug information */
 159       if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
 160         req_str = MC_request_to_string(req, value);
 161         XBT_DEBUG("Execute: %s", req_str);
 162         xbt_free(req_str);
 163       }
 164
 165       MC_state_set_executed_request(state, req, value);
 166       mc_stats->executed_transitions++;
 167
 168       /* Answer the request */
 169       SIMIX_simcall_pre(req, value); /* After this call req is no longer usefull */
 170
 171       /* Wait for requests (schedules processes) */
 172       MC_wait_for_requests();
 173
 174       /* Create the new expanded state */
 175       MC_SET_RAW_MEM;
 176
 177       next_state = MC_state_new();
 178
 179       if(!is_visited_state()){
 180
 181         /* Get an enabled process and insert it in the interleave set of the next state */
 182         xbt_swag_foreach(process, simix_global->process_list){
 183           if(MC_process_is_enabled(process)){
 184             MC_state_interleave_process(next_state, process);
 185           }
 186         }
 187
 188         if(_sg_mc_checkpoint && ((xbt_fifo_size(mc_stack_safety) + 1) % _sg_mc_checkpoint == 0)){
 189           next_state->system_state = MC_take_snapshot();
 190         }
 191
 192       }else{
 193
 194         XBT_DEBUG("State already visited !");
 195
 196       }
 197
 198       xbt_fifo_unshift(mc_stack_safety, next_state);
 199       MC_UNSET_RAW_MEM;
 200
 201       /* FIXME: Update Statistics
 202          mc_stats->state_size +=
 203          xbt_setset_set_size(next_state->enabled_transitions);*/
 204
 205       /* Let's loop again */
 206
 207       /* The interleave set is empty or the maximum depth is reached, let's back-track */
 208     } else {
 209
 210       if(xbt_fifo_size(mc_stack_safety) == _sg_mc_max_depth)
 211         XBT_WARN("/!\\ Max depth reached ! /!\\ ");
 212       else
 213         XBT_DEBUG("There are no more processes to interleave.");
 214
 215       /* Trash the current state, no longer needed */
 216       MC_SET_RAW_MEM;
 217       xbt_fifo_shift(mc_stack_safety);
 218       MC_state_delete(state);
 219       MC_UNSET_RAW_MEM;
 220
 221       /* Check for deadlocks */
 222       if(MC_deadlock_check()){
 223         MC_show_deadlock(NULL);
 224         return;
 225       }
 226
 227       MC_SET_RAW_MEM;
 228       /* Traverse the stack backwards until a state with a non empty interleave
 229          set is found, deleting all the states that have it empty in the way.
 230          For each deleted state, check if the request that has generated it
 231          (from it's predecesor state), depends on any other previous request
 232          executed before it. If it does then add it to the interleave set of the
 233          state that executed that previous request. */
 234
 235       while ((state = xbt_fifo_shift(mc_stack_safety)) != NULL) {
 236         if(MC_state_interleave_size(state) == 0){
 237           req = MC_state_get_internal_request(state);
 238           xbt_fifo_foreach(mc_stack_safety, item, prev_state, mc_state_t) {
 239             if(MC_request_depend(req, MC_state_get_internal_request(prev_state))){
 240               if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
 241                 XBT_DEBUG("Dependent Transitions:");
 242                 prev_req = MC_state_get_executed_request(prev_state, &value);
 243                 req_str = MC_request_to_string(prev_req, value);
 244                 XBT_DEBUG("%s (state=%p)", req_str, prev_state);
 245                 xbt_free(req_str);
 246                 prev_req = MC_state_get_executed_request(state, &value);
 247                 req_str = MC_request_to_string(prev_req, value);
 248                 XBT_DEBUG("%s (state=%p)", req_str, state);
 249                 xbt_free(req_str);
 250               }
 251
 252               break;
 253
 254             }else if(req->issuer == MC_state_get_executed_request(prev_state, &value)->issuer){
 255
 256               break;
 257
 258             }else{
 259
 260               MC_state_remove_interleave_process(prev_state, req->issuer);
 261
 262             }
 263
 264           }
 265         }
 266
 267         if (MC_state_interleave_size(state)) {
 268           /* We found a back-tracking point, let's loop */
 269           if(_sg_mc_checkpoint){
 270             if(state->system_state != NULL){
 271               MC_restore_snapshot(state->system_state);
 272               xbt_fifo_unshift(mc_stack_safety, state);
 273               XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety));
 274               MC_UNSET_RAW_MEM;
 275             }else{
 276               pos = xbt_fifo_size(mc_stack_safety);
 277               item = xbt_fifo_get_first_item(mc_stack_safety);
 278               while(pos>0){
 279                 restore_state = (mc_state_t) xbt_fifo_get_item_content(item);
 280                 if(restore_state->system_state != NULL){
 281                   break;
 282                 }else{
 283                   item = xbt_fifo_get_next_item(item);
 284                   pos--;
 285                 }
 286               }
 287               MC_restore_snapshot(restore_state->system_state);
 288               xbt_fifo_unshift(mc_stack_safety, state);
 289               XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety));
 290               MC_UNSET_RAW_MEM;
 291               MC_replay(mc_stack_safety, pos);
 292             }
 293           }else{
 294             xbt_fifo_unshift(mc_stack_safety, state);
 295             XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety));
 296             MC_UNSET_RAW_MEM;
 297             MC_replay(mc_stack_safety, -1);
 298           }
 299           break;
 300         } else {
 301           MC_state_delete(state);
 302         }
 303       }
 304       MC_UNSET_RAW_MEM;
 305     }
 306   }
 307   MC_print_statistics(mc_stats);
 308   MC_UNSET_RAW_MEM;
 309
 310   return;
 311 }
 312
 313
 314
 315