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