src/mc/mc_dpor.c

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