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