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 int nb_visited_states = 0;
  13
  14 static int is_visited_state(void);
  15 static void visited_state_free(mc_safety_visited_state_t state);
  16 static void visited_state_free_voidp(void *s);
  17
  18 static void visited_state_free(mc_safety_visited_state_t state){
  19   if(state){
  20     MC_free_snapshot(state->system_state);
  21     xbt_free(state);
  22   }
  23 }
  24
  25 static void visited_state_free_voidp(void *s){
  26   visited_state_free((mc_safety_visited_state_t) * (void **) s);
  27 }
  28
  29 static int is_visited_state(){
  30
  31   nb_visited_states++;
  32
  33   if(_sg_mc_visited == 0)
  34     return 0;
  35
  36   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
  37
  38   MC_SET_RAW_MEM;
  39
  40   mc_safety_visited_state_t new_state = NULL;
  41   new_state = xbt_new0(s_mc_safety_visited_state_t, 1);
  42   new_state->system_state = MC_take_snapshot();
  43   new_state->num = nb_visited_states;
  44
  45   MC_UNSET_RAW_MEM;
  46
  47   if(xbt_dynar_is_empty(visited_states)){
  48
  49     MC_SET_RAW_MEM;
  50     xbt_dynar_push(visited_states, &new_state);
  51     MC_UNSET_RAW_MEM;
  52
  53     if(raw_mem_set)
  54       MC_SET_RAW_MEM;
  55
  56     return 0;
  57
  58   }else{
  59
  60     MC_SET_RAW_MEM;
  61
  62     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);
  63
  64     unsigned int cursor = 0;
  65     int previous_cursor = 0, next_cursor = 0;
  66     int start = 0;
  67     int end = xbt_dynar_length(visited_states) - 1;
  68
  69     mc_safety_visited_state_t state_test = NULL;
  70     size_t chunks_used_test;
  71     int same_chunks_not_found = 1;
  72
  73     while(start <= end && same_chunks_not_found){
  74       cursor = (start + end) / 2;
  75       state_test = (mc_safety_visited_state_t)xbt_dynar_get_as(visited_states, cursor, mc_safety_visited_state_t);
  76       chunks_used_test = mmalloc_get_chunks_used((xbt_mheap_t)(state_test->system_state)->regions[get_heap_region_index(state_test->system_state)]->data);
  77       if(chunks_used_test < current_chunks_used)
  78         start = cursor + 1;
  79       if(chunks_used_test > current_chunks_used)
  80         end = cursor - 1;
  81       if(chunks_used_test == current_chunks_used){
  82         same_chunks_not_found = 0;
  83         if(snapshot_compare(new_state->system_state, state_test->system_state, NULL, NULL) == 0){
  84           xbt_dynar_remove_at(visited_states, cursor, NULL);
  85           xbt_dynar_insert_at(visited_states, cursor, &new_state);
  86           if(raw_mem_set)
  87             MC_SET_RAW_MEM;
  88           else
  89             MC_UNSET_RAW_MEM;
  90           return 1;
  91         }else{
  92           /* Search another state with same number of chunks used */
  93           previous_cursor = cursor - 1;
  94           while(previous_cursor >= 0){
  95             state_test = (mc_safety_visited_state_t)xbt_dynar_get_as(visited_states, previous_cursor, mc_safety_visited_state_t);
  96             chunks_used_test = mmalloc_get_chunks_used((xbt_mheap_t)(state_test->system_state)->regions[get_heap_region_index(state_test->system_state)]->data);
  97             if(chunks_used_test != current_chunks_used)
  98               break;
  99             if(snapshot_compare(new_state->system_state, state_test->system_state, NULL, NULL) == 0){
 100               xbt_dynar_remove_at(visited_states, previous_cursor, NULL);
 101               xbt_dynar_insert_at(visited_states, previous_cursor, &new_state);
 102               if(raw_mem_set)
 103                 MC_SET_RAW_MEM;
 104               else
 105                 MC_UNSET_RAW_MEM;
 106               return 1;
 107             }
 108             previous_cursor--;
 109           }
 110           next_cursor = cursor + 1;
 111           while(next_cursor < xbt_dynar_length(visited_states)){
 112             state_test = (mc_safety_visited_state_t)xbt_dynar_get_as(visited_states, next_cursor, mc_safety_visited_state_t);
 113             chunks_used_test = mmalloc_get_chunks_used((xbt_mheap_t)(state_test->system_state)->regions[get_heap_region_index(state_test->system_state)]->data);
 114             if(chunks_used_test != current_chunks_used)
 115               break;
 116             if(snapshot_compare(new_state->system_state, state_test->system_state, NULL, NULL) == 0){
 117               xbt_dynar_remove_at(visited_states, next_cursor, NULL);
 118               xbt_dynar_insert_at(visited_states, next_cursor, &new_state);
 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     if(xbt_dynar_length(visited_states) == _sg_mc_visited){
 132       int min = nb_visited_states;
 133       unsigned int cursor2 = 0;
 134       unsigned int index;
 135       xbt_dynar_foreach(visited_states, cursor2, state_test){
 136         if(state_test->num < min){
 137           index = cursor2;
 138           min = state_test->num;
 139         }
 140       }
 141       xbt_dynar_remove_at(visited_states, index, NULL);
 142     }
 143
 144     if(cursor > 0)
 145       cursor--;
 146
 147     if(chunks_used_test < current_chunks_used)
 148       xbt_dynar_insert_at(visited_states, cursor + 1, &new_state);
 149     else
 150       xbt_dynar_insert_at(visited_states, cursor, &new_state);
 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;
 218   smx_simcall_t req = NULL, prev_req = NULL;
 219   s_smx_simcall_t req2;
 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;
 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       /* Answer the request */
 256       SIMIX_simcall_pre(req, value); /* After this call req is no longer usefull */
 257
 258       /* Wait for requests (schedules processes) */
 259       MC_wait_for_requests();
 260
 261       /* Create the new expanded state */
 262       MC_SET_RAW_MEM;
 263
 264       next_state = MC_state_new();
 265
 266       if(!is_visited_state()){
 267
 268         /* Get an enabled process and insert it in the interleave set of the next state */
 269         xbt_swag_foreach(process, simix_global->process_list){
 270           if(MC_process_is_enabled(process)){
 271             MC_state_interleave_process(next_state, process);
 272             XBT_DEBUG("Process %lu enabled with simcall %d", process->pid, process->simcall.call);
 273           }
 274         }
 275
 276         if(_sg_mc_checkpoint && ((xbt_fifo_size(mc_stack_safety) + 1) % _sg_mc_checkpoint == 0)){
 277           next_state->system_state = MC_take_snapshot();
 278         }
 279
 280       }else{
 281
 282         XBT_DEBUG("State already visited !");
 283
 284       }
 285
 286       xbt_fifo_unshift(mc_stack_safety, next_state);
 287       MC_UNSET_RAW_MEM;
 288
 289       /* Let's loop again */
 290
 291       /* The interleave set is empty or the maximum depth is reached, let's back-track */
 292     } else {
 293
 294       if(xbt_fifo_size(mc_stack_safety) == _sg_mc_max_depth)
 295         XBT_WARN("/!\\ Max depth reached ! /!\\ ");
 296       else
 297         XBT_DEBUG("There are no more processes to interleave.");
 298
 299       /* Trash the current state, no longer needed */
 300       MC_SET_RAW_MEM;
 301       xbt_fifo_shift(mc_stack_safety);
 302       MC_state_delete(state);
 303       MC_UNSET_RAW_MEM;
 304
 305       /* Check for deadlocks */
 306       if(MC_deadlock_check()){
 307         MC_show_deadlock(NULL);
 308         return;
 309       }
 310
 311       MC_SET_RAW_MEM;
 312       /* Traverse the stack backwards until a state with a non empty interleave
 313          set is found, deleting all the states that have it empty in the way.
 314          For each deleted state, check if the request that has generated it
 315          (from it's predecesor state), depends on any other previous request
 316          executed before it. If it does then add it to the interleave set of the
 317          state that executed that previous request. */
 318
 319       while ((state = xbt_fifo_shift(mc_stack_safety)) != NULL) {
 320         req = MC_state_get_internal_request(state);
 321         xbt_fifo_foreach(mc_stack_safety, item, prev_state, mc_state_t) {
 322           if(MC_request_depend(req, MC_state_get_internal_request(prev_state))){
 323             if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
 324               XBT_DEBUG("Dependent Transitions:");
 325               prev_req = MC_state_get_executed_request(prev_state, &value);
 326               req_str = MC_request_to_string(prev_req, value);
 327               XBT_DEBUG("%s (state=%p)", req_str, prev_state);
 328               xbt_free(req_str);
 329               prev_req = MC_state_get_executed_request(state, &value);
 330               req_str = MC_request_to_string(prev_req, value);
 331               XBT_DEBUG("%s (state=%p)", req_str, state);
 332               xbt_free(req_str);
 333             }
 334
 335             break;
 336
 337           }else if(req->issuer == MC_state_get_internal_request(prev_state)->issuer){
 338
 339             XBT_DEBUG("Simcall %d and %d with same issuer", req->call, MC_state_get_internal_request(prev_state)->call);
 340             break;
 341
 342           }else{
 343
 344             MC_state_remove_interleave_process(prev_state, req->issuer);
 345             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);
 346
 347           }
 348         }
 349
 350         if (MC_state_interleave_size(state)) {
 351           /* We found a back-tracking point, let's loop */
 352           if(_sg_mc_checkpoint){
 353             if(state->system_state != NULL){
 354               MC_restore_snapshot(state->system_state);
 355               xbt_fifo_unshift(mc_stack_safety, state);
 356               MC_UNSET_RAW_MEM;
 357             }else{
 358               pos = xbt_fifo_size(mc_stack_safety);
 359               item = xbt_fifo_get_first_item(mc_stack_safety);
 360               while(pos>0){
 361                 restore_state = (mc_state_t) xbt_fifo_get_item_content(item);
 362                 if(restore_state->system_state != NULL){
 363                   break;
 364                 }else{
 365                   item = xbt_fifo_get_next_item(item);
 366                   pos--;
 367                 }
 368               }
 369               MC_restore_snapshot(restore_state->system_state);
 370               xbt_fifo_unshift(mc_stack_safety, state);
 371               MC_UNSET_RAW_MEM;
 372               MC_replay(mc_stack_safety, pos);
 373             }
 374           }else{
 375             xbt_fifo_unshift(mc_stack_safety, state);
 376             MC_UNSET_RAW_MEM;
 377             MC_replay(mc_stack_safety, -1);
 378           }
 379
 380           MC_SET_RAW_MEM;
 381           req2 = *req;
 382           for(i=0; i<simix_process_maxpid; i++)
 383             interleave_proc[i] = 0;
 384           i=0;
 385           while((i < MC_state_interleave_size(state))){
 386             i++;
 387             prev_req = MC_state_get_request(state, &value);
 388             if(prev_req != NULL){
 389               MC_state_set_executed_request(state, prev_req, value);
 390               prev_req = MC_state_get_internal_request(state);
 391               if(MC_request_depend(&req2, prev_req)){
 392                 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);
 393                 interleave_proc[prev_req->issuer->pid] = 1;
 394               }else{
 395                 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);
 396                 MC_state_remove_interleave_process(state, prev_req->issuer);
 397               }
 398             }
 399           }
 400           xbt_swag_foreach(process, simix_global->process_list){
 401             if(interleave_proc[process->pid] == 1)
 402               MC_state_interleave_process(state, process);
 403           }
 404           XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety));
 405           MC_UNSET_RAW_MEM;
 406           break;
 407         } else {
 408           MC_state_delete(state);
 409         }
 410       }
 411       MC_UNSET_RAW_MEM;
 412     }
 413   }
 414   MC_print_statistics(mc_stats);
 415   MC_UNSET_RAW_MEM;
 416
 417   return;
 418 }
 419
 420
 421
 422