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   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
 506   while (xbt_fifo_size(mc_stack_safety) > 0) {
 507
 508     /* Get current state */
 509     state = (mc_state_t)
 510       xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_safety));
 511
 512     XBT_DEBUG("**************************************************");
 513     XBT_DEBUG("Exploration depth=%d (state=%p, num %d)(%u interleave, user_max_depth %d, first_enabled_state size : %d)",
 514               xbt_fifo_size(mc_stack_safety), state, state->num,
 515               MC_state_interleave_size(state), user_max_depth_reached, xbt_dict_size(first_enabled_state));
 516
 517     interleave_size = MC_state_interleave_size(state);
 518
 519     /* Update statistics */
 520     mc_stats->visited_states++;
 521
 522     /* If there are processes to interleave and the maximum depth has not been reached
 523        then perform one step of the exploration algorithm */
 524     if (xbt_fifo_size(mc_stack_safety) <= _sg_mc_max_depth && !user_max_depth_reached &&
 525         (req = MC_state_get_request(state, &value)) && visited_state == -1) {
 526
 527       /* Debug information */
 528       if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
 529         req_str = MC_request_to_string(req, value);
 530         XBT_DEBUG("Execute: %s", req_str);
 531         xbt_free(req_str);
 532       }
 533
 534       MC_SET_RAW_MEM;
 535       if(dot_output != NULL)
 536         req_str = MC_request_get_dot_output(req, value);
 537       MC_UNSET_RAW_MEM;
 538
 539       MC_state_set_executed_request(state, req, value);
 540       mc_stats->executed_transitions++;
 541
 542       if(mc_reduce_kind ==  e_mc_reduce_dpor){
 543         MC_SET_RAW_MEM;
 544         char *key = bprintf("%lu", req->issuer->pid);
 545         xbt_dict_remove(first_enabled_state, key);
 546         xbt_free(key);
 547         MC_UNSET_RAW_MEM;
 548       }
 549
 550       if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
 551         if(req->call == SIMCALL_COMM_ISEND)
 552           comm_pattern = 1;
 553         else if(req->call == SIMCALL_COMM_IRECV)
 554           comm_pattern = 2;
 555       }
 556
 557       /* Answer the request */
 558       SIMIX_simcall_pre(req, value); /* After this call req is no longer usefull */
 559
 560       if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
 561         MC_SET_RAW_MEM;
 562         if(comm_pattern != 0){
 563           if(!initial_state_safety->initial_communications_pattern_done)
 564             get_comm_pattern(initial_communications_pattern, req, comm_pattern);
 565           else
 566             get_comm_pattern(communications_pattern, req, comm_pattern);
 567         }
 568         MC_UNSET_RAW_MEM;
 569         comm_pattern = 0;
 570       }
 571
 572       /* Wait for requests (schedules processes) */
 573       MC_wait_for_requests();
 574
 575       /* Create the new expanded state */
 576       MC_SET_RAW_MEM;
 577
 578       next_state = MC_state_new();
 579
 580       if((visited_state = is_visited_state()) == -1){
 581
 582         /* Get an enabled process and insert it in the interleave set of the next state */
 583         xbt_swag_foreach(process, simix_global->process_list){
 584           if(MC_process_is_enabled(process)){
 585             MC_state_interleave_process(next_state, process);
 586             if(mc_reduce_kind != e_mc_reduce_none)
 587               break;
 588           }
 589         }
 590
 591         if(_sg_mc_checkpoint && ((xbt_fifo_size(mc_stack_safety) + 1) % _sg_mc_checkpoint == 0)){
 592           next_state->system_state = MC_take_snapshot(next_state->num);
 593         }
 594
 595         if(dot_output != NULL)
 596           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str);
 597
 598       }else{
 599
 600         if(dot_output != NULL)
 601           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visited_state, req_str);
 602
 603       }
 604
 605       xbt_fifo_unshift(mc_stack_safety, next_state);
 606
 607       if(mc_reduce_kind ==  e_mc_reduce_dpor){
 608         /* Insert in dict all enabled processes, if not included yet */
 609         xbt_swag_foreach(process, simix_global->process_list){
 610           if(MC_process_is_enabled(process)){
 611             char *key = bprintf("%lu", process->pid);
 612             if(xbt_dict_get_or_null(first_enabled_state, key) == NULL){
 613               char *data = bprintf("%d", xbt_fifo_size(mc_stack_safety));
 614               xbt_dict_set(first_enabled_state, key, data, NULL);
 615             }
 616             xbt_free(key);
 617           }
 618         }
 619       }
 620
 621       if(dot_output != NULL)
 622         xbt_free(req_str);
 623
 624       MC_UNSET_RAW_MEM;
 625
 626       /* Let's loop again */
 627
 628       /* The interleave set is empty or the maximum depth is reached, let's back-track */
 629     } else {
 630
 631       if((xbt_fifo_size(mc_stack_safety) > _sg_mc_max_depth) || user_max_depth_reached || visited_state != -1){
 632
 633         if(user_max_depth_reached && visited_state == -1)
 634           XBT_DEBUG("User max depth reached !");
 635         else if(visited_state == -1)
 636           XBT_WARN("/!\\ Max depth reached ! /!\\ ");
 637
 638         visited_state = -1;
 639
 640         if(mc_reduce_kind ==  e_mc_reduce_dpor){
 641           /* Interleave enabled processes in the state in which they have been enabled for the first time */
 642           xbt_swag_foreach(process, simix_global->process_list){
 643             if(MC_process_is_enabled(process)){
 644               char *key = bprintf("%lu", process->pid);
 645               enabled = (int)strtoul(xbt_dict_get_or_null(first_enabled_state, key), 0, 10);
 646               xbt_free(key);
 647               int cursor = xbt_fifo_size(mc_stack_safety);
 648               xbt_fifo_foreach(mc_stack_safety, item, state_test, mc_state_t){
 649                 if(cursor-- == enabled){
 650                   if(!MC_state_process_is_done(state_test, process) && state_test->num != state->num){
 651                     XBT_DEBUG("Interleave process %lu in state %d", process->pid, state_test->num);
 652                     MC_state_interleave_process(state_test, process);
 653                     break;
 654                   }
 655                 }
 656               }
 657             }
 658           }
 659         }
 660
 661       }else{
 662
 663         XBT_DEBUG("There are no more processes to interleave. (depth %d)", xbt_fifo_size(mc_stack_safety) + 1);
 664
 665       }
 666
 667       MC_SET_RAW_MEM;
 668
 669       if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
 670         if(initial_state_safety->initial_communications_pattern_done){
 671           if(interleave_size == 0){ /* if (interleave_size > 0), process interleaved but not enabled => "incorrect" path, determinism not evaluated */
 672             //print_communications_pattern(communications_pattern);
 673             deterministic_pattern(initial_communications_pattern, communications_pattern);
 674             if(initial_state_safety->comm_deterministic == 0 && _sg_mc_comms_determinism){
 675               XBT_INFO("****************************************************");
 676               XBT_INFO("***** Non-deterministic communications pattern *****");
 677               XBT_INFO("****************************************************");
 678               XBT_INFO("Initial communications pattern:");
 679               print_communications_pattern(initial_communications_pattern);
 680               XBT_INFO("Communications pattern counter-example:");
 681               print_communications_pattern(communications_pattern);
 682               MC_print_statistics(mc_stats);
 683               return;
 684             }else if(initial_state_safety->send_deterministic == 0 && _sg_mc_send_determinism){
 685               XBT_INFO("****************************************************");
 686               XBT_INFO("***** Non-send-deterministic communications pattern *****");
 687               XBT_INFO("****************************************************");
 688               XBT_INFO("Initial communications pattern:");
 689               print_communications_pattern(initial_communications_pattern);
 690               XBT_INFO("Communications pattern counter-example:");
 691               print_communications_pattern(communications_pattern);
 692               MC_print_statistics(mc_stats);
 693               return;
 694             }
 695           }
 696         }else{
 697           initial_state_safety->initial_communications_pattern_done = 1;
 698         }
 699       }
 700
 701       /* Trash the current state, no longer needed */
 702       xbt_fifo_shift(mc_stack_safety);
 703       MC_state_delete(state);
 704       XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1);
 705
 706       MC_UNSET_RAW_MEM;
 707
 708       /* Check for deadlocks */
 709       if(MC_deadlock_check()){
 710         MC_show_deadlock(NULL);
 711         return;
 712       }
 713
 714       MC_SET_RAW_MEM;
 715       /* Traverse the stack backwards until a state with a non empty interleave
 716          set is found, deleting all the states that have it empty in the way.
 717          For each deleted state, check if the request that has generated it
 718          (from it's predecesor state), depends on any other previous request
 719          executed before it. If it does then add it to the interleave set of the
 720          state that executed that previous request. */
 721
 722       while ((state = xbt_fifo_shift(mc_stack_safety)) != NULL) {
 723         if(mc_reduce_kind != e_mc_reduce_none){
 724           req = MC_state_get_internal_request(state);
 725           xbt_fifo_foreach(mc_stack_safety, item, prev_state, mc_state_t) {
 726             if(MC_request_depend(req, MC_state_get_internal_request(prev_state))){
 727               if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
 728                 XBT_DEBUG("Dependent Transitions:");
 729                 prev_req = MC_state_get_executed_request(prev_state, &value);
 730                 req_str = MC_request_to_string(prev_req, value);
 731                 XBT_DEBUG("%s (state=%d)", req_str, prev_state->num);
 732                 xbt_free(req_str);
 733                 prev_req = MC_state_get_executed_request(state, &value);
 734                 req_str = MC_request_to_string(prev_req, value);
 735                 XBT_DEBUG("%s (state=%d)", req_str, state->num);
 736                 xbt_free(req_str);
 737               }
 738
 739               if(!MC_state_process_is_done(prev_state, req->issuer))
 740                 MC_state_interleave_process(prev_state, req->issuer);
 741               else
 742                 XBT_DEBUG("Process %p is in done set", req->issuer);
 743
 744               break;
 745
 746             }else if(req->issuer == MC_state_get_internal_request(prev_state)->issuer){
 747
 748               XBT_DEBUG("Simcall %d and %d with same issuer", req->call, MC_state_get_internal_request(prev_state)->call);
 749               break;
 750
 751             }else{
 752
 753               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);
 754
 755             }
 756           }
 757         }
 758
 759         if (MC_state_interleave_size(state) && xbt_fifo_size(mc_stack_safety) < _sg_mc_max_depth) {
 760           /* We found a back-tracking point, let's loop */
 761           XBT_DEBUG("Back-tracking to state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1);
 762           if(_sg_mc_checkpoint){
 763             if(state->system_state != NULL){
 764               MC_restore_snapshot(state->system_state);
 765               xbt_fifo_unshift(mc_stack_safety, state);
 766               MC_UNSET_RAW_MEM;
 767             }else{
 768               pos = xbt_fifo_size(mc_stack_safety);
 769               item = xbt_fifo_get_first_item(mc_stack_safety);
 770               while(pos>0){
 771                 restored_state = (mc_state_t) xbt_fifo_get_item_content(item);
 772                 if(restored_state->system_state != NULL){
 773                   break;
 774                 }else{
 775                   item = xbt_fifo_get_next_item(item);
 776                   pos--;
 777                 }
 778               }
 779               MC_restore_snapshot(restored_state->system_state);
 780               xbt_fifo_unshift(mc_stack_safety, state);
 781               MC_UNSET_RAW_MEM;
 782               MC_replay(mc_stack_safety, pos);
 783             }
 784           }else{
 785             xbt_fifo_unshift(mc_stack_safety, state);
 786             MC_UNSET_RAW_MEM;
 787             MC_replay(mc_stack_safety, -1);
 788           }
 789           XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num, xbt_fifo_size(mc_stack_safety));
 790           break;
 791         } else {
 792           /*req = MC_state_get_internal_request(state);
 793           if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
 794             if(req->call == SIMCALL_COMM_ISEND || req->call == SIMCALL_COMM_IRECV){
 795               if(!xbt_dynar_is_empty(communications_pattern))
 796                 xbt_dynar_remove_at(communications_pattern, xbt_dynar_length(communications_pattern) - 1, NULL);
 797             }
 798             }*/
 799           XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1);
 800           MC_state_delete(state);
 801         }
 802       }
 803       MC_UNSET_RAW_MEM;
 804     }
 805   }
 806   MC_print_statistics(mc_stats);
 807   MC_UNSET_RAW_MEM;
 808
 809   return;
 810 }
 811
 812
 813
 814