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 static void visited_state_free(mc_safety_visited_state_t state);
  15 static void visited_state_free_voidp(void *s);
  16
  17 static void visited_state_free(mc_safety_visited_state_t state){
  18   if(state){
  19     MC_free_snapshot(state->system_state);
  20     xbt_free(state);
  21   }
  22 }
  23
  24 static void visited_state_free_voidp(void *s){
  25   visited_state_free((mc_safety_visited_state_t) * (void **) s);
  26 }
  27
  28 static int is_visited_state(){
  29
  30   if(_sg_mc_visited == 0)
  31     return 0;
  32
  33   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
  34
  35   MC_SET_RAW_MEM;
  36
  37   mc_safety_visited_state_t new_state = NULL;
  38   new_state = xbt_new0(s_mc_safety_visited_state_t, 1);
  39   new_state->system_state = MC_take_snapshot();
  40   new_state->num = mc_stats->expanded_states;
  41
  42   MC_UNSET_RAW_MEM;
  43
  44   if(xbt_dynar_is_empty(visited_states)){
  45
  46     MC_SET_RAW_MEM;
  47     xbt_dynar_push(visited_states, &new_state);
  48     MC_UNSET_RAW_MEM;
  49
  50     if(raw_mem_set)
  51       MC_SET_RAW_MEM;
  52
  53     return 0;
  54
  55   }else{
  56
  57     MC_SET_RAW_MEM;
  58
  59     size_t current_chunks_used = new_state->system_state->heap_chunks_used;
  60
  61     unsigned int cursor = 0;
  62     int previous_cursor = 0, next_cursor = 0;
  63     int start = 0;
  64     int end = xbt_dynar_length(visited_states) - 1;
  65
  66     mc_safety_visited_state_t state_test = NULL;
  67     size_t chunks_used_test;
  68     int same_chunks_not_found = 1;
  69
  70     while(start <= end && same_chunks_not_found){
  71       cursor = (start + end) / 2;
  72       state_test = (mc_safety_visited_state_t)xbt_dynar_get_as(visited_states, cursor, mc_safety_visited_state_t);
  73       chunks_used_test = state_test->system_state->heap_chunks_used;
  74       if(chunks_used_test < current_chunks_used)
  75         start = cursor + 1;
  76       if(chunks_used_test > current_chunks_used)
  77         end = cursor - 1;
  78       if(chunks_used_test == current_chunks_used){
  79         same_chunks_not_found = 0;
  80         if(snapshot_compare(new_state->system_state, state_test->system_state) == 0){
  81           xbt_dynar_remove_at(visited_states, cursor, NULL);
  82           xbt_dynar_insert_at(visited_states, cursor, &new_state);
  83           if(raw_mem_set)
  84             MC_SET_RAW_MEM;
  85           else
  86             MC_UNSET_RAW_MEM;
  87           return 1;
  88         }else{
  89           /* Search another state with same number of chunks used */
  90           previous_cursor = cursor - 1;
  91           while(previous_cursor >= 0){
  92             state_test = (mc_safety_visited_state_t)xbt_dynar_get_as(visited_states, previous_cursor, mc_safety_visited_state_t);
  93             chunks_used_test = state_test->system_state->heap_chunks_used;
  94             if(chunks_used_test != current_chunks_used)
  95               break;
  96             if(snapshot_compare(new_state->system_state, state_test->system_state) == 0){
  97               xbt_dynar_remove_at(visited_states, previous_cursor, NULL);
  98               xbt_dynar_insert_at(visited_states, previous_cursor, &new_state);
  99               if(raw_mem_set)
 100                 MC_SET_RAW_MEM;
 101               else
 102                 MC_UNSET_RAW_MEM;
 103               return 1;
 104             }
 105             previous_cursor--;
 106           }
 107           next_cursor = cursor + 1;
 108           while(next_cursor < xbt_dynar_length(visited_states)){
 109             state_test = (mc_safety_visited_state_t)xbt_dynar_get_as(visited_states, next_cursor, mc_safety_visited_state_t);
 110             chunks_used_test = state_test->system_state->heap_chunks_used;
 111             if(chunks_used_test != current_chunks_used)
 112               break;
 113             if(snapshot_compare(new_state->system_state, state_test->system_state) == 0){
 114               xbt_dynar_remove_at(visited_states, next_cursor, NULL);
 115               xbt_dynar_insert_at(visited_states, next_cursor, &new_state);
 116               if(raw_mem_set)
 117                 MC_SET_RAW_MEM;
 118               else
 119                 MC_UNSET_RAW_MEM;
 120               return 1;
 121             }
 122             next_cursor++;
 123           }
 124         }
 125       }
 126     }
 127
 128     state_test = (mc_safety_visited_state_t)xbt_dynar_get_as(visited_states, cursor, mc_safety_visited_state_t);
 129     chunks_used_test = state_test->system_state->heap_chunks_used;
 130
 131     if(chunks_used_test < current_chunks_used)
 132       xbt_dynar_insert_at(visited_states, cursor + 1, &new_state);
 133     else
 134       xbt_dynar_insert_at(visited_states, cursor, &new_state);
 135
 136     if(xbt_dynar_length(visited_states) > _sg_mc_visited){
 137       int min = mc_stats->expanded_states;
 138       unsigned int cursor2 = 0;
 139       unsigned int index = 0;
 140       xbt_dynar_foreach(visited_states, cursor2, state_test){
 141         if(state_test->num < min){
 142           index = cursor2;
 143           min = state_test->num;
 144         }
 145       }
 146       xbt_dynar_remove_at(visited_states, index, NULL);
 147     }
 148
 149     MC_UNSET_RAW_MEM;
 150
 151     if(raw_mem_set)
 152       MC_SET_RAW_MEM;
 153
 154     return 0;
 155
 156   }
 157 }
 158
 159 /**
 160  *  \brief Initialize the DPOR exploration algorithm
 161  */
 162 void MC_dpor_init()
 163 {
 164
 165   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 166
 167   mc_state_t initial_state = NULL;
 168   smx_process_t process;
 169
 170   /* Create the initial state and push it into the exploration stack */
 171   MC_SET_RAW_MEM;
 172
 173   initial_state = MC_state_new();
 174   visited_states = xbt_dynar_new(sizeof(mc_safety_visited_state_t), visited_state_free_voidp);
 175
 176   MC_UNSET_RAW_MEM;
 177
 178   XBT_DEBUG("**************************************************");
 179   XBT_DEBUG("Initial state");
 180
 181   /* Wait for requests (schedules processes) */
 182   MC_wait_for_requests();
 183
 184   MC_SET_RAW_MEM;
 185
 186   /* Get an enabled process and insert it in the interleave set of the initial state */
 187   xbt_swag_foreach(process, simix_global->process_list){
 188     if(MC_process_is_enabled(process)){
 189       MC_state_interleave_process(initial_state, process);
 190       XBT_DEBUG("Process %lu enabled with simcall %d", process->pid, process->simcall.call);
 191     }
 192   }
 193
 194   xbt_fifo_unshift(mc_stack_safety, initial_state);
 195
 196   MC_UNSET_RAW_MEM;
 197
 198   if(raw_mem_set)
 199     MC_SET_RAW_MEM;
 200   else
 201     MC_UNSET_RAW_MEM;
 202
 203 }
 204
 205
 206 /**
 207  *   \brief Perform the model-checking operation using a depth-first search exploration
 208  *         with Dynamic Partial Order Reductions
 209  */
 210 void MC_dpor(void)
 211 {
 212
 213   char *req_str;
 214   int value, value2;
 215   smx_simcall_t req = NULL, prev_req = NULL, req2 = NULL;
 216   s_smx_simcall_t req3;
 217   mc_state_t state = NULL, prev_state = NULL, next_state = NULL, restore_state=NULL;
 218   smx_process_t process = NULL;
 219   xbt_fifo_item_t item = NULL;
 220   int pos, i, interleave_size;
 221   int interleave_proc[simix_process_maxpid];
 222
 223   while (xbt_fifo_size(mc_stack_safety) > 0) {
 224
 225     /* Get current state */
 226     state = (mc_state_t)
 227       xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_safety));
 228
 229     XBT_DEBUG("**************************************************");
 230     XBT_DEBUG("Exploration depth=%d (state=%p)(%u interleave)",
 231               xbt_fifo_size(mc_stack_safety), state,
 232               MC_state_interleave_size(state));
 233
 234     /* Update statistics */
 235     mc_stats->visited_states++;
 236
 237     /* If there are processes to interleave and the maximum depth has not been reached
 238        then perform one step of the exploration algorithm */
 239     if (xbt_fifo_size(mc_stack_safety) < _sg_mc_max_depth &&
 240         (req = MC_state_get_request(state, &value))) {
 241
 242       /* Debug information */
 243       if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
 244         req_str = MC_request_to_string(req, value);
 245         XBT_DEBUG("Execute: %s", req_str);
 246         xbt_free(req_str);
 247       }
 248
 249       MC_state_set_executed_request(state, req, value);
 250       mc_stats->executed_transitions++;
 251
 252       if(MC_state_interleave_size(state)){
 253         MC_SET_RAW_MEM;
 254         req2 = MC_state_get_internal_request(state);
 255         req3 = *req2;
 256         for(i=0; i<simix_process_maxpid; i++)
 257           interleave_proc[i] = 0;
 258         i=0;
 259         interleave_size = MC_state_interleave_size(state);
 260         while(i < interleave_size){
 261           i++;
 262           prev_req = MC_state_get_request(state, &value2);
 263           if(prev_req != NULL){
 264             MC_state_set_executed_request(state, prev_req, value2);
 265             prev_req = MC_state_get_internal_request(state);
 266             if(MC_request_depend(&req3, prev_req)){
 267               XBT_DEBUG("Simcall %d in process %lu dependant with simcall %d in process %lu", req3.call, req3.issuer->pid, prev_req->call, prev_req->issuer->pid);
 268               interleave_proc[prev_req->issuer->pid] = 1;
 269             }else{
 270               XBT_DEBUG("Simcall %d in process %lu independant with simcall %d in process %lu", req3.call, req3.issuer->pid, prev_req->call, prev_req->issuer->pid);
 271               MC_state_remove_interleave_process(state, prev_req->issuer);
 272             }
 273           }
 274         }
 275         xbt_swag_foreach(process, simix_global->process_list){
 276           if(interleave_proc[process->pid] == 1)
 277             MC_state_interleave_process(state, process);
 278         }
 279         MC_UNSET_RAW_MEM;
 280       }
 281
 282       MC_state_set_executed_request(state, req, value);
 283
 284       /* Answer the request */
 285       SIMIX_simcall_pre(req, value); /* After this call req is no longer usefull */
 286
 287       /* Wait for requests (schedules processes) */
 288       MC_wait_for_requests();
 289
 290       /* Create the new expanded state */
 291       MC_SET_RAW_MEM;
 292
 293       next_state = MC_state_new();
 294
 295       if(!is_visited_state()){
 296
 297         /* Get an enabled process and insert it in the interleave set of the next state */
 298         xbt_swag_foreach(process, simix_global->process_list){
 299           if(MC_process_is_enabled(process)){
 300             MC_state_interleave_process(next_state, process);
 301             XBT_DEBUG("Process %lu enabled with simcall %d", process->pid, process->simcall.call);
 302           }
 303         }
 304
 305         if(_sg_mc_checkpoint && ((xbt_fifo_size(mc_stack_safety) + 1) % _sg_mc_checkpoint == 0)){
 306           next_state->system_state = MC_take_snapshot();
 307         }
 308
 309       }else{
 310
 311         XBT_DEBUG("State already visited !");
 312
 313       }
 314
 315       xbt_fifo_unshift(mc_stack_safety, next_state);
 316       MC_UNSET_RAW_MEM;
 317
 318       /* Let's loop again */
 319
 320       /* The interleave set is empty or the maximum depth is reached, let's back-track */
 321     } else {
 322
 323       if(xbt_fifo_size(mc_stack_safety) == _sg_mc_max_depth)
 324         XBT_WARN("/!\\ Max depth reached ! /!\\ ");
 325       else
 326         XBT_DEBUG("There are no more processes to interleave.");
 327
 328       /* Trash the current state, no longer needed */
 329       MC_SET_RAW_MEM;
 330       xbt_fifo_shift(mc_stack_safety);
 331       MC_state_delete(state);
 332       MC_UNSET_RAW_MEM;
 333
 334       /* Check for deadlocks */
 335       if(MC_deadlock_check()){
 336         MC_show_deadlock(NULL);
 337         return;
 338       }
 339
 340       MC_SET_RAW_MEM;
 341       /* Traverse the stack backwards until a state with a non empty interleave
 342          set is found, deleting all the states that have it empty in the way.
 343          For each deleted state, check if the request that has generated it
 344          (from it's predecesor state), depends on any other previous request
 345          executed before it. If it does then add it to the interleave set of the
 346          state that executed that previous request. */
 347
 348       while ((state = xbt_fifo_shift(mc_stack_safety)) != NULL) {
 349         req = MC_state_get_internal_request(state);
 350         xbt_fifo_foreach(mc_stack_safety, item, prev_state, mc_state_t) {
 351           if(MC_request_depend(req, MC_state_get_internal_request(prev_state))){
 352             if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
 353               XBT_DEBUG("Dependent Transitions:");
 354               prev_req = MC_state_get_executed_request(prev_state, &value);
 355               req_str = MC_request_to_string(prev_req, value);
 356               XBT_DEBUG("%s (state=%p)", req_str, prev_state);
 357               xbt_free(req_str);
 358               prev_req = MC_state_get_executed_request(state, &value);
 359               req_str = MC_request_to_string(prev_req, value);
 360               XBT_DEBUG("%s (state=%p)", req_str, state);
 361               xbt_free(req_str);
 362             }
 363
 364             break;
 365
 366           }else if(req->issuer == MC_state_get_internal_request(prev_state)->issuer){
 367
 368             XBT_DEBUG("Simcall %d and %d with same issuer", req->call, MC_state_get_internal_request(prev_state)->call);
 369             break;
 370
 371           }else{
 372
 373             MC_state_remove_interleave_process(prev_state, req->issuer);
 374             XBT_DEBUG("Simcall %d in process %lu independant with simcall %d process %lu", req->call, req->issuer->pid, MC_state_get_internal_request(prev_state)->call, MC_state_get_internal_request(prev_state)->issuer->pid);
 375
 376           }
 377         }
 378
 379         if (MC_state_interleave_size(state)) {
 380           /* We found a back-tracking point, let's loop */
 381           if(_sg_mc_checkpoint){
 382             if(state->system_state != NULL){
 383               MC_restore_snapshot(state->system_state);
 384               xbt_fifo_unshift(mc_stack_safety, state);
 385               MC_UNSET_RAW_MEM;
 386             }else{
 387               pos = xbt_fifo_size(mc_stack_safety);
 388               item = xbt_fifo_get_first_item(mc_stack_safety);
 389               while(pos>0){
 390                 restore_state = (mc_state_t) xbt_fifo_get_item_content(item);
 391                 if(restore_state->system_state != NULL){
 392                   break;
 393                 }else{
 394                   item = xbt_fifo_get_next_item(item);
 395                   pos--;
 396                 }
 397               }
 398               MC_restore_snapshot(restore_state->system_state);
 399               xbt_fifo_unshift(mc_stack_safety, state);
 400               MC_UNSET_RAW_MEM;
 401               MC_replay(mc_stack_safety, pos);
 402             }
 403           }else{
 404             xbt_fifo_unshift(mc_stack_safety, state);
 405             MC_UNSET_RAW_MEM;
 406             MC_replay(mc_stack_safety, -1);
 407           }
 408           XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety));
 409           break;
 410         } else {
 411           MC_state_delete(state);
 412         }
 413       }
 414       MC_UNSET_RAW_MEM;
 415     }
 416   }
 417   MC_print_statistics(mc_stats);
 418   MC_UNSET_RAW_MEM;
 419
 420   return;
 421 }
 422
 423
 424
 425