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 = mmalloc_get_chunks_used((xbt_mheap_t)(new_state->system_state)->regions[get_heap_region_index(new_state->system_state)]->data);
  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 = mmalloc_get_chunks_used((xbt_mheap_t)(state_test->system_state)->regions[get_heap_region_index(state_test->system_state)]->data);
  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, NULL, NULL) == 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 = mmalloc_get_chunks_used((xbt_mheap_t)(state_test->system_state)->regions[get_heap_region_index(state_test->system_state)]->data);
  94             if(chunks_used_test != current_chunks_used)
  95               break;
  96             if(snapshot_compare(new_state->system_state, state_test->system_state, NULL, NULL) == 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 = mmalloc_get_chunks_used((xbt_mheap_t)(state_test->system_state)->regions[get_heap_region_index(state_test->system_state)]->data);
 111             if(chunks_used_test != current_chunks_used)
 112               break;
 113             if(snapshot_compare(new_state->system_state, state_test->system_state, NULL, NULL) == 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 = mmalloc_get_chunks_used((xbt_mheap_t)(state_test->system_state)->regions[get_heap_region_index(state_test->system_state)]->data);
 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;
 215   smx_simcall_t req = NULL, prev_req = NULL;
 216   s_smx_simcall_t req2;
 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;
 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       /* Answer the request */
 253       SIMIX_simcall_pre(req, value); /* After this call req is no longer usefull */
 254
 255       /* Wait for requests (schedules processes) */
 256       MC_wait_for_requests();
 257
 258       /* Create the new expanded state */
 259       MC_SET_RAW_MEM;
 260
 261       next_state = MC_state_new();
 262
 263       if(!is_visited_state()){
 264
 265         /* Get an enabled process and insert it in the interleave set of the next state */
 266         xbt_swag_foreach(process, simix_global->process_list){
 267           if(MC_process_is_enabled(process)){
 268             MC_state_interleave_process(next_state, process);
 269             XBT_DEBUG("Process %lu enabled with simcall %d", process->pid, process->simcall.call);
 270           }
 271         }
 272
 273         if(_sg_mc_checkpoint && ((xbt_fifo_size(mc_stack_safety) + 1) % _sg_mc_checkpoint == 0)){
 274           next_state->system_state = MC_take_snapshot();
 275         }
 276
 277       }else{
 278
 279         XBT_DEBUG("State already visited !");
 280
 281       }
 282
 283       xbt_fifo_unshift(mc_stack_safety, next_state);
 284       MC_UNSET_RAW_MEM;
 285
 286       /* Let's loop again */
 287
 288       /* The interleave set is empty or the maximum depth is reached, let's back-track */
 289     } else {
 290
 291       if(xbt_fifo_size(mc_stack_safety) == _sg_mc_max_depth)
 292         XBT_WARN("/!\\ Max depth reached ! /!\\ ");
 293       else
 294         XBT_DEBUG("There are no more processes to interleave.");
 295
 296       /* Trash the current state, no longer needed */
 297       MC_SET_RAW_MEM;
 298       xbt_fifo_shift(mc_stack_safety);
 299       MC_state_delete(state);
 300       MC_UNSET_RAW_MEM;
 301
 302       /* Check for deadlocks */
 303       if(MC_deadlock_check()){
 304         MC_show_deadlock(NULL);
 305         return;
 306       }
 307
 308       MC_SET_RAW_MEM;
 309       /* Traverse the stack backwards until a state with a non empty interleave
 310          set is found, deleting all the states that have it empty in the way.
 311          For each deleted state, check if the request that has generated it
 312          (from it's predecesor state), depends on any other previous request
 313          executed before it. If it does then add it to the interleave set of the
 314          state that executed that previous request. */
 315
 316       while ((state = xbt_fifo_shift(mc_stack_safety)) != NULL) {
 317         req = MC_state_get_internal_request(state);
 318         xbt_fifo_foreach(mc_stack_safety, item, prev_state, mc_state_t) {
 319           if(MC_request_depend(req, MC_state_get_internal_request(prev_state))){
 320             if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
 321               XBT_DEBUG("Dependent Transitions:");
 322               prev_req = MC_state_get_executed_request(prev_state, &value);
 323               req_str = MC_request_to_string(prev_req, value);
 324               XBT_DEBUG("%s (state=%p)", req_str, prev_state);
 325               xbt_free(req_str);
 326               prev_req = MC_state_get_executed_request(state, &value);
 327               req_str = MC_request_to_string(prev_req, value);
 328               XBT_DEBUG("%s (state=%p)", req_str, state);
 329               xbt_free(req_str);
 330             }
 331
 332             break;
 333
 334           }else if(req->issuer == MC_state_get_internal_request(prev_state)->issuer){
 335
 336             XBT_DEBUG("Simcall %d and %d with same issuer", req->call, MC_state_get_internal_request(prev_state)->call);
 337             break;
 338
 339           }else{
 340
 341             MC_state_remove_interleave_process(prev_state, req->issuer);
 342             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);
 343
 344           }
 345         }
 346
 347         if (MC_state_interleave_size(state)) {
 348           /* We found a back-tracking point, let's loop */
 349           if(_sg_mc_checkpoint){
 350             if(state->system_state != NULL){
 351               MC_restore_snapshot(state->system_state);
 352               xbt_fifo_unshift(mc_stack_safety, state);
 353               MC_UNSET_RAW_MEM;
 354             }else{
 355               pos = xbt_fifo_size(mc_stack_safety);
 356               item = xbt_fifo_get_first_item(mc_stack_safety);
 357               while(pos>0){
 358                 restore_state = (mc_state_t) xbt_fifo_get_item_content(item);
 359                 if(restore_state->system_state != NULL){
 360                   break;
 361                 }else{
 362                   item = xbt_fifo_get_next_item(item);
 363                   pos--;
 364                 }
 365               }
 366               MC_restore_snapshot(restore_state->system_state);
 367               xbt_fifo_unshift(mc_stack_safety, state);
 368               MC_UNSET_RAW_MEM;
 369               MC_replay(mc_stack_safety, pos);
 370             }
 371           }else{
 372             xbt_fifo_unshift(mc_stack_safety, state);
 373             MC_UNSET_RAW_MEM;
 374             MC_replay(mc_stack_safety, -1);
 375           }
 376
 377           MC_SET_RAW_MEM;
 378           req2 = *req;
 379           for(i=0; i<simix_process_maxpid; i++)
 380             interleave_proc[i] = 0;
 381           i=0;
 382           while((i < MC_state_interleave_size(state))){
 383             i++;
 384             prev_req = MC_state_get_request(state, &value);
 385             if(prev_req != NULL){
 386               MC_state_set_executed_request(state, prev_req, value);
 387               prev_req = MC_state_get_internal_request(state);
 388               if(MC_request_depend(&req2, prev_req)){
 389                 XBT_DEBUG("Simcall %d in process %lu dependant with simcall %d in process %lu", req2.call, req2.issuer->pid, prev_req->call, prev_req->issuer->pid);
 390                 interleave_proc[prev_req->issuer->pid] = 1;
 391               }else{
 392                 XBT_DEBUG("Simcall %d in process %lu independant with simcall %d in process %lu", req2.call, req2.issuer->pid, prev_req->call, prev_req->issuer->pid);
 393                 MC_state_remove_interleave_process(state, prev_req->issuer);
 394               }
 395             }
 396           }
 397           xbt_swag_foreach(process, simix_global->process_list){
 398             if(interleave_proc[process->pid] == 1)
 399               MC_state_interleave_process(state, process);
 400           }
 401           XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety));
 402           MC_UNSET_RAW_MEM;
 403           break;
 404         } else {
 405           MC_state_delete(state);
 406         }
 407       }
 408       MC_UNSET_RAW_MEM;
 409     }
 410   }
 411   MC_print_statistics(mc_stats);
 412   MC_UNSET_RAW_MEM;
 413
 414   return;
 415 }
 416
 417
 418
 419