From: Marion Guthmuller Date: Mon, 12 Aug 2013 17:35:02 +0000 (+0200) Subject: model-checker : extend ignore mechanism with new user primitive MC_ignore X-Git-Tag: v3_9_90~128^2~16 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/50376f845bf79ba752eb226efdeb2a46b2ff88cf model-checker : extend ignore mechanism with new user primitive MC_ignore --- diff --git a/include/simgrid/modelchecker.h b/include/simgrid/modelchecker.h index 376ab927a7..fae8a40498 100644 --- a/include/simgrid/modelchecker.h +++ b/include/simgrid/modelchecker.h @@ -26,6 +26,7 @@ XBT_PUBLIC(void) MC_automaton_new_propositional_symbol(const char* id, void* fct XBT_PUBLIC(void *) MC_snapshot(void); XBT_PUBLIC(int) MC_compare_snapshots(void *s1, void *s2); XBT_PUBLIC(void) MC_cut(void); +XBT_PUBLIC(void) MC_ignore(void *addr, size_t size); #else diff --git a/src/include/mc/mc.h b/src/include/mc/mc.h index 6432098c3e..0fd382658e 100644 --- a/src/include/mc/mc.h +++ b/src/include/mc/mc.h @@ -56,8 +56,8 @@ void MC_automaton_load(const char *file); /****************************** MC ignore **********************************/ XBT_PUBLIC(void) MC_ignore_heap(void *address, size_t size); XBT_PUBLIC(void) MC_remove_ignore_heap(void *address, size_t size); -XBT_PUBLIC(void) MC_ignore_local_variable(const char *var_name, const char *frame, ...); -XBT_PUBLIC(void) MC_ignore_global_variable(const char *var_name, ...); +XBT_PUBLIC(void) MC_ignore_local_variable(const char *var_name, const char *frame); +XBT_PUBLIC(void) MC_ignore_global_variable(const char *var_name); void MC_new_stack_area(void *stack, char *name, void *context, size_t size); /********************************* Memory *************************************/ diff --git a/src/mc/mc_checkpoint.c b/src/mc/mc_checkpoint.c index ce65e39336..30dfc176d3 100644 --- a/src/mc/mc_checkpoint.c +++ b/src/mc/mc_checkpoint.c @@ -689,6 +689,24 @@ static xbt_dynar_t MC_take_snapshot_ignore(){ } +static void MC_dump_checkpoint_ignore(mc_snapshot_t snapshot){ + + unsigned int cursor = 0; + mc_checkpoint_ignore_region_t region; + size_t offset; + + xbt_dynar_foreach(mc_checkpoint_ignore, cursor, region){ + if(region->addr > snapshot->regions[0]->start_addr && (char *)(region->addr) < (char *)snapshot->regions[0]->start_addr + STD_HEAP_SIZE){ + offset = (char *)region->addr - (char *)snapshot->regions[0]->start_addr; + memset((char *)snapshot->regions[0]->start_addr + offset, 0, region->size); + }else if(region->addr > snapshot->regions[2]->start_addr && (char *)(region->addr) < (char*)snapshot->regions[2]->start_addr + snapshot->regions[2]->size){ + offset = (char *)region->addr - (char *)snapshot->regions[2]->start_addr; + memset((char *)snapshot->regions[2]->start_addr + offset, 0, region->size); + } + } + +} + mc_snapshot_t MC_take_snapshot(){ @@ -710,6 +728,8 @@ mc_snapshot_t MC_take_snapshot(){ //MC_get_hash_local(snapshot->hash_local, snapshot->stacks); } + MC_dump_checkpoint_ignore(snapshot); + MC_UNSET_RAW_MEM; if(raw_mem) diff --git a/src/mc/mc_compare.c b/src/mc/mc_compare.c index 5d8ac72471..083710abc1 100644 --- a/src/mc/mc_compare.c +++ b/src/mc/mc_compare.c @@ -221,7 +221,7 @@ static int compare_global_variables(int region_type, mc_mem_region_t r1, mc_mem_ if(!compared_pointers){ compared_pointers = xbt_dynar_new(sizeof(pointers_pair_t), NULL); - MC_ignore_global_variable("compared_pointers", 1); + MC_ignore_global_variable("compared_pointers"); }else{ xbt_dynar_reset(compared_pointers); } @@ -270,7 +270,7 @@ static int compare_local_variables(mc_snapshot_stack_t stack1, mc_snapshot_stack if(!compared_pointers){ compared_pointers = xbt_dynar_new(sizeof(pointers_pair_t), NULL); - MC_ignore_global_variable("compared_pointers", 1); + MC_ignore_global_variable("compared_pointers"); }else{ xbt_dynar_reset(compared_pointers); } @@ -621,7 +621,7 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){ int MC_compare_snapshots(void *s1, void *s2){ - MC_ignore_local_variable("self", "simcall_BODY_mc_snapshot", 1); + MC_ignore_local_variable("self", "simcall_BODY_mc_snapshot"); return simcall_mc_compare_snapshots(s1, s2); diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index 328a69dd8b..68a564cdaf 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -1221,14 +1221,14 @@ static void MC_dwarf_get_variables(const char *elf_file, xbt_dict_t location_lis /******************************* Ignore mechanism *******************************/ /*********************************************************************************/ +xbt_dynar_t mc_checkpoint_ignore; + typedef struct s_mc_stack_ignore_variable{ - int in_libsimgrid; char *var_name; char *frame; }s_mc_stack_ignore_variable_t, *mc_stack_ignore_variable_t; typedef struct s_mc_data_bss_ignore_variable{ - int in_libsimgrid; char *name; }s_mc_data_bss_ignore_variable_t, *mc_data_bss_ignore_variable_t; @@ -1261,6 +1261,14 @@ 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); +} + +static void checkpoint_ignore_region_free_voidp(void *r){ + checkpoint_ignore_region_free((mc_checkpoint_ignore_region_t) * (void **) r); +} + /***********************************************************************/ void MC_ignore_heap(void *address, size_t size){ @@ -1365,39 +1373,27 @@ void MC_remove_ignore_heap(void *address, size_t size){ } -void MC_ignore_global_variable(const char *name, ...){ +void MC_ignore_global_variable(const char *name){ int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); MC_SET_RAW_MEM; - va_list ap; - va_start(ap, name); - int in_libsimgrid = va_arg(ap, int); - va_end(ap); - - xbt_dynar_t variables = NULL; - - if(in_libsimgrid == 1){ - variables = mc_global_variables_libsimgrid; - }else{ - variables = mc_global_variables_binary; - } - - if(variables){ + if(mc_global_variables_libsimgrid){ unsigned int cursor = 0; dw_variable_t current_var; int start = 0; - int end = xbt_dynar_length(variables) - 1; + int end = xbt_dynar_length(mc_global_variables_libsimgrid) - 1; int var_found; while(start <= end){ cursor = (start + end) /2; - current_var = (dw_variable_t)xbt_dynar_get_as(variables, cursor, dw_variable_t); + current_var = (dw_variable_t)xbt_dynar_get_as(mc_global_variables_libsimgrid, cursor, dw_variable_t); if(strcmp(current_var->name, name) == 0){ - xbt_dynar_remove_at(variables, cursor, NULL); - var_found = 1; + xbt_dynar_remove_at(mc_global_variables_libsimgrid, cursor, NULL); + start = 0; + end = xbt_dynar_length(mc_global_variables_libsimgrid) - 1; break; }else if(strcmp(current_var->name, name) < 0){ start = cursor + 1; @@ -1405,14 +1401,7 @@ void MC_ignore_global_variable(const char *name, ...){ end = cursor - 1; } } - - if(var_found){ - if(in_libsimgrid == 1) - MC_ignore_global_variable(name, 1); - else - MC_ignore_global_variable(name); - } - + }else{ if(mc_data_bss_comparison_ignore == NULL) @@ -1421,7 +1410,6 @@ void MC_ignore_global_variable(const char *name, ...){ mc_data_bss_ignore_variable_t var = NULL; var = xbt_new0(s_mc_data_bss_ignore_variable_t, 1); var->name = strdup(name); - var->in_libsimgrid = (in_libsimgrid == 1); if(xbt_dynar_is_empty(mc_data_bss_comparison_ignore)){ @@ -1463,31 +1451,18 @@ void MC_ignore_global_variable(const char *name, ...){ MC_SET_RAW_MEM; } -void MC_ignore_local_variable(const char *var_name, const char *frame_name, ...){ +void MC_ignore_local_variable(const char *var_name, const char *frame_name){ int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); MC_SET_RAW_MEM; - va_list ap; - va_start(ap, frame_name); - int in_libsimgrid = va_arg(ap, int); - va_end(ap); - - xbt_dict_t variables = NULL; - - if(in_libsimgrid == 1){ - variables = mc_local_variables_libsimgrid; - }else{ - variables = mc_local_variables_binary; - } - - if(variables){ + if(mc_local_variables_libsimgrid){ unsigned int cursor = 0; dw_variable_t current_var; int start, end; - if(strcmp(frame_name, "*") == 0){ /* Remove variable in all frames (binary and libsimgrid) */ - xbt_dict_cursor_t dict_cursor, dict_cursor2; + if(strcmp(frame_name, "*") == 0){ /* Remove variable in all frames */ + xbt_dict_cursor_t dict_cursor; char *current_frame_name; dw_frame_t frame; xbt_dict_foreach(mc_local_variables_libsimgrid, dict_cursor, current_frame_name, frame){ @@ -1495,24 +1470,7 @@ void MC_ignore_local_variable(const char *var_name, const char *frame_name, ...) end = xbt_dynar_length(frame->variables) - 1; while(start <= end){ cursor = (start + end) / 2; - current_var = (dw_variable_t)xbt_dynar_get_as(frame->variables, cursor, dw_variable_t); - if(strcmp(current_var->name, var_name) == 0){ - xbt_dynar_remove_at(frame->variables, cursor, NULL); - start = 0; - end = xbt_dynar_length(frame->variables) - 1; - }else if(strcmp(current_var->name, var_name) < 0){ - start = cursor + 1; - }else{ - end = cursor - 1; - } - } - } - xbt_dict_foreach(mc_local_variables_binary, dict_cursor2, current_frame_name, frame){ - start = 0; - end = xbt_dynar_length(frame->variables) - 1; - while(start <= end){ - cursor = (start + end) / 2; - current_var = (dw_variable_t)xbt_dynar_get_as(frame->variables, cursor, dw_variable_t); + current_var = (dw_variable_t)xbt_dynar_get_as(frame->variables, cursor, dw_variable_t); if(strcmp(current_var->name, var_name) == 0){ xbt_dynar_remove_at(frame->variables, cursor, NULL); start = 0; @@ -1525,7 +1483,7 @@ void MC_ignore_local_variable(const char *var_name, const char *frame_name, ...) } } }else{ - xbt_dynar_t variables_list = ((dw_frame_t)xbt_dict_get_or_null(variables, frame_name))->variables; + xbt_dynar_t variables_list = ((dw_frame_t)xbt_dict_get_or_null(mc_local_variables_libsimgrid, frame_name))->variables; start = 0; end = xbt_dynar_length(variables_list) - 1; while(start <= end){ @@ -1549,7 +1507,6 @@ void MC_ignore_local_variable(const char *var_name, const char *frame_name, ...) mc_stack_ignore_variable_t var = NULL; var = xbt_new0(s_mc_stack_ignore_variable_t, 1); - var->in_libsimgrid = (in_libsimgrid == 1); var->var_name = strdup(var_name); var->frame = strdup(frame_name); @@ -1623,6 +1580,25 @@ void MC_new_stack_area(void *stack, char *name, void* context, size_t size){ MC_SET_RAW_MEM; } +void MC_ignore(void *addr, size_t size){ + + int raw_mem_set= (mmalloc_get_current_heap() == raw_heap); + + MC_SET_RAW_MEM; + + if(mc_checkpoint_ignore == NULL) + mc_checkpoint_ignore = xbt_dynar_new(sizeof(mc_checkpoint_ignore_region_t), checkpoint_ignore_region_free_voidp); + + mc_checkpoint_ignore_region_t region = xbt_new0(s_mc_checkpoint_ignore_region_t, 1); + region->addr = addr; + region->size = size; + + xbt_dynar_push(mc_checkpoint_ignore, ®ion); + + if(!raw_mem_set) + MC_UNSET_RAW_MEM; +} + /******************************* Initialisation of MC *******************************/ /*********************************************************************************/ @@ -1633,59 +1609,9 @@ static void MC_dump_ignored_local_variables(void){ unsigned int cursor = 0; mc_stack_ignore_variable_t current_var; - xbt_dict_t variables; xbt_dynar_foreach(mc_stack_comparison_ignore, cursor, current_var){ - - if(current_var->in_libsimgrid == 1){ - variables = mc_local_variables_libsimgrid; - }else{ - variables = mc_local_variables_binary; - } - - unsigned int cursor2 = 0; - dw_variable_t var; - int start, end; - - if(strcmp(current_var->frame, "*") == 0){ - xbt_dict_cursor_t dict_cursor; - char *frame_name; - dw_frame_t frame; - xbt_dict_foreach(variables, dict_cursor, frame_name, frame){ - start = 0; - end = xbt_dynar_length(frame->variables) - 1; - while(start <= end){ - cursor2 = (start + end) / 2; - var = (dw_variable_t)xbt_dynar_get_as(frame->variables, cursor2, dw_variable_t); - if(strcmp(var->name, current_var->var_name) == 0){ - xbt_dynar_remove_at(frame->variables, cursor2, NULL); - start = 0; - end = xbt_dynar_length(frame->variables) - 1; - }else if(strcmp(var->name, current_var->var_name) < 0){ - start = cursor2 + 1; - }else{ - end = cursor2 - 1; - } - } - } - }else{ - xbt_dynar_t variables_list = ((dw_frame_t)xbt_dict_get_or_null(variables, current_var->frame))->variables; - start = 0; - end = xbt_dynar_length(variables_list) - 1; - while(start <= end){ - cursor2 = (start + end) / 2; - var = (dw_variable_t)xbt_dynar_get_as(variables_list, cursor2, dw_variable_t); - if(strcmp(var->name, current_var->var_name) == 0){ - xbt_dynar_remove_at(variables_list, cursor2, NULL); - start = 0; - end = xbt_dynar_length(variables_list) - 1; - }else if(strcmp(var->name, current_var->var_name) < 0){ - start = cursor2 + 1; - }else{ - end = cursor2 - 1; - } - } - } + MC_ignore_local_variable(current_var->var_name, current_var->frame); } xbt_dynar_free(&mc_stack_comparison_ignore); @@ -1700,41 +1626,13 @@ static void MC_dump_ignored_global_variables(void){ unsigned int cursor = 0; mc_data_bss_ignore_variable_t current_var; - xbt_dynar_t variables; - - unsigned int cursor2 = 0; - dw_variable_t var; - int start, end; xbt_dynar_foreach(mc_data_bss_comparison_ignore, cursor, current_var){ - - if(current_var->in_libsimgrid == 1){ - variables = mc_global_variables_libsimgrid; - }else{ - variables = mc_global_variables_binary; - } - - cursor2 = 0; - start = 0; - end = xbt_dynar_length(variables) - 1; - - while(start <= end){ - cursor2 = (start + end) / 2; - var = (dw_variable_t)xbt_dynar_get_as(variables, cursor2, dw_variable_t); - if(strcmp(var->name, current_var->name) == 0){ - xbt_dynar_remove_at(variables, cursor2, NULL); - return; - }else if(strcmp(var->name, current_var->name) < 0){ - start = cursor2 + 1; - }else{ - end = cursor2 - 1; - } - } + MC_ignore_global_variable(current_var->name); } xbt_dynar_free(&mc_data_bss_comparison_ignore); mc_data_bss_comparison_ignore = NULL; - } @@ -1771,6 +1669,8 @@ void MC_init(){ xbt_dict_free(&libsimgrid_location_list); xbt_dict_free(&binary_location_list); + XBT_INFO("Get debug information done !"); + /* Remove variables ignored before getting list of variables */ MC_dump_ignored_local_variables(); MC_dump_ignored_global_variables(); @@ -1783,34 +1683,32 @@ void MC_init(){ /* Ignore some variables from xbt/ex.h used by exception e for stacks comparison */ MC_ignore_local_variable("e", "*"); - MC_ignore_local_variable("__ex_cleanup", "*", 1); - MC_ignore_local_variable("__ex_mctx_en", "*", 1); - MC_ignore_local_variable("__ex_mctx_me", "*", 1); - MC_ignore_local_variable("__xbt_ex_ctx_ptr", "*", 1); - MC_ignore_local_variable("_log_ev", "*", 1); - MC_ignore_local_variable("_throw_ctx", "*", 1); - MC_ignore_local_variable("ctx", "*", 1); + MC_ignore_local_variable("__ex_cleanup", "*"); + MC_ignore_local_variable("__ex_mctx_en", "*"); + MC_ignore_local_variable("__ex_mctx_me", "*"); + MC_ignore_local_variable("__xbt_ex_ctx_ptr", "*"); + MC_ignore_local_variable("_log_ev", "*"); + MC_ignore_local_variable("_throw_ctx", "*"); + MC_ignore_local_variable("ctx", "*"); - MC_ignore_local_variable("next_context", "smx_ctx_sysv_suspend_serial", 1); - MC_ignore_local_variable("i", "smx_ctx_sysv_suspend_serial", 1); + MC_ignore_local_variable("next_context", "smx_ctx_sysv_suspend_serial"); + MC_ignore_local_variable("i", "smx_ctx_sysv_suspend_serial"); /* Ignore local variable about time used for tracing */ - MC_ignore_local_variable("start_time", "*", 1); + MC_ignore_local_variable("start_time", "*"); - MC_ignore_global_variable("mc_comp_times", 1); - MC_ignore_global_variable("mc_snapshot_comparison_time", 1); - MC_ignore_global_variable("mc_time", 1); - MC_ignore_global_variable("smpi_current_rank", 1); - MC_ignore_global_variable("smx_current_context_serial", 1); - MC_ignore_global_variable("smx_current_context_key", 1); - MC_ignore_global_variable("sysv_maestro_context", 1); - MC_ignore_global_variable("counter", 1); /* Static variable used for tracing */ + MC_ignore_global_variable("mc_comp_times"); + MC_ignore_global_variable("mc_snapshot_comparison_time"); + MC_ignore_global_variable("mc_time"); + MC_ignore_global_variable("smpi_current_rank"); + MC_ignore_global_variable("smx_current_context_serial"); + MC_ignore_global_variable("smx_current_context_key"); + MC_ignore_global_variable("sysv_maestro_context"); + MC_ignore_global_variable("counter"); /* Static variable used for tracing */ if(raw_mem_set) MC_SET_RAW_MEM; - XBT_INFO("Get debug information done !"); - } static void MC_init_dot_output(){ /* FIXME : more colors */ diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h index 5d297e23ad..b460411f9a 100644 --- a/src/mc/mc_private.h +++ b/src/mc/mc_private.h @@ -58,11 +58,18 @@ typedef struct s_mc_global_t{ char *prev_req; }s_mc_global_t, *mc_global_t; +typedef struct s_mc_checkpoint_ignore_region{ + void *addr; + size_t size; +}s_mc_checkpoint_ignore_region_t, *mc_checkpoint_ignore_region_t; + mc_snapshot_t SIMIX_pre_mc_snapshot(smx_simcall_t simcall); mc_snapshot_t MC_take_snapshot(void); void MC_restore_snapshot(mc_snapshot_t); void MC_free_snapshot(mc_snapshot_t); +extern xbt_dynar_t mc_checkpoint_ignore; + /********************************* MC Global **********************************/ extern double *mc_time; diff --git a/src/simix/smx_network.c b/src/simix/smx_network.c index d51abb9adf..f8f4ffe649 100644 --- a/src/simix/smx_network.c +++ b/src/simix/smx_network.c @@ -31,7 +31,7 @@ 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", 1); + MC_ignore_global_variable("smx_total_comms"); } void SIMIX_network_exit(void) diff --git a/src/xbt/mmalloc/mm_diff.c b/src/xbt/mmalloc/mm_diff.c index 89e1c04879..52896d9526 100644 --- a/src/xbt/mmalloc/mm_diff.c +++ b/src/xbt/mmalloc/mm_diff.c @@ -320,16 +320,16 @@ void init_heap_information(xbt_mheap_t heap1, xbt_mheap_t heap2, xbt_dynar_t i1, to_ignore2 = i2; if(MC_is_active()){ - MC_ignore_global_variable("heaplimit", 1); - MC_ignore_global_variable("s_heap", 1); - MC_ignore_global_variable("heapbase1", 1); - MC_ignore_global_variable("heapbase2", 1); - MC_ignore_global_variable("heapinfo1", 1); - MC_ignore_global_variable("heapinfo2", 1); - MC_ignore_global_variable("heapsize1", 1); - MC_ignore_global_variable("heapsize2", 1); - MC_ignore_global_variable("to_ignore1", 1); - MC_ignore_global_variable("to_ignore2", 1); + MC_ignore_global_variable("heaplimit"); + MC_ignore_global_variable("s_heap"); + MC_ignore_global_variable("heapbase1"); + MC_ignore_global_variable("heapbase2"); + MC_ignore_global_variable("heapinfo1"); + MC_ignore_global_variable("heapinfo2"); + MC_ignore_global_variable("heapsize1"); + MC_ignore_global_variable("heapsize2"); + MC_ignore_global_variable("to_ignore1"); + MC_ignore_global_variable("to_ignore2"); } }