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