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 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;
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);
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;
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;
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);
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);
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);
161 if(pattern->comm->comm.rdv != NULL)
162 pattern->rdv = strdup(pattern->comm->comm.rdv->name);
164 pattern->rdv = strdup(pattern->comm->comm.rdv_cpy->name);
166 xbt_dynar_push(list, &pattern);
168 if(!pattern->completed)
169 xbt_dynar_push_as(incomplete_communications_pattern, int, xbt_dynar_length(list) - 1);
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");
180 XBT_INFO("[(%lu) %s <- %s] %s ", current_comm->dst_proc, current_comm->dst_host, current_comm->src_host, "iRecv");
184 static void visited_state_free(mc_visited_state_t state){
186 MC_free_snapshot(state->system_state);
191 static void visited_state_free_voidp(void *s){
192 visited_state_free((mc_visited_state_t) * (void **) s);
195 /** \brief Save the current state
197 * \return Snapshot of the current state.
199 static mc_visited_state_t visited_state_new(){
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;
213 /** \brief Find a suitable subrange of candidate duplicates for a given state
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
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.
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.
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);
233 int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
237 int cursor = 0, previous_cursor, next_cursor;
238 mc_visited_state_t state_test;
240 int end = xbt_dynar_length(all_states) - 1;
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){
247 }else if(state_test->nb_processes > state->nb_processes){
250 if(state_test->heap_bytes_used < state->heap_bytes_used){
252 }else if(state_test->heap_bytes_used > state->heap_bytes_used){
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)
261 *min = previous_cursor;
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)
285 /** \brief Take a snapshot the current state and process it.
287 * \return number of the duplicate state or -1 (not visited)
289 static int is_visited_state(){
291 if(_sg_mc_visited == 0)
294 int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
298 mc_visited_state_t new_state = visited_state_new();
300 if(xbt_dynar_is_empty(visited_states)){
302 xbt_dynar_push(visited_states, &new_state);
311 int min = -1, max = -1, index;
313 mc_visited_state_t state_test;
316 index = get_search_interval(visited_states, new_state, &min, &max);
318 if(min != -1 && max != -1){
320 // Parallell implementation
321 /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_states, min), (max-min)+1, new_state);
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;
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);
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);
336 return new_state->other_num;
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:
345 if(state_test->other_num == -1)
346 new_state->other_num = state_test->num;
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);
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);
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);
360 return new_state->other_num;
365 // The state has not been visited, add it to the list:
366 xbt_dynar_insert_at(visited_states, min, &new_state);
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);
375 if(state_test->heap_bytes_used < new_state->heap_bytes_used)
376 xbt_dynar_insert_at(visited_states, index + 1, &new_state);
378 xbt_dynar_insert_at(visited_states, index, &new_state);
383 // We have reached the maximum number of stored states;
384 if(xbt_dynar_length(visited_states) > _sg_mc_visited){
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){
393 min2 = state_test->num;
398 xbt_dynar_remove_at(visited_states, index2, NULL);
410 * \brief Initialize the DPOR exploration algorithm
415 int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
417 mc_state_t initial_state = NULL;
418 smx_process_t process;
420 /* Create the initial state and push it into the exploration stack */
423 if(_sg_mc_visited > 0)
424 visited_states = xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp);
426 if(mc_reduce_kind == e_mc_reduce_dpor)
427 first_enabled_state = xbt_dict_new_homogeneous(&xbt_free_f);
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);
436 initial_state = MC_state_new();
440 XBT_DEBUG("**************************************************");
441 XBT_DEBUG("Initial state");
443 /* Wait for requests (schedules processes) */
444 MC_wait_for_requests();
446 MC_ignore_heap(simix_global->process_to_run->data, 0);
447 MC_ignore_heap(simix_global->process_that_ran->data, 0);
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)
460 xbt_fifo_unshift(mc_stack_safety, initial_state);
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);
487 /** \brief Model-check the application using a DFS exploration
488 * with DPOR (Dynamic Partial Order Reductions)
493 char *req_str = NULL;
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;
501 int visited_state = -1;
503 int interleave_size = 0;
504 int comm_pattern = 0;
506 while (xbt_fifo_size(mc_stack_safety) > 0) {
508 /* Get current state */
510 xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_safety));
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));
517 interleave_size = MC_state_interleave_size(state);
519 /* Update statistics */
520 mc_stats->visited_states++;
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) {
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);
535 if(dot_output != NULL)
536 req_str = MC_request_get_dot_output(req, value);
539 MC_state_set_executed_request(state, req, value);
540 mc_stats->executed_transitions++;
542 if(mc_reduce_kind == e_mc_reduce_dpor){
544 char *key = bprintf("%lu", req->issuer->pid);
545 xbt_dict_remove(first_enabled_state, key);
550 if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
551 if(req->call == SIMCALL_COMM_ISEND)
553 else if(req->call == SIMCALL_COMM_IRECV)
557 /* Answer the request */
558 SIMIX_simcall_pre(req, value); /* After this call req is no longer usefull */
560 if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
562 if(comm_pattern != 0){
563 if(!initial_state_safety->initial_communications_pattern_done)
564 get_comm_pattern(initial_communications_pattern, req, comm_pattern);
566 get_comm_pattern(communications_pattern, req, comm_pattern);
572 /* Wait for requests (schedules processes) */
573 MC_wait_for_requests();
575 /* Create the new expanded state */
578 next_state = MC_state_new();
580 if((visited_state = is_visited_state()) == -1){
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)
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);
595 if(dot_output != NULL)
596 fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str);
600 if(dot_output != NULL)
601 fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visited_state, req_str);
605 xbt_fifo_unshift(mc_stack_safety, next_state);
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);
621 if(dot_output != NULL)
626 /* Let's loop again */
628 /* The interleave set is empty or the maximum depth is reached, let's back-track */
631 if((xbt_fifo_size(mc_stack_safety) > _sg_mc_max_depth) || user_max_depth_reached || visited_state != -1){
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 ! /!\\ ");
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);
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);
663 XBT_DEBUG("There are no more processes to interleave. (depth %d)", xbt_fifo_size(mc_stack_safety) + 1);
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);
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);
697 initial_state_safety->initial_communications_pattern_done = 1;
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);
708 /* Check for deadlocks */
709 if(MC_deadlock_check()){
710 MC_show_deadlock(NULL);
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. */
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);
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);
739 if(!MC_state_process_is_done(prev_state, req->issuer))
740 MC_state_interleave_process(prev_state, req->issuer);
742 XBT_DEBUG("Process %p is in done set", req->issuer);
746 }else if(req->issuer == MC_state_get_internal_request(prev_state)->issuer){
748 XBT_DEBUG("Simcall %d and %d with same issuer", req->call, MC_state_get_internal_request(prev_state)->call);
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);
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);
768 pos = xbt_fifo_size(mc_stack_safety);
769 item = xbt_fifo_get_first_item(mc_stack_safety);
771 restored_state = (mc_state_t) xbt_fifo_get_item_content(item);
772 if(restored_state->system_state != NULL){
775 item = xbt_fifo_get_next_item(item);
779 MC_restore_snapshot(restored_state->system_state);
780 xbt_fifo_unshift(mc_stack_safety, state);
782 MC_replay(mc_stack_safety, pos);
785 xbt_fifo_unshift(mc_stack_safety, state);
787 MC_replay(mc_stack_safety, -1);
789 XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num, xbt_fifo_size(mc_stack_safety));
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);
799 XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1);
800 MC_state_delete(state);
806 MC_print_statistics(mc_stats);