src/mc/mc_dpor.c

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