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 #include "xbt/mmalloc/mmprivate.h"
11 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_dpor, mc,
12 "Logging specific to MC DPOR exploration");
14 /********** Global variables **********/
16 xbt_dynar_t visited_states;
17 xbt_dict_t first_enabled_state;
18 xbt_dynar_t initial_communications_pattern;
19 xbt_dynar_t incomplete_communications_pattern;
20 xbt_dynar_t communications_pattern;
23 /********** Static functions ***********/
25 static void comm_pattern_free(mc_comm_pattern_t p){
32 static void comm_pattern_free_voidp( void *p){
33 comm_pattern_free((mc_comm_pattern_t) * (void **)p);
36 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){
37 mc_comm_pattern_t current_comm;
38 while(*idx < xbt_dynar_length(pattern)){
39 current_comm = (mc_comm_pattern_t)xbt_dynar_get_as(pattern, *idx, mc_comm_pattern_t);
40 if(current_comm->type == type && type == SIMIX_COMM_SEND){
41 if(current_comm->src_proc == proc)
43 }else if(current_comm->type == type && type == SIMIX_COMM_RECEIVE){
44 if(current_comm->dst_proc == proc)
52 static int compare_comm_pattern(mc_comm_pattern_t comm1, mc_comm_pattern_t comm2){
53 if(strcmp(comm1->rdv, comm2->rdv) != 0)
55 if(comm1->src_proc != comm2->src_proc)
57 if(comm1->dst_proc != comm2->dst_proc)
59 if(comm1->data_size != comm2->data_size)
61 if(memcmp(comm1->data, comm2->data, comm1->data_size) != 0)
66 static void deterministic_pattern(xbt_dynar_t initial_pattern, xbt_dynar_t pattern){
68 if(!xbt_dynar_is_empty(incomplete_communications_pattern))
71 unsigned int cursor = 0, send_index = 0, recv_index = 0;
72 mc_comm_pattern_t comm1, comm2;
73 int comm_comparison = 0;
74 int current_process = 0;
75 while(current_process < simix_process_maxpid){
76 while(cursor < xbt_dynar_length(initial_pattern)){
77 comm1 = (mc_comm_pattern_t)xbt_dynar_get_as(initial_pattern, cursor, mc_comm_pattern_t);
78 if(comm1->type == SIMIX_COMM_SEND && comm1->src_proc == current_process){
79 comm2 = get_comm_pattern_from_idx(pattern, &send_index, comm1->type, current_process);
80 comm_comparison = compare_comm_pattern(comm1, comm2);
81 if(comm_comparison == 1){
82 initial_state_safety->send_deterministic = 0;
83 initial_state_safety->comm_deterministic = 0;
87 }else if(comm1->type == SIMIX_COMM_RECEIVE && comm1->dst_proc == current_process){
88 comm2 = get_comm_pattern_from_idx(pattern, &recv_index, comm1->type, current_process);
89 comm_comparison = compare_comm_pattern(comm1, comm2);
90 if(comm_comparison == 1){
91 initial_state_safety->comm_deterministic = 0;
92 if(!_sg_mc_send_determinism)
106 void complete_comm_pattern(xbt_dynar_t list, smx_action_t comm){
107 mc_comm_pattern_t current_pattern;
108 unsigned int cursor = 0;
112 xbt_dynar_foreach(incomplete_communications_pattern, cursor, index){
113 current_pattern = (mc_comm_pattern_t)xbt_dynar_get_as(list, index, mc_comm_pattern_t);
114 if(current_pattern->comm == comm){
115 current_pattern->src_proc = comm->comm.src_proc->pid;
116 current_pattern->dst_proc = comm->comm.dst_proc->pid;
117 current_pattern->src_host = simcall_host_get_name(comm->comm.src_proc->smx_host);
118 current_pattern->dst_host = simcall_host_get_name(comm->comm.dst_proc->smx_host);
119 if(current_pattern->data_size == -1){
120 current_pattern->data_size = *(comm->comm.dst_buff_size);
121 current_pattern->data = xbt_malloc0(current_pattern->data_size);
122 addr_pointed = *(void **)comm->comm.src_buff;
123 if(addr_pointed > std_heap && addr_pointed < ((xbt_mheap_t)std_heap)->breakval)
124 memcpy(current_pattern->data, addr_pointed, current_pattern->data_size);
126 memcpy(current_pattern->data, comm->comm.src_buff, current_pattern->data_size);
128 xbt_dynar_remove_at(incomplete_communications_pattern, cursor, NULL);
137 void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, int call){
138 mc_comm_pattern_t pattern = NULL;
139 pattern = xbt_new0(s_mc_comm_pattern_t, 1);
140 pattern->num = ++nb_comm_pattern;
141 pattern->data_size = -1;
143 if(call == 1){ // ISEND
144 pattern->comm = simcall_comm_isend__get__result(request);
145 pattern->type = SIMIX_COMM_SEND;
146 pattern->src_proc = pattern->comm->comm.src_proc->pid;
147 pattern->src_host = simcall_host_get_name(request->issuer->smx_host);
148 pattern->data_size = pattern->comm->comm.src_buff_size;
149 pattern->data = xbt_malloc0(pattern->data_size);
150 addr_pointed = *(void **)pattern->comm->comm.src_buff;
151 if(addr_pointed > std_heap && addr_pointed < ((xbt_mheap_t)std_heap)->breakval)
152 memcpy(pattern->data, addr_pointed, pattern->data_size);
154 memcpy(pattern->data, pattern->comm->comm.src_buff, pattern->data_size);
156 pattern->comm = simcall_comm_irecv__get__result(request);
157 pattern->type = SIMIX_COMM_RECEIVE;
158 pattern->dst_proc = pattern->comm->comm.dst_proc->pid;
159 pattern->dst_host = simcall_host_get_name(pattern->comm->comm.dst_proc->smx_host);
162 if(pattern->comm->comm.rdv != NULL)
163 pattern->rdv = strdup(pattern->comm->comm.rdv->name);
165 pattern->rdv = strdup(pattern->comm->comm.rdv_cpy->name);
167 xbt_dynar_push(list, &pattern);
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 -> (%lu) %s] %s ", current_comm->src_proc, current_comm->src_host, current_comm->dst_proc, current_comm->dst_host, "iSend");
180 XBT_INFO("[(%lu) %s <- (%lu) %s] %s ", current_comm->dst_proc, current_comm->dst_host, current_comm->src_proc, 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() == mc_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() == mc_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() == mc_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;
505 smx_action_t current_comm;
507 while (xbt_fifo_size(mc_stack_safety) > 0) {
509 /* Get current state */
511 xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_safety));
513 XBT_DEBUG("**************************************************");
514 XBT_DEBUG("Exploration depth=%d (state=%p, num %d)(%u interleave, user_max_depth %d, first_enabled_state size : %d)",
515 xbt_fifo_size(mc_stack_safety), state, state->num,
516 MC_state_interleave_size(state), user_max_depth_reached, xbt_dict_size(first_enabled_state));
518 interleave_size = MC_state_interleave_size(state);
520 /* Update statistics */
521 mc_stats->visited_states++;
523 /* If there are processes to interleave and the maximum depth has not been reached
524 then perform one step of the exploration algorithm */
525 if (xbt_fifo_size(mc_stack_safety) <= _sg_mc_max_depth && !user_max_depth_reached &&
526 (req = MC_state_get_request(state, &value)) && visited_state == -1) {
528 /* Debug information */
529 if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
530 req_str = MC_request_to_string(req, value);
531 XBT_DEBUG("Execute: %s", req_str);
536 if(dot_output != NULL)
537 req_str = MC_request_get_dot_output(req, value);
540 MC_state_set_executed_request(state, req, value);
541 mc_stats->executed_transitions++;
543 if(mc_reduce_kind == e_mc_reduce_dpor){
545 char *key = bprintf("%lu", req->issuer->pid);
546 xbt_dict_remove(first_enabled_state, key);
551 /* TODO : handle test and testany simcalls */
552 if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
553 if(req->call == SIMCALL_COMM_ISEND)
555 else if(req->call == SIMCALL_COMM_IRECV)
557 else if(req->call == SIMCALL_COMM_WAIT)
559 else if(req->call == SIMCALL_COMM_WAITANY)
563 /* Answer the request */
564 SIMIX_simcall_pre(req, value); /* After this call req is no longer usefull */
566 if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
568 if(comm_pattern == 1 || comm_pattern == 2){
569 if(!initial_state_safety->initial_communications_pattern_done)
570 get_comm_pattern(initial_communications_pattern, req, comm_pattern);
572 get_comm_pattern(communications_pattern, req, comm_pattern);
573 }else if(comm_pattern == 3){
574 current_comm = simcall_comm_wait__get__comm(req);
575 if(current_comm->comm.refcount == 1){ /* First wait only must be considered */
576 if(!initial_state_safety->initial_communications_pattern_done)
577 complete_comm_pattern(initial_communications_pattern, current_comm);
579 complete_comm_pattern(communications_pattern, current_comm);
581 }else if(comm_pattern == 4){
582 current_comm = xbt_dynar_get_as(simcall_comm_waitany__get__comms(req), value, smx_action_t);
583 if(current_comm->comm.refcount == 1){ /* First wait only must be considered */
584 if(!initial_state_safety->initial_communications_pattern_done)
585 complete_comm_pattern(initial_communications_pattern, current_comm);
587 complete_comm_pattern(communications_pattern, current_comm);
594 /* Wait for requests (schedules processes) */
595 MC_wait_for_requests();
597 /* Create the new expanded state */
600 next_state = MC_state_new();
602 if((visited_state = is_visited_state()) == -1){
604 /* Get an enabled process and insert it in the interleave set of the next state */
605 xbt_swag_foreach(process, simix_global->process_list){
606 if(MC_process_is_enabled(process)){
607 MC_state_interleave_process(next_state, process);
608 if(mc_reduce_kind != e_mc_reduce_none)
613 if(_sg_mc_checkpoint && ((xbt_fifo_size(mc_stack_safety) + 1) % _sg_mc_checkpoint == 0)){
614 next_state->system_state = MC_take_snapshot(next_state->num);
617 if(dot_output != NULL)
618 fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str);
622 if(dot_output != NULL)
623 fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visited_state, req_str);
627 xbt_fifo_unshift(mc_stack_safety, next_state);
629 if(mc_reduce_kind == e_mc_reduce_dpor){
630 /* Insert in dict all enabled processes, if not included yet */
631 xbt_swag_foreach(process, simix_global->process_list){
632 if(MC_process_is_enabled(process)){
633 char *key = bprintf("%lu", process->pid);
634 if(xbt_dict_get_or_null(first_enabled_state, key) == NULL){
635 char *data = bprintf("%d", xbt_fifo_size(mc_stack_safety));
636 xbt_dict_set(first_enabled_state, key, data, NULL);
643 if(dot_output != NULL)
648 /* Let's loop again */
650 /* The interleave set is empty or the maximum depth is reached, let's back-track */
653 if((xbt_fifo_size(mc_stack_safety) > _sg_mc_max_depth) || user_max_depth_reached || visited_state != -1){
655 if(user_max_depth_reached && visited_state == -1)
656 XBT_DEBUG("User max depth reached !");
657 else if(visited_state == -1)
658 XBT_WARN("/!\\ Max depth reached ! /!\\ ");
662 if(mc_reduce_kind == e_mc_reduce_dpor){
663 /* Interleave enabled processes in the state in which they have been enabled for the first time */
664 xbt_swag_foreach(process, simix_global->process_list){
665 if(MC_process_is_enabled(process)){
666 char *key = bprintf("%lu", process->pid);
667 enabled = (int)strtoul(xbt_dict_get_or_null(first_enabled_state, key), 0, 10);
669 int cursor = xbt_fifo_size(mc_stack_safety);
670 xbt_fifo_foreach(mc_stack_safety, item, state_test, mc_state_t){
671 if(cursor-- == enabled){
672 if(!MC_state_process_is_done(state_test, process) && state_test->num != state->num){
673 XBT_DEBUG("Interleave process %lu in state %d", process->pid, state_test->num);
674 MC_state_interleave_process(state_test, process);
685 XBT_DEBUG("There are no more processes to interleave. (depth %d)", xbt_fifo_size(mc_stack_safety) + 1);
691 if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
692 if(initial_state_safety->initial_communications_pattern_done){
693 if(interleave_size == 0){ /* if (interleave_size > 0), process interleaved but not enabled => "incorrect" path, determinism not evaluated */
694 //print_communications_pattern(communications_pattern);
695 deterministic_pattern(initial_communications_pattern, communications_pattern);
696 if(initial_state_safety->comm_deterministic == 0 && _sg_mc_comms_determinism){
697 XBT_INFO("****************************************************");
698 XBT_INFO("***** Non-deterministic communications pattern *****");
699 XBT_INFO("****************************************************");
700 XBT_INFO("Initial communications pattern:");
701 print_communications_pattern(initial_communications_pattern);
702 XBT_INFO("Communications pattern counter-example:");
703 print_communications_pattern(communications_pattern);
704 MC_print_statistics(mc_stats);
706 }else if(initial_state_safety->send_deterministic == 0 && _sg_mc_send_determinism){
707 XBT_INFO("****************************************************");
708 XBT_INFO("***** Non-send-deterministic communications pattern *****");
709 XBT_INFO("****************************************************");
710 XBT_INFO("Initial communications pattern:");
711 print_communications_pattern(initial_communications_pattern);
712 XBT_INFO("Communications pattern counter-example:");
713 print_communications_pattern(communications_pattern);
714 MC_print_statistics(mc_stats);
719 initial_state_safety->initial_communications_pattern_done = 1;
723 /* Trash the current state, no longer needed */
724 xbt_fifo_shift(mc_stack_safety);
725 MC_state_delete(state);
726 XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1);
730 /* Check for deadlocks */
731 if(MC_deadlock_check()){
732 MC_show_deadlock(NULL);
737 /* Traverse the stack backwards until a state with a non empty interleave
738 set is found, deleting all the states that have it empty in the way.
739 For each deleted state, check if the request that has generated it
740 (from it's predecesor state), depends on any other previous request
741 executed before it. If it does then add it to the interleave set of the
742 state that executed that previous request. */
744 while ((state = xbt_fifo_shift(mc_stack_safety)) != NULL) {
745 if(mc_reduce_kind == e_mc_reduce_dpor){
746 req = MC_state_get_internal_request(state);
747 xbt_fifo_foreach(mc_stack_safety, item, prev_state, mc_state_t) {
748 if(MC_request_depend(req, MC_state_get_internal_request(prev_state))){
749 if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
750 XBT_DEBUG("Dependent Transitions:");
751 prev_req = MC_state_get_executed_request(prev_state, &value);
752 req_str = MC_request_to_string(prev_req, value);
753 XBT_DEBUG("%s (state=%d)", req_str, prev_state->num);
755 prev_req = MC_state_get_executed_request(state, &value);
756 req_str = MC_request_to_string(prev_req, value);
757 XBT_DEBUG("%s (state=%d)", req_str, state->num);
761 if(!MC_state_process_is_done(prev_state, req->issuer))
762 MC_state_interleave_process(prev_state, req->issuer);
764 XBT_DEBUG("Process %p is in done set", req->issuer);
768 }else if(req->issuer == MC_state_get_internal_request(prev_state)->issuer){
770 XBT_DEBUG("Simcall %d and %d with same issuer", req->call, MC_state_get_internal_request(prev_state)->call);
775 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);
781 if (MC_state_interleave_size(state) && xbt_fifo_size(mc_stack_safety) < _sg_mc_max_depth) {
782 /* We found a back-tracking point, let's loop */
783 XBT_DEBUG("Back-tracking to state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1);
784 if(_sg_mc_checkpoint){
785 if(state->system_state != NULL){
786 MC_restore_snapshot(state->system_state);
787 xbt_fifo_unshift(mc_stack_safety, state);
790 pos = xbt_fifo_size(mc_stack_safety);
791 item = xbt_fifo_get_first_item(mc_stack_safety);
793 restored_state = (mc_state_t) xbt_fifo_get_item_content(item);
794 if(restored_state->system_state != NULL){
797 item = xbt_fifo_get_next_item(item);
801 MC_restore_snapshot(restored_state->system_state);
802 xbt_fifo_unshift(mc_stack_safety, state);
804 MC_replay(mc_stack_safety, pos);
807 xbt_fifo_unshift(mc_stack_safety, state);
809 MC_replay(mc_stack_safety, -1);
811 XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num, xbt_fifo_size(mc_stack_safety));
814 /*req = MC_state_get_internal_request(state);
815 if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
816 if(req->call == SIMCALL_COMM_ISEND || req->call == SIMCALL_COMM_IRECV){
817 if(!xbt_dynar_is_empty(communications_pattern))
818 xbt_dynar_remove_at(communications_pattern, xbt_dynar_length(communications_pattern) - 1, NULL);
821 XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1);
822 MC_state_delete(state);
828 MC_print_statistics(mc_stats);