src/mc/mc_dpor.c

   1 /* Copyright (c) 2008-2013. The SimGrid Team.
   2  * All rights reserved.                                                     */
   3
   4 /* This program is free software; you can redistribute it and/or modify it
   5  * under the terms of the license (GNU LGPL) which comes with this package. */
   6
   7 #include "mc_private.h"
   8
   9 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_dpor, mc,
  10                                 "Logging specific to MC DPOR exploration");
  11
  12 /********** Global variables **********/
  13
  14 xbt_dynar_t visited_states;
  15 xbt_dict_t first_enabled_state;
  16 xbt_dynar_t initial_communications_pattern;
  17 xbt_dynar_t communications_pattern;
  18 int nb_comm_pattern;
  19
  20 /********** Static functions ***********/
  21
  22 static void comm_pattern_free(mc_comm_pattern_t p){
  23   xbt_free(p->rdv);
  24   xbt_free(p->data);
  25   xbt_free(p);
  26   p = NULL;
  27 }
  28
  29 static void comm_pattern_free_voidp( void *p){
  30   comm_pattern_free((mc_comm_pattern_t) * (void **)p);
  31 }
  32
  33 static mc_comm_pattern_t get_comm_pattern_from_idx(xbt_dynar_t pattern, unsigned int *idx, e_smx_comm_type_t type, unsigned long proc){
  34   mc_comm_pattern_t current_comm;
  35   while(*idx < xbt_dynar_length(pattern)){
  36     current_comm = (mc_comm_pattern_t)xbt_dynar_get_as(pattern, *idx, mc_comm_pattern_t);
  37     if(current_comm->type == type && type == SIMIX_COMM_SEND){
  38       if(current_comm->src_proc == proc)
  39         return current_comm;
  40     }else if(current_comm->type == type && type == SIMIX_COMM_RECEIVE){
  41       if(current_comm->dst_proc == proc)
  42         return current_comm;
  43     }
  44     (*idx)++;
  45   }
  46   return NULL;
  47 }
  48
  49 static int compare_comm_pattern(mc_comm_pattern_t comm1, mc_comm_pattern_t comm2){
  50   if(strcmp(comm1->rdv, comm2->rdv) != 0)
  51     return 1;
  52   if(comm1->src_proc != comm2->src_proc)
  53     return 1;
  54   if(comm1->dst_proc != comm2->dst_proc)
  55     return 1;
  56   if(comm1->data_size != comm2->data_size)
  57     return 1;
  58   if(memcmp(comm1->data, comm2->data, comm1->data_size) != 0)
  59     return 1;
  60   return 0;
  61 }
  62
  63 static void deterministic_pattern(xbt_dynar_t initial_pattern, xbt_dynar_t pattern){
  64   unsigned int cursor = 0, send_index = 0, recv_index = 0;
  65   mc_comm_pattern_t comm1, comm2;
  66   int comm_comparison = 0;
  67   int current_process = 0;
  68   while(current_process < simix_process_maxpid){
  69     while(cursor < xbt_dynar_length(initial_pattern)){
  70       comm1 = (mc_comm_pattern_t)xbt_dynar_get_as(initial_pattern, cursor, mc_comm_pattern_t);
  71       if(comm1->type == SIMIX_COMM_SEND && comm1->src_proc == current_process){
  72         comm2 = get_comm_pattern_from_idx(pattern, &send_index, comm1->type, current_process);
  73         comm_comparison = compare_comm_pattern(comm1, comm2);
  74         if(comm_comparison == 1){
  75           initial_state_safety->send_deterministic = 0;
  76           initial_state_safety->comm_deterministic = 0;
  77           return;
  78         }
  79         send_index++;
  80       }else if(comm1->type == SIMIX_COMM_RECEIVE && comm1->dst_proc == current_process){
  81         comm2 = get_comm_pattern_from_idx(pattern, &recv_index, comm1->type, current_process);
  82         comm_comparison = compare_comm_pattern(comm1, comm2);
  83         if(comm_comparison == 1){
  84           initial_state_safety->comm_deterministic = 0;
  85         }
  86         recv_index++;
  87       }
  88       cursor++;
  89     }
  90     cursor = 0;
  91     send_index = 0;
  92     recv_index = 0;
  93     current_process++;
  94   }
  95 }
  96
  97 static int complete_comm_pattern(xbt_dynar_t list, mc_comm_pattern_t pattern){
  98   mc_comm_pattern_t current_pattern;
  99   unsigned int cursor = 0;
 100   xbt_dynar_foreach(list, cursor, current_pattern){
 101     if(current_pattern->comm == pattern->comm){
 102       if(!current_pattern->completed){
 103         current_pattern->src_proc = pattern->comm->comm.src_proc->pid;
 104         current_pattern->dst_proc = pattern->comm->comm.dst_proc->pid;
 105         current_pattern->data_size = pattern->comm->comm.src_buff_size;
 106         current_pattern->data = xbt_malloc0(current_pattern->data_size);
 107         current_pattern->matched_comm = pattern->num;
 108         memcpy(current_pattern->data, current_pattern->comm->comm.src_buff, current_pattern->data_size);
 109         current_pattern->completed = 1;
 110         return current_pattern->num;
 111       }
 112     }
 113   }
 114   return -1;
 115 }
 116
 117 void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, int call){
 118   mc_comm_pattern_t pattern = NULL;
 119   pattern = xbt_new0(s_mc_comm_pattern_t, 1);
 120   pattern->num = ++nb_comm_pattern;
 121   pattern->completed = 0;
 122   if(call == 1){ // ISEND
 123     pattern->comm = simcall_comm_isend__get__result(request);
 124     pattern->type = SIMIX_COMM_SEND;
 125     if(pattern->comm->comm.dst_proc != NULL){
 126
 127       pattern->matched_comm = complete_comm_pattern(list, pattern);
 128       pattern->dst_proc = pattern->comm->comm.dst_proc->pid;
 129       pattern->completed = 1;
 130     }
 131     pattern->src_proc = pattern->comm->comm.src_proc->pid;
 132     pattern->data_size = pattern->comm->comm.src_buff_size;
 133     pattern->data=xbt_malloc0(pattern->data_size);
 134     memcpy(pattern->data, pattern->comm->comm.src_buff, pattern->data_size);
 135   }else{ // IRECV
 136     pattern->comm = simcall_comm_irecv__get__result(request);
 137     pattern->type = SIMIX_COMM_RECEIVE;
 138     if(pattern->comm->comm.src_proc != NULL){
 139       pattern->matched_comm = complete_comm_pattern(list, pattern);
 140       pattern->src_proc = pattern->comm->comm.src_proc->pid;
 141       pattern->completed = 1;
 142       pattern->data_size = pattern->comm->comm.src_buff_size;
 143       pattern->data=xbt_malloc0(pattern->data_size);
 144       memcpy(pattern->data, pattern->comm->comm.src_buff, pattern->data_size);
 145     }
 146     pattern->dst_proc = pattern->comm->comm.dst_proc->pid;
 147   }
 148   if(pattern->comm->comm.rdv != NULL)
 149     pattern->rdv = strdup(pattern->comm->comm.rdv->name);
 150   else
 151     pattern->rdv = strdup(pattern->comm->comm.rdv_cpy->name);
 152   xbt_dynar_push(list, &pattern);
 153 }
 154
 155 static void print_communications_pattern(xbt_dynar_t comms_pattern){
 156   unsigned int cursor = 0;
 157   mc_comm_pattern_t current_comm;
 158   xbt_dynar_foreach(comms_pattern, cursor, current_comm){
 159     // fprintf(stderr, "%s (%d - comm %p, src : %lu, dst %lu, rdv name %s, data %p, matched with %d)\n", current_comm->type == SIMIX_COMM_SEND ? "iSend" : "iRecv", current_comm->num, current_comm->comm, current_comm->src_proc, current_comm->dst_proc, current_comm->rdv, current_comm->data, current_comm->matched_comm);
 160   }
 161 }
 162
 163 static void visited_state_free(mc_visited_state_t state){
 164   if(state){
 165     MC_free_snapshot(state->system_state);
 166     xbt_free(state);
 167   }
 168 }
 169
 170 static void visited_state_free_voidp(void *s){
 171   visited_state_free((mc_visited_state_t) * (void **) s);
 172 }
 173
 174 /** \brief Save the current state
 175  *
 176  *  \return Snapshot of the current state.
 177  */
 178 static mc_visited_state_t visited_state_new(){
 179
 180   mc_visited_state_t new_state = NULL;
 181   new_state = xbt_new0(s_mc_visited_state_t, 1);
 182   new_state->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
 183   new_state->nb_processes = xbt_swag_size(simix_global->process_list);
 184   new_state->system_state = MC_take_snapshot(mc_stats->expanded_states);
 185   new_state->num = mc_stats->expanded_states;
 186   new_state->other_num = -1;
 187
 188   return new_state;
 189
 190 }
 191
 192 /** \brief Find a suitable subrange of candidate duplicates for a given state
 193  *
 194  *  \param all_ pairs dynamic array of states with candidate duplicates of the current state;
 195  *  \param pair current state;
 196  *  \param min (output) index of the beginning of the the subrange
 197  *  \param max (output) index of the enf of the subrange
 198  *
 199  *  Given a suitably ordered array of state, this function extracts a subrange
 200  *  (with index *min <= i <= *max) with candidate duplicates of the given state.
 201  *  This function uses only fast discriminating criterions and does not use the
 202  *  full state comparison algorithms.
 203  *
 204  *  The states in all_pairs MUST be ordered using a (given) weak order
 205  *  (based on nb_processes and heap_bytes_used).
 206  *  The subrange is the subrange of "equivalence" of the given state.
 207  */
 208 static int get_search_interval(xbt_dynar_t all_states, mc_visited_state_t state, int *min, int *max){
 209
 210   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 211
 212   MC_SET_RAW_MEM;
 213
 214   int cursor = 0, previous_cursor, next_cursor;
 215   mc_visited_state_t state_test;
 216   int start = 0;
 217   int end = xbt_dynar_length(all_states) - 1;
 218
 219   while(start <= end){
 220     cursor = (start + end) / 2;
 221     state_test = (mc_visited_state_t)xbt_dynar_get_as(all_states, cursor, mc_visited_state_t);
 222     if(state_test->nb_processes < state->nb_processes){
 223       start = cursor + 1;
 224     }else if(state_test->nb_processes > state->nb_processes){
 225       end = cursor - 1;
 226     }else{
 227       if(state_test->heap_bytes_used < state->heap_bytes_used){
 228         start = cursor +1;
 229       }else if(state_test->heap_bytes_used > state->heap_bytes_used){
 230         end = cursor - 1;
 231       }else{
 232         *min = *max = cursor;
 233         previous_cursor = cursor - 1;
 234         while(previous_cursor >= 0){
 235           state_test = (mc_visited_state_t)xbt_dynar_get_as(all_states, previous_cursor, mc_visited_state_t);
 236           if(state_test->nb_processes != state->nb_processes || state_test->heap_bytes_used != state->heap_bytes_used)
 237             break;
 238           *min = previous_cursor;
 239           previous_cursor--;
 240         }
 241         next_cursor = cursor + 1;
 242         while(next_cursor < xbt_dynar_length(all_states)){
 243           state_test = (mc_visited_state_t)xbt_dynar_get_as(all_states, next_cursor, mc_visited_state_t);
 244           if(state_test->nb_processes != state->nb_processes || state_test->heap_bytes_used != state->heap_bytes_used)
 245             break;
 246           *max = next_cursor;
 247           next_cursor++;
 248         }
 249         if(!raw_mem_set)
 250           MC_UNSET_RAW_MEM;
 251         return -1;
 252       }
 253      }
 254   }
 255
 256   if(!raw_mem_set)
 257     MC_UNSET_RAW_MEM;
 258
 259   return cursor;
 260 }
 261
 262 /** \brief Take a snapshot the current state and process it.
 263  *
 264  *  \return number of the duplicate state or -1 (not visited)
 265  */
 266 static int is_visited_state(){
 267
 268   if(_sg_mc_visited == 0)
 269     return -1;
 270
 271   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 272
 273   MC_SET_RAW_MEM;
 274
 275   mc_visited_state_t new_state = visited_state_new();
 276
 277   if(xbt_dynar_is_empty(visited_states)){
 278
 279     xbt_dynar_push(visited_states, &new_state);
 280
 281     if(!raw_mem_set)
 282       MC_UNSET_RAW_MEM;
 283
 284     return -1;
 285
 286   }else{
 287
 288     int min = -1, max = -1, index;
 289     //int res;
 290     mc_visited_state_t state_test;
 291     int cursor;
 292
 293     index = get_search_interval(visited_states, new_state, &min, &max);
 294
 295     if(min != -1 && max != -1){
 296
 297       // Parallell implementation
 298       /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_states, min), (max-min)+1, new_state);
 299       if(res != -1){
 300         state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, (min+res)-1, mc_visited_state_t);
 301         if(state_test->other_num == -1)
 302           new_state->other_num = state_test->num;
 303         else
 304           new_state->other_num = state_test->other_num;
 305         if(dot_output == NULL)
 306           XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
 307         else
 308           XBT_DEBUG("State %d already visited ! (equal to state %d (state %d in dot_output))", new_state->num, state_test->num, new_state->other_num);
 309         xbt_dynar_remove_at(visited_states, (min + res) - 1, NULL);
 310         xbt_dynar_insert_at(visited_states, (min+res) - 1, &new_state);
 311         if(!raw_mem_set)
 312           MC_UNSET_RAW_MEM;
 313         return new_state->other_num;
 314         }*/
 315
 316       cursor = min;
 317       while(cursor <= max){
 318         state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, cursor, mc_visited_state_t);
 319         if(snapshot_compare(state_test, new_state) == 0){
 320           // The state has been visited:
 321
 322           if(state_test->other_num == -1)
 323             new_state->other_num = state_test->num;
 324           else
 325             new_state->other_num = state_test->other_num;
 326           if(dot_output == NULL)
 327             XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
 328           else
 329             XBT_DEBUG("State %d already visited ! (equal to state %d (state %d in dot_output))", new_state->num, state_test->num, new_state->other_num);
 330
 331           // Replace the old state with the new one (why?):
 332           xbt_dynar_remove_at(visited_states, cursor, NULL);
 333           xbt_dynar_insert_at(visited_states, cursor, &new_state);
 334
 335           if(!raw_mem_set)
 336             MC_UNSET_RAW_MEM;
 337           return new_state->other_num;
 338         }
 339         cursor++;
 340       }
 341
 342       // The state has not been visited, add it to the list:
 343       xbt_dynar_insert_at(visited_states, min, &new_state);
 344
 345     }else{
 346
 347       // The state has not been visited: insert the state in the dynamic array.
 348       state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, index, mc_visited_state_t);
 349       if(state_test->nb_processes < new_state->nb_processes){
 350         xbt_dynar_insert_at(visited_states, index+1, &new_state);
 351       }else{
 352         if(state_test->heap_bytes_used < new_state->heap_bytes_used)
 353           xbt_dynar_insert_at(visited_states, index + 1, &new_state);
 354         else
 355           xbt_dynar_insert_at(visited_states, index, &new_state);
 356       }
 357
 358     }
 359
 360     // We have reached the maximum number of stored states;
 361     if(xbt_dynar_length(visited_states) > _sg_mc_visited){
 362
 363       // Find the (index of the) older state:
 364       int min2 = mc_stats->expanded_states;
 365       unsigned int cursor2 = 0;
 366       unsigned int index2 = 0;
 367       xbt_dynar_foreach(visited_states, cursor2, state_test){
 368         if(state_test->num < min2){
 369           index2 = cursor2;
 370           min2 = state_test->num;
 371         }
 372       }
 373
 374       // and drop it:
 375       xbt_dynar_remove_at(visited_states, index2, NULL);
 376     }
 377
 378     if(!raw_mem_set)
 379       MC_UNSET_RAW_MEM;
 380
 381     return -1;
 382
 383   }
 384 }
 385
 386 /**
 387  *  \brief Initialize the DPOR exploration algorithm
 388  */
 389 void MC_dpor_init()
 390 {
 391
 392   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 393
 394   mc_state_t initial_state = NULL;
 395   smx_process_t process;
 396
 397   /* Create the initial state and push it into the exploration stack */
 398   MC_SET_RAW_MEM;
 399
 400   if(_sg_mc_visited > 0)
 401     visited_states = xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp);
 402
 403   first_enabled_state = xbt_dict_new_homogeneous(&xbt_free_f);
 404
 405   initial_communications_pattern = xbt_dynar_new(sizeof(mc_comm_pattern_t), comm_pattern_free_voidp);
 406   communications_pattern = xbt_dynar_new(sizeof(mc_comm_pattern_t), comm_pattern_free_voidp);
 407   nb_comm_pattern = 0;
 408
 409   initial_state = MC_state_new();
 410
 411   MC_UNSET_RAW_MEM;
 412
 413   XBT_DEBUG("**************************************************");
 414   XBT_DEBUG("Initial state");
 415
 416   /* Wait for requests (schedules processes) */
 417   MC_wait_for_requests();
 418
 419   MC_ignore_heap(simix_global->process_to_run->data, 0);
 420   MC_ignore_heap(simix_global->process_that_ran->data, 0);
 421
 422   MC_SET_RAW_MEM;
 423
 424   /* Get an enabled process and insert it in the interleave set of the initial state */
 425   xbt_swag_foreach(process, simix_global->process_list){
 426     if(MC_process_is_enabled(process)){
 427       MC_state_interleave_process(initial_state, process);
 428       if(mc_reduce_kind != e_mc_reduce_none)
 429         break;
 430     }
 431   }
 432
 433   xbt_fifo_unshift(mc_stack_safety, initial_state);
 434
 435   /* To ensure the soundness of DPOR, we have to keep a list of
 436      processes which are still enabled at each step of the exploration.
 437      If max depth is reached, we interleave them in the state in which they have
 438      been enabled for the first time. */
 439   xbt_swag_foreach(process, simix_global->process_list){
 440     if(MC_process_is_enabled(process)){
 441       char *key = bprintf("%lu", process->pid);
 442       char *data = bprintf("%d", xbt_fifo_size(mc_stack_safety));
 443       xbt_dict_set(first_enabled_state, key, data, NULL);
 444       xbt_free(key);
 445     }
 446   }
 447
 448   MC_UNSET_RAW_MEM;
 449
 450   if(raw_mem_set)
 451     MC_SET_RAW_MEM;
 452   else
 453     MC_UNSET_RAW_MEM;
 454
 455 }
 456
 457
 458 /** \brief Model-check the application using a DFS exploration
 459  *         with DPOR (Dynamic Partial Order Reductions)
 460  */
 461 void MC_dpor(void)
 462 {
 463
 464   char *req_str = NULL;
 465   int value;
 466   smx_simcall_t req = NULL, prev_req = NULL;
 467   mc_state_t state = NULL, prev_state = NULL, next_state = NULL, restored_state=NULL;
 468   smx_process_t process = NULL;
 469   xbt_fifo_item_t item = NULL;
 470   mc_state_t state_test = NULL;
 471   int pos;
 472   int visited_state = -1;
 473   int enabled = 0;
 474   int interleave_size = 0;
 475   int comm_pattern = 0;
 476
 477   while (xbt_fifo_size(mc_stack_safety) > 0) {
 478
 479     /* Get current state */
 480     state = (mc_state_t)
 481       xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_safety));
 482
 483     XBT_DEBUG("**************************************************");
 484     XBT_DEBUG("Exploration depth=%d (state=%p, num %d)(%u interleave, user_max_depth %d, first_enabled_state size : %d)",
 485               xbt_fifo_size(mc_stack_safety), state, state->num,
 486               MC_state_interleave_size(state), user_max_depth_reached, xbt_dict_size(first_enabled_state));
 487
 488     interleave_size = MC_state_interleave_size(state);
 489
 490     /* Update statistics */
 491     mc_stats->visited_states++;
 492
 493     /* If there are processes to interleave and the maximum depth has not been reached
 494        then perform one step of the exploration algorithm */
 495     if (xbt_fifo_size(mc_stack_safety) <= _sg_mc_max_depth && !user_max_depth_reached &&
 496         (req = MC_state_get_request(state, &value)) && visited_state == -1) {
 497
 498       /* Debug information */
 499       if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
 500         req_str = MC_request_to_string(req, value);
 501         XBT_DEBUG("Execute: %s", req_str);
 502         xbt_free(req_str);
 503       }
 504
 505       MC_SET_RAW_MEM;
 506       if(dot_output != NULL)
 507         req_str = MC_request_get_dot_output(req, value);
 508       MC_UNSET_RAW_MEM;
 509
 510       MC_state_set_executed_request(state, req, value);
 511       mc_stats->executed_transitions++;
 512
 513       MC_SET_RAW_MEM;
 514       char *key = bprintf("%lu", req->issuer->pid);
 515       xbt_dict_remove(first_enabled_state, key);
 516       xbt_free(key);
 517       MC_UNSET_RAW_MEM;
 518
 519       if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
 520         if(req->call == SIMCALL_COMM_ISEND)
 521           comm_pattern = 1;
 522         else if(req->call == SIMCALL_COMM_IRECV)
 523           comm_pattern = 2;
 524       }
 525
 526       /* Answer the request */
 527       SIMIX_simcall_pre(req, value); /* After this call req is no longer usefull */
 528
 529       if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
 530         MC_SET_RAW_MEM;
 531         if(comm_pattern != 0){
 532           if(!initial_state_safety->initial_communications_pattern_done)
 533             get_comm_pattern(initial_communications_pattern, req, comm_pattern);
 534           else
 535             get_comm_pattern(communications_pattern, req, comm_pattern);
 536         }
 537         MC_UNSET_RAW_MEM;
 538         comm_pattern = 0;
 539       }
 540
 541       /* Wait for requests (schedules processes) */
 542       MC_wait_for_requests();
 543
 544       /* Create the new expanded state */
 545       MC_SET_RAW_MEM;
 546
 547       next_state = MC_state_new();
 548
 549       if((visited_state = is_visited_state()) == -1){
 550
 551         /* Get an enabled process and insert it in the interleave set of the next state */
 552         xbt_swag_foreach(process, simix_global->process_list){
 553           if(MC_process_is_enabled(process)){
 554             MC_state_interleave_process(next_state, process);
 555             if(mc_reduce_kind != e_mc_reduce_none)
 556               break;
 557           }
 558         }
 559
 560         if(_sg_mc_checkpoint && ((xbt_fifo_size(mc_stack_safety) + 1) % _sg_mc_checkpoint == 0)){
 561           next_state->system_state = MC_take_snapshot(next_state->num);
 562         }
 563
 564         if(dot_output != NULL)
 565           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str);
 566
 567       }else{
 568
 569         if(dot_output != NULL)
 570           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visited_state, req_str);
 571
 572       }
 573
 574       xbt_fifo_unshift(mc_stack_safety, next_state);
 575
 576       /* Insert in dict all enabled processes, if not included yet */
 577       xbt_swag_foreach(process, simix_global->process_list){
 578         if(MC_process_is_enabled(process)){
 579           char *key = bprintf("%lu", process->pid);
 580           if(xbt_dict_get_or_null(first_enabled_state, key) == NULL){
 581             char *data = bprintf("%d", xbt_fifo_size(mc_stack_safety));
 582             xbt_dict_set(first_enabled_state, key, data, NULL);
 583           }
 584           xbt_free(key);
 585         }
 586       }
 587
 588       if(dot_output != NULL)
 589         xbt_free(req_str);
 590
 591       MC_UNSET_RAW_MEM;
 592
 593       /* Let's loop again */
 594
 595       /* The interleave set is empty or the maximum depth is reached, let's back-track */
 596     } else {
 597
 598       if((xbt_fifo_size(mc_stack_safety) > _sg_mc_max_depth) || user_max_depth_reached || visited_state != -1){
 599
 600         if(user_max_depth_reached && visited_state == -1)
 601           XBT_DEBUG("User max depth reached !");
 602         else if(visited_state == -1)
 603           XBT_WARN("/!\\ Max depth reached ! /!\\ ");
 604
 605         visited_state = -1;
 606
 607         /* Interleave enabled processes in the state in which they have been enabled for the first time */
 608         xbt_swag_foreach(process, simix_global->process_list){
 609           if(MC_process_is_enabled(process)){
 610             char *key = bprintf("%lu", process->pid);
 611             enabled = (int)strtoul(xbt_dict_get_or_null(first_enabled_state, key), 0, 10);
 612             xbt_free(key);
 613             int cursor = xbt_fifo_size(mc_stack_safety);
 614             xbt_fifo_foreach(mc_stack_safety, item, state_test, mc_state_t){
 615               if(cursor-- == enabled){
 616                 if(!MC_state_process_is_done(state_test, process) && state_test->num != state->num){
 617                   XBT_DEBUG("Interleave process %lu in state %d", process->pid, state_test->num);
 618                   MC_state_interleave_process(state_test, process);
 619                   break;
 620                 }
 621               }
 622             }
 623           }
 624         }
 625
 626       }else{
 627
 628         XBT_DEBUG("There are no more processes to interleave. (depth %d)", xbt_fifo_size(mc_stack_safety) + 1);
 629
 630       }
 631
 632       MC_SET_RAW_MEM;
 633
 634       if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
 635         if(initial_state_safety->initial_communications_pattern_done){
 636           if(interleave_size == 0){ /* if (interleave_size > 0), process interleaved but not enabled => "incorrect" path, determinism not evaluated */
 637             //print_communications_pattern(communications_pattern);
 638             deterministic_pattern(initial_communications_pattern, communications_pattern);
 639             if(initial_state_safety->comm_deterministic == 0 && _sg_mc_comms_determinism){
 640               XBT_INFO("****************************************************");
 641               XBT_INFO("***** Non-deterministic communications pattern *****");
 642               XBT_INFO("****************************************************");
 643               XBT_INFO("Initial communications pattern:");
 644               print_communications_pattern(initial_communications_pattern);
 645               XBT_INFO("Communications pattern counter-example:");
 646               print_communications_pattern(communications_pattern);
 647               MC_print_statistics(mc_stats);
 648               return;
 649             }else if(initial_state_safety->send_deterministic == 0 && _sg_mc_send_determinism){
 650               XBT_INFO("****************************************************");
 651               XBT_INFO("***** Non-send-deterministic communications pattern *****");
 652               XBT_INFO("****************************************************");
 653               XBT_INFO("Initial communications pattern:");
 654               print_communications_pattern(initial_communications_pattern);
 655               XBT_INFO("Communications pattern counter-example:");
 656               print_communications_pattern(communications_pattern);
 657               MC_print_statistics(mc_stats);
 658               return;
 659             }
 660           }
 661         }else{
 662           initial_state_safety->initial_communications_pattern_done = 1;
 663         }
 664       }
 665
 666       /* Trash the current state, no longer needed */
 667       xbt_fifo_shift(mc_stack_safety);
 668       MC_state_delete(state);
 669       XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1);
 670
 671       MC_UNSET_RAW_MEM;
 672
 673       /* Check for deadlocks */
 674       if(MC_deadlock_check()){
 675         MC_show_deadlock(NULL);
 676         return;
 677       }
 678
 679       MC_SET_RAW_MEM;
 680       /* Traverse the stack backwards until a state with a non empty interleave
 681          set is found, deleting all the states that have it empty in the way.
 682          For each deleted state, check if the request that has generated it
 683          (from it's predecesor state), depends on any other previous request
 684          executed before it. If it does then add it to the interleave set of the
 685          state that executed that previous request. */
 686
 687       while ((state = xbt_fifo_shift(mc_stack_safety)) != NULL) {
 688         if(mc_reduce_kind != e_mc_reduce_none){
 689           req = MC_state_get_internal_request(state);
 690           xbt_fifo_foreach(mc_stack_safety, item, prev_state, mc_state_t) {
 691             if(MC_request_depend(req, MC_state_get_internal_request(prev_state))){
 692               if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
 693                 XBT_DEBUG("Dependent Transitions:");
 694                 prev_req = MC_state_get_executed_request(prev_state, &value);
 695                 req_str = MC_request_to_string(prev_req, value);
 696                 XBT_DEBUG("%s (state=%d)", req_str, prev_state->num);
 697                 xbt_free(req_str);
 698                 prev_req = MC_state_get_executed_request(state, &value);
 699                 req_str = MC_request_to_string(prev_req, value);
 700                 XBT_DEBUG("%s (state=%d)", req_str, state->num);
 701                 xbt_free(req_str);
 702               }
 703
 704               if(!MC_state_process_is_done(prev_state, req->issuer))
 705                 MC_state_interleave_process(prev_state, req->issuer);
 706               else
 707                 XBT_DEBUG("Process %p is in done set", req->issuer);
 708
 709               break;
 710
 711             }else if(req->issuer == MC_state_get_internal_request(prev_state)->issuer){
 712
 713               XBT_DEBUG("Simcall %d and %d with same issuer", req->call, MC_state_get_internal_request(prev_state)->call);
 714               break;
 715
 716             }else{
 717
 718               XBT_DEBUG("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant", req->call, req->issuer->pid, state->num, MC_state_get_internal_request(prev_state)->call, MC_state_get_internal_request(prev_state)->issuer->pid, prev_state->num);
 719
 720             }
 721           }
 722         }
 723
 724         if (MC_state_interleave_size(state) && xbt_fifo_size(mc_stack_safety) < _sg_mc_max_depth) {
 725           /* We found a back-tracking point, let's loop */
 726           XBT_DEBUG("Back-tracking to state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1);
 727           if(_sg_mc_checkpoint){
 728             if(state->system_state != NULL){
 729               MC_restore_snapshot(state->system_state);
 730               xbt_fifo_unshift(mc_stack_safety, state);
 731               MC_UNSET_RAW_MEM;
 732             }else{
 733               pos = xbt_fifo_size(mc_stack_safety);
 734               item = xbt_fifo_get_first_item(mc_stack_safety);
 735               while(pos>0){
 736                 restored_state = (mc_state_t) xbt_fifo_get_item_content(item);
 737                 if(restored_state->system_state != NULL){
 738                   break;
 739                 }else{
 740                   item = xbt_fifo_get_next_item(item);
 741                   pos--;
 742                 }
 743               }
 744               MC_restore_snapshot(restored_state->system_state);
 745               xbt_fifo_unshift(mc_stack_safety, state);
 746               MC_UNSET_RAW_MEM;
 747               MC_replay(mc_stack_safety, pos);
 748             }
 749           }else{
 750             xbt_fifo_unshift(mc_stack_safety, state);
 751             MC_UNSET_RAW_MEM;
 752             MC_replay(mc_stack_safety, -1);
 753           }
 754           XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num, xbt_fifo_size(mc_stack_safety));
 755           break;
 756         } else {
 757           req = MC_state_get_internal_request(state);
 758           if(_sg_mc_comms_determinism){
 759             if(req->call == SIMCALL_COMM_ISEND || req->call == SIMCALL_COMM_IRECV){
 760               if(!xbt_dynar_is_empty(communications_pattern))
 761                 xbt_dynar_remove_at(communications_pattern, xbt_dynar_length(communications_pattern) - 1, NULL);
 762             }
 763           }
 764           XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1);
 765           MC_state_delete(state);
 766         }
 767       }
 768       MC_UNSET_RAW_MEM;
 769     }
 770   }
 771   MC_print_statistics(mc_stats);
 772   MC_UNSET_RAW_MEM;
 773
 774   return;
 775 }
 776
 777
 778
 779