src/mc/mc_dpor.c

   1 /* Copyright (c) 2008 Martin Quinson, Cristian Rosa.
   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 "private.h"
   8
   9 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_dpor, mc,
  10                                 "Logging specific to MC DPOR exploration");
  11
  12 /**
  13  *  \brief Initialize the DPOR exploration algorithm
  14  */
  15 void MC_dpor_init()
  16 {
  17   mc_state_t initial_state = NULL;
  18   smx_process_t process;
  19
  20   /* Create the initial state and push it into the exploration stack */
  21   MC_SET_RAW_MEM;
  22   initial_state = MC_state_new();
  23   xbt_fifo_unshift(mc_stack, initial_state);
  24   MC_UNSET_RAW_MEM;
  25
  26   XBT_DEBUG("**************************************************");
  27   XBT_DEBUG("Initial state");
  28
  29   /* Wait for requests (schedules processes) */
  30   MC_wait_for_requests();
  31
  32   MC_SET_RAW_MEM;
  33   /* Get an enabled process and insert it in the interleave set of the initial state */
  34   xbt_swag_foreach(process, simix_global->process_list){
  35     if(MC_process_is_enabled(process)){
  36       MC_state_interleave_process(initial_state, process);
  37       break;
  38     }
  39   }
  40   MC_UNSET_RAW_MEM;
  41
  42   /* FIXME: Update Statistics
  43   mc_stats->state_size +=
  44       xbt_setset_set_size(initial_state->enabled_transitions); */
  45 }
  46
  47
  48 /**
  49  *      \brief Perform the model-checking operation using a depth-first search exploration
  50  *         with Dynamic Partial Order Reductions
  51  */
  52 void MC_dpor(void)
  53 {
  54   char *req_str;
  55   int value;
  56   smx_req_t req = NULL, prev_req = NULL;
  57   mc_state_t state = NULL, prev_state = NULL, next_state = NULL;
  58   smx_process_t process = NULL;
  59   xbt_fifo_item_t item = NULL;
  60
  61   while (xbt_fifo_size(mc_stack) > 0) {
  62
  63     /* Get current state */
  64     state = (mc_state_t)
  65       xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
  66
  67     XBT_DEBUG("**************************************************");
  68     XBT_DEBUG("Exploration depth=%d (state=%p)(%u interleave)",
  69            xbt_fifo_size(mc_stack), state,
  70            MC_state_interleave_size(state));
  71
  72     /* Update statistics */
  73     mc_stats->visited_states++;
  74
  75     /* If there are processes to interleave and the maximum depth has not been reached
  76        then perform one step of the exploration algorithm */
  77     if (xbt_fifo_size(mc_stack) < MAX_DEPTH &&
  78         (req = MC_state_get_request(state, &value))) {
  79
  80       /* Debug information */
  81       if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
  82         req_str = MC_request_to_string(req, value);
  83         XBT_DEBUG("Execute: %s", req_str);
  84         xbt_free(req_str);
  85       }
  86
  87       MC_state_set_executed_request(state, req, value);
  88       mc_stats->executed_transitions++;
  89
  90       /* Answer the request */
  91       SIMIX_request_pre(req, value); /* After this call req is no longer usefull */
  92
  93       /* Wait for requests (schedules processes) */
  94       MC_wait_for_requests();
  95
  96       /* Create the new expanded state */
  97       MC_SET_RAW_MEM;
  98       next_state = MC_state_new();
  99       xbt_fifo_unshift(mc_stack, next_state);
 100
 101       /* Get an enabled process and insert it in the interleave set of the next state */
 102       xbt_swag_foreach(process, simix_global->process_list){
 103         if(MC_process_is_enabled(process)){
 104           MC_state_interleave_process(next_state, process);
 105           break;
 106         }
 107       }
 108       MC_UNSET_RAW_MEM;
 109
 110       /* FIXME: Update Statistics
 111       mc_stats->state_size +=
 112           xbt_setset_set_size(next_state->enabled_transitions);*/
 113
 114       /* Let's loop again */
 115
 116       /* The interleave set is empty or the maximum depth is reached, let's back-track */
 117     } else {
 118       XBT_DEBUG("There are no more processes to interleave.");
 119
 120       /* Trash the current state, no longer needed */
 121       MC_SET_RAW_MEM;
 122       xbt_fifo_shift(mc_stack);
 123       MC_state_delete(state);
 124       MC_UNSET_RAW_MEM;
 125
 126       /* Check for deadlocks */
 127       if(MC_deadlock_check()){
 128         MC_show_deadlock(NULL);
 129         return;
 130       }
 131
 132       MC_SET_RAW_MEM;
 133       /* Traverse the stack backwards until a state with a non empty interleave
 134          set is found, deleting all the states that have it empty in the way.
 135          For each deleted state, check if the request that has generated it
 136          (from it's predecesor state), depends on any other previous request
 137          executed before it. If it does then add it to the interleave set of the
 138          state that executed that previous request. */
 139       while ((state = xbt_fifo_shift(mc_stack)) != NULL) {
 140         req = MC_state_get_internal_request(state);
 141         xbt_fifo_foreach(mc_stack, item, prev_state, mc_state_t) {
 142           if(MC_request_depend(req, MC_state_get_internal_request(prev_state))){
 143             if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
 144               XBT_DEBUG("Dependent Transitions:");
 145               prev_req = MC_state_get_executed_request(prev_state, &value);
 146               req_str = MC_request_to_string(prev_req, value);
 147               XBT_DEBUG("%s (state=%p)", req_str, prev_state);
 148               xbt_free(req_str);
 149               prev_req = MC_state_get_executed_request(state, &value);
 150               req_str = MC_request_to_string(prev_req, value);
 151               XBT_DEBUG("%s (state=%p)", req_str, state);
 152               xbt_free(req_str);
 153             }
 154
 155             if(!MC_state_process_is_done(prev_state, req->issuer))
 156               MC_state_interleave_process(prev_state, req->issuer);
 157             else
 158               XBT_DEBUG("Process %p is in done set", req->issuer);
 159
 160             break;
 161           }
 162         }
 163         if (MC_state_interleave_size(state)) {
 164           /* We found a back-tracking point, let's loop */
 165           xbt_fifo_unshift(mc_stack, state);
 166           XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack));
 167           MC_UNSET_RAW_MEM;
 168           MC_replay(mc_stack);
 169           break;
 170         } else {
 171           MC_state_delete(state);
 172         }
 173       }
 174       MC_UNSET_RAW_MEM;
 175     }
 176   }
 177   MC_UNSET_RAW_MEM;
 178   return;
 179 }
 180
 181
 182 /********************* DPOR without replay *********************/
 183
 184 mc_state_ws_t new_state_ws(mc_snapshot_t s, mc_state_t gs){
 185   mc_state_ws_t sws = NULL;
 186   sws = xbt_new0(s_mc_state_ws_t, 1);
 187   sws->system_state = s;
 188   sws->graph_state = gs;
 189   return sws;
 190 }
 191
 192 void MC_dpor_with_restore_snapshot_init(){
 193
 194   XBT_DEBUG("**************************************************");
 195   XBT_DEBUG("DPOR (with restore snapshot) init");
 196   XBT_DEBUG("**************************************************");
 197
 198   mc_state_t initial_graph_state;
 199   smx_process_t process;
 200   mc_snapshot_t initial_system_snapshot;
 201   mc_state_ws_t initial_state ;
 202
 203   MC_wait_for_requests();
 204
 205   MC_SET_RAW_MEM;
 206
 207   initial_system_snapshot = xbt_new0(s_mc_snapshot_t, 1);
 208
 209   initial_graph_state = MC_state_new();
 210   xbt_swag_foreach(process, simix_global->process_list){
 211     if(MC_process_is_enabled(process)){
 212       MC_state_interleave_process(initial_graph_state, process);
 213       break;
 214     }
 215   }
 216
 217   MC_take_snapshot(initial_system_snapshot);
 218
 219   initial_state = new_state_ws(initial_system_snapshot, initial_graph_state);
 220   xbt_fifo_unshift(mc_snapshot_stack, initial_state);
 221
 222   MC_UNSET_RAW_MEM;
 223
 224   MC_dpor_with_restore_snapshot();
 225
 226 }
 227
 228 void MC_dpor_with_restore_snapshot(){
 229
 230   smx_process_t process = NULL;
 231
 232   if(xbt_fifo_size(mc_snapshot_stack) == 0)
 233     return;
 234
 235   int value;
 236   mc_state_t next_graph_state = NULL;
 237   smx_req_t req = NULL, prev_req = NULL;
 238   char *req_str;
 239   xbt_fifo_item_t item = NULL;
 240
 241   mc_snapshot_t next_snapshot;
 242   mc_state_ws_t current_state;
 243   mc_state_ws_t prev_state;
 244   mc_state_ws_t next_state;
 245
 246   while(xbt_fifo_size(mc_snapshot_stack) > 0){
 247
 248     current_state = (mc_state_ws_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_snapshot_stack));
 249
 250
 251     XBT_DEBUG("**************************************************");
 252     XBT_DEBUG("Depth : %d, State : %p , %u interleave", xbt_fifo_size(mc_snapshot_stack),current_state, MC_state_interleave_size(current_state->graph_state));
 253
 254
 255     if((xbt_fifo_size(mc_snapshot_stack) < MAX_DEPTH) && (req = MC_state_get_request(current_state->graph_state, &value))){
 256
 257       /* Debug information */
 258       if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
 259         req_str = MC_request_to_string(req, value);
 260         XBT_DEBUG("Execute: %s", req_str);
 261         xbt_free(req_str);
 262       }
 263
 264       MC_state_set_executed_request(current_state->graph_state, req, value);
 265
 266       /* Answer the request */
 267       SIMIX_request_pre(req, value);
 268
 269       /* Wait for requests (schedules processes) */
 270       MC_wait_for_requests();
 271
 272       /* Create the new expanded graph_state */
 273       MC_SET_RAW_MEM;
 274
 275       next_graph_state = MC_state_new();
 276
 277       /* Get an enabled process and insert it in the interleave set of the next graph_state */
 278       xbt_swag_foreach(process, simix_global->process_list){
 279         if(MC_process_is_enabled(process)){
 280           MC_state_interleave_process(next_graph_state, process);
 281           break;
 282         }
 283       }
 284
 285       next_snapshot = xbt_new0(s_mc_snapshot_t, 1);
 286       MC_take_snapshot(next_snapshot);
 287
 288       next_state = new_state_ws(next_snapshot, next_graph_state);
 289       xbt_fifo_unshift(mc_snapshot_stack, next_state);
 290
 291       MC_UNSET_RAW_MEM;
 292
 293     }else{
 294       XBT_DEBUG("There are no more processes to interleave.");
 295
 296       /* Trash the current state, no longer needed */
 297       MC_SET_RAW_MEM;
 298       xbt_fifo_shift(mc_snapshot_stack);
 299       MC_UNSET_RAW_MEM;
 300
 301       while((current_state = xbt_fifo_shift(mc_snapshot_stack)) != NULL){
 302         req = MC_state_get_internal_request(current_state->graph_state);
 303         xbt_fifo_foreach(mc_snapshot_stack, item, prev_state, mc_state_ws_t) {
 304           if(MC_request_depend(req, MC_state_get_internal_request(prev_state->graph_state))){
 305             if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
 306               XBT_DEBUG("Dependent Transitions:");
 307               prev_req = MC_state_get_executed_request(prev_state->graph_state, &value);
 308               req_str = MC_request_to_string(prev_req, value);
 309               XBT_DEBUG("%s (state=%p)", req_str, prev_state->graph_state);
 310               xbt_free(req_str);
 311               prev_req = MC_state_get_executed_request(current_state->graph_state, &value);
 312               req_str = MC_request_to_string(prev_req, value);
 313               XBT_DEBUG("%s (state=%p)", req_str, current_state->graph_state);
 314               xbt_free(req_str);
 315             }
 316
 317             if(!MC_state_process_is_done(prev_state->graph_state, req->issuer)){
 318               MC_state_interleave_process(prev_state->graph_state, req->issuer);
 319
 320             } else {
 321               XBT_DEBUG("Process %p is in done set", req->issuer);
 322             }
 323
 324             break;
 325           }
 326         }
 327
 328         if(MC_state_interleave_size(current_state->graph_state)){
 329           MC_restore_snapshot(current_state->system_state);
 330           xbt_fifo_unshift(mc_snapshot_stack, current_state);
 331           XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_snapshot_stack));
 332           MC_UNSET_RAW_MEM;
 333           break;
 334         }
 335       }
 336
 337       MC_UNSET_RAW_MEM;
 338
 339     }
 340   }
 341   MC_UNSET_RAW_MEM;
 342   return;
 343 }
 344
 345
 346
 347 /************ DPOR 2 (invisible and independant transitions) ************/
 348
 349 xbt_dynar_t reached_pairs_prop;
 350
 351 mc_prop_ato_t new_proposition(char* id, int value){
 352   mc_prop_ato_t prop = NULL;
 353   prop = xbt_new0(s_mc_prop_ato_t, 1);
 354   prop->id = strdup(id);
 355   prop->value = value;
 356   return prop;
 357 }
 358
 359 mc_pair_prop_t new_pair_prop(mc_snapshot_t sn, mc_state_t sg, xbt_state_t st){
 360   mc_pair_prop_t pair = NULL;
 361   pair = xbt_new0(s_mc_pair_prop_t, 1);
 362   pair->system_state = sn;
 363   pair->automaton_state = st;
 364   pair->graph_state = sg;
 365   pair->propositions = xbt_dynar_new(sizeof(mc_prop_ato_t), NULL);
 366   mc_stats_pair->expanded_pairs++;
 367   return pair;
 368 }
 369
 370 int reached_prop(mc_pair_prop_t pair){
 371
 372   char* hash_reached = malloc(sizeof(char)*160);
 373   unsigned int c= 0;
 374
 375   MC_SET_RAW_MEM;
 376   char *hash = malloc(sizeof(char)*160);
 377   xbt_sha((char *)&pair, hash);
 378   xbt_dynar_foreach(reached_pairs_prop, c, hash_reached){
 379     if(strcmp(hash, hash_reached) == 0){
 380       MC_UNSET_RAW_MEM;
 381       return 1;
 382     }
 383   }
 384
 385   MC_UNSET_RAW_MEM;
 386   return 0;
 387 }
 388
 389 void set_pair_prop_reached(mc_pair_prop_t pair){
 390
 391   if(reached_prop(pair) == 0){
 392     MC_SET_RAW_MEM;
 393     char *hash = malloc(sizeof(char)*160) ;
 394     xbt_sha((char *)&pair, hash);
 395     xbt_dynar_push(reached_pairs_prop, &hash);
 396     MC_UNSET_RAW_MEM;
 397   }
 398
 399 }
 400
 401
 402 void MC_dpor2_init(xbt_automaton_t a)
 403 {
 404   mc_pair_prop_t initial_pair = NULL;
 405   mc_state_t initial_graph_state = NULL;
 406   mc_snapshot_t initial_system_state = NULL;
 407   xbt_state_t initial_automaton_state = NULL;
 408   smx_process_t process;
 409
 410
 411   MC_SET_RAW_MEM;
 412   initial_graph_state = MC_state_new();
 413   MC_UNSET_RAW_MEM;
 414
 415   /* Wait for requests (schedules processes) */
 416   MC_wait_for_requests();
 417
 418   MC_SET_RAW_MEM;
 419   xbt_swag_foreach(process, simix_global->process_list){
 420     if(MC_process_is_enabled(process)){
 421       MC_state_interleave_process(initial_graph_state, process);
 422       break;
 423     }
 424   }
 425   MC_UNSET_RAW_MEM;
 426
 427   unsigned int cursor = 0;
 428   unsigned int cursor2 = 0;
 429   xbt_state_t automaton_state = NULL;
 430   int res;
 431   xbt_transition_t transition_succ;
 432
 433   xbt_dynar_foreach(a->states, cursor, automaton_state){
 434     if(automaton_state->type == -1){
 435       xbt_dynar_foreach(automaton_state->out, cursor2, transition_succ){
 436         res = MC_automaton_evaluate_label(a, transition_succ->label);
 437         if((res == 1) || (res == 2)){
 438           initial_automaton_state = transition_succ->dst;
 439           break;
 440         }
 441       }
 442     }
 443
 444     if(xbt_fifo_size(mc_snapshot_stack) > 0)
 445       break;
 446   }
 447
 448   if(xbt_fifo_size(mc_snapshot_stack) == 0){
 449     cursor = 0;
 450     xbt_dynar_foreach(a->states, cursor, automaton_state){
 451       if(automaton_state->type == -1){
 452         initial_automaton_state = automaton_state;
 453         break;
 454       }
 455     }
 456   }
 457
 458   reached_pairs_prop = xbt_dynar_new(sizeof(char *), NULL);
 459
 460   MC_SET_RAW_MEM;
 461   initial_system_state = xbt_new0(s_mc_snapshot_t, 1);
 462   MC_take_snapshot(initial_system_state);
 463   initial_pair = new_pair_prop(initial_system_state, initial_graph_state, initial_automaton_state);
 464   cursor = 0;
 465   xbt_propositional_symbol_t ps;
 466   xbt_dynar_foreach(a->propositional_symbols, cursor, ps){
 467     int (*f)() = ps->function;
 468     int val = (*f)();
 469     mc_prop_ato_t pa = new_proposition(ps->pred, val);
 470     xbt_dynar_push(initial_pair->propositions, &pa);
 471   }
 472   xbt_fifo_unshift(mc_snapshot_stack, initial_pair);
 473   MC_UNSET_RAW_MEM;
 474
 475
 476
 477   XBT_DEBUG("**************************************************");
 478   XBT_DEBUG("Initial pair");
 479
 480   MC_dpor2(a, 0);
 481
 482 }
 483
 484
 485 void MC_dpor2(xbt_automaton_t a, int search_cycle)
 486 {
 487   char *req_str;
 488   int value;
 489   smx_req_t req = NULL, prev_req = NULL;
 490   mc_state_t next_graph_state = NULL;
 491   mc_snapshot_t next_system_state = NULL;
 492   xbt_state_t next_automaton_state = NULL;
 493   xbt_transition_t transition_succ;
 494   unsigned int cursor;
 495   int res;
 496   mc_pair_prop_t pair = NULL, next_pair = NULL, prev_pair = NULL;
 497   smx_process_t process = NULL;
 498   xbt_fifo_item_t item = NULL;
 499
 500   while (xbt_fifo_size(mc_snapshot_stack) > 0) {
 501
 502     /* Get current pair */
 503     pair = (mc_pair_prop_t)
 504       xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_snapshot_stack));
 505
 506     XBT_DEBUG("**************************************************");
 507     XBT_DEBUG("Exploration depth=%d (pair=%p)(%u interleave)",
 508            xbt_fifo_size(mc_snapshot_stack), pair,
 509            MC_state_interleave_size(pair->graph_state));
 510
 511     XBT_DEBUG("Propositions (%lu): ", xbt_dynar_length(pair->propositions));
 512
 513     cursor = 0;
 514     mc_prop_ato_t prop_at;
 515     xbt_dynar_foreach(pair->propositions, cursor, prop_at){
 516       XBT_DEBUG("Id : %s, value : %d", prop_at->id, prop_at->value);
 517     }
 518
 519
 520     /* Update statistics */
 521     mc_stats_pair->visited_pairs++;
 522
 523     /* Test acceptance pair and acceptance cycle*/
 524
 525     if(pair->automaton_state->type == 1){
 526       if(search_cycle == 0){
 527         set_pair_prop_reached(pair);
 528         XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", pair->graph_state, pair->automaton_state, pair->automaton_state->id);
 529       }else{
 530         if(reached_prop(pair) == 1){
 531           XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 532           XBT_INFO("|             ACCEPTANCE CYCLE            |");
 533           XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 534           XBT_INFO("Counter-example that violates formula :");
 535           MC_show_snapshot_stack(mc_snapshot_stack);
 536           MC_dump_snapshot_stack(mc_snapshot_stack);
 537           MC_print_statistics_pairs(mc_stats_pair);
 538           exit(0);
 539         }
 540       }
 541     }
 542
 543     /* If there are processes to interleave and the maximum depth has not been reached
 544        then perform one step of the exploration algorithm */
 545     if (xbt_fifo_size(mc_snapshot_stack) < MAX_DEPTH &&
 546         (req = MC_state_get_request(pair->graph_state, &value))) {
 547
 548       /* Debug information */
 549       if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
 550         req_str = MC_request_to_string(req, value);
 551         XBT_DEBUG("Execute: %s", req_str);
 552         xbt_free(req_str);
 553       }
 554
 555       MC_state_set_executed_request(pair->graph_state, req, value);
 556       //mc_stats_pairs->executed_transitions++;
 557
 558       /* Answer the request */
 559       SIMIX_request_pre(req, value); /* After this call req is no longer usefull */
 560
 561       /* Wait for requests (schedules processes) */
 562       MC_wait_for_requests();
 563
 564       /* Create the new expanded state */
 565       MC_SET_RAW_MEM;
 566       next_graph_state = MC_state_new();
 567
 568       /* Get an enabled process and insert it in the interleave set of the next state */
 569       xbt_swag_foreach(process, simix_global->process_list){
 570         if(MC_process_is_enabled(process)){
 571           MC_state_interleave_process(next_graph_state, process);
 572           break;
 573         }
 574       }
 575
 576       next_system_state = xbt_new0(s_mc_snapshot_t, 1);
 577       MC_take_snapshot(next_system_state);
 578       MC_UNSET_RAW_MEM;
 579
 580       cursor = 0;
 581       xbt_dynar_foreach(pair->automaton_state->out, cursor, transition_succ){
 582         res = MC_automaton_evaluate_label(a, transition_succ->label);
 583         if((res == 1) || (res == 2)){ // enabled transition in automaton
 584           next_automaton_state = transition_succ->dst;
 585           break;
 586         }
 587       }
 588
 589       if(next_automaton_state == NULL){
 590         next_automaton_state = pair->automaton_state;
 591       }
 592
 593       MC_SET_RAW_MEM;
 594       next_pair = new_pair_prop(next_system_state, next_graph_state, next_automaton_state);
 595       cursor = 0;
 596       xbt_propositional_symbol_t ps;
 597       xbt_dynar_foreach(a->propositional_symbols, cursor, ps){
 598         int (*f)() = ps->function;
 599         int val = (*f)();
 600         mc_prop_ato_t pa = new_proposition(ps->pred, val);
 601         xbt_dynar_push(next_pair->propositions, &pa);
 602       }
 603       xbt_fifo_unshift(mc_snapshot_stack, next_pair);
 604       MC_UNSET_RAW_MEM;
 605
 606
 607
 608
 609
 610       /* Let's loop again */
 611
 612       /* The interleave set is empty or the maximum depth is reached, let's back-track */
 613     } else {
 614       XBT_DEBUG("There are no more processes to interleave.");
 615
 616       /* Trash the current state, no longer needed */
 617       MC_SET_RAW_MEM;
 618       xbt_fifo_shift(mc_snapshot_stack);
 619       //MC_state_delete(state);
 620       MC_UNSET_RAW_MEM;
 621
 622       /* Check for deadlocks */
 623       if(MC_deadlock_check()){
 624         MC_show_deadlock(NULL);
 625         return;
 626       }
 627
 628       MC_SET_RAW_MEM;
 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       while ((pair = xbt_fifo_shift(mc_snapshot_stack)) != NULL) {
 636         req = MC_state_get_internal_request(pair->graph_state);
 637         xbt_fifo_foreach(mc_snapshot_stack, item, prev_pair, mc_pair_prop_t) {
 638           if(MC_request_depend(req, MC_state_get_internal_request(prev_pair->graph_state))){
 639             if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
 640               XBT_DEBUG("Dependent Transitions:");
 641               prev_req = MC_state_get_executed_request(prev_pair->graph_state, &value);
 642               req_str = MC_request_to_string(prev_req, value);
 643               XBT_DEBUG("%s (pair=%p)", req_str, prev_pair);
 644               xbt_free(req_str);
 645               prev_req = MC_state_get_executed_request(pair->graph_state, &value);
 646               req_str = MC_request_to_string(prev_req, value);
 647               XBT_DEBUG("%s (pair=%p)", req_str, pair);
 648               xbt_free(req_str);
 649             }
 650
 651             if(!MC_state_process_is_done(prev_pair->graph_state, req->issuer))
 652               MC_state_interleave_process(prev_pair->graph_state, req->issuer);
 653             else
 654               XBT_DEBUG("Process %p is in done set", req->issuer);
 655
 656             break;
 657           }
 658         }
 659         if (MC_state_interleave_size(pair->graph_state)) {
 660           /* We found a back-tracking point, let's loop */
 661           MC_restore_snapshot(pair->system_state);
 662           xbt_fifo_unshift(mc_snapshot_stack, pair);
 663           XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_snapshot_stack));
 664           MC_UNSET_RAW_MEM;
 665           break;
 666         } else {
 667           //MC_state_delete(state);
 668         }
 669       }
 670       MC_UNSET_RAW_MEM;
 671     }
 672   }
 673   MC_UNSET_RAW_MEM;
 674   return;
 675 }