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