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 incomplete_communications_pattern;
18 xbt_dynar_t communications_pattern;
21 /********** Static functions ***********/
23 static void comm_pattern_free(mc_comm_pattern_t p){
30 static void comm_pattern_free_voidp( void *p){
31 comm_pattern_free((mc_comm_pattern_t) * (void **)p);
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)
41 }else if(current_comm->type == type && type == SIMIX_COMM_RECEIVE){
42 if(current_comm->dst_proc == proc)
50 static int compare_comm_pattern(mc_comm_pattern_t comm1, mc_comm_pattern_t comm2){
51 if(strcmp(comm1->rdv, comm2->rdv) != 0)
53 if(comm1->src_proc != comm2->src_proc)
55 if(comm1->dst_proc != comm2->dst_proc)
57 if(comm1->data_size != comm2->data_size)
59 if(memcmp(comm1->data, comm2->data, comm1->data_size) != 0)
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;
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)
100 void complete_comm_pattern(xbt_dynar_t list, smx_action_t comm){
101 mc_comm_pattern_t current_pattern;
102 unsigned int cursor = 0;
105 xbt_dynar_foreach(incomplete_communications_pattern, cursor, index){
106 current_pattern = (mc_comm_pattern_t)xbt_dynar_get_as(list, index, mc_comm_pattern_t);
107 if(current_pattern->comm == comm){
108 current_pattern->src_proc = comm->comm.src_proc->pid;
109 current_pattern->dst_proc = comm->comm.dst_proc->pid;
110 current_pattern->src_host = simcall_host_get_name(comm->comm.src_proc->smx_host);
111 current_pattern->dst_host = simcall_host_get_name(comm->comm.dst_proc->smx_host);
112 if(current_pattern->data_size == -1){
113 current_pattern->data_size = *(comm->comm.dst_buff_size);
114 current_pattern->data = xbt_malloc0(current_pattern->data_size);
115 memcpy(current_pattern->data, current_pattern->comm->comm.dst_buff, current_pattern->data_size);
117 xbt_dynar_remove_at(incomplete_communications_pattern, cursor, NULL);
126 void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, int call){
127 mc_comm_pattern_t pattern = NULL;
128 pattern = xbt_new0(s_mc_comm_pattern_t, 1);
129 pattern->num = ++nb_comm_pattern;
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 pattern->src_proc = pattern->comm->comm.src_proc->pid;
135 pattern->src_host = simcall_host_get_name(request->issuer->smx_host);
136 pattern->data_size = pattern->comm->comm.src_buff_size;
137 pattern->data=xbt_malloc0(pattern->data_size);
138 memcpy(pattern->data, pattern->comm->comm.src_buff, pattern->data_size);
140 pattern->comm = simcall_comm_irecv__get__result(request);
141 pattern->type = SIMIX_COMM_RECEIVE;
142 pattern->dst_proc = pattern->comm->comm.dst_proc->pid;
143 pattern->dst_host = simcall_host_get_name(pattern->comm->comm.dst_proc->smx_host);
146 if(pattern->comm->comm.rdv != NULL)
147 pattern->rdv = strdup(pattern->comm->comm.rdv->name);
149 pattern->rdv = strdup(pattern->comm->comm.rdv_cpy->name);
151 xbt_dynar_push(list, &pattern);
153 xbt_dynar_push_as(incomplete_communications_pattern, int, xbt_dynar_length(list) - 1);
157 static void print_communications_pattern(xbt_dynar_t comms_pattern){
158 unsigned int cursor = 0;
159 mc_comm_pattern_t current_comm;
160 xbt_dynar_foreach(comms_pattern, cursor, current_comm){
161 if(current_comm->type == SIMIX_COMM_SEND)
162 XBT_INFO("[(%lu) %s -> (%lu) %s] %s ", current_comm->src_proc, current_comm->src_host, current_comm->dst_proc, current_comm->dst_host, "iSend");
164 XBT_INFO("[(%lu) %s <- (%lu) %s] %s ", current_comm->dst_proc, current_comm->dst_host, current_comm->src_proc, current_comm->src_host, "iRecv");
168 static void visited_state_free(mc_visited_state_t state){
170 MC_free_snapshot(state->system_state);
175 static void visited_state_free_voidp(void *s){
176 visited_state_free((mc_visited_state_t) * (void **) s);
179 /** \brief Save the current state
181 * \return Snapshot of the current state.
183 static mc_visited_state_t visited_state_new(){
185 mc_visited_state_t new_state = NULL;
186 new_state = xbt_new0(s_mc_visited_state_t, 1);
187 new_state->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
188 new_state->nb_processes = xbt_swag_size(simix_global->process_list);
189 new_state->system_state = MC_take_snapshot(mc_stats->expanded_states);
190 new_state->num = mc_stats->expanded_states;
191 new_state->other_num = -1;
197 /** \brief Find a suitable subrange of candidate duplicates for a given state
199 * \param all_ pairs dynamic array of states with candidate duplicates of the current state;
200 * \param pair current state;
201 * \param min (output) index of the beginning of the the subrange
202 * \param max (output) index of the enf of the subrange
204 * Given a suitably ordered array of state, this function extracts a subrange
205 * (with index *min <= i <= *max) with candidate duplicates of the given state.
206 * This function uses only fast discriminating criterions and does not use the
207 * full state comparison algorithms.
209 * The states in all_pairs MUST be ordered using a (given) weak order
210 * (based on nb_processes and heap_bytes_used).
211 * The subrange is the subrange of "equivalence" of the given state.
213 static int get_search_interval(xbt_dynar_t all_states, mc_visited_state_t state, int *min, int *max){
214 XBT_VERB("Searching interval for state %i: nd_processes=%zu heap_bytes_used=%zu",
215 state->num, (size_t)state->nb_processes, (size_t)state->heap_bytes_used);
217 int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
221 int cursor = 0, previous_cursor, next_cursor;
222 mc_visited_state_t state_test;
224 int end = xbt_dynar_length(all_states) - 1;
227 cursor = (start + end) / 2;
228 state_test = (mc_visited_state_t)xbt_dynar_get_as(all_states, cursor, mc_visited_state_t);
229 if(state_test->nb_processes < state->nb_processes){
231 }else if(state_test->nb_processes > state->nb_processes){
234 if(state_test->heap_bytes_used < state->heap_bytes_used){
236 }else if(state_test->heap_bytes_used > state->heap_bytes_used){
239 *min = *max = cursor;
240 previous_cursor = cursor - 1;
241 while(previous_cursor >= 0){
242 state_test = (mc_visited_state_t)xbt_dynar_get_as(all_states, previous_cursor, mc_visited_state_t);
243 if(state_test->nb_processes != state->nb_processes || state_test->heap_bytes_used != state->heap_bytes_used)
245 *min = previous_cursor;
248 next_cursor = cursor + 1;
249 while(next_cursor < xbt_dynar_length(all_states)){
250 state_test = (mc_visited_state_t)xbt_dynar_get_as(all_states, next_cursor, mc_visited_state_t);
251 if(state_test->nb_processes != state->nb_processes || state_test->heap_bytes_used != state->heap_bytes_used)
269 /** \brief Take a snapshot the current state and process it.
271 * \return number of the duplicate state or -1 (not visited)
273 static int is_visited_state(){
275 if(_sg_mc_visited == 0)
278 int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
282 mc_visited_state_t new_state = visited_state_new();
284 if(xbt_dynar_is_empty(visited_states)){
286 xbt_dynar_push(visited_states, &new_state);
295 int min = -1, max = -1, index;
297 mc_visited_state_t state_test;
300 index = get_search_interval(visited_states, new_state, &min, &max);
302 if(min != -1 && max != -1){
304 // Parallell implementation
305 /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_states, min), (max-min)+1, new_state);
307 state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, (min+res)-1, mc_visited_state_t);
308 if(state_test->other_num == -1)
309 new_state->other_num = state_test->num;
311 new_state->other_num = state_test->other_num;
312 if(dot_output == NULL)
313 XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
315 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);
316 xbt_dynar_remove_at(visited_states, (min + res) - 1, NULL);
317 xbt_dynar_insert_at(visited_states, (min+res) - 1, &new_state);
320 return new_state->other_num;
324 while(cursor <= max){
325 state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, cursor, mc_visited_state_t);
326 if(snapshot_compare(state_test, new_state) == 0){
327 // The state has been visited:
329 if(state_test->other_num == -1)
330 new_state->other_num = state_test->num;
332 new_state->other_num = state_test->other_num;
333 if(dot_output == NULL)
334 XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
336 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);
338 // Replace the old state with the new one (why?):
339 xbt_dynar_remove_at(visited_states, cursor, NULL);
340 xbt_dynar_insert_at(visited_states, cursor, &new_state);
344 return new_state->other_num;
349 // The state has not been visited, add it to the list:
350 xbt_dynar_insert_at(visited_states, min, &new_state);
354 // The state has not been visited: insert the state in the dynamic array.
355 state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, index, mc_visited_state_t);
356 if(state_test->nb_processes < new_state->nb_processes){
357 xbt_dynar_insert_at(visited_states, index+1, &new_state);
359 if(state_test->heap_bytes_used < new_state->heap_bytes_used)
360 xbt_dynar_insert_at(visited_states, index + 1, &new_state);
362 xbt_dynar_insert_at(visited_states, index, &new_state);
367 // We have reached the maximum number of stored states;
368 if(xbt_dynar_length(visited_states) > _sg_mc_visited){
370 // Find the (index of the) older state:
371 int min2 = mc_stats->expanded_states;
372 unsigned int cursor2 = 0;
373 unsigned int index2 = 0;
374 xbt_dynar_foreach(visited_states, cursor2, state_test){
375 if(state_test->num < min2){
377 min2 = state_test->num;
382 xbt_dynar_remove_at(visited_states, index2, NULL);
394 * \brief Initialize the DPOR exploration algorithm
399 int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
401 mc_state_t initial_state = NULL;
402 smx_process_t process;
404 /* Create the initial state and push it into the exploration stack */
407 if(_sg_mc_visited > 0)
408 visited_states = xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp);
410 if(mc_reduce_kind == e_mc_reduce_dpor)
411 first_enabled_state = xbt_dict_new_homogeneous(&xbt_free_f);
413 if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
414 initial_communications_pattern = xbt_dynar_new(sizeof(mc_comm_pattern_t), comm_pattern_free_voidp);
415 communications_pattern = xbt_dynar_new(sizeof(mc_comm_pattern_t), comm_pattern_free_voidp);
416 incomplete_communications_pattern = xbt_dynar_new(sizeof(int), NULL);
420 initial_state = MC_state_new();
424 XBT_DEBUG("**************************************************");
425 XBT_DEBUG("Initial state");
427 /* Wait for requests (schedules processes) */
428 MC_wait_for_requests();
430 MC_ignore_heap(simix_global->process_to_run->data, 0);
431 MC_ignore_heap(simix_global->process_that_ran->data, 0);
435 /* Get an enabled process and insert it in the interleave set of the initial state */
436 xbt_swag_foreach(process, simix_global->process_list){
437 if(MC_process_is_enabled(process)){
438 MC_state_interleave_process(initial_state, process);
439 if(mc_reduce_kind != e_mc_reduce_none)
444 xbt_fifo_unshift(mc_stack_safety, initial_state);
446 if(mc_reduce_kind == e_mc_reduce_dpor){
447 /* To ensure the soundness of DPOR, we have to keep a list of
448 processes which are still enabled at each step of the exploration.
449 If max depth is reached, we interleave them in the state in which they have
450 been enabled for the first time. */
451 xbt_swag_foreach(process, simix_global->process_list){
452 if(MC_process_is_enabled(process)){
453 char *key = bprintf("%lu", process->pid);
454 char *data = bprintf("%d", xbt_fifo_size(mc_stack_safety));
455 xbt_dict_set(first_enabled_state, key, data, NULL);
471 /** \brief Model-check the application using a DFS exploration
472 * with DPOR (Dynamic Partial Order Reductions)
477 char *req_str = NULL;
479 smx_simcall_t req = NULL, prev_req = NULL;
480 mc_state_t state = NULL, prev_state = NULL, next_state = NULL, restored_state=NULL;
481 smx_process_t process = NULL;
482 xbt_fifo_item_t item = NULL;
483 mc_state_t state_test = NULL;
485 int visited_state = -1;
487 int interleave_size = 0;
488 int comm_pattern = 0;
490 while (xbt_fifo_size(mc_stack_safety) > 0) {
492 /* Get current state */
494 xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_safety));
496 XBT_DEBUG("**************************************************");
497 XBT_DEBUG("Exploration depth=%d (state=%p, num %d)(%u interleave, user_max_depth %d, first_enabled_state size : %d)",
498 xbt_fifo_size(mc_stack_safety), state, state->num,
499 MC_state_interleave_size(state), user_max_depth_reached, xbt_dict_size(first_enabled_state));
501 interleave_size = MC_state_interleave_size(state);
503 /* Update statistics */
504 mc_stats->visited_states++;
506 /* If there are processes to interleave and the maximum depth has not been reached
507 then perform one step of the exploration algorithm */
508 if (xbt_fifo_size(mc_stack_safety) <= _sg_mc_max_depth && !user_max_depth_reached &&
509 (req = MC_state_get_request(state, &value)) && visited_state == -1) {
511 /* Debug information */
512 if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
513 req_str = MC_request_to_string(req, value);
514 XBT_DEBUG("Execute: %s", req_str);
519 if(dot_output != NULL)
520 req_str = MC_request_get_dot_output(req, value);
523 MC_state_set_executed_request(state, req, value);
524 mc_stats->executed_transitions++;
526 if(mc_reduce_kind == e_mc_reduce_dpor){
528 char *key = bprintf("%lu", req->issuer->pid);
529 xbt_dict_remove(first_enabled_state, key);
534 if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
535 if(req->call == SIMCALL_COMM_ISEND)
537 else if(req->call == SIMCALL_COMM_IRECV)
539 else if(req->call == SIMCALL_COMM_WAIT)
543 /* Answer the request */
544 SIMIX_simcall_pre(req, value); /* After this call req is no longer usefull */
546 if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
548 if(comm_pattern == 1 || comm_pattern == 2){
549 if(!initial_state_safety->initial_communications_pattern_done)
550 get_comm_pattern(initial_communications_pattern, req, comm_pattern);
552 get_comm_pattern(communications_pattern, req, comm_pattern);
553 }else if(comm_pattern == 3){
554 if(!initial_state_safety->initial_communications_pattern_done)
555 complete_comm_pattern(initial_communications_pattern, simcall_comm_wait__get__comm(req));
557 complete_comm_pattern(communications_pattern, simcall_comm_wait__get__comm(req));
563 /* Wait for requests (schedules processes) */
564 MC_wait_for_requests();
566 /* Create the new expanded state */
569 next_state = MC_state_new();
571 if((visited_state = is_visited_state()) == -1){
573 /* Get an enabled process and insert it in the interleave set of the next state */
574 xbt_swag_foreach(process, simix_global->process_list){
575 if(MC_process_is_enabled(process)){
576 MC_state_interleave_process(next_state, process);
577 if(mc_reduce_kind != e_mc_reduce_none)
582 if(_sg_mc_checkpoint && ((xbt_fifo_size(mc_stack_safety) + 1) % _sg_mc_checkpoint == 0)){
583 next_state->system_state = MC_take_snapshot(next_state->num);
586 if(dot_output != NULL)
587 fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str);
591 if(dot_output != NULL)
592 fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visited_state, req_str);
596 xbt_fifo_unshift(mc_stack_safety, next_state);
598 if(mc_reduce_kind == e_mc_reduce_dpor){
599 /* Insert in dict all enabled processes, if not included yet */
600 xbt_swag_foreach(process, simix_global->process_list){
601 if(MC_process_is_enabled(process)){
602 char *key = bprintf("%lu", process->pid);
603 if(xbt_dict_get_or_null(first_enabled_state, key) == NULL){
604 char *data = bprintf("%d", xbt_fifo_size(mc_stack_safety));
605 xbt_dict_set(first_enabled_state, key, data, NULL);
612 if(dot_output != NULL)
617 /* Let's loop again */
619 /* The interleave set is empty or the maximum depth is reached, let's back-track */
622 if((xbt_fifo_size(mc_stack_safety) > _sg_mc_max_depth) || user_max_depth_reached || visited_state != -1){
624 if(user_max_depth_reached && visited_state == -1)
625 XBT_DEBUG("User max depth reached !");
626 else if(visited_state == -1)
627 XBT_WARN("/!\\ Max depth reached ! /!\\ ");
631 if(mc_reduce_kind == e_mc_reduce_dpor){
632 /* Interleave enabled processes in the state in which they have been enabled for the first time */
633 xbt_swag_foreach(process, simix_global->process_list){
634 if(MC_process_is_enabled(process)){
635 char *key = bprintf("%lu", process->pid);
636 enabled = (int)strtoul(xbt_dict_get_or_null(first_enabled_state, key), 0, 10);
638 int cursor = xbt_fifo_size(mc_stack_safety);
639 xbt_fifo_foreach(mc_stack_safety, item, state_test, mc_state_t){
640 if(cursor-- == enabled){
641 if(!MC_state_process_is_done(state_test, process) && state_test->num != state->num){
642 XBT_DEBUG("Interleave process %lu in state %d", process->pid, state_test->num);
643 MC_state_interleave_process(state_test, process);
654 XBT_DEBUG("There are no more processes to interleave. (depth %d)", xbt_fifo_size(mc_stack_safety) + 1);
660 if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
661 if(initial_state_safety->initial_communications_pattern_done){
662 if(interleave_size == 0){ /* if (interleave_size > 0), process interleaved but not enabled => "incorrect" path, determinism not evaluated */
663 //print_communications_pattern(communications_pattern);
664 deterministic_pattern(initial_communications_pattern, communications_pattern);
665 if(initial_state_safety->comm_deterministic == 0 && _sg_mc_comms_determinism){
666 XBT_INFO("****************************************************");
667 XBT_INFO("***** Non-deterministic communications pattern *****");
668 XBT_INFO("****************************************************");
669 XBT_INFO("Initial communications pattern:");
670 print_communications_pattern(initial_communications_pattern);
671 XBT_INFO("Communications pattern counter-example:");
672 print_communications_pattern(communications_pattern);
673 MC_print_statistics(mc_stats);
675 }else if(initial_state_safety->send_deterministic == 0 && _sg_mc_send_determinism){
676 XBT_INFO("****************************************************");
677 XBT_INFO("***** Non-send-deterministic communications pattern *****");
678 XBT_INFO("****************************************************");
679 XBT_INFO("Initial communications pattern:");
680 print_communications_pattern(initial_communications_pattern);
681 XBT_INFO("Communications pattern counter-example:");
682 print_communications_pattern(communications_pattern);
683 MC_print_statistics(mc_stats);
688 initial_state_safety->initial_communications_pattern_done = 1;
692 /* Trash the current state, no longer needed */
693 xbt_fifo_shift(mc_stack_safety);
694 MC_state_delete(state);
695 XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1);
699 /* Check for deadlocks */
700 if(MC_deadlock_check()){
701 MC_show_deadlock(NULL);
706 /* Traverse the stack backwards until a state with a non empty interleave
707 set is found, deleting all the states that have it empty in the way.
708 For each deleted state, check if the request that has generated it
709 (from it's predecesor state), depends on any other previous request
710 executed before it. If it does then add it to the interleave set of the
711 state that executed that previous request. */
713 while ((state = xbt_fifo_shift(mc_stack_safety)) != NULL) {
714 if(mc_reduce_kind == e_mc_reduce_dpor){
715 req = MC_state_get_internal_request(state);
716 xbt_fifo_foreach(mc_stack_safety, item, prev_state, mc_state_t) {
717 if(MC_request_depend(req, MC_state_get_internal_request(prev_state))){
718 if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
719 XBT_DEBUG("Dependent Transitions:");
720 prev_req = MC_state_get_executed_request(prev_state, &value);
721 req_str = MC_request_to_string(prev_req, value);
722 XBT_DEBUG("%s (state=%d)", req_str, prev_state->num);
724 prev_req = MC_state_get_executed_request(state, &value);
725 req_str = MC_request_to_string(prev_req, value);
726 XBT_DEBUG("%s (state=%d)", req_str, state->num);
730 if(!MC_state_process_is_done(prev_state, req->issuer))
731 MC_state_interleave_process(prev_state, req->issuer);
733 XBT_DEBUG("Process %p is in done set", req->issuer);
737 }else if(req->issuer == MC_state_get_internal_request(prev_state)->issuer){
739 XBT_DEBUG("Simcall %d and %d with same issuer", req->call, MC_state_get_internal_request(prev_state)->call);
744 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);
750 if (MC_state_interleave_size(state) && xbt_fifo_size(mc_stack_safety) < _sg_mc_max_depth) {
751 /* We found a back-tracking point, let's loop */
752 XBT_DEBUG("Back-tracking to state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1);
753 if(_sg_mc_checkpoint){
754 if(state->system_state != NULL){
755 MC_restore_snapshot(state->system_state);
756 xbt_fifo_unshift(mc_stack_safety, state);
759 pos = xbt_fifo_size(mc_stack_safety);
760 item = xbt_fifo_get_first_item(mc_stack_safety);
762 restored_state = (mc_state_t) xbt_fifo_get_item_content(item);
763 if(restored_state->system_state != NULL){
766 item = xbt_fifo_get_next_item(item);
770 MC_restore_snapshot(restored_state->system_state);
771 xbt_fifo_unshift(mc_stack_safety, state);
773 MC_replay(mc_stack_safety, pos);
776 xbt_fifo_unshift(mc_stack_safety, state);
778 MC_replay(mc_stack_safety, -1);
780 XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num, xbt_fifo_size(mc_stack_safety));
783 /*req = MC_state_get_internal_request(state);
784 if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
785 if(req->call == SIMCALL_COMM_ISEND || req->call == SIMCALL_COMM_IRECV){
786 if(!xbt_dynar_is_empty(communications_pattern))
787 xbt_dynar_remove_at(communications_pattern, xbt_dynar_length(communications_pattern) - 1, NULL);
790 XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1);
791 MC_state_delete(state);
797 MC_print_statistics(mc_stats);