src/mc/mc_dpor.c

   1 /* Copyright (c) 2008-2014. The SimGrid Team.
   2  * All rights reserved.                                                     */
   3
   4 /* This program is free software; you can redistribute it and/or modify it
   5  * under the terms of the license (GNU LGPL) which comes with this package. */
   6
   7 #include "mc_private.h"
   8
   9 #include "xbt/mmalloc/mmprivate.h"
  10
  11 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_dpor, mc,
  12                                 "Logging specific to MC DPOR exploration");
  13
  14 /********** Global variables **********/
  15
  16 xbt_dynar_t visited_states;
  17 xbt_dict_t first_enabled_state;
  18 xbt_dynar_t initial_communications_pattern;
  19 xbt_dynar_t incomplete_communications_pattern;
  20 xbt_dynar_t communications_pattern;
  21 int nb_comm_pattern;
  22
  23 /********** Static functions ***********/
  24
  25 static void comm_pattern_free(mc_comm_pattern_t p){
  26   xbt_free(p->rdv);
  27   xbt_free(p->data);
  28   xbt_free(p);
  29   p = NULL;
  30 }
  31
  32 static void comm_pattern_free_voidp( void *p){
  33   comm_pattern_free((mc_comm_pattern_t) * (void **)p);
  34 }
  35
  36 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){
  37   mc_comm_pattern_t current_comm;
  38   while(*idx < xbt_dynar_length(pattern)){
  39     current_comm = (mc_comm_pattern_t)xbt_dynar_get_as(pattern, *idx, mc_comm_pattern_t);
  40     if(current_comm->type == type && type == SIMIX_COMM_SEND){
  41       if(current_comm->src_proc == proc)
  42         return current_comm;
  43     }else if(current_comm->type == type && type == SIMIX_COMM_RECEIVE){
  44       if(current_comm->dst_proc == proc)
  45         return current_comm;
  46     }
  47     (*idx)++;
  48   }
  49   return NULL;
  50 }
  51
  52 static int compare_comm_pattern(mc_comm_pattern_t comm1, mc_comm_pattern_t comm2){
  53   if(strcmp(comm1->rdv, comm2->rdv) != 0)
  54     return 1;
  55   if(comm1->src_proc != comm2->src_proc)
  56     return 1;
  57   if(comm1->dst_proc != comm2->dst_proc)
  58     return 1;
  59   if(comm1->data_size != comm2->data_size)
  60     return 1;
  61   if(memcmp(comm1->data, comm2->data, comm1->data_size) != 0)
  62     return 1;
  63   return 0;
  64 }
  65
  66 static void deterministic_pattern(xbt_dynar_t initial_pattern, xbt_dynar_t pattern){
  67
  68   if(!xbt_dynar_is_empty(incomplete_communications_pattern))
  69     xbt_die("Oh oh ...");
  70
  71   unsigned int cursor = 0, send_index = 0, recv_index = 0;
  72   mc_comm_pattern_t comm1, comm2;
  73   int comm_comparison = 0;
  74   int current_process = 0;
  75   while(current_process < simix_process_maxpid){
  76     while(cursor < xbt_dynar_length(initial_pattern)){
  77       comm1 = (mc_comm_pattern_t)xbt_dynar_get_as(initial_pattern, cursor, mc_comm_pattern_t);
  78       if(comm1->type == SIMIX_COMM_SEND && comm1->src_proc == current_process){
  79         comm2 = get_comm_pattern_from_idx(pattern, &send_index, comm1->type, current_process);
  80         comm_comparison = compare_comm_pattern(comm1, comm2);
  81         if(comm_comparison == 1){
  82           initial_state_safety->send_deterministic = 0;
  83           initial_state_safety->comm_deterministic = 0;
  84           return;
  85         }
  86         send_index++;
  87       }else if(comm1->type == SIMIX_COMM_RECEIVE && comm1->dst_proc == current_process){
  88         comm2 = get_comm_pattern_from_idx(pattern, &recv_index, comm1->type, current_process);
  89         comm_comparison = compare_comm_pattern(comm1, comm2);
  90         if(comm_comparison == 1){
  91           initial_state_safety->comm_deterministic = 0;
  92           if(!_sg_mc_send_determinism)
  93             return;
  94         }
  95         recv_index++;
  96       }
  97       cursor++;
  98     }
  99     cursor = 0;
 100     send_index = 0;
 101     recv_index = 0;
 102     current_process++;
 103   }
 104 }
 105
 106 void complete_comm_pattern(xbt_dynar_t list, smx_action_t comm){
 107   mc_comm_pattern_t current_pattern;
 108   unsigned int cursor = 0;
 109   int index;
 110   int completed = 0;
 111   void *addr_pointed;
 112   xbt_dynar_foreach(incomplete_communications_pattern, cursor, index){
 113     current_pattern = (mc_comm_pattern_t)xbt_dynar_get_as(list, index, mc_comm_pattern_t);
 114     if(current_pattern->comm == comm){
 115       current_pattern->src_proc = comm->comm.src_proc->pid;
 116       current_pattern->dst_proc = comm->comm.dst_proc->pid;
 117       current_pattern->src_host = simcall_host_get_name(comm->comm.src_proc->smx_host);
 118       current_pattern->dst_host = simcall_host_get_name(comm->comm.dst_proc->smx_host);
 119       if(current_pattern->data_size == -1){
 120         current_pattern->data_size = *(comm->comm.dst_buff_size);
 121         current_pattern->data = xbt_malloc0(current_pattern->data_size);
 122         addr_pointed = *(void **)comm->comm.src_buff;
 123         if(addr_pointed > std_heap && addr_pointed < ((xbt_mheap_t)std_heap)->breakval)
 124           memcpy(current_pattern->data, addr_pointed, current_pattern->data_size);
 125         else
 126           memcpy(current_pattern->data, comm->comm.src_buff, current_pattern->data_size);
 127       }
 128       xbt_dynar_remove_at(incomplete_communications_pattern, cursor, NULL);
 129       completed++;
 130       if(completed == 2)
 131         return;
 132       cursor--;
 133     }
 134   }
 135 }
 136
 137 void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, int call){
 138   mc_comm_pattern_t pattern = NULL;
 139   pattern = xbt_new0(s_mc_comm_pattern_t, 1);
 140   pattern->num = ++nb_comm_pattern;
 141   pattern->data_size = -1;
 142   void * addr_pointed;
 143   if(call == 1){ // ISEND
 144     pattern->comm = simcall_comm_isend__get__result(request);
 145     pattern->type = SIMIX_COMM_SEND;
 146     pattern->src_proc = pattern->comm->comm.src_proc->pid;
 147     pattern->src_host = simcall_host_get_name(request->issuer->smx_host);
 148     pattern->data_size = pattern->comm->comm.src_buff_size;
 149     pattern->data = xbt_malloc0(pattern->data_size);
 150     addr_pointed = *(void **)pattern->comm->comm.src_buff;
 151     if(addr_pointed > std_heap && addr_pointed < ((xbt_mheap_t)std_heap)->breakval)
 152       memcpy(pattern->data, addr_pointed, pattern->data_size);
 153     else
 154       memcpy(pattern->data, pattern->comm->comm.src_buff, pattern->data_size);
 155   }else{ // IRECV
 156     pattern->comm = simcall_comm_irecv__get__result(request);
 157     pattern->type = SIMIX_COMM_RECEIVE;
 158     pattern->dst_proc = pattern->comm->comm.dst_proc->pid;
 159     pattern->dst_host = simcall_host_get_name(pattern->comm->comm.dst_proc->smx_host);
 160   }
 161
 162   if(pattern->comm->comm.rdv != NULL)
 163     pattern->rdv = strdup(pattern->comm->comm.rdv->name);
 164   else
 165     pattern->rdv = strdup(pattern->comm->comm.rdv_cpy->name);
 166
 167   xbt_dynar_push(list, &pattern);
 168
 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 -> (%lu) %s] %s ", current_comm->src_proc, current_comm->src_host, current_comm->dst_proc, current_comm->dst_host, "iSend");
 179     else
 180       XBT_INFO("[(%lu) %s <- (%lu) %s] %s ", current_comm->dst_proc, current_comm->dst_host, current_comm->src_proc, 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   if(mc_reduce_kind == e_mc_reduce_dpor)
 427     first_enabled_state = xbt_dict_new_homogeneous(&xbt_free_f);
 428
 429   if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
 430     initial_communications_pattern = xbt_dynar_new(sizeof(mc_comm_pattern_t), comm_pattern_free_voidp);
 431     communications_pattern = xbt_dynar_new(sizeof(mc_comm_pattern_t), comm_pattern_free_voidp);
 432     incomplete_communications_pattern = xbt_dynar_new(sizeof(int), NULL);
 433     nb_comm_pattern = 0;
 434   }
 435
 436   initial_state = MC_state_new();
 437
 438   MC_UNSET_RAW_MEM;
 439
 440   XBT_DEBUG("**************************************************");
 441   XBT_DEBUG("Initial state");
 442
 443   /* Wait for requests (schedules processes) */
 444   MC_wait_for_requests();
 445
 446   MC_ignore_heap(simix_global->process_to_run->data, 0);
 447   MC_ignore_heap(simix_global->process_that_ran->data, 0);
 448
 449   MC_SET_RAW_MEM;
 450
 451   /* Get an enabled process and insert it in the interleave set of the initial state */
 452   xbt_swag_foreach(process, simix_global->process_list){
 453     if(MC_process_is_enabled(process)){
 454       MC_state_interleave_process(initial_state, process);
 455       if(mc_reduce_kind != e_mc_reduce_none)
 456         break;
 457     }
 458   }
 459
 460   xbt_fifo_unshift(mc_stack_safety, initial_state);
 461
 462   if(mc_reduce_kind == e_mc_reduce_dpor){
 463     /* To ensure the soundness of DPOR, we have to keep a list of
 464        processes which are still enabled at each step of the exploration.
 465        If max depth is reached, we interleave them in the state in which they have
 466        been enabled for the first time. */
 467     xbt_swag_foreach(process, simix_global->process_list){
 468       if(MC_process_is_enabled(process)){
 469         char *key = bprintf("%lu", process->pid);
 470         char *data = bprintf("%d", xbt_fifo_size(mc_stack_safety));
 471         xbt_dict_set(first_enabled_state, key, data, NULL);
 472         xbt_free(key);
 473       }
 474     }
 475   }
 476
 477   MC_UNSET_RAW_MEM;
 478
 479   if(raw_mem_set)
 480     MC_SET_RAW_MEM;
 481   else
 482     MC_UNSET_RAW_MEM;
 483
 484 }
 485
 486
 487 /** \brief Model-check the application using a DFS exploration
 488  *         with DPOR (Dynamic Partial Order Reductions)
 489  */
 490 void MC_dpor(void)
 491 {
 492
 493   char *req_str = NULL;
 494   int value;
 495   smx_simcall_t req = NULL, prev_req = NULL;
 496   mc_state_t state = NULL, prev_state = NULL, next_state = NULL, restored_state=NULL;
 497   smx_process_t process = NULL;
 498   xbt_fifo_item_t item = NULL;
 499   mc_state_t state_test = NULL;
 500   int pos;
 501   int visited_state = -1;
 502   int enabled = 0;
 503   int interleave_size = 0;
 504   int comm_pattern = 0;
 505   smx_action_t current_comm;
 506
 507   while (xbt_fifo_size(mc_stack_safety) > 0) {
 508
 509     /* Get current state */
 510     state = (mc_state_t)
 511       xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_safety));
 512
 513     XBT_DEBUG("**************************************************");
 514     XBT_DEBUG("Exploration depth=%d (state=%p, num %d)(%u interleave, user_max_depth %d, first_enabled_state size : %d)",
 515               xbt_fifo_size(mc_stack_safety), state, state->num,
 516               MC_state_interleave_size(state), user_max_depth_reached, xbt_dict_size(first_enabled_state));
 517
 518     interleave_size = MC_state_interleave_size(state);
 519
 520     /* Update statistics */
 521     mc_stats->visited_states++;
 522
 523     /* If there are processes to interleave and the maximum depth has not been reached
 524        then perform one step of the exploration algorithm */
 525     if (xbt_fifo_size(mc_stack_safety) <= _sg_mc_max_depth && !user_max_depth_reached &&
 526         (req = MC_state_get_request(state, &value)) && visited_state == -1) {
 527
 528       /* Debug information */
 529       if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
 530         req_str = MC_request_to_string(req, value);
 531         XBT_DEBUG("Execute: %s", req_str);
 532         xbt_free(req_str);
 533       }
 534
 535       MC_SET_RAW_MEM;
 536       if(dot_output != NULL)
 537         req_str = MC_request_get_dot_output(req, value);
 538       MC_UNSET_RAW_MEM;
 539
 540       MC_state_set_executed_request(state, req, value);
 541       mc_stats->executed_transitions++;
 542
 543       if(mc_reduce_kind ==  e_mc_reduce_dpor){
 544         MC_SET_RAW_MEM;
 545         char *key = bprintf("%lu", req->issuer->pid);
 546         xbt_dict_remove(first_enabled_state, key);
 547         xbt_free(key);
 548         MC_UNSET_RAW_MEM;
 549       }
 550
 551       /* TODO : handle test and testany simcalls */
 552       if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
 553         if(req->call == SIMCALL_COMM_ISEND)
 554           comm_pattern = 1;
 555         else if(req->call == SIMCALL_COMM_IRECV)
 556           comm_pattern = 2;
 557         else if(req->call == SIMCALL_COMM_WAIT)
 558           comm_pattern = 3;
 559         else if(req->call == SIMCALL_COMM_WAITANY)
 560           comm_pattern = 4;
 561       }
 562
 563       /* Answer the request */
 564       SIMIX_simcall_pre(req, value); /* After this call req is no longer usefull */
 565
 566       if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
 567         MC_SET_RAW_MEM;
 568         if(comm_pattern == 1 || comm_pattern == 2){
 569           if(!initial_state_safety->initial_communications_pattern_done)
 570             get_comm_pattern(initial_communications_pattern, req, comm_pattern);
 571           else
 572             get_comm_pattern(communications_pattern, req, comm_pattern);
 573         }else if(comm_pattern == 3){
 574           current_comm = simcall_comm_wait__get__comm(req);
 575           if(current_comm->comm.refcount == 1){ /* First wait only must be considered */
 576             if(!initial_state_safety->initial_communications_pattern_done)
 577               complete_comm_pattern(initial_communications_pattern, current_comm);
 578             else
 579               complete_comm_pattern(communications_pattern, current_comm);
 580           }
 581         }else if(comm_pattern == 4){
 582           current_comm = xbt_dynar_get_as(simcall_comm_waitany__get__comms(req), value, smx_action_t);
 583           if(current_comm->comm.refcount == 1){ /* First wait only must be considered */
 584             if(!initial_state_safety->initial_communications_pattern_done)
 585               complete_comm_pattern(initial_communications_pattern, current_comm);
 586             else
 587               complete_comm_pattern(communications_pattern, current_comm);
 588           }
 589         }
 590         MC_UNSET_RAW_MEM;
 591         comm_pattern = 0;
 592       }
 593
 594       /* Wait for requests (schedules processes) */
 595       MC_wait_for_requests();
 596
 597       /* Create the new expanded state */
 598       MC_SET_RAW_MEM;
 599
 600       next_state = MC_state_new();
 601
 602       if((visited_state = is_visited_state()) == -1){
 603
 604         /* Get an enabled process and insert it in the interleave set of the next state */
 605         xbt_swag_foreach(process, simix_global->process_list){
 606           if(MC_process_is_enabled(process)){
 607             MC_state_interleave_process(next_state, process);
 608             if(mc_reduce_kind != e_mc_reduce_none)
 609               break;
 610           }
 611         }
 612
 613         if(_sg_mc_checkpoint && ((xbt_fifo_size(mc_stack_safety) + 1) % _sg_mc_checkpoint == 0)){
 614           next_state->system_state = MC_take_snapshot(next_state->num);
 615         }
 616
 617         if(dot_output != NULL)
 618           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str);
 619
 620       }else{
 621
 622         if(dot_output != NULL)
 623           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visited_state, req_str);
 624
 625       }
 626
 627       xbt_fifo_unshift(mc_stack_safety, next_state);
 628
 629       if(mc_reduce_kind ==  e_mc_reduce_dpor){
 630         /* Insert in dict all enabled processes, if not included yet */
 631         xbt_swag_foreach(process, simix_global->process_list){
 632           if(MC_process_is_enabled(process)){
 633             char *key = bprintf("%lu", process->pid);
 634             if(xbt_dict_get_or_null(first_enabled_state, key) == NULL){
 635               char *data = bprintf("%d", xbt_fifo_size(mc_stack_safety));
 636               xbt_dict_set(first_enabled_state, key, data, NULL);
 637             }
 638             xbt_free(key);
 639           }
 640         }
 641       }
 642
 643       if(dot_output != NULL)
 644         xbt_free(req_str);
 645
 646       MC_UNSET_RAW_MEM;
 647
 648       /* Let's loop again */
 649
 650       /* The interleave set is empty or the maximum depth is reached, let's back-track */
 651     } else {
 652
 653       if((xbt_fifo_size(mc_stack_safety) > _sg_mc_max_depth) || user_max_depth_reached || visited_state != -1){
 654
 655         if(user_max_depth_reached && visited_state == -1)
 656           XBT_DEBUG("User max depth reached !");
 657         else if(visited_state == -1)
 658           XBT_WARN("/!\\ Max depth reached ! /!\\ ");
 659
 660         visited_state = -1;
 661
 662         if(mc_reduce_kind ==  e_mc_reduce_dpor){
 663           /* Interleave enabled processes in the state in which they have been enabled for the first time */
 664           xbt_swag_foreach(process, simix_global->process_list){
 665             if(MC_process_is_enabled(process)){
 666               char *key = bprintf("%lu", process->pid);
 667               enabled = (int)strtoul(xbt_dict_get_or_null(first_enabled_state, key), 0, 10);
 668               xbt_free(key);
 669               int cursor = xbt_fifo_size(mc_stack_safety);
 670               xbt_fifo_foreach(mc_stack_safety, item, state_test, mc_state_t){
 671                 if(cursor-- == enabled){
 672                   if(!MC_state_process_is_done(state_test, process) && state_test->num != state->num){
 673                     XBT_DEBUG("Interleave process %lu in state %d", process->pid, state_test->num);
 674                     MC_state_interleave_process(state_test, process);
 675                     break;
 676                   }
 677                 }
 678               }
 679             }
 680           }
 681         }
 682
 683       }else{
 684
 685         XBT_DEBUG("There are no more processes to interleave. (depth %d)", xbt_fifo_size(mc_stack_safety) + 1);
 686
 687       }
 688
 689       MC_SET_RAW_MEM;
 690
 691       if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
 692         if(initial_state_safety->initial_communications_pattern_done){
 693           if(interleave_size == 0){ /* if (interleave_size > 0), process interleaved but not enabled => "incorrect" path, determinism not evaluated */
 694             //print_communications_pattern(communications_pattern);
 695             deterministic_pattern(initial_communications_pattern, communications_pattern);
 696             if(initial_state_safety->comm_deterministic == 0 && _sg_mc_comms_determinism){
 697               XBT_INFO("****************************************************");
 698               XBT_INFO("***** Non-deterministic communications pattern *****");
 699               XBT_INFO("****************************************************");
 700               XBT_INFO("Initial communications pattern:");
 701               print_communications_pattern(initial_communications_pattern);
 702               XBT_INFO("Communications pattern counter-example:");
 703               print_communications_pattern(communications_pattern);
 704               MC_print_statistics(mc_stats);
 705               return;
 706             }else if(initial_state_safety->send_deterministic == 0 && _sg_mc_send_determinism){
 707               XBT_INFO("****************************************************");
 708               XBT_INFO("***** Non-send-deterministic communications pattern *****");
 709               XBT_INFO("****************************************************");
 710               XBT_INFO("Initial communications pattern:");
 711               print_communications_pattern(initial_communications_pattern);
 712               XBT_INFO("Communications pattern counter-example:");
 713               print_communications_pattern(communications_pattern);
 714               MC_print_statistics(mc_stats);
 715               return;
 716             }
 717           }
 718         }else{
 719           initial_state_safety->initial_communications_pattern_done = 1;
 720         }
 721       }
 722
 723       /* Trash the current state, no longer needed */
 724       xbt_fifo_shift(mc_stack_safety);
 725       MC_state_delete(state);
 726       XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1);
 727
 728       MC_UNSET_RAW_MEM;
 729
 730       /* Check for deadlocks */
 731       if(MC_deadlock_check()){
 732         MC_show_deadlock(NULL);
 733         return;
 734       }
 735
 736       MC_SET_RAW_MEM;
 737       /* Traverse the stack backwards until a state with a non empty interleave
 738          set is found, deleting all the states that have it empty in the way.
 739          For each deleted state, check if the request that has generated it
 740          (from it's predecesor state), depends on any other previous request
 741          executed before it. If it does then add it to the interleave set of the
 742          state that executed that previous request. */
 743
 744       while ((state = xbt_fifo_shift(mc_stack_safety)) != NULL) {
 745         if(mc_reduce_kind == e_mc_reduce_dpor){
 746           req = MC_state_get_internal_request(state);
 747           xbt_fifo_foreach(mc_stack_safety, item, prev_state, mc_state_t) {
 748             if(MC_request_depend(req, MC_state_get_internal_request(prev_state))){
 749               if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
 750                 XBT_DEBUG("Dependent Transitions:");
 751                 prev_req = MC_state_get_executed_request(prev_state, &value);
 752                 req_str = MC_request_to_string(prev_req, value);
 753                 XBT_DEBUG("%s (state=%d)", req_str, prev_state->num);
 754                 xbt_free(req_str);
 755                 prev_req = MC_state_get_executed_request(state, &value);
 756                 req_str = MC_request_to_string(prev_req, value);
 757                 XBT_DEBUG("%s (state=%d)", req_str, state->num);
 758                 xbt_free(req_str);
 759               }
 760
 761               if(!MC_state_process_is_done(prev_state, req->issuer))
 762                 MC_state_interleave_process(prev_state, req->issuer);
 763               else
 764                 XBT_DEBUG("Process %p is in done set", req->issuer);
 765
 766               break;
 767
 768             }else if(req->issuer == MC_state_get_internal_request(prev_state)->issuer){
 769
 770               XBT_DEBUG("Simcall %d and %d with same issuer", req->call, MC_state_get_internal_request(prev_state)->call);
 771               break;
 772
 773             }else{
 774
 775               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);
 776
 777             }
 778           }
 779         }
 780
 781         if (MC_state_interleave_size(state) && xbt_fifo_size(mc_stack_safety) < _sg_mc_max_depth) {
 782           /* We found a back-tracking point, let's loop */
 783           XBT_DEBUG("Back-tracking to state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1);
 784           if(_sg_mc_checkpoint){
 785             if(state->system_state != NULL){
 786               MC_restore_snapshot(state->system_state);
 787               xbt_fifo_unshift(mc_stack_safety, state);
 788               MC_UNSET_RAW_MEM;
 789             }else{
 790               pos = xbt_fifo_size(mc_stack_safety);
 791               item = xbt_fifo_get_first_item(mc_stack_safety);
 792               while(pos>0){
 793                 restored_state = (mc_state_t) xbt_fifo_get_item_content(item);
 794                 if(restored_state->system_state != NULL){
 795                   break;
 796                 }else{
 797                   item = xbt_fifo_get_next_item(item);
 798                   pos--;
 799                 }
 800               }
 801               MC_restore_snapshot(restored_state->system_state);
 802               xbt_fifo_unshift(mc_stack_safety, state);
 803               MC_UNSET_RAW_MEM;
 804               MC_replay(mc_stack_safety, pos);
 805             }
 806           }else{
 807             xbt_fifo_unshift(mc_stack_safety, state);
 808             MC_UNSET_RAW_MEM;
 809             MC_replay(mc_stack_safety, -1);
 810           }
 811           XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num, xbt_fifo_size(mc_stack_safety));
 812           break;
 813         } else {
 814           /*req = MC_state_get_internal_request(state);
 815           if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
 816             if(req->call == SIMCALL_COMM_ISEND || req->call == SIMCALL_COMM_IRECV){
 817               if(!xbt_dynar_is_empty(communications_pattern))
 818                 xbt_dynar_remove_at(communications_pattern, xbt_dynar_length(communications_pattern) - 1, NULL);
 819             }
 820             }*/
 821           XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1);
 822           MC_state_delete(state);
 823         }
 824       }
 825       MC_UNSET_RAW_MEM;
 826     }
 827   }
 828   MC_print_statistics(mc_stats);
 829   MC_UNSET_RAW_MEM;
 830
 831   return;
 832 }
 833
 834
 835
 836