X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/f3ae712a1b95294052b6e8136d0f0f2d4b30e6eb..fec07ddcf333c9cc6e00b9cb60c5245b4c5b6700:/src/mc/mc_dpor.c diff --git a/src/mc/mc_dpor.c b/src/mc/mc_dpor.c index 5ab8aed15e..c4ccb59628 100644 --- a/src/mc/mc_dpor.c +++ b/src/mc/mc_dpor.c @@ -14,6 +14,7 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_dpor, mc, xbt_dynar_t visited_states; xbt_dict_t first_enabled_state; xbt_dynar_t initial_communications_pattern; +xbt_dynar_t incomplete_communications_pattern; xbt_dynar_t communications_pattern; int nb_comm_pattern; @@ -82,6 +83,8 @@ static void deterministic_pattern(xbt_dynar_t initial_pattern, xbt_dynar_t patte comm_comparison = compare_comm_pattern(comm1, comm2); if(comm_comparison == 1){ initial_state_safety->comm_deterministic = 0; + if(!_sg_mc_send_determinism) + return; } recv_index++; } @@ -97,20 +100,23 @@ static void deterministic_pattern(xbt_dynar_t initial_pattern, xbt_dynar_t patte static int complete_comm_pattern(xbt_dynar_t list, mc_comm_pattern_t pattern){ mc_comm_pattern_t current_pattern; unsigned int cursor = 0; - xbt_dynar_foreach(list, cursor, current_pattern){ + int index; + xbt_dynar_foreach(incomplete_communications_pattern, cursor, index){ + current_pattern = (mc_comm_pattern_t)xbt_dynar_get_as(list, index, mc_comm_pattern_t); if(current_pattern->comm == pattern->comm){ - if(!current_pattern->completed){ - current_pattern->src_proc = pattern->comm->comm.src_proc->pid; - current_pattern->src_host = simcall_host_get_name(pattern->comm->comm.src_proc->smx_host); - current_pattern->dst_proc = pattern->comm->comm.dst_proc->pid; - current_pattern->dst_host = simcall_host_get_name(pattern->comm->comm.dst_proc->smx_host); + current_pattern->src_proc = pattern->comm->comm.src_proc->pid; + current_pattern->dst_proc = pattern->comm->comm.dst_proc->pid; + current_pattern->src_host = simcall_host_get_name(pattern->comm->comm.src_proc->smx_host); + current_pattern->dst_host = simcall_host_get_name(pattern->comm->comm.dst_proc->smx_host); + if(current_pattern->data_size == -1){ current_pattern->data_size = pattern->comm->comm.src_buff_size; current_pattern->data = xbt_malloc0(current_pattern->data_size); - current_pattern->matched_comm = pattern->num; memcpy(current_pattern->data, current_pattern->comm->comm.src_buff, current_pattern->data_size); - current_pattern->completed = 1; - return current_pattern->num; } + current_pattern->matched_comm = pattern->num; + current_pattern->completed = 1; + xbt_dynar_remove_at(incomplete_communications_pattern, cursor, NULL); + return current_pattern->num; } } return -1; @@ -121,14 +127,15 @@ void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, int call){ pattern = xbt_new0(s_mc_comm_pattern_t, 1); pattern->num = ++nb_comm_pattern; pattern->completed = 0; + pattern->data_size = -1; if(call == 1){ // ISEND pattern->comm = simcall_comm_isend__get__result(request); pattern->type = SIMIX_COMM_SEND; if(pattern->comm->comm.dst_proc != NULL){ pattern->matched_comm = complete_comm_pattern(list, pattern); pattern->dst_proc = pattern->comm->comm.dst_proc->pid; - pattern->completed = 1; pattern->dst_host = simcall_host_get_name(pattern->comm->comm.dst_proc->smx_host); + pattern->completed = 1; } pattern->src_proc = pattern->comm->comm.src_proc->pid; pattern->src_host = simcall_host_get_name(request->issuer->smx_host); @@ -141,20 +148,26 @@ void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, int call){ if(pattern->comm->comm.src_proc != NULL){ pattern->matched_comm = complete_comm_pattern(list, pattern); pattern->src_proc = pattern->comm->comm.src_proc->pid; - pattern->src_host = simcall_host_get_name(pattern->comm->comm.src_proc->smx_host); + pattern->src_host = simcall_host_get_name(request->issuer->smx_host); pattern->completed = 1; pattern->data_size = pattern->comm->comm.src_buff_size; pattern->data=xbt_malloc0(pattern->data_size); memcpy(pattern->data, pattern->comm->comm.src_buff, pattern->data_size); } pattern->dst_proc = pattern->comm->comm.dst_proc->pid; - pattern->dst_host = simcall_host_get_name(request->issuer->smx_host); + pattern->dst_host = simcall_host_get_name(pattern->comm->comm.dst_proc->smx_host); } + if(pattern->comm->comm.rdv != NULL) pattern->rdv = strdup(pattern->comm->comm.rdv->name); else pattern->rdv = strdup(pattern->comm->comm.rdv_cpy->name); + xbt_dynar_push(list, &pattern); + + if(!pattern->completed) + xbt_dynar_push_as(incomplete_communications_pattern, int, xbt_dynar_length(list) - 1); + } static void print_communications_pattern(xbt_dynar_t comms_pattern){ @@ -217,9 +230,9 @@ static int get_search_interval(xbt_dynar_t all_states, mc_visited_state_t state, XBT_VERB("Searching interval for state %i: nd_processes=%zu heap_bytes_used=%zu", state->num, (size_t)state->nb_processes, (size_t)state->heap_bytes_used); - int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; int cursor = 0, previous_cursor, next_cursor; mc_visited_state_t state_test; @@ -257,14 +270,14 @@ static int get_search_interval(xbt_dynar_t all_states, mc_visited_state_t state, next_cursor++; } if(!raw_mem_set) - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; return -1; } } } if(!raw_mem_set) - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; return cursor; } @@ -278,9 +291,9 @@ static int is_visited_state(){ if(_sg_mc_visited == 0) return -1; - int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; mc_visited_state_t new_state = visited_state_new(); @@ -289,7 +302,7 @@ static int is_visited_state(){ xbt_dynar_push(visited_states, &new_state); if(!raw_mem_set) - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; return -1; @@ -319,7 +332,7 @@ static int is_visited_state(){ xbt_dynar_remove_at(visited_states, (min + res) - 1, NULL); xbt_dynar_insert_at(visited_states, (min+res) - 1, &new_state); if(!raw_mem_set) - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; return new_state->other_num; }*/ @@ -343,7 +356,7 @@ static int is_visited_state(){ xbt_dynar_insert_at(visited_states, cursor, &new_state); if(!raw_mem_set) - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; return new_state->other_num; } cursor++; @@ -386,7 +399,7 @@ static int is_visited_state(){ } if(!raw_mem_set) - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; return -1; @@ -399,26 +412,30 @@ static int is_visited_state(){ void MC_dpor_init() { - int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); mc_state_t initial_state = NULL; smx_process_t process; /* Create the initial state and push it into the exploration stack */ - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; if(_sg_mc_visited > 0) visited_states = xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp); - first_enabled_state = xbt_dict_new_homogeneous(&xbt_free_f); + if(mc_reduce_kind == e_mc_reduce_dpor) + first_enabled_state = xbt_dict_new_homogeneous(&xbt_free_f); - initial_communications_pattern = xbt_dynar_new(sizeof(mc_comm_pattern_t), comm_pattern_free_voidp); - communications_pattern = xbt_dynar_new(sizeof(mc_comm_pattern_t), comm_pattern_free_voidp); - nb_comm_pattern = 0; + if(_sg_mc_comms_determinism || _sg_mc_send_determinism){ + initial_communications_pattern = xbt_dynar_new(sizeof(mc_comm_pattern_t), comm_pattern_free_voidp); + communications_pattern = xbt_dynar_new(sizeof(mc_comm_pattern_t), comm_pattern_free_voidp); + incomplete_communications_pattern = xbt_dynar_new(sizeof(int), NULL); + nb_comm_pattern = 0; + } initial_state = MC_state_new(); - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; XBT_DEBUG("**************************************************"); XBT_DEBUG("Initial state"); @@ -429,7 +446,7 @@ void MC_dpor_init() MC_ignore_heap(simix_global->process_to_run->data, 0); MC_ignore_heap(simix_global->process_that_ran->data, 0); - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; /* Get an enabled process and insert it in the interleave set of the initial state */ xbt_swag_foreach(process, simix_global->process_list){ @@ -442,25 +459,27 @@ void MC_dpor_init() xbt_fifo_unshift(mc_stack_safety, initial_state); - /* To ensure the soundness of DPOR, we have to keep a list of - processes which are still enabled at each step of the exploration. - If max depth is reached, we interleave them in the state in which they have - been enabled for the first time. */ - xbt_swag_foreach(process, simix_global->process_list){ - if(MC_process_is_enabled(process)){ - char *key = bprintf("%lu", process->pid); - char *data = bprintf("%d", xbt_fifo_size(mc_stack_safety)); - xbt_dict_set(first_enabled_state, key, data, NULL); - xbt_free(key); + if(mc_reduce_kind == e_mc_reduce_dpor){ + /* To ensure the soundness of DPOR, we have to keep a list of + processes which are still enabled at each step of the exploration. + If max depth is reached, we interleave them in the state in which they have + been enabled for the first time. */ + xbt_swag_foreach(process, simix_global->process_list){ + if(MC_process_is_enabled(process)){ + char *key = bprintf("%lu", process->pid); + char *data = bprintf("%d", xbt_fifo_size(mc_stack_safety)); + xbt_dict_set(first_enabled_state, key, data, NULL); + xbt_free(key); + } } } - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; if(raw_mem_set) - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; else - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; } @@ -512,20 +531,22 @@ void MC_dpor(void) xbt_free(req_str); } - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; if(dot_output != NULL) req_str = MC_request_get_dot_output(req, value); - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; MC_state_set_executed_request(state, req, value); mc_stats->executed_transitions++; - MC_SET_RAW_MEM; - char *key = bprintf("%lu", req->issuer->pid); - xbt_dict_remove(first_enabled_state, key); - xbt_free(key); - MC_UNSET_RAW_MEM; - + if(mc_reduce_kind == e_mc_reduce_dpor){ + MC_SET_MC_HEAP; + char *key = bprintf("%lu", req->issuer->pid); + xbt_dict_remove(first_enabled_state, key); + xbt_free(key); + MC_SET_STD_HEAP; + } + if(_sg_mc_comms_determinism || _sg_mc_send_determinism){ if(req->call == SIMCALL_COMM_ISEND) comm_pattern = 1; @@ -537,14 +558,14 @@ void MC_dpor(void) SIMIX_simcall_pre(req, value); /* After this call req is no longer usefull */ if(_sg_mc_comms_determinism || _sg_mc_send_determinism){ - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; if(comm_pattern != 0){ if(!initial_state_safety->initial_communications_pattern_done) get_comm_pattern(initial_communications_pattern, req, comm_pattern); else get_comm_pattern(communications_pattern, req, comm_pattern); } - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; comm_pattern = 0; } @@ -552,7 +573,7 @@ void MC_dpor(void) MC_wait_for_requests(); /* Create the new expanded state */ - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; next_state = MC_state_new(); @@ -583,22 +604,24 @@ void MC_dpor(void) xbt_fifo_unshift(mc_stack_safety, next_state); - /* Insert in dict all enabled processes, if not included yet */ - xbt_swag_foreach(process, simix_global->process_list){ - if(MC_process_is_enabled(process)){ - char *key = bprintf("%lu", process->pid); - if(xbt_dict_get_or_null(first_enabled_state, key) == NULL){ - char *data = bprintf("%d", xbt_fifo_size(mc_stack_safety)); - xbt_dict_set(first_enabled_state, key, data, NULL); + if(mc_reduce_kind == e_mc_reduce_dpor){ + /* Insert in dict all enabled processes, if not included yet */ + xbt_swag_foreach(process, simix_global->process_list){ + if(MC_process_is_enabled(process)){ + char *key = bprintf("%lu", process->pid); + if(xbt_dict_get_or_null(first_enabled_state, key) == NULL){ + char *data = bprintf("%d", xbt_fifo_size(mc_stack_safety)); + xbt_dict_set(first_enabled_state, key, data, NULL); + } + xbt_free(key); } - xbt_free(key); } } if(dot_output != NULL) xbt_free(req_str); - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; /* Let's loop again */ @@ -614,19 +637,21 @@ void MC_dpor(void) visited_state = -1; - /* Interleave enabled processes in the state in which they have been enabled for the first time */ - xbt_swag_foreach(process, simix_global->process_list){ - if(MC_process_is_enabled(process)){ - char *key = bprintf("%lu", process->pid); - enabled = (int)strtoul(xbt_dict_get_or_null(first_enabled_state, key), 0, 10); - xbt_free(key); - int cursor = xbt_fifo_size(mc_stack_safety); - xbt_fifo_foreach(mc_stack_safety, item, state_test, mc_state_t){ - if(cursor-- == enabled){ - if(!MC_state_process_is_done(state_test, process) && state_test->num != state->num){ - XBT_DEBUG("Interleave process %lu in state %d", process->pid, state_test->num); - MC_state_interleave_process(state_test, process); - break; + if(mc_reduce_kind == e_mc_reduce_dpor){ + /* Interleave enabled processes in the state in which they have been enabled for the first time */ + xbt_swag_foreach(process, simix_global->process_list){ + if(MC_process_is_enabled(process)){ + char *key = bprintf("%lu", process->pid); + enabled = (int)strtoul(xbt_dict_get_or_null(first_enabled_state, key), 0, 10); + xbt_free(key); + int cursor = xbt_fifo_size(mc_stack_safety); + xbt_fifo_foreach(mc_stack_safety, item, state_test, mc_state_t){ + if(cursor-- == enabled){ + if(!MC_state_process_is_done(state_test, process) && state_test->num != state->num){ + XBT_DEBUG("Interleave process %lu in state %d", process->pid, state_test->num); + MC_state_interleave_process(state_test, process); + break; + } } } } @@ -639,7 +664,7 @@ void MC_dpor(void) } - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; if(_sg_mc_comms_determinism || _sg_mc_send_determinism){ if(initial_state_safety->initial_communications_pattern_done){ @@ -678,7 +703,7 @@ void MC_dpor(void) MC_state_delete(state); XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1); - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; /* Check for deadlocks */ if(MC_deadlock_check()){ @@ -686,7 +711,7 @@ void MC_dpor(void) return; } - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; /* Traverse the stack backwards until a state with a non empty interleave set is found, deleting all the states that have it empty in the way. For each deleted state, check if the request that has generated it @@ -738,7 +763,7 @@ void MC_dpor(void) if(state->system_state != NULL){ MC_restore_snapshot(state->system_state); xbt_fifo_unshift(mc_stack_safety, state); - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; }else{ pos = xbt_fifo_size(mc_stack_safety); item = xbt_fifo_get_first_item(mc_stack_safety); @@ -753,33 +778,33 @@ void MC_dpor(void) } MC_restore_snapshot(restored_state->system_state); xbt_fifo_unshift(mc_stack_safety, state); - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; MC_replay(mc_stack_safety, pos); } }else{ xbt_fifo_unshift(mc_stack_safety, state); - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; MC_replay(mc_stack_safety, -1); } XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num, xbt_fifo_size(mc_stack_safety)); break; } else { - req = MC_state_get_internal_request(state); - if(_sg_mc_comms_determinism){ + /*req = MC_state_get_internal_request(state); + if(_sg_mc_comms_determinism || _sg_mc_send_determinism){ if(req->call == SIMCALL_COMM_ISEND || req->call == SIMCALL_COMM_IRECV){ if(!xbt_dynar_is_empty(communications_pattern)) xbt_dynar_remove_at(communications_pattern, xbt_dynar_length(communications_pattern) - 1, NULL); } - } + }*/ XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1); MC_state_delete(state); } } - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; } } MC_print_statistics(mc_stats); - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; return; }