From: Gabriel Corona Date: Mon, 24 Feb 2014 08:27:07 +0000 (+0100) Subject: Merge branch 'mc-perf' into mc X-Git-Tag: v3_11~199^2~2^2~24 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/fa89cb46ee9cce80179056e44c26ca5de4c4ac9c?hp=-c Merge branch 'mc-perf' into mc --- fa89cb46ee9cce80179056e44c26ca5de4c4ac9c diff --combined src/include/mc/mc.h index 28f184b598,298c779903..88bfb651bb --- a/src/include/mc/mc.h +++ b/src/include/mc/mc.h @@@ -26,10 -26,10 +26,11 @@@ extern int _sg_do_model_check extern int _sg_mc_checkpoint; extern char* _sg_mc_property_file; extern int _sg_mc_timeout; + extern int _sg_mc_hash; extern int _sg_mc_max_depth; extern int _sg_mc_visited; extern char* _sg_mc_dot_output_file; +extern int _sg_mc_comms_determinism; extern xbt_dynar_t mc_heap_comparison_ignore; extern xbt_dynar_t stacks_areas; @@@ -41,10 -41,10 +42,11 @@@ void _mc_cfg_cb_reduce(const char *name void _mc_cfg_cb_checkpoint(const char *name, int pos); void _mc_cfg_cb_property(const char *name, int pos); void _mc_cfg_cb_timeout(const char *name, int pos); + void _mc_cfg_cb_hash(const char *name, int pos); void _mc_cfg_cb_max_depth(const char *name, int pos); void _mc_cfg_cb_visited(const char *name, int pos); void _mc_cfg_cb_dot_output(const char *name, int pos); +void _mc_cfg_cb_comms_determinism(const char *name, int pos); XBT_PUBLIC(void) MC_do_the_modelcheck_for_real(void); diff --combined src/mc/mc_dpor.c index a3e2949111,40178859de..d0b158d7f3 --- a/src/mc/mc_dpor.c +++ b/src/mc/mc_dpor.c @@@ -172,6 -172,10 +172,10 @@@ static void visited_state_free_voidp(vo visited_state_free((mc_visited_state_t) * (void **) s); } + /** \brief Save the current state + * + * \return Snapshot of the current state. + */ static mc_visited_state_t visited_state_new(){ mc_visited_state_t new_state = NULL; @@@ -186,6 -190,22 +190,22 @@@ } + /** \brief Find a suitable subrange of candidate duplicates for a given state + * + * \param all_ pairs dynamic array of states with candidate duplicates of the current state; + * \param pair current state; + * \param min (output) index of the beginning of the the subrange + * \param max (output) index of the enf of the subrange + * + * Given a suitably ordered array of state, this function extracts a subrange + * (with index *min <= i <= *max) with candidate duplicates of the given state. + * This function uses only fast discriminating criterions and does not use the + * full state comparison algorithms. + * + * The states in all_pairs MUST be ordered using a (given) weak order + * (based on nb_processes and heap_bytes_used). + * The subrange is the subrange of "equivalence" of the given state. + */ static int get_search_interval(xbt_dynar_t all_states, mc_visited_state_t state, int *min, int *max){ int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); @@@ -240,6 -260,10 +260,10 @@@ return cursor; } + /** \brief Take a snapshot the current state and process it. + * + * \return number of the duplicate state or -1 (not visited) + */ static int is_visited_state(){ if(_sg_mc_visited == 0) @@@ -270,6 -294,8 +294,8 @@@ index = get_search_interval(visited_states, new_state, &min, &max); if(min != -1 && max != -1){ + + // Parallell implementation /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_states, min), (max-min)+1, new_state); if(res != -1){ state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, (min+res)-1, mc_visited_state_t); @@@ -287,10 -313,13 +313,13 @@@ MC_UNSET_RAW_MEM; return new_state->other_num; }*/ + cursor = min; while(cursor <= max){ state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, cursor, mc_visited_state_t); if(snapshot_compare(state_test, new_state) == 0){ + // The state has been visited: + if(state_test->other_num == -1) new_state->other_num = state_test->num; else @@@ -299,16 -328,24 +328,24 @@@ XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num); else 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); + + // Replace the old state with the new one (why?): xbt_dynar_remove_at(visited_states, cursor, NULL); xbt_dynar_insert_at(visited_states, cursor, &new_state); + if(!raw_mem_set) MC_UNSET_RAW_MEM; return new_state->other_num; } cursor++; } + + // The state has not been visited, add it to the list: xbt_dynar_insert_at(visited_states, min, &new_state); + }else{ + + // The state has not been visited: insert the state in the dynamic array. state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, index, mc_visited_state_t); if(state_test->nb_processes < new_state->nb_processes){ xbt_dynar_insert_at(visited_states, index+1, &new_state); @@@ -318,9 -355,13 +355,13 @@@ else xbt_dynar_insert_at(visited_states, index, &new_state); } + } + // We have reached the maximum number of stored states; if(xbt_dynar_length(visited_states) > _sg_mc_visited){ + + // Find the (index of the) older state: int min2 = mc_stats->expanded_states; unsigned int cursor2 = 0; unsigned int index2 = 0; @@@ -330,6 -371,8 +371,8 @@@ min2 = state_test->num; } } + + // and drop it: xbt_dynar_remove_at(visited_states, index2, NULL); } @@@ -413,9 -456,8 +456,8 @@@ void MC_dpor_init( } - /** - * \brief Perform the model-checking operation using a depth-first search exploration - * with Dynamic Partial Order Reductions + /** \brief Model-check the application using a DFS exploration + * with DPOR (Dynamic Partial Order Reductions) */ void MC_dpor(void) { @@@ -423,15 -465,15 +465,15 @@@ char *req_str = NULL; int value; smx_simcall_t req = NULL, prev_req = NULL; - mc_state_t state = NULL, prev_state = NULL, next_state = NULL, restore_state=NULL; + mc_state_t state = NULL, prev_state = NULL, next_state = NULL, restored_state=NULL; smx_process_t process = NULL; xbt_fifo_item_t item = NULL; mc_state_t state_test = NULL; int pos; int visited_state = -1; int enabled = 0; - int comm_pattern = 0; int interleave_size = 0; + int comm_pattern = 0; while (xbt_fifo_size(mc_stack_safety) > 0) { @@@ -474,28 -516,25 +516,28 @@@ xbt_dict_remove(first_enabled_state, key); xbt_free(key); MC_UNSET_RAW_MEM; - - if(req->call == SIMCALL_COMM_ISEND) - comm_pattern = 1; - else if(req->call == SIMCALL_COMM_IRECV) - comm_pattern = 2; + + if(_sg_mc_comms_determinism){ + if(req->call == SIMCALL_COMM_ISEND) + comm_pattern = 1; + else if(req->call == SIMCALL_COMM_IRECV) + comm_pattern = 2; + } /* Answer the request */ SIMIX_simcall_pre(req, value); /* After this call req is no longer usefull */ - MC_SET_RAW_MEM; - 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); + if(_sg_mc_comms_determinism){ + MC_SET_RAW_MEM; + 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; + comm_pattern = 0; } - MC_UNSET_RAW_MEM; - - comm_pattern = 0; /* Wait for requests (schedules processes) */ MC_wait_for_requests(); @@@ -589,24 -628,24 +631,24 @@@ } MC_SET_RAW_MEM; - if(0) { - if(!initial_state_safety->initial_communications_pattern_done){ - print_communications_pattern(initial_communications_pattern); - }else{ - if(interleave_size == 0){ /* if (interleave_size > 0), process interleaved but not enabled => "incorrect" path, determinism not evaluated */ - print_communications_pattern(communications_pattern); - deterministic_pattern(initial_communications_pattern, communications_pattern); + + if(_sg_mc_comms_determinism){ + if(!initial_state_safety->initial_communications_pattern_done){ + //print_communications_pattern(initial_communications_pattern); + }else{ + if(interleave_size == 0){ /* if (interleave_size > 0), process interleaved but not enabled => "incorrect" path, determinism not evaluated */ + //print_communications_pattern(communications_pattern); + deterministic_pattern(initial_communications_pattern, communications_pattern); + } } + initial_state_safety->initial_communications_pattern_done = 1; } - initial_state_safety->initial_communications_pattern_done = 1; - } - MC_UNSET_RAW_MEM; /* Trash the current state, no longer needed */ - MC_SET_RAW_MEM; xbt_fifo_shift(mc_stack_safety); 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; /* Check for deadlocks */ @@@ -672,15 -711,15 +714,15 @@@ pos = xbt_fifo_size(mc_stack_safety); item = xbt_fifo_get_first_item(mc_stack_safety); while(pos>0){ - restore_state = (mc_state_t) xbt_fifo_get_item_content(item); - if(restore_state->system_state != NULL){ + restored_state = (mc_state_t) xbt_fifo_get_item_content(item); + if(restored_state->system_state != NULL){ break; }else{ item = xbt_fifo_get_next_item(item); pos--; } } - MC_restore_snapshot(restore_state->system_state); + MC_restore_snapshot(restored_state->system_state); xbt_fifo_unshift(mc_stack_safety, state); MC_UNSET_RAW_MEM; MC_replay(mc_stack_safety, pos); @@@ -694,11 -733,10 +736,11 @@@ break; } else { req = MC_state_get_internal_request(state); - if(req->call == SIMCALL_COMM_ISEND || req->call == SIMCALL_COMM_IRECV){ - // fprintf(stderr, "Remove state with isend or irecv\n"); - if(!xbt_dynar_is_empty(communications_pattern)) - xbt_dynar_remove_at(communications_pattern, xbt_dynar_length(communications_pattern) - 1, NULL); + if(_sg_mc_comms_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); diff --combined src/mc/mc_global.c index 668bea076b,588ba67183..f92085fc14 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@@ -30,10 -30,10 +30,11 @@@ int _sg_do_model_check = 0 int _sg_mc_checkpoint=0; char* _sg_mc_property_file=NULL; int _sg_mc_timeout=0; + int _sg_mc_hash=0; int _sg_mc_max_depth=1000; int _sg_mc_visited=0; char *_sg_mc_dot_output_file = NULL; +int _sg_mc_comms_determinism=0; int user_max_depth_reached = 0; @@@ -71,6 -71,13 +72,13 @@@ void _mc_cfg_cb_timeout(const char *nam _sg_mc_timeout= xbt_cfg_get_boolean(_sg_cfg_set, name); } + void _mc_cfg_cb_hash(const char *name, int pos) { + if (_sg_cfg_init_status && !_sg_do_model_check) { + xbt_die("You are specifying a value to enable/disable the use of global hash to speedup state comparaison, but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry."); + } + _sg_mc_hash= xbt_cfg_get_boolean(_sg_cfg_set, name); + } + void _mc_cfg_cb_max_depth(const char *name, int pos) { if (_sg_cfg_init_status && !_sg_do_model_check) { xbt_die("You are specifying a max depth value after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry."); @@@ -92,13 -99,6 +100,13 @@@ void _mc_cfg_cb_dot_output(const char * _sg_mc_dot_output_file= xbt_cfg_get_string(_sg_cfg_set, name); } +void _mc_cfg_cb_comms_determinism(const char *name, int pos) { + if (_sg_cfg_init_status && !_sg_do_model_check) { + xbt_die("You are specifying a value to enable/disable the detection of determinism in the communications schemes after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry."); + } + _sg_mc_comms_determinism= xbt_cfg_get_boolean(_sg_cfg_set, name); +} + /* MC global data structures */ mc_state_t mc_current_state = NULL; char mc_replay_mode = FALSE; @@@ -123,8 -123,6 +131,6 @@@ mc_object_info_t mc_libsimgrid_info = N mc_object_info_t mc_binary_info = NULL; /* Ignore mechanism */ - xbt_dynar_t mc_stack_comparison_ignore; - xbt_dynar_t mc_data_bss_comparison_ignore; extern xbt_dynar_t mc_heap_comparison_ignore; extern xbt_dynar_t stacks_areas; @@@ -181,25 -179,155 +187,155 @@@ void dw_variable_free_voidp(void *t) dw_variable_free((dw_variable_t) * (void **) t); } - // object_info + // ***** object_info mc_object_info_t MC_new_object_info(void) { mc_object_info_t res = xbt_new0(s_mc_object_info_t, 1); res->local_variables = xbt_dict_new_homogeneous(NULL); res->global_variables = xbt_dynar_new(sizeof(dw_variable_t), dw_variable_free_voidp); res->types = xbt_dict_new_homogeneous(NULL); + res->types_by_name = xbt_dict_new_homogeneous(NULL); return res; } + void MC_free_object_info(mc_object_info_t* info) { xbt_free(&(*info)->file_name); xbt_dict_free(&(*info)->local_variables); xbt_dynar_free(&(*info)->global_variables); xbt_dict_free(&(*info)->types); + xbt_dict_free(&(*info)->types_by_name); xbt_free(info); + xbt_dynar_free(&(*info)->functions_index); *info = NULL; } + // ***** Helpers + + void* MC_object_base_address(mc_object_info_t info) { + void* result = info->start_exec; + if(info->start_rw!=NULL && result > (void*) info->start_rw) result = info->start_rw; + if(info->start_ro!=NULL && result > (void*) info->start_ro) result = info->start_ro; + return result; + } + + // ***** Functions index + + static int MC_compare_frame_index_items(mc_function_index_item_t a, mc_function_index_item_t b) { + if(a->low_pc < b->low_pc) + return -1; + else if(a->low_pc == b->low_pc) + return 0; + else + return 1; + } + + static void MC_make_functions_index(mc_object_info_t info) { + xbt_dynar_t index = xbt_dynar_new(sizeof(s_mc_function_index_item_t), NULL); + + // Populate the array: + dw_frame_t frame = NULL; + xbt_dict_cursor_t cursor = NULL; + const char* name = NULL; + xbt_dict_foreach(info->local_variables, cursor, name, frame) { + if(frame->low_pc==NULL) + continue; + s_mc_function_index_item_t entry; + entry.low_pc = frame->low_pc; + entry.high_pc = frame->high_pc; + entry.function = frame; + xbt_dynar_push(index, &entry); + } + + mc_function_index_item_t base = (mc_function_index_item_t) xbt_dynar_get_ptr(index, 0); + + // Sort the array by low_pc: + qsort(base, + xbt_dynar_length(index), + sizeof(s_mc_function_index_item_t), + (int (*)(const void *, const void *))MC_compare_frame_index_items); + + info->functions_index = index; + } + + mc_object_info_t MC_ip_find_object_info(void* ip) { + mc_object_info_t infos[2] = { mc_binary_info, mc_libsimgrid_info }; + size_t n = 2; + size_t i; + for(i=0; i!=n; ++i) { + if(ip >= (void*)infos[i]->start_exec && ip <= (void*)infos[i]->end_exec) { + return infos[i]; + } + } + return NULL; + } + + static dw_frame_t MC_find_function_by_ip_and_object(void* ip, mc_object_info_t info) { + xbt_dynar_t dynar = info->functions_index; + mc_function_index_item_t base = (mc_function_index_item_t) xbt_dynar_get_ptr(dynar, 0); + int i = 0; + int j = xbt_dynar_length(dynar) - 1; + while(j>=i) { + int k = i + ((j-i)/2); + if(ip < base[k].low_pc) { + j = k-1; + } else if(ip > base[k].high_pc) { + i = k+1; + } else { + return base[k].function; + } + } + return NULL; + } + + dw_frame_t MC_find_function_by_ip(void* ip) { + mc_object_info_t info = MC_ip_find_object_info(ip); + if(info==NULL) + return NULL; + else + return MC_find_function_by_ip_and_object(ip, info); + } + + static void MC_post_process_variables(mc_object_info_t info) { + unsigned cursor = 0; + dw_variable_t variable = NULL; + xbt_dynar_foreach(info->global_variables, cursor, variable) { + if(variable->type_origin) { + variable->type = xbt_dict_get_or_null(info->types, variable->type_origin); + } + } + } + + static void MC_post_process_functions(mc_object_info_t info) { + xbt_dict_cursor_t cursor = NULL; + char* key = NULL; + dw_frame_t function = NULL; + xbt_dict_foreach(info->local_variables, cursor, key, function) { + unsigned cursor2 = 0; + dw_variable_t variable = NULL; + xbt_dynar_foreach(function->variables, cursor2, variable) { + if(variable->type_origin) { + variable->type = xbt_dict_get_or_null(info->types, variable->type_origin); + } + } + } + } + + /** \brief Finds informations about a given shared object/executable */ + mc_object_info_t MC_find_object_info(memory_map_t maps, char* name, int executable) { + mc_object_info_t result = MC_new_object_info(); + if(executable) + result->flags |= MC_OBJECT_INFO_EXECUTABLE; + result->file_name = xbt_strdup(name); + MC_find_object_address(maps, result); + MC_dwarf_get_variables(result); + MC_post_process_types(result); + MC_post_process_variables(result); + MC_post_process_functions(result); + MC_make_functions_index(result); + return result; + } + /*************************************************************************/ static dw_location_t MC_dwarf_get_location(xbt_dict_t location_list, char *expr){ @@@ -441,6 -569,7 +577,7 @@@ void MC_dwarf_register_variable(mc_obje MC_dwarf_register_non_global_variable(info, frame, variable); } + /******************************* Ignore mechanism *******************************/ /*********************************************************************************/ @@@ -451,10 -580,6 +588,6 @@@ typedef struct s_mc_stack_ignore_variab char *frame; }s_mc_stack_ignore_variable_t, *mc_stack_ignore_variable_t; - typedef struct s_mc_data_bss_ignore_variable{ - char *name; - }s_mc_data_bss_ignore_variable_t, *mc_data_bss_ignore_variable_t; - /**************************** Free functions ******************************/ static void stack_ignore_variable_free(mc_stack_ignore_variable_t v){ @@@ -475,15 -600,6 +608,6 @@@ void heap_ignore_region_free_voidp(voi heap_ignore_region_free((mc_heap_ignore_region_t) * (void **) r); } - static void data_bss_ignore_variable_free(mc_data_bss_ignore_variable_t v){ - xbt_free(v->name); - xbt_free(v); - } - - static void data_bss_ignore_variable_free_voidp(void *v){ - data_bss_ignore_variable_free((mc_data_bss_ignore_variable_t) * (void **) v); - } - static void checkpoint_ignore_region_free(mc_checkpoint_ignore_region_t r){ xbt_free(r); } @@@ -598,7 -714,7 +722,7 @@@ void MC_ignore_global_variable(const ch MC_SET_RAW_MEM; - if(mc_libsimgrid_info){ + xbt_assert(mc_libsimgrid_info, "MC subsystem not initialized"); unsigned int cursor = 0; dw_variable_t current_var; @@@ -618,49 -734,6 +742,6 @@@ end = cursor - 1; } } - - }else{ - - if(mc_data_bss_comparison_ignore == NULL) - mc_data_bss_comparison_ignore = xbt_dynar_new(sizeof(mc_data_bss_ignore_variable_t), data_bss_ignore_variable_free_voidp); - - mc_data_bss_ignore_variable_t var = NULL; - var = xbt_new0(s_mc_data_bss_ignore_variable_t, 1); - var->name = strdup(name); - - if(xbt_dynar_is_empty(mc_data_bss_comparison_ignore)){ - - xbt_dynar_insert_at(mc_data_bss_comparison_ignore, 0, &var); - - }else{ - - unsigned int cursor = 0; - int start = 0; - int end = xbt_dynar_length(mc_data_bss_comparison_ignore) - 1; - mc_data_bss_ignore_variable_t current_var = NULL; - - while(start <= end){ - cursor = (start + end) / 2; - current_var = (mc_data_bss_ignore_variable_t)xbt_dynar_get_as(mc_data_bss_comparison_ignore, cursor, mc_data_bss_ignore_variable_t); - if(strcmp(current_var->name, name) == 0){ - data_bss_ignore_variable_free(var); - if(!raw_mem_set) - MC_UNSET_RAW_MEM; - return; - }else if(strcmp(current_var->name, name) < 0){ - start = cursor + 1; - }else{ - end = cursor - 1; - } - } - - if(strcmp(current_var->name, name) < 0) - xbt_dynar_insert_at(mc_data_bss_comparison_ignore, cursor + 1, &var); - else - xbt_dynar_insert_at(mc_data_bss_comparison_ignore, cursor, &var); - - } - } if(!raw_mem_set) MC_UNSET_RAW_MEM; @@@ -672,7 -745,6 +753,6 @@@ void MC_ignore_local_variable(const cha MC_SET_RAW_MEM; - if(mc_libsimgrid_info){ unsigned int cursor = 0; dw_variable_t current_var; int start, end; @@@ -733,61 -805,6 +813,6 @@@ } } } - }else{ - - if(mc_stack_comparison_ignore == NULL) - mc_stack_comparison_ignore = xbt_dynar_new(sizeof(mc_stack_ignore_variable_t), stack_ignore_variable_free_voidp); - - mc_stack_ignore_variable_t var = NULL; - var = xbt_new0(s_mc_stack_ignore_variable_t, 1); - var->var_name = strdup(var_name); - var->frame = strdup(frame_name); - - if(xbt_dynar_is_empty(mc_stack_comparison_ignore)){ - - xbt_dynar_insert_at(mc_stack_comparison_ignore, 0, &var); - - }else{ - - unsigned int cursor = 0; - int start = 0; - int end = xbt_dynar_length(mc_stack_comparison_ignore) - 1; - mc_stack_ignore_variable_t current_var = NULL; - - while(start <= end){ - cursor = (start + end) / 2; - current_var = (mc_stack_ignore_variable_t)xbt_dynar_get_as(mc_stack_comparison_ignore, cursor, mc_stack_ignore_variable_t); - if(strcmp(current_var->frame, frame_name) == 0){ - if(strcmp(current_var->var_name, var_name) == 0){ - stack_ignore_variable_free(var); - if(!raw_mem_set) - MC_UNSET_RAW_MEM; - return; - }else if(strcmp(current_var->var_name, var_name) < 0){ - start = cursor + 1; - }else{ - end = cursor - 1; - } - }else if(strcmp(current_var->frame, frame_name) < 0){ - start = cursor + 1; - }else{ - end = cursor - 1; - } - } - - if(strcmp(current_var->frame, frame_name) == 0){ - if(strcmp(current_var->var_name, var_name) < 0){ - xbt_dynar_insert_at(mc_stack_comparison_ignore, cursor + 1, &var); - }else{ - xbt_dynar_insert_at(mc_stack_comparison_ignore, cursor, &var); - } - }else if(strcmp(current_var->frame, frame_name) < 0){ - xbt_dynar_insert_at(mc_stack_comparison_ignore, cursor + 1, &var); - }else{ - xbt_dynar_insert_at(mc_stack_comparison_ignore, cursor, &var); - } - } - } if(!raw_mem_set) MC_UNSET_RAW_MEM; @@@ -879,49 -896,30 +904,30 @@@ void MC_ignore(void *addr, size_t size) /******************************* Initialisation of MC *******************************/ /*********************************************************************************/ - static void MC_dump_ignored_local_variables(void){ - - if(mc_stack_comparison_ignore == NULL || xbt_dynar_is_empty(mc_stack_comparison_ignore)) - return; - - unsigned int cursor = 0; - mc_stack_ignore_variable_t current_var; - - xbt_dynar_foreach(mc_stack_comparison_ignore, cursor, current_var){ - MC_ignore_local_variable(current_var->var_name, current_var->frame); + static void MC_post_process_object_info(mc_object_info_t info) { + mc_object_info_t other_info = info == mc_binary_info ? mc_libsimgrid_info : mc_binary_info; + xbt_dict_cursor_t cursor = NULL; + char* key = NULL; + dw_type_t type = NULL; + xbt_dict_foreach(info->types, cursor, key, type){ + if(type->name && type->byte_size == 0) { + type->other_object_same_type = xbt_dict_get_or_null(other_info->types_by_name, type->name); + } } - - xbt_dynar_free(&mc_stack_comparison_ignore); - mc_stack_comparison_ignore = NULL; - } - static void MC_dump_ignored_global_variables(void){ - - if(mc_data_bss_comparison_ignore == NULL || xbt_dynar_is_empty(mc_data_bss_comparison_ignore)) - return; - - unsigned int cursor = 0; - mc_data_bss_ignore_variable_t current_var; - - xbt_dynar_foreach(mc_data_bss_comparison_ignore, cursor, current_var){ - MC_ignore_global_variable(current_var->name); - } - - xbt_dynar_free(&mc_data_bss_comparison_ignore); - mc_data_bss_comparison_ignore = NULL; - - } - - static void MC_init_debug_info(); - static void MC_init_debug_info() { + static void MC_init_debug_info(void) { XBT_INFO("Get debug information ..."); memory_map_t maps = MC_get_memory_map(); /* Get local variables for state equality detection */ - mc_binary_info = MC_find_object_info(maps, xbt_binary_name); - mc_libsimgrid_info = MC_find_object_info(maps, libsimgrid_path); + mc_binary_info = MC_find_object_info(maps, xbt_binary_name, 1); + mc_libsimgrid_info = MC_find_object_info(maps, libsimgrid_path, 0); + + // Use information of the other objects: + MC_post_process_object_info(mc_binary_info); + MC_post_process_object_info(mc_libsimgrid_info); MC_free_memory_map(maps); XBT_INFO("Get debug information done !"); @@@ -941,10 -939,6 +947,6 @@@ void MC_init() MC_init_memory_map_info(); MC_init_debug_info(); - /* Remove variables ignored before getting list of variables */ - MC_dump_ignored_local_variables(); - MC_dump_ignored_global_variables(); - /* Init parmap */ parmap = xbt_parmap_mc_new(xbt_os_get_numcores(), XBT_PARMAP_DEFAULT); @@@ -973,6 -967,7 +975,7 @@@ MC_ignore_global_variable("counter"); /* Static variable used for tracing */ MC_ignore_global_variable("maestro_stack_start"); MC_ignore_global_variable("maestro_stack_end"); + MC_ignore_global_variable("smx_total_comms"); MC_ignore_heap(&(simix_global->process_to_run), sizeof(simix_global->process_to_run)); MC_ignore_heap(&(simix_global->process_that_ran), sizeof(simix_global->process_that_ran)); @@@ -1244,8 -1239,7 +1247,8 @@@ void MC_replay(xbt_fifo_t stack, int st xbt_free(key); } } - xbt_dynar_reset(communications_pattern); + if(_sg_mc_comms_determinism) + xbt_dynar_reset(communications_pattern); MC_UNSET_RAW_MEM; @@@ -1276,23 -1270,20 +1279,23 @@@ } } - if(req->call == SIMCALL_COMM_ISEND) - comm_pattern = 1; - else if(req->call == SIMCALL_COMM_IRECV) + if(_sg_mc_comms_determinism){ + if(req->call == SIMCALL_COMM_ISEND) + comm_pattern = 1; + else if(req->call == SIMCALL_COMM_IRECV) comm_pattern = 2; - + } + SIMIX_simcall_pre(req, value); - MC_SET_RAW_MEM; - if(comm_pattern != 0){ - get_comm_pattern(communications_pattern, req, comm_pattern); + if(_sg_mc_comms_determinism){ + MC_SET_RAW_MEM; + if(comm_pattern != 0){ + get_comm_pattern(communications_pattern, req, comm_pattern); + } + MC_UNSET_RAW_MEM; + comm_pattern = 0; } - MC_UNSET_RAW_MEM; - - comm_pattern = 0; MC_wait_for_requests(); @@@ -1574,9 -1565,9 +1577,9 @@@ void MC_print_statistics(mc_stats_t sta fprintf(dot_output, "}\n"); fclose(dot_output); } - if(initial_state_safety != NULL){ - // XBT_INFO("Communication-deterministic : %s", !initial_state_safety->comm_deterministic ? "No" : "Yes"); - // XBT_INFO("Send-deterministic : %s", !initial_state_safety->send_deterministic ? "No" : "Yes"); + if(initial_state_safety != NULL && _sg_mc_comms_determinism){ + XBT_INFO("Communication-deterministic : %s", !initial_state_safety->comm_deterministic ? "No" : "Yes"); + XBT_INFO("Send-deterministic : %s", !initial_state_safety->send_deterministic ? "No" : "Yes"); } MC_UNSET_RAW_MEM; } diff --combined src/mc/mc_liveness.c index 2ff658db94,ebbb77726d..54f5143d8b --- a/src/mc/mc_liveness.c +++ b/src/mc/mc_liveness.c @@@ -36,6 -36,10 +36,10 @@@ static xbt_dynar_t get_atomic_propositi return values; } + /** \brief Find a suitable subrange of candidate duplicates for a given state + * + * See mc_dpor.c with a similar (same?) function. + */ static int get_search_interval(xbt_dynar_t all_pairs, mc_visited_pair_t pair, int *min, int *max){ int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); @@@ -114,12 -118,15 +118,15 @@@ static mc_visited_pair_t is_reached_acc index = get_search_interval(acceptance_pairs, pair, &min, &max); if(min != -1 && max != -1){ // Acceptance pair with same number of processes and same heap bytes used exists + + // Parallell implementation /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(acceptance_pairs, min), (max-min)+1, pair); if(res != -1){ if(!raw_mem_set) MC_UNSET_RAW_MEM; return ((mc_pair_t)xbt_dynar_get_as(acceptance_pairs, (min+res)-1, mc_pair_t))->num; }*/ + cursor = min; while(cursor <= max){ pair_test = (mc_visited_pair_t)xbt_dynar_get_as(acceptance_pairs, cursor, mc_visited_pair_t); @@@ -192,6 -199,9 +199,9 @@@ static void remove_acceptance_pair(int MC_UNSET_RAW_MEM; } + /** \brief Checks whether a given state has already been visited by the algorithm. + * + */ static int is_visited_pair(mc_visited_pair_t pair, int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions){ if(_sg_mc_visited == 0) @@@ -264,7 -274,7 +274,7 @@@ if(dot_output == NULL) XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", new_pair->num, pair_test->num); else - XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", new_pair->num, pair_test->num, pair->other_num); + XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", new_pair->num, pair_test->num, new_pair->other_num); xbt_dynar_remove_at(visited_pairs, cursor, NULL); xbt_dynar_insert_at(visited_pairs, cursor, &new_pair); pair_test->visited_removed = 1; diff --combined src/simgrid/sg_config.c index 7a1ceb4867,ad88f30f75..4886b39b2e --- a/src/simgrid/sg_config.c +++ b/src/simgrid/sg_config.c @@@ -564,7 -564,7 +564,7 @@@ void sg_config_init(int *argc, char **a /* do stateful model-checking */ xbt_cfg_register(&_sg_cfg_set, "model-check/checkpoint", "Specify the amount of steps between checkpoints during stateful model-checking (default: 0 => stateless verification). " - "If value=on, one checkpoint is saved for each step => faster verification, but huge memory consumption; higher values are good compromises between speed and memory consumption.", + "If value=1, one checkpoint is saved for each step => faster verification, but huge memory consumption; higher values are good compromises between speed and memory consumption.", xbt_cfgelm_int, 0, 1, _mc_cfg_cb_checkpoint, NULL); xbt_cfg_setdefault_int(_sg_cfg_set, "model-check/checkpoint", 0); @@@ -574,12 -574,6 +574,12 @@@ xbt_cfgelm_string, 0, 1, _mc_cfg_cb_property, NULL); xbt_cfg_setdefault_string(_sg_cfg_set, "model-check/property", ""); + /* do determinism model-checking */ + xbt_cfg_register(&_sg_cfg_set, "model-check/communications_determinism", + "Enable/disable the detection of determinism in the communications schemes", + xbt_cfgelm_boolean, 0, 1, _mc_cfg_cb_comms_determinism, NULL); + xbt_cfg_setdefault_boolean(_sg_cfg_set, "model-check/communications_determinism", "no"); + /* Specify the kind of model-checking reduction */ xbt_cfg_register(&_sg_cfg_set, "model-check/reduction", "Specify the kind of exploration reduction (either none or DPOR)", @@@ -592,6 -586,12 +592,12 @@@ xbt_cfgelm_boolean, 0, 1, _mc_cfg_cb_timeout, NULL); xbt_cfg_setdefault_boolean(_sg_cfg_set, "model-check/timeout", "no"); + /* Enable/disable global hash computation with model-checking */ + xbt_cfg_register(&_sg_cfg_set, "model-check/hash", + "Enable/Disable state hash for state comparison", + xbt_cfgelm_boolean, 0, 1, _mc_cfg_cb_hash, NULL); + xbt_cfg_setdefault_boolean(_sg_cfg_set, "model-check/hash", "no"); + /* Set max depth exploration */ xbt_cfg_register(&_sg_cfg_set, "model-check/max_depth", "Specify the max depth of exploration (default : 1000)", diff --combined src/simix/smx_network.c index 1ca73e5e6b,428ef6af6a..1068eeff26 --- a/src/simix/smx_network.c +++ b/src/simix/smx_network.c @@@ -31,8 -31,6 +31,6 @@@ static void SIMIX_comm_start(smx_action void SIMIX_network_init(void) { rdv_points = xbt_dict_new_homogeneous(SIMIX_rdv_free); - if(MC_is_active()) - MC_ignore_global_variable("smx_total_comms"); } void SIMIX_network_exit(void) @@@ -445,7 -443,7 +443,7 @@@ smx_action_t SIMIX_comm_isend(smx_proce if (MC_is_active()) { other_action->state = SIMIX_RUNNING; - return other_action; + return (detached ? NULL : other_action); } SIMIX_comm_start(other_action);