1 /* Copyright (c) 2008-2013. 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("[(%d) %s -> %s] %s ", current_comm->src_proc, current_comm->src_host, current_comm->dst_host, "iSend");
167 XBT_INFO("[(%d) %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){
218 int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
222 int cursor = 0, previous_cursor, next_cursor;
223 mc_visited_state_t state_test;
225 int end = xbt_dynar_length(all_states) - 1;
228 cursor = (start + end) / 2;
229 state_test = (mc_visited_state_t)xbt_dynar_get_as(all_states, cursor, mc_visited_state_t);
230 if(state_test->nb_processes < state->nb_processes){
232 }else if(state_test->nb_processes > state->nb_processes){
235 if(state_test->heap_bytes_used < state->heap_bytes_used){
237 }else if(state_test->heap_bytes_used > state->heap_bytes_used){
240 *min = *max = cursor;
241 previous_cursor = cursor - 1;
242 while(previous_cursor >= 0){
243 state_test = (mc_visited_state_t)xbt_dynar_get_as(all_states, previous_cursor, mc_visited_state_t);
244 if(state_test->nb_processes != state->nb_processes || state_test->heap_bytes_used != state->heap_bytes_used)
246 *min = previous_cursor;
249 next_cursor = cursor + 1;
250 while(next_cursor < xbt_dynar_length(all_states)){
251 state_test = (mc_visited_state_t)xbt_dynar_get_as(all_states, next_cursor, mc_visited_state_t);
252 if(state_test->nb_processes != state->nb_processes || state_test->heap_bytes_used != state->heap_bytes_used)
270 /** \brief Take a snapshot the current state and process it.
272 * \return number of the duplicate state or -1 (not visited)
274 static int is_visited_state(){
276 if(_sg_mc_visited == 0)
279 int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
283 mc_visited_state_t new_state = visited_state_new();
285 if(xbt_dynar_is_empty(visited_states)){
287 xbt_dynar_push(visited_states, &new_state);
296 int min = -1, max = -1, index;
298 mc_visited_state_t state_test;
301 index = get_search_interval(visited_states, new_state, &min, &max);
303 if(min != -1 && max != -1){
305 // Parallell implementation
306 /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_states, min), (max-min)+1, new_state);
308 state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, (min+res)-1, mc_visited_state_t);
309 if(state_test->other_num == -1)
310 new_state->other_num = state_test->num;
312 new_state->other_num = state_test->other_num;
313 if(dot_output == NULL)
314 XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
316 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);
317 xbt_dynar_remove_at(visited_states, (min + res) - 1, NULL);
318 xbt_dynar_insert_at(visited_states, (min+res) - 1, &new_state);
321 return new_state->other_num;
325 while(cursor <= max){
326 state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, cursor, mc_visited_state_t);
327 if(snapshot_compare(state_test, new_state) == 0){
328 // The state has been visited:
330 if(state_test->other_num == -1)
331 new_state->other_num = state_test->num;
333 new_state->other_num = state_test->other_num;
334 if(dot_output == NULL)
335 XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
337 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);
339 // Replace the old state with the new one (why?):
340 xbt_dynar_remove_at(visited_states, cursor, NULL);
341 xbt_dynar_insert_at(visited_states, cursor, &new_state);
345 return new_state->other_num;
350 // The state has not been visited, add it to the list:
351 xbt_dynar_insert_at(visited_states, min, &new_state);
355 // The state has not been visited: insert the state in the dynamic array.
356 state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, index, mc_visited_state_t);
357 if(state_test->nb_processes < new_state->nb_processes){
358 xbt_dynar_insert_at(visited_states, index+1, &new_state);
360 if(state_test->heap_bytes_used < new_state->heap_bytes_used)
361 xbt_dynar_insert_at(visited_states, index + 1, &new_state);
363 xbt_dynar_insert_at(visited_states, index, &new_state);
368 // We have reached the maximum number of stored states;
369 if(xbt_dynar_length(visited_states) > _sg_mc_visited){
371 // Find the (index of the) older state:
372 int min2 = mc_stats->expanded_states;
373 unsigned int cursor2 = 0;
374 unsigned int index2 = 0;
375 xbt_dynar_foreach(visited_states, cursor2, state_test){
376 if(state_test->num < min2){
378 min2 = state_test->num;
383 xbt_dynar_remove_at(visited_states, index2, NULL);
395 * \brief Initialize the DPOR exploration algorithm
400 int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
402 mc_state_t initial_state = NULL;
403 smx_process_t process;
405 /* Create the initial state and push it into the exploration stack */
408 if(_sg_mc_visited > 0)
409 visited_states = xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp);
411 first_enabled_state = xbt_dict_new_homogeneous(&xbt_free_f);
413 initial_communications_pattern = xbt_dynar_new(sizeof(mc_comm_pattern_t), comm_pattern_free_voidp);
414 communications_pattern = xbt_dynar_new(sizeof(mc_comm_pattern_t), comm_pattern_free_voidp);
417 initial_state = MC_state_new();
421 XBT_DEBUG("**************************************************");
422 XBT_DEBUG("Initial state");
424 /* Wait for requests (schedules processes) */
425 MC_wait_for_requests();
427 MC_ignore_heap(simix_global->process_to_run->data, 0);
428 MC_ignore_heap(simix_global->process_that_ran->data, 0);
432 /* Get an enabled process and insert it in the interleave set of the initial state */
433 xbt_swag_foreach(process, simix_global->process_list){
434 if(MC_process_is_enabled(process)){
435 MC_state_interleave_process(initial_state, process);
436 if(mc_reduce_kind != e_mc_reduce_none)
441 xbt_fifo_unshift(mc_stack_safety, initial_state);
443 /* To ensure the soundness of DPOR, we have to keep a list of
444 processes which are still enabled at each step of the exploration.
445 If max depth is reached, we interleave them in the state in which they have
446 been enabled for the first time. */
447 xbt_swag_foreach(process, simix_global->process_list){
448 if(MC_process_is_enabled(process)){
449 char *key = bprintf("%lu", process->pid);
450 char *data = bprintf("%d", xbt_fifo_size(mc_stack_safety));
451 xbt_dict_set(first_enabled_state, key, data, NULL);
466 /** \brief Model-check the application using a DFS exploration
467 * with DPOR (Dynamic Partial Order Reductions)
472 char *req_str = NULL;
474 smx_simcall_t req = NULL, prev_req = NULL;
475 mc_state_t state = NULL, prev_state = NULL, next_state = NULL, restored_state=NULL;
476 smx_process_t process = NULL;
477 xbt_fifo_item_t item = NULL;
478 mc_state_t state_test = NULL;
480 int visited_state = -1;
482 int interleave_size = 0;
483 int comm_pattern = 0;
485 while (xbt_fifo_size(mc_stack_safety) > 0) {
487 /* Get current state */
489 xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_safety));
491 XBT_DEBUG("**************************************************");
492 XBT_DEBUG("Exploration depth=%d (state=%p, num %d)(%u interleave, user_max_depth %d, first_enabled_state size : %d)",
493 xbt_fifo_size(mc_stack_safety), state, state->num,
494 MC_state_interleave_size(state), user_max_depth_reached, xbt_dict_size(first_enabled_state));
496 interleave_size = MC_state_interleave_size(state);
498 /* Update statistics */
499 mc_stats->visited_states++;
501 /* If there are processes to interleave and the maximum depth has not been reached
502 then perform one step of the exploration algorithm */
503 if (xbt_fifo_size(mc_stack_safety) <= _sg_mc_max_depth && !user_max_depth_reached &&
504 (req = MC_state_get_request(state, &value)) && visited_state == -1) {
506 /* Debug information */
507 if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
508 req_str = MC_request_to_string(req, value);
509 XBT_DEBUG("Execute: %s", req_str);
514 if(dot_output != NULL)
515 req_str = MC_request_get_dot_output(req, value);
518 MC_state_set_executed_request(state, req, value);
519 mc_stats->executed_transitions++;
522 char *key = bprintf("%lu", req->issuer->pid);
523 xbt_dict_remove(first_enabled_state, key);
527 if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
528 if(req->call == SIMCALL_COMM_ISEND)
530 else if(req->call == SIMCALL_COMM_IRECV)
534 /* Answer the request */
535 SIMIX_simcall_pre(req, value); /* After this call req is no longer usefull */
537 if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
539 if(comm_pattern != 0){
540 if(!initial_state_safety->initial_communications_pattern_done)
541 get_comm_pattern(initial_communications_pattern, req, comm_pattern);
543 get_comm_pattern(communications_pattern, req, comm_pattern);
549 /* Wait for requests (schedules processes) */
550 MC_wait_for_requests();
552 /* Create the new expanded state */
555 next_state = MC_state_new();
557 if((visited_state = is_visited_state()) == -1){
559 /* Get an enabled process and insert it in the interleave set of the next state */
560 xbt_swag_foreach(process, simix_global->process_list){
561 if(MC_process_is_enabled(process)){
562 MC_state_interleave_process(next_state, process);
563 if(mc_reduce_kind != e_mc_reduce_none)
568 if(_sg_mc_checkpoint && ((xbt_fifo_size(mc_stack_safety) + 1) % _sg_mc_checkpoint == 0)){
569 next_state->system_state = MC_take_snapshot(next_state->num);
572 if(dot_output != NULL)
573 fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str);
577 if(dot_output != NULL)
578 fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visited_state, req_str);
582 xbt_fifo_unshift(mc_stack_safety, next_state);
584 /* Insert in dict all enabled processes, if not included yet */
585 xbt_swag_foreach(process, simix_global->process_list){
586 if(MC_process_is_enabled(process)){
587 char *key = bprintf("%lu", process->pid);
588 if(xbt_dict_get_or_null(first_enabled_state, key) == NULL){
589 char *data = bprintf("%d", xbt_fifo_size(mc_stack_safety));
590 xbt_dict_set(first_enabled_state, key, data, NULL);
596 if(dot_output != NULL)
601 /* Let's loop again */
603 /* The interleave set is empty or the maximum depth is reached, let's back-track */
606 if((xbt_fifo_size(mc_stack_safety) > _sg_mc_max_depth) || user_max_depth_reached || visited_state != -1){
608 if(user_max_depth_reached && visited_state == -1)
609 XBT_DEBUG("User max depth reached !");
610 else if(visited_state == -1)
611 XBT_WARN("/!\\ Max depth reached ! /!\\ ");
615 /* Interleave enabled processes in the state in which they have been enabled for the first time */
616 xbt_swag_foreach(process, simix_global->process_list){
617 if(MC_process_is_enabled(process)){
618 char *key = bprintf("%lu", process->pid);
619 enabled = (int)strtoul(xbt_dict_get_or_null(first_enabled_state, key), 0, 10);
621 int cursor = xbt_fifo_size(mc_stack_safety);
622 xbt_fifo_foreach(mc_stack_safety, item, state_test, mc_state_t){
623 if(cursor-- == enabled){
624 if(!MC_state_process_is_done(state_test, process) && state_test->num != state->num){
625 XBT_DEBUG("Interleave process %lu in state %d", process->pid, state_test->num);
626 MC_state_interleave_process(state_test, process);
636 XBT_DEBUG("There are no more processes to interleave. (depth %d)", xbt_fifo_size(mc_stack_safety) + 1);
642 if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
643 if(initial_state_safety->initial_communications_pattern_done){
644 if(interleave_size == 0){ /* if (interleave_size > 0), process interleaved but not enabled => "incorrect" path, determinism not evaluated */
645 //print_communications_pattern(communications_pattern);
646 deterministic_pattern(initial_communications_pattern, communications_pattern);
647 if(initial_state_safety->comm_deterministic == 0 && _sg_mc_comms_determinism){
648 XBT_INFO("****************************************************");
649 XBT_INFO("***** Non-deterministic communications pattern *****");
650 XBT_INFO("****************************************************");
651 XBT_INFO("Initial communications pattern:");
652 print_communications_pattern(initial_communications_pattern);
653 XBT_INFO("Communications pattern counter-example:");
654 print_communications_pattern(communications_pattern);
655 MC_print_statistics(mc_stats);
657 }else if(initial_state_safety->send_deterministic == 0 && _sg_mc_send_determinism){
658 XBT_INFO("****************************************************");
659 XBT_INFO("***** Non-send-deterministic communications pattern *****");
660 XBT_INFO("****************************************************");
661 XBT_INFO("Initial communications pattern:");
662 print_communications_pattern(initial_communications_pattern);
663 XBT_INFO("Communications pattern counter-example:");
664 print_communications_pattern(communications_pattern);
665 MC_print_statistics(mc_stats);
670 initial_state_safety->initial_communications_pattern_done = 1;
674 /* Trash the current state, no longer needed */
675 xbt_fifo_shift(mc_stack_safety);
676 MC_state_delete(state);
677 XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1);
681 /* Check for deadlocks */
682 if(MC_deadlock_check()){
683 MC_show_deadlock(NULL);
688 /* Traverse the stack backwards until a state with a non empty interleave
689 set is found, deleting all the states that have it empty in the way.
690 For each deleted state, check if the request that has generated it
691 (from it's predecesor state), depends on any other previous request
692 executed before it. If it does then add it to the interleave set of the
693 state that executed that previous request. */
695 while ((state = xbt_fifo_shift(mc_stack_safety)) != NULL) {
696 if(mc_reduce_kind != e_mc_reduce_none){
697 req = MC_state_get_internal_request(state);
698 xbt_fifo_foreach(mc_stack_safety, item, prev_state, mc_state_t) {
699 if(MC_request_depend(req, MC_state_get_internal_request(prev_state))){
700 if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
701 XBT_DEBUG("Dependent Transitions:");
702 prev_req = MC_state_get_executed_request(prev_state, &value);
703 req_str = MC_request_to_string(prev_req, value);
704 XBT_DEBUG("%s (state=%d)", req_str, prev_state->num);
706 prev_req = MC_state_get_executed_request(state, &value);
707 req_str = MC_request_to_string(prev_req, value);
708 XBT_DEBUG("%s (state=%d)", req_str, state->num);
712 if(!MC_state_process_is_done(prev_state, req->issuer))
713 MC_state_interleave_process(prev_state, req->issuer);
715 XBT_DEBUG("Process %p is in done set", req->issuer);
719 }else if(req->issuer == MC_state_get_internal_request(prev_state)->issuer){
721 XBT_DEBUG("Simcall %d and %d with same issuer", req->call, MC_state_get_internal_request(prev_state)->call);
726 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);
732 if (MC_state_interleave_size(state) && xbt_fifo_size(mc_stack_safety) < _sg_mc_max_depth) {
733 /* We found a back-tracking point, let's loop */
734 XBT_DEBUG("Back-tracking to state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1);
735 if(_sg_mc_checkpoint){
736 if(state->system_state != NULL){
737 MC_restore_snapshot(state->system_state);
738 xbt_fifo_unshift(mc_stack_safety, state);
741 pos = xbt_fifo_size(mc_stack_safety);
742 item = xbt_fifo_get_first_item(mc_stack_safety);
744 restored_state = (mc_state_t) xbt_fifo_get_item_content(item);
745 if(restored_state->system_state != NULL){
748 item = xbt_fifo_get_next_item(item);
752 MC_restore_snapshot(restored_state->system_state);
753 xbt_fifo_unshift(mc_stack_safety, state);
755 MC_replay(mc_stack_safety, pos);
758 xbt_fifo_unshift(mc_stack_safety, state);
760 MC_replay(mc_stack_safety, -1);
762 XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num, xbt_fifo_size(mc_stack_safety));
765 req = MC_state_get_internal_request(state);
766 if(_sg_mc_comms_determinism){
767 if(req->call == SIMCALL_COMM_ISEND || req->call == SIMCALL_COMM_IRECV){
768 if(!xbt_dynar_is_empty(communications_pattern))
769 xbt_dynar_remove_at(communications_pattern, xbt_dynar_length(communications_pattern) - 1, NULL);
772 XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1);
773 MC_state_delete(state);
779 MC_print_statistics(mc_stats);