1 /* Copyright (c) 2008-2014. The SimGrid Team.
2 * All rights reserved. */
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. */
7 #include "mc_private.h"
9 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_dpor, mc,
10 "Logging specific to MC DPOR exploration");
12 /********** Global variables **********/
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;
20 /********** Static functions ***********/
22 static void comm_pattern_free(mc_comm_pattern_t p){
29 static void comm_pattern_free_voidp( void *p){
30 comm_pattern_free((mc_comm_pattern_t) * (void **)p);
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)
40 }else if(current_comm->type == type && type == SIMIX_COMM_RECEIVE){
41 if(current_comm->dst_proc == proc)
49 static int compare_comm_pattern(mc_comm_pattern_t comm1, mc_comm_pattern_t comm2){
50 if(strcmp(comm1->rdv, comm2->rdv) != 0)
52 if(comm1->src_proc != comm2->src_proc)
54 if(comm1->dst_proc != comm2->dst_proc)
56 if(comm1->data_size != comm2->data_size)
58 if(memcmp(comm1->data, comm2->data, comm1->data_size) != 0)
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;
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;
97 static int complete_comm_pattern(xbt_dynar_t list, mc_comm_pattern_t pattern){
98 mc_comm_pattern_t current_pattern;
99 unsigned int cursor = 0;
100 xbt_dynar_foreach(list, cursor, current_pattern){
101 if(current_pattern->comm == pattern->comm){
102 if(!current_pattern->completed){
103 current_pattern->src_proc = pattern->comm->comm.src_proc->pid;
104 current_pattern->src_host = simcall_host_get_name(pattern->comm->comm.src_proc->smx_host);
105 current_pattern->dst_proc = pattern->comm->comm.dst_proc->pid;
106 current_pattern->dst_host = simcall_host_get_name(pattern->comm->comm.dst_proc->smx_host);
107 current_pattern->data_size = pattern->comm->comm.src_buff_size;
108 current_pattern->data = xbt_malloc0(current_pattern->data_size);
109 current_pattern->matched_comm = pattern->num;
110 memcpy(current_pattern->data, current_pattern->comm->comm.src_buff, current_pattern->data_size);
111 current_pattern->completed = 1;
112 return current_pattern->num;
119 void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, int call){
120 mc_comm_pattern_t pattern = NULL;
121 pattern = xbt_new0(s_mc_comm_pattern_t, 1);
122 pattern->num = ++nb_comm_pattern;
123 pattern->completed = 0;
124 if(call == 1){ // ISEND
125 pattern->comm = simcall_comm_isend__get__result(request);
126 pattern->type = SIMIX_COMM_SEND;
127 if(pattern->comm->comm.dst_proc != NULL){
128 pattern->matched_comm = complete_comm_pattern(list, pattern);
129 pattern->dst_proc = pattern->comm->comm.dst_proc->pid;
130 pattern->completed = 1;
131 pattern->dst_host = simcall_host_get_name(pattern->comm->comm.dst_proc->smx_host);
133 pattern->src_proc = pattern->comm->comm.src_proc->pid;
134 pattern->src_host = simcall_host_get_name(request->issuer->smx_host);
135 pattern->data_size = pattern->comm->comm.src_buff_size;
136 pattern->data=xbt_malloc0(pattern->data_size);
137 memcpy(pattern->data, pattern->comm->comm.src_buff, pattern->data_size);
139 pattern->comm = simcall_comm_irecv__get__result(request);
140 pattern->type = SIMIX_COMM_RECEIVE;
141 if(pattern->comm->comm.src_proc != NULL){
142 pattern->matched_comm = complete_comm_pattern(list, pattern);
143 pattern->src_proc = pattern->comm->comm.src_proc->pid;
144 pattern->src_host = simcall_host_get_name(pattern->comm->comm.src_proc->smx_host);
145 pattern->completed = 1;
146 pattern->data_size = pattern->comm->comm.src_buff_size;
147 pattern->data=xbt_malloc0(pattern->data_size);
148 memcpy(pattern->data, pattern->comm->comm.src_buff, pattern->data_size);
150 pattern->dst_proc = pattern->comm->comm.dst_proc->pid;
151 pattern->dst_host = simcall_host_get_name(request->issuer->smx_host);
153 if(pattern->comm->comm.rdv != NULL)
154 pattern->rdv = strdup(pattern->comm->comm.rdv->name);
156 pattern->rdv = strdup(pattern->comm->comm.rdv_cpy->name);
157 xbt_dynar_push(list, &pattern);
160 static void print_communications_pattern(xbt_dynar_t comms_pattern){
161 unsigned int cursor = 0;
162 mc_comm_pattern_t current_comm;
163 xbt_dynar_foreach(comms_pattern, cursor, current_comm){
164 if(current_comm->type == SIMIX_COMM_SEND)
165 XBT_INFO("[(%lu) %s -> %s] %s ", current_comm->src_proc, current_comm->src_host, current_comm->dst_host, "iSend");
167 XBT_INFO("[(%lu) %s <- %s] %s ", current_comm->dst_proc, current_comm->dst_host, current_comm->src_host, "iRecv");
171 static void visited_state_free(mc_visited_state_t state){
173 MC_free_snapshot(state->system_state);
178 static void visited_state_free_voidp(void *s){
179 visited_state_free((mc_visited_state_t) * (void **) s);
182 /** \brief Save the current state
184 * \return Snapshot of the current state.
186 static mc_visited_state_t visited_state_new(){
188 mc_visited_state_t new_state = NULL;
189 new_state = xbt_new0(s_mc_visited_state_t, 1);
190 new_state->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
191 new_state->nb_processes = xbt_swag_size(simix_global->process_list);
192 new_state->system_state = MC_take_snapshot(mc_stats->expanded_states);
193 new_state->num = mc_stats->expanded_states;
194 new_state->other_num = -1;
200 /** \brief Find a suitable subrange of candidate duplicates for a given state
202 * \param all_ pairs dynamic array of states with candidate duplicates of the current state;
203 * \param pair current state;
204 * \param min (output) index of the beginning of the the subrange
205 * \param max (output) index of the enf of the subrange
207 * Given a suitably ordered array of state, this function extracts a subrange
208 * (with index *min <= i <= *max) with candidate duplicates of the given state.
209 * This function uses only fast discriminating criterions and does not use the
210 * full state comparison algorithms.
212 * The states in all_pairs MUST be ordered using a (given) weak order
213 * (based on nb_processes and heap_bytes_used).
214 * The subrange is the subrange of "equivalence" of the given state.
216 static int get_search_interval(xbt_dynar_t all_states, mc_visited_state_t state, int *min, int *max){
217 XBT_VERB("Searching interval for state %i: nd_processes=%zu heap_bytes_used=%zu",
218 state->num, (size_t)state->nb_processes, (size_t)state->heap_bytes_used);
220 int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
224 int cursor = 0, previous_cursor, next_cursor;
225 mc_visited_state_t state_test;
227 int end = xbt_dynar_length(all_states) - 1;
230 cursor = (start + end) / 2;
231 state_test = (mc_visited_state_t)xbt_dynar_get_as(all_states, cursor, mc_visited_state_t);
232 if(state_test->nb_processes < state->nb_processes){
234 }else if(state_test->nb_processes > state->nb_processes){
237 if(state_test->heap_bytes_used < state->heap_bytes_used){
239 }else if(state_test->heap_bytes_used > state->heap_bytes_used){
242 *min = *max = cursor;
243 previous_cursor = cursor - 1;
244 while(previous_cursor >= 0){
245 state_test = (mc_visited_state_t)xbt_dynar_get_as(all_states, previous_cursor, mc_visited_state_t);
246 if(state_test->nb_processes != state->nb_processes || state_test->heap_bytes_used != state->heap_bytes_used)
248 *min = previous_cursor;
251 next_cursor = cursor + 1;
252 while(next_cursor < xbt_dynar_length(all_states)){
253 state_test = (mc_visited_state_t)xbt_dynar_get_as(all_states, next_cursor, mc_visited_state_t);
254 if(state_test->nb_processes != state->nb_processes || state_test->heap_bytes_used != state->heap_bytes_used)
272 /** \brief Take a snapshot the current state and process it.
274 * \return number of the duplicate state or -1 (not visited)
276 static int is_visited_state(){
278 if(_sg_mc_visited == 0)
281 int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
285 mc_visited_state_t new_state = visited_state_new();
287 if(xbt_dynar_is_empty(visited_states)){
289 xbt_dynar_push(visited_states, &new_state);
298 int min = -1, max = -1, index;
300 mc_visited_state_t state_test;
303 index = get_search_interval(visited_states, new_state, &min, &max);
305 if(min != -1 && max != -1){
307 // Parallell implementation
308 /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_states, min), (max-min)+1, new_state);
310 state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, (min+res)-1, mc_visited_state_t);
311 if(state_test->other_num == -1)
312 new_state->other_num = state_test->num;
314 new_state->other_num = state_test->other_num;
315 if(dot_output == NULL)
316 XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
318 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);
319 xbt_dynar_remove_at(visited_states, (min + res) - 1, NULL);
320 xbt_dynar_insert_at(visited_states, (min+res) - 1, &new_state);
323 return new_state->other_num;
327 while(cursor <= max){
328 state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, cursor, mc_visited_state_t);
329 if(snapshot_compare(state_test, new_state) == 0){
330 // The state has been visited:
332 if(state_test->other_num == -1)
333 new_state->other_num = state_test->num;
335 new_state->other_num = state_test->other_num;
336 if(dot_output == NULL)
337 XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
339 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);
341 // Replace the old state with the new one (why?):
342 xbt_dynar_remove_at(visited_states, cursor, NULL);
343 xbt_dynar_insert_at(visited_states, cursor, &new_state);
347 return new_state->other_num;
352 // The state has not been visited, add it to the list:
353 xbt_dynar_insert_at(visited_states, min, &new_state);
357 // The state has not been visited: insert the state in the dynamic array.
358 state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, index, mc_visited_state_t);
359 if(state_test->nb_processes < new_state->nb_processes){
360 xbt_dynar_insert_at(visited_states, index+1, &new_state);
362 if(state_test->heap_bytes_used < new_state->heap_bytes_used)
363 xbt_dynar_insert_at(visited_states, index + 1, &new_state);
365 xbt_dynar_insert_at(visited_states, index, &new_state);
370 // We have reached the maximum number of stored states;
371 if(xbt_dynar_length(visited_states) > _sg_mc_visited){
373 // Find the (index of the) older state:
374 int min2 = mc_stats->expanded_states;
375 unsigned int cursor2 = 0;
376 unsigned int index2 = 0;
377 xbt_dynar_foreach(visited_states, cursor2, state_test){
378 if(state_test->num < min2){
380 min2 = state_test->num;
385 xbt_dynar_remove_at(visited_states, index2, NULL);
397 * \brief Initialize the DPOR exploration algorithm
402 int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
404 mc_state_t initial_state = NULL;
405 smx_process_t process;
407 /* Create the initial state and push it into the exploration stack */
410 if(_sg_mc_visited > 0)
411 visited_states = xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp);
413 first_enabled_state = xbt_dict_new_homogeneous(&xbt_free_f);
415 initial_communications_pattern = xbt_dynar_new(sizeof(mc_comm_pattern_t), comm_pattern_free_voidp);
416 communications_pattern = xbt_dynar_new(sizeof(mc_comm_pattern_t), comm_pattern_free_voidp);
419 initial_state = MC_state_new();
423 XBT_DEBUG("**************************************************");
424 XBT_DEBUG("Initial state");
426 /* Wait for requests (schedules processes) */
427 MC_wait_for_requests();
429 MC_ignore_heap(simix_global->process_to_run->data, 0);
430 MC_ignore_heap(simix_global->process_that_ran->data, 0);
434 /* Get an enabled process and insert it in the interleave set of the initial state */
435 xbt_swag_foreach(process, simix_global->process_list){
436 if(MC_process_is_enabled(process)){
437 MC_state_interleave_process(initial_state, process);
438 if(mc_reduce_kind != e_mc_reduce_none)
443 xbt_fifo_unshift(mc_stack_safety, initial_state);
445 /* To ensure the soundness of DPOR, we have to keep a list of
446 processes which are still enabled at each step of the exploration.
447 If max depth is reached, we interleave them in the state in which they have
448 been enabled for the first time. */
449 xbt_swag_foreach(process, simix_global->process_list){
450 if(MC_process_is_enabled(process)){
451 char *key = bprintf("%lu", process->pid);
452 char *data = bprintf("%d", xbt_fifo_size(mc_stack_safety));
453 xbt_dict_set(first_enabled_state, key, data, NULL);
468 /** \brief Model-check the application using a DFS exploration
469 * with DPOR (Dynamic Partial Order Reductions)
474 char *req_str = NULL;
476 smx_simcall_t req = NULL, prev_req = NULL;
477 mc_state_t state = NULL, prev_state = NULL, next_state = NULL, restored_state=NULL;
478 smx_process_t process = NULL;
479 xbt_fifo_item_t item = NULL;
480 mc_state_t state_test = NULL;
482 int visited_state = -1;
484 int interleave_size = 0;
485 int comm_pattern = 0;
487 while (xbt_fifo_size(mc_stack_safety) > 0) {
489 /* Get current state */
491 xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_safety));
493 XBT_DEBUG("**************************************************");
494 XBT_DEBUG("Exploration depth=%d (state=%p, num %d)(%u interleave, user_max_depth %d, first_enabled_state size : %d)",
495 xbt_fifo_size(mc_stack_safety), state, state->num,
496 MC_state_interleave_size(state), user_max_depth_reached, xbt_dict_size(first_enabled_state));
498 interleave_size = MC_state_interleave_size(state);
500 /* Update statistics */
501 mc_stats->visited_states++;
503 /* If there are processes to interleave and the maximum depth has not been reached
504 then perform one step of the exploration algorithm */
505 if (xbt_fifo_size(mc_stack_safety) <= _sg_mc_max_depth && !user_max_depth_reached &&
506 (req = MC_state_get_request(state, &value)) && visited_state == -1) {
508 /* Debug information */
509 if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
510 req_str = MC_request_to_string(req, value);
511 XBT_DEBUG("Execute: %s", req_str);
516 if(dot_output != NULL)
517 req_str = MC_request_get_dot_output(req, value);
520 MC_state_set_executed_request(state, req, value);
521 mc_stats->executed_transitions++;
524 char *key = bprintf("%lu", req->issuer->pid);
525 xbt_dict_remove(first_enabled_state, key);
529 if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
530 if(req->call == SIMCALL_COMM_ISEND)
532 else if(req->call == SIMCALL_COMM_IRECV)
536 /* Answer the request */
537 SIMIX_simcall_pre(req, value); /* After this call req is no longer usefull */
539 if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
541 if(comm_pattern != 0){
542 if(!initial_state_safety->initial_communications_pattern_done)
543 get_comm_pattern(initial_communications_pattern, req, comm_pattern);
545 get_comm_pattern(communications_pattern, req, comm_pattern);
551 /* Wait for requests (schedules processes) */
552 MC_wait_for_requests();
554 /* Create the new expanded state */
557 next_state = MC_state_new();
559 if((visited_state = is_visited_state()) == -1){
561 /* Get an enabled process and insert it in the interleave set of the next state */
562 xbt_swag_foreach(process, simix_global->process_list){
563 if(MC_process_is_enabled(process)){
564 MC_state_interleave_process(next_state, process);
565 if(mc_reduce_kind != e_mc_reduce_none)
570 if(_sg_mc_checkpoint && ((xbt_fifo_size(mc_stack_safety) + 1) % _sg_mc_checkpoint == 0)){
571 next_state->system_state = MC_take_snapshot(next_state->num);
574 if(dot_output != NULL)
575 fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str);
579 if(dot_output != NULL)
580 fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visited_state, req_str);
584 xbt_fifo_unshift(mc_stack_safety, next_state);
586 /* Insert in dict all enabled processes, if not included yet */
587 xbt_swag_foreach(process, simix_global->process_list){
588 if(MC_process_is_enabled(process)){
589 char *key = bprintf("%lu", process->pid);
590 if(xbt_dict_get_or_null(first_enabled_state, key) == NULL){
591 char *data = bprintf("%d", xbt_fifo_size(mc_stack_safety));
592 xbt_dict_set(first_enabled_state, key, data, NULL);
598 if(dot_output != NULL)
603 /* Let's loop again */
605 /* The interleave set is empty or the maximum depth is reached, let's back-track */
608 if((xbt_fifo_size(mc_stack_safety) > _sg_mc_max_depth) || user_max_depth_reached || visited_state != -1){
610 if(user_max_depth_reached && visited_state == -1)
611 XBT_DEBUG("User max depth reached !");
612 else if(visited_state == -1)
613 XBT_WARN("/!\\ Max depth reached ! /!\\ ");
617 /* Interleave enabled processes in the state in which they have been enabled for the first time */
618 xbt_swag_foreach(process, simix_global->process_list){
619 if(MC_process_is_enabled(process)){
620 char *key = bprintf("%lu", process->pid);
621 enabled = (int)strtoul(xbt_dict_get_or_null(first_enabled_state, key), 0, 10);
623 int cursor = xbt_fifo_size(mc_stack_safety);
624 xbt_fifo_foreach(mc_stack_safety, item, state_test, mc_state_t){
625 if(cursor-- == enabled){
626 if(!MC_state_process_is_done(state_test, process) && state_test->num != state->num){
627 XBT_DEBUG("Interleave process %lu in state %d", process->pid, state_test->num);
628 MC_state_interleave_process(state_test, process);
638 XBT_DEBUG("There are no more processes to interleave. (depth %d)", xbt_fifo_size(mc_stack_safety) + 1);
644 if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
645 if(initial_state_safety->initial_communications_pattern_done){
646 if(interleave_size == 0){ /* if (interleave_size > 0), process interleaved but not enabled => "incorrect" path, determinism not evaluated */
647 //print_communications_pattern(communications_pattern);
648 deterministic_pattern(initial_communications_pattern, communications_pattern);
649 if(initial_state_safety->comm_deterministic == 0 && _sg_mc_comms_determinism){
650 XBT_INFO("****************************************************");
651 XBT_INFO("***** Non-deterministic communications pattern *****");
652 XBT_INFO("****************************************************");
653 XBT_INFO("Initial communications pattern:");
654 print_communications_pattern(initial_communications_pattern);
655 XBT_INFO("Communications pattern counter-example:");
656 print_communications_pattern(communications_pattern);
657 MC_print_statistics(mc_stats);
659 }else if(initial_state_safety->send_deterministic == 0 && _sg_mc_send_determinism){
660 XBT_INFO("****************************************************");
661 XBT_INFO("***** Non-send-deterministic communications pattern *****");
662 XBT_INFO("****************************************************");
663 XBT_INFO("Initial communications pattern:");
664 print_communications_pattern(initial_communications_pattern);
665 XBT_INFO("Communications pattern counter-example:");
666 print_communications_pattern(communications_pattern);
667 MC_print_statistics(mc_stats);
672 initial_state_safety->initial_communications_pattern_done = 1;
676 /* Trash the current state, no longer needed */
677 xbt_fifo_shift(mc_stack_safety);
678 MC_state_delete(state);
679 XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1);
683 /* Check for deadlocks */
684 if(MC_deadlock_check()){
685 MC_show_deadlock(NULL);
690 /* Traverse the stack backwards until a state with a non empty interleave
691 set is found, deleting all the states that have it empty in the way.
692 For each deleted state, check if the request that has generated it
693 (from it's predecesor state), depends on any other previous request
694 executed before it. If it does then add it to the interleave set of the
695 state that executed that previous request. */
697 while ((state = xbt_fifo_shift(mc_stack_safety)) != NULL) {
698 if(mc_reduce_kind != e_mc_reduce_none){
699 req = MC_state_get_internal_request(state);
700 xbt_fifo_foreach(mc_stack_safety, item, prev_state, mc_state_t) {
701 if(MC_request_depend(req, MC_state_get_internal_request(prev_state))){
702 if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
703 XBT_DEBUG("Dependent Transitions:");
704 prev_req = MC_state_get_executed_request(prev_state, &value);
705 req_str = MC_request_to_string(prev_req, value);
706 XBT_DEBUG("%s (state=%d)", req_str, prev_state->num);
708 prev_req = MC_state_get_executed_request(state, &value);
709 req_str = MC_request_to_string(prev_req, value);
710 XBT_DEBUG("%s (state=%d)", req_str, state->num);
714 if(!MC_state_process_is_done(prev_state, req->issuer))
715 MC_state_interleave_process(prev_state, req->issuer);
717 XBT_DEBUG("Process %p is in done set", req->issuer);
721 }else if(req->issuer == MC_state_get_internal_request(prev_state)->issuer){
723 XBT_DEBUG("Simcall %d and %d with same issuer", req->call, MC_state_get_internal_request(prev_state)->call);
728 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);
734 if (MC_state_interleave_size(state) && xbt_fifo_size(mc_stack_safety) < _sg_mc_max_depth) {
735 /* We found a back-tracking point, let's loop */
736 XBT_DEBUG("Back-tracking to state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1);
737 if(_sg_mc_checkpoint){
738 if(state->system_state != NULL){
739 MC_restore_snapshot(state->system_state);
740 xbt_fifo_unshift(mc_stack_safety, state);
743 pos = xbt_fifo_size(mc_stack_safety);
744 item = xbt_fifo_get_first_item(mc_stack_safety);
746 restored_state = (mc_state_t) xbt_fifo_get_item_content(item);
747 if(restored_state->system_state != NULL){
750 item = xbt_fifo_get_next_item(item);
754 MC_restore_snapshot(restored_state->system_state);
755 xbt_fifo_unshift(mc_stack_safety, state);
757 MC_replay(mc_stack_safety, pos);
760 xbt_fifo_unshift(mc_stack_safety, state);
762 MC_replay(mc_stack_safety, -1);
764 XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num, xbt_fifo_size(mc_stack_safety));
767 req = MC_state_get_internal_request(state);
768 if(_sg_mc_comms_determinism){
769 if(req->call == SIMCALL_COMM_ISEND || req->call == SIMCALL_COMM_IRECV){
770 if(!xbt_dynar_is_empty(communications_pattern))
771 xbt_dynar_remove_at(communications_pattern, xbt_dynar_length(communications_pattern) - 1, NULL);
774 XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1);
775 MC_state_delete(state);
781 MC_print_statistics(mc_stats);