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   // XBT_DEBUG("Communication-deterministic : %d, Send-deterministic : %d", initial_state_safety->comm_deterministic, initial_state_safety->send_deterministic);
  96 }
  97
  98 static int complete_comm_pattern(xbt_dynar_t list, mc_comm_pattern_t pattern){
  99   mc_comm_pattern_t current_pattern;
 100   unsigned int cursor = 0;
 101   xbt_dynar_foreach(list, cursor, current_pattern){
 102     if(current_pattern->comm == pattern->comm){
 103       if(!current_pattern->completed){
 104         current_pattern->src_proc = pattern->comm->comm.src_proc->pid;
 105         current_pattern->dst_proc = pattern->comm->comm.dst_proc->pid;
 106         current_pattern->data_size = pattern->comm->comm.src_buff_size;
 107         current_pattern->data = xbt_malloc0(current_pattern->data_size);
 108         current_pattern->matched_comm = pattern->num;
 109         memcpy(current_pattern->data, current_pattern->comm->comm.src_buff, current_pattern->data_size);
 110         current_pattern->completed = 1;
 111         return current_pattern->num;
 112       }
 113     }
 114   }
 115   return -1;
 116 }
 117
 118 void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, int call){
 119   mc_comm_pattern_t pattern = NULL;
 120   pattern = xbt_new0(s_mc_comm_pattern_t, 1);
 121   pattern->num = ++nb_comm_pattern;
 122   pattern->completed = 0;
 123   if(call == 1){ // ISEND
 124     pattern->comm = simcall_comm_isend__get__result(request);
 125     pattern->type = SIMIX_COMM_SEND;
 126     if(pattern->comm->comm.dst_proc != NULL){
 127
 128       pattern->matched_comm = complete_comm_pattern(list, pattern);
 129       pattern->dst_proc = pattern->comm->comm.dst_proc->pid;
 130       pattern->completed = 1;
 131     }
 132     pattern->src_proc = pattern->comm->comm.src_proc->pid;
 133     pattern->data_size = pattern->comm->comm.src_buff_size;
 134     pattern->data=xbt_malloc0(pattern->data_size);
 135     memcpy(pattern->data, pattern->comm->comm.src_buff, pattern->data_size);
 136   }else{ // IRECV
 137     pattern->comm = simcall_comm_irecv__get__result(request);
 138     pattern->type = SIMIX_COMM_RECEIVE;
 139     if(pattern->comm->comm.src_proc != NULL){
 140       pattern->matched_comm = complete_comm_pattern(list, pattern);
 141       pattern->src_proc = pattern->comm->comm.src_proc->pid;
 142       pattern->completed = 1;
 143       pattern->data_size = pattern->comm->comm.src_buff_size;
 144       pattern->data=xbt_malloc0(pattern->data_size);
 145       memcpy(pattern->data, pattern->comm->comm.src_buff, pattern->data_size);
 146     }
 147     pattern->dst_proc = pattern->comm->comm.dst_proc->pid;
 148   }
 149   if(pattern->comm->comm.rdv != NULL)
 150     pattern->rdv = strdup(pattern->comm->comm.rdv->name);
 151   else
 152     pattern->rdv = strdup(pattern->comm->comm.rdv_cpy->name);
 153   xbt_dynar_push(list, &pattern);
 154 }
 155
 156 static void print_communications_pattern(xbt_dynar_t comms_pattern){
 157   unsigned int cursor = 0;
 158   mc_comm_pattern_t current_comm;
 159   xbt_dynar_foreach(comms_pattern, cursor, current_comm){
 160     // 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);
 161   }
 162 }
 163
 164 static void visited_state_free(mc_visited_state_t state){
 165   if(state){
 166     MC_free_snapshot(state->system_state);
 167     xbt_free(state);
 168   }
 169 }
 170
 171 static void visited_state_free_voidp(void *s){
 172   visited_state_free((mc_visited_state_t) * (void **) s);
 173 }
 174
 175 static mc_visited_state_t visited_state_new(){
 176
 177   mc_visited_state_t new_state = NULL;
 178   new_state = xbt_new0(s_mc_visited_state_t, 1);
 179   new_state->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
 180   new_state->nb_processes = xbt_swag_size(simix_global->process_list);
 181   new_state->system_state = MC_take_snapshot(mc_stats->expanded_states);
 182   new_state->num = mc_stats->expanded_states;
 183   new_state->other_num = -1;
 184
 185   return new_state;
 186
 187 }
 188
 189 static int get_search_interval(xbt_dynar_t all_states, mc_visited_state_t state, int *min, int *max){
 190
 191   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 192
 193   MC_SET_RAW_MEM;
 194
 195   int cursor = 0, previous_cursor, next_cursor;
 196   mc_visited_state_t state_test;
 197   int start = 0;
 198   int end = xbt_dynar_length(all_states) - 1;
 199
 200   while(start <= end){
 201     cursor = (start + end) / 2;
 202     state_test = (mc_visited_state_t)xbt_dynar_get_as(all_states, cursor, mc_visited_state_t);
 203     if(state_test->nb_processes < state->nb_processes){
 204       start = cursor + 1;
 205     }else if(state_test->nb_processes > state->nb_processes){
 206       end = cursor - 1;
 207     }else{
 208       if(state_test->heap_bytes_used < state->heap_bytes_used){
 209         start = cursor +1;
 210       }else if(state_test->heap_bytes_used > state->heap_bytes_used){
 211         end = cursor - 1;
 212       }else{
 213         *min = *max = cursor;
 214         previous_cursor = cursor - 1;
 215         while(previous_cursor >= 0){
 216           state_test = (mc_visited_state_t)xbt_dynar_get_as(all_states, previous_cursor, mc_visited_state_t);
 217           if(state_test->nb_processes != state->nb_processes || state_test->heap_bytes_used != state->heap_bytes_used)
 218             break;
 219           *min = previous_cursor;
 220           previous_cursor--;
 221         }
 222         next_cursor = cursor + 1;
 223         while(next_cursor < xbt_dynar_length(all_states)){
 224           state_test = (mc_visited_state_t)xbt_dynar_get_as(all_states, next_cursor, mc_visited_state_t);
 225           if(state_test->nb_processes != state->nb_processes || state_test->heap_bytes_used != state->heap_bytes_used)
 226             break;
 227           *max = next_cursor;
 228           next_cursor++;
 229         }
 230         if(!raw_mem_set)
 231           MC_UNSET_RAW_MEM;
 232         return -1;
 233       }
 234      }
 235   }
 236
 237   if(!raw_mem_set)
 238     MC_UNSET_RAW_MEM;
 239
 240   return cursor;
 241 }
 242
 243 static int is_visited_state(){
 244
 245   if(_sg_mc_visited == 0)
 246     return -1;
 247
 248   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 249
 250   MC_SET_RAW_MEM;
 251
 252   mc_visited_state_t new_state = visited_state_new();
 253
 254   if(xbt_dynar_is_empty(visited_states)){
 255
 256     xbt_dynar_push(visited_states, &new_state);
 257
 258     if(!raw_mem_set)
 259       MC_UNSET_RAW_MEM;
 260
 261     return -1;
 262
 263   }else{
 264
 265     int min = -1, max = -1, index;
 266     //int res;
 267     mc_visited_state_t state_test;
 268     int cursor;
 269
 270     index = get_search_interval(visited_states, new_state, &min, &max);
 271
 272     if(min != -1 && max != -1){
 273       /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_states, min), (max-min)+1, new_state);
 274       if(res != -1){
 275         state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, (min+res)-1, mc_visited_state_t);
 276         if(state_test->other_num == -1)
 277           new_state->other_num = state_test->num;
 278         else
 279           new_state->other_num = state_test->other_num;
 280         if(dot_output == NULL)
 281           XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
 282         else
 283           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);
 284         xbt_dynar_remove_at(visited_states, (min + res) - 1, NULL);
 285         xbt_dynar_insert_at(visited_states, (min+res) - 1, &new_state);
 286         if(!raw_mem_set)
 287           MC_UNSET_RAW_MEM;
 288         return new_state->other_num;
 289         }*/
 290       cursor = min;
 291       while(cursor <= max){
 292         state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, cursor, mc_visited_state_t);
 293         if(snapshot_compare(state_test, new_state) == 0){
 294           if(state_test->other_num == -1)
 295             new_state->other_num = state_test->num;
 296           else
 297             new_state->other_num = state_test->other_num;
 298           if(dot_output == NULL)
 299             XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
 300           else
 301             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);
 302           xbt_dynar_remove_at(visited_states, cursor, NULL);
 303           xbt_dynar_insert_at(visited_states, cursor, &new_state);
 304           if(!raw_mem_set)
 305             MC_UNSET_RAW_MEM;
 306           return new_state->other_num;
 307         }
 308         cursor++;
 309       }
 310       xbt_dynar_insert_at(visited_states, min, &new_state);
 311     }else{
 312       state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, index, mc_visited_state_t);
 313       if(state_test->nb_processes < new_state->nb_processes){
 314         xbt_dynar_insert_at(visited_states, index+1, &new_state);
 315       }else{
 316         if(state_test->heap_bytes_used < new_state->heap_bytes_used)
 317           xbt_dynar_insert_at(visited_states, index + 1, &new_state);
 318         else
 319           xbt_dynar_insert_at(visited_states, index, &new_state);
 320       }
 321     }
 322
 323     if(xbt_dynar_length(visited_states) > _sg_mc_visited){
 324       int min2 = mc_stats->expanded_states;
 325       unsigned int cursor2 = 0;
 326       unsigned int index2 = 0;
 327       xbt_dynar_foreach(visited_states, cursor2, state_test){
 328         if(state_test->num < min2){
 329           index2 = cursor2;
 330           min2 = state_test->num;
 331         }
 332       }
 333       xbt_dynar_remove_at(visited_states, index2, NULL);
 334     }
 335
 336     if(!raw_mem_set)
 337       MC_UNSET_RAW_MEM;
 338
 339     return -1;
 340
 341   }
 342 }
 343
 344 /**
 345  *  \brief Initialize the DPOR exploration algorithm
 346  */
 347 void MC_dpor_init()
 348 {
 349
 350   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 351
 352   mc_state_t initial_state = NULL;
 353   smx_process_t process;
 354
 355   /* Create the initial state and push it into the exploration stack */
 356   MC_SET_RAW_MEM;
 357
 358   if(_sg_mc_visited > 0)
 359     visited_states = xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp);
 360
 361   first_enabled_state = xbt_dict_new_homogeneous(&xbt_free_f);
 362
 363   initial_communications_pattern = xbt_dynar_new(sizeof(mc_comm_pattern_t), comm_pattern_free_voidp);
 364   communications_pattern = xbt_dynar_new(sizeof(mc_comm_pattern_t), comm_pattern_free_voidp);
 365   nb_comm_pattern = 0;
 366
 367   initial_state = MC_state_new();
 368
 369   MC_UNSET_RAW_MEM;
 370
 371   XBT_DEBUG("**************************************************");
 372   XBT_DEBUG("Initial state");
 373
 374   /* Wait for requests (schedules processes) */
 375   MC_wait_for_requests();
 376
 377   MC_ignore_heap(simix_global->process_to_run->data, 0);
 378   MC_ignore_heap(simix_global->process_that_ran->data, 0);
 379
 380   MC_SET_RAW_MEM;
 381
 382   /* Get an enabled process and insert it in the interleave set of the initial state */
 383   xbt_swag_foreach(process, simix_global->process_list){
 384     if(MC_process_is_enabled(process)){
 385       MC_state_interleave_process(initial_state, process);
 386       if(mc_reduce_kind != e_mc_reduce_none)
 387         break;
 388     }
 389   }
 390
 391   xbt_fifo_unshift(mc_stack_safety, initial_state);
 392
 393   /* To ensure the soundness of DPOR, we have to keep a list of
 394      processes which are still enabled at each step of the exploration.
 395      If max depth is reached, we interleave them in the state in which they have
 396      been enabled for the first time. */
 397   xbt_swag_foreach(process, simix_global->process_list){
 398     if(MC_process_is_enabled(process)){
 399       char *key = bprintf("%lu", process->pid);
 400       char *data = bprintf("%d", xbt_fifo_size(mc_stack_safety));
 401       xbt_dict_set(first_enabled_state, key, data, NULL);
 402       xbt_free(key);
 403     }
 404   }
 405
 406   MC_UNSET_RAW_MEM;
 407
 408   if(raw_mem_set)
 409     MC_SET_RAW_MEM;
 410   else
 411     MC_UNSET_RAW_MEM;
 412
 413 }
 414
 415
 416 /**
 417  *   \brief Perform the model-checking operation using a depth-first search exploration
 418  *         with Dynamic Partial Order Reductions
 419  */
 420 void MC_dpor(void)
 421 {
 422
 423   char *req_str = NULL;
 424   int value;
 425   smx_simcall_t req = NULL, prev_req = NULL;
 426   mc_state_t state = NULL, prev_state = NULL, next_state = NULL, restored_state=NULL;
 427   smx_process_t process = NULL;
 428   xbt_fifo_item_t item = NULL;
 429   mc_state_t state_test = NULL;
 430   int pos;
 431   int visited_state = -1;
 432   int enabled = 0;
 433   int interleave_size = 0;
 434   int comm_pattern = 0;
 435
 436   while (xbt_fifo_size(mc_stack_safety) > 0) {
 437
 438     /* Get current state */
 439     state = (mc_state_t)
 440       xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_safety));
 441
 442     XBT_DEBUG("**************************************************");
 443     XBT_DEBUG("Exploration depth=%d (state=%p, num %d)(%u interleave, user_max_depth %d, first_enabled_state size : %d)",
 444               xbt_fifo_size(mc_stack_safety), state, state->num,
 445               MC_state_interleave_size(state), user_max_depth_reached, xbt_dict_size(first_enabled_state));
 446
 447     interleave_size = MC_state_interleave_size(state);
 448
 449     /* Update statistics */
 450     mc_stats->visited_states++;
 451
 452     /* If there are processes to interleave and the maximum depth has not been reached
 453        then perform one step of the exploration algorithm */
 454     if (xbt_fifo_size(mc_stack_safety) <= _sg_mc_max_depth && !user_max_depth_reached &&
 455         (req = MC_state_get_request(state, &value)) && visited_state == -1) {
 456
 457       /* Debug information */
 458       if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
 459         req_str = MC_request_to_string(req, value);
 460         XBT_DEBUG("Execute: %s", req_str);
 461         xbt_free(req_str);
 462       }
 463
 464       MC_SET_RAW_MEM;
 465       if(dot_output != NULL)
 466         req_str = MC_request_get_dot_output(req, value);
 467       MC_UNSET_RAW_MEM;
 468
 469       MC_state_set_executed_request(state, req, value);
 470       mc_stats->executed_transitions++;
 471
 472       MC_SET_RAW_MEM;
 473       char *key = bprintf("%lu", req->issuer->pid);
 474       xbt_dict_remove(first_enabled_state, key);
 475       xbt_free(key);
 476       MC_UNSET_RAW_MEM;
 477
 478       if(_sg_mc_comms_determinism){
 479         if(req->call == SIMCALL_COMM_ISEND)
 480           comm_pattern = 1;
 481         else if(req->call == SIMCALL_COMM_IRECV)
 482           comm_pattern = 2;
 483       }
 484
 485       /* Answer the request */
 486       SIMIX_simcall_pre(req, value); /* After this call req is no longer usefull */
 487
 488       if(_sg_mc_comms_determinism){
 489         MC_SET_RAW_MEM;
 490         if(comm_pattern != 0){
 491           if(!initial_state_safety->initial_communications_pattern_done)
 492             get_comm_pattern(initial_communications_pattern, req, comm_pattern);
 493           else
 494             get_comm_pattern(communications_pattern, req, comm_pattern);
 495         }
 496         MC_UNSET_RAW_MEM;
 497         comm_pattern = 0;
 498       }
 499
 500       /* Wait for requests (schedules processes) */
 501       MC_wait_for_requests();
 502
 503       /* Create the new expanded state */
 504       MC_SET_RAW_MEM;
 505
 506       next_state = MC_state_new();
 507
 508       if((visited_state = is_visited_state()) == -1){
 509
 510         /* Get an enabled process and insert it in the interleave set of the next state */
 511         xbt_swag_foreach(process, simix_global->process_list){
 512           if(MC_process_is_enabled(process)){
 513             MC_state_interleave_process(next_state, process);
 514             if(mc_reduce_kind != e_mc_reduce_none)
 515               break;
 516           }
 517         }
 518
 519         if(_sg_mc_checkpoint && ((xbt_fifo_size(mc_stack_safety) + 1) % _sg_mc_checkpoint == 0)){
 520           next_state->system_state = MC_take_snapshot(next_state->num);
 521         }
 522
 523         if(dot_output != NULL)
 524           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str);
 525
 526       }else{
 527
 528         if(dot_output != NULL)
 529           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visited_state, req_str);
 530
 531       }
 532
 533       xbt_fifo_unshift(mc_stack_safety, next_state);
 534
 535       /* Insert in dict all enabled processes, if not included yet */
 536       xbt_swag_foreach(process, simix_global->process_list){
 537         if(MC_process_is_enabled(process)){
 538           char *key = bprintf("%lu", process->pid);
 539           if(xbt_dict_get_or_null(first_enabled_state, key) == NULL){
 540             char *data = bprintf("%d", xbt_fifo_size(mc_stack_safety));
 541             xbt_dict_set(first_enabled_state, key, data, NULL);
 542           }
 543           xbt_free(key);
 544         }
 545       }
 546
 547       if(dot_output != NULL)
 548         xbt_free(req_str);
 549
 550       MC_UNSET_RAW_MEM;
 551
 552       /* Let's loop again */
 553
 554       /* The interleave set is empty or the maximum depth is reached, let's back-track */
 555     } else {
 556
 557       if((xbt_fifo_size(mc_stack_safety) > _sg_mc_max_depth) || user_max_depth_reached || visited_state != -1){
 558
 559         if(user_max_depth_reached && visited_state == -1)
 560           XBT_DEBUG("User max depth reached !");
 561         else if(visited_state == -1)
 562           XBT_WARN("/!\\ Max depth reached ! /!\\ ");
 563
 564         visited_state = -1;
 565
 566         /* Interleave enabled processes in the state in which they have been enabled for the first time */
 567         xbt_swag_foreach(process, simix_global->process_list){
 568           if(MC_process_is_enabled(process)){
 569             char *key = bprintf("%lu", process->pid);
 570             enabled = (int)strtoul(xbt_dict_get_or_null(first_enabled_state, key), 0, 10);
 571             xbt_free(key);
 572             int cursor = xbt_fifo_size(mc_stack_safety);
 573             xbt_fifo_foreach(mc_stack_safety, item, state_test, mc_state_t){
 574               if(cursor-- == enabled){
 575                 if(!MC_state_process_is_done(state_test, process) && state_test->num != state->num){
 576                   XBT_DEBUG("Interleave process %lu in state %d", process->pid, state_test->num);
 577                   MC_state_interleave_process(state_test, process);
 578                   break;
 579                 }
 580               }
 581             }
 582           }
 583         }
 584
 585       }else{
 586
 587         XBT_DEBUG("There are no more processes to interleave. (depth %d)", xbt_fifo_size(mc_stack_safety) + 1);
 588
 589       }
 590
 591       MC_SET_RAW_MEM;
 592
 593       if(_sg_mc_comms_determinism){
 594         if(!initial_state_safety->initial_communications_pattern_done){
 595           //print_communications_pattern(initial_communications_pattern);
 596         }else{
 597           if(interleave_size == 0){ /* if (interleave_size > 0), process interleaved but not enabled => "incorrect" path, determinism not evaluated */
 598             //print_communications_pattern(communications_pattern);
 599             deterministic_pattern(initial_communications_pattern, communications_pattern);
 600           }
 601         }
 602         initial_state_safety->initial_communications_pattern_done = 1;
 603       }
 604
 605       /* Trash the current state, no longer needed */
 606       xbt_fifo_shift(mc_stack_safety);
 607       MC_state_delete(state);
 608       XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1);
 609
 610       MC_UNSET_RAW_MEM;
 611
 612       /* Check for deadlocks */
 613       if(MC_deadlock_check()){
 614         MC_show_deadlock(NULL);
 615         return;
 616       }
 617
 618       MC_SET_RAW_MEM;
 619       /* Traverse the stack backwards until a state with a non empty interleave
 620          set is found, deleting all the states that have it empty in the way.
 621          For each deleted state, check if the request that has generated it
 622          (from it's predecesor state), depends on any other previous request
 623          executed before it. If it does then add it to the interleave set of the
 624          state that executed that previous request. */
 625
 626       while ((state = xbt_fifo_shift(mc_stack_safety)) != NULL) {
 627         if(mc_reduce_kind != e_mc_reduce_none){
 628           req = MC_state_get_internal_request(state);
 629           xbt_fifo_foreach(mc_stack_safety, item, prev_state, mc_state_t) {
 630             if(MC_request_depend(req, MC_state_get_internal_request(prev_state))){
 631               if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
 632                 XBT_DEBUG("Dependent Transitions:");
 633                 prev_req = MC_state_get_executed_request(prev_state, &value);
 634                 req_str = MC_request_to_string(prev_req, value);
 635                 XBT_DEBUG("%s (state=%d)", req_str, prev_state->num);
 636                 xbt_free(req_str);
 637                 prev_req = MC_state_get_executed_request(state, &value);
 638                 req_str = MC_request_to_string(prev_req, value);
 639                 XBT_DEBUG("%s (state=%d)", req_str, state->num);
 640                 xbt_free(req_str);
 641               }
 642
 643               if(!MC_state_process_is_done(prev_state, req->issuer))
 644                 MC_state_interleave_process(prev_state, req->issuer);
 645               else
 646                 XBT_DEBUG("Process %p is in done set", req->issuer);
 647
 648               break;
 649
 650             }else if(req->issuer == MC_state_get_internal_request(prev_state)->issuer){
 651
 652               XBT_DEBUG("Simcall %d and %d with same issuer", req->call, MC_state_get_internal_request(prev_state)->call);
 653               break;
 654
 655             }else{
 656
 657               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);
 658
 659             }
 660           }
 661         }
 662
 663         if (MC_state_interleave_size(state) && xbt_fifo_size(mc_stack_safety) < _sg_mc_max_depth) {
 664           /* We found a back-tracking point, let's loop */
 665           XBT_DEBUG("Back-tracking to state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1);
 666           if(_sg_mc_checkpoint){
 667             if(state->system_state != NULL){
 668               MC_restore_snapshot(state->system_state);
 669               xbt_fifo_unshift(mc_stack_safety, state);
 670               MC_UNSET_RAW_MEM;
 671             }else{
 672               pos = xbt_fifo_size(mc_stack_safety);
 673               item = xbt_fifo_get_first_item(mc_stack_safety);
 674               while(pos>0){
 675                 restored_state = (mc_state_t) xbt_fifo_get_item_content(item);
 676                 if(restored_state->system_state != NULL){
 677                   break;
 678                 }else{
 679                   item = xbt_fifo_get_next_item(item);
 680                   pos--;
 681                 }
 682               }
 683               MC_restore_snapshot(restored_state->system_state);
 684               xbt_fifo_unshift(mc_stack_safety, state);
 685               MC_UNSET_RAW_MEM;
 686               MC_replay(mc_stack_safety, pos);
 687             }
 688           }else{
 689             xbt_fifo_unshift(mc_stack_safety, state);
 690             MC_UNSET_RAW_MEM;
 691             MC_replay(mc_stack_safety, -1);
 692           }
 693           XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num, xbt_fifo_size(mc_stack_safety));
 694           break;
 695         } else {
 696           req = MC_state_get_internal_request(state);
 697           if(_sg_mc_comms_determinism){
 698             if(req->call == SIMCALL_COMM_ISEND || req->call == SIMCALL_COMM_IRECV){
 699               if(!xbt_dynar_is_empty(communications_pattern))
 700                 xbt_dynar_remove_at(communications_pattern, xbt_dynar_length(communications_pattern) - 1, NULL);
 701             }
 702           }
 703           XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1);
 704           MC_state_delete(state);
 705         }
 706       }
 707       MC_UNSET_RAW_MEM;
 708     }
 709   }
 710   MC_print_statistics(mc_stats);
 711   MC_UNSET_RAW_MEM;
 712
 713   return;
 714 }
 715
 716
 717
 718