X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/de2ba1766285962d449105925be099707e0102e6..d0c5cc5a4f87a98928093830eab689dcdd0dd603:/src/mc/mc_global.c?ds=sidebyside diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index 02600ef677..ae9f437c1d 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -63,19 +63,34 @@ void _mc_cfg_cb_timeout(const char *name, int pos) { xbt_cfg_set_int(_surf_cfg_set,"model-check",1); } +void _mc_cfg_cb_max_depth(const char *name, int pos) { + if (_surf_init_status && !_surf_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."); + } + _surf_mc_max_depth= xbt_cfg_get_int(_surf_cfg_set, name); + xbt_cfg_set_int(_surf_cfg_set,"model-check",1); +} + +void _mc_cfg_cb_stateful(const char *name, int pos) { + if (_surf_init_status && !_surf_do_model_check) { + xbt_die("You are trying to change stateful mode 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."); + } + _surf_mc_stateful= xbt_cfg_get_int(_surf_cfg_set, name); + xbt_cfg_set_int(_surf_cfg_set,"model-check",1); +} + /* MC global data structures */ mc_state_t mc_current_state = NULL; char mc_replay_mode = FALSE; double *mc_time = NULL; -mc_snapshot_t initial_snapshot = NULL; -int raw_mem_set; /* Safety */ xbt_fifo_t mc_stack_safety = NULL; mc_stats_t mc_stats = NULL; +mc_global_t initial_state_safety = NULL; /* Liveness */ @@ -107,7 +122,7 @@ void MC_do_the_modelcheck_for_real() { mc_reduce_kind=e_mc_reduce_dpor; XBT_INFO("Check a safety property"); - MC_modelcheck(); + MC_modelcheck_safety(); } else { @@ -120,62 +135,14 @@ void MC_do_the_modelcheck_for_real() { } } -/** - * \brief Initialize the model-checker data structures - */ -void MC_init_safety(void) -{ - - raw_mem_set = (mmalloc_get_current_heap() == raw_heap); - - /* Check if MC is already initialized */ - if (initial_snapshot) - return; - - mc_time = xbt_new0(double, simix_process_maxpid); - - /* Initialize the data structures that must be persistent across every - iteration of the model-checker (in RAW memory) */ - - MC_SET_RAW_MEM; - - /* Initialize statistics */ - mc_stats = xbt_new0(s_mc_stats_t, 1); - mc_stats->state_size = 1; - - /* Create exploration stack */ - mc_stack_safety = xbt_fifo_new(); - - MC_UNSET_RAW_MEM; - - MC_dpor_init(); - - MC_SET_RAW_MEM; - /* Save the initial state */ - initial_snapshot = xbt_new0(s_mc_snapshot_t, 1); - MC_take_snapshot(initial_snapshot); - MC_UNSET_RAW_MEM; - - if(raw_mem_set) - MC_SET_RAW_MEM; - -} void MC_compare(void){ compare = 1; } +void MC_init(){ -void MC_modelcheck(void) -{ - MC_init_safety(); - MC_dpor(); - MC_exit(); -} - -void MC_init_liveness(){ - - raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); mc_time = xbt_new0(double, simix_process_maxpid); @@ -203,15 +170,6 @@ void MC_init_liveness(){ xbt_dict_t libsimgrid_location_list = MC_get_location_list(ls_path); MC_get_local_variables(ls_path, libsimgrid_location_list, &mc_local_variables); - initial_state_liveness = xbt_new0(s_mc_global_t, 1); - initial_state_liveness->snapshot_comparison_times = xbt_dynar_new(sizeof(double), NULL); - initial_state_liveness->chunks_used_comparison_times = xbt_dynar_new(sizeof(double), NULL); - initial_state_liveness->stacks_sizes_comparison_times = xbt_dynar_new(sizeof(double), NULL); - initial_state_liveness->program_data_segment_comparison_times = xbt_dynar_new(sizeof(double), NULL); - initial_state_liveness->libsimgrid_data_segment_comparison_times = xbt_dynar_new(sizeof(double), NULL); - initial_state_liveness->heap_comparison_times = xbt_dynar_new(sizeof(double), NULL); - initial_state_liveness->stacks_comparison_times = xbt_dynar_new(sizeof(double), NULL); - MC_UNSET_RAW_MEM; MC_init_memory_map_info(); @@ -220,27 +178,86 @@ void MC_init_liveness(){ get_libsimgrid_plt_section(); get_binary_plt_section(); + /* Ignore some variables from xbt/ex.h used by exception e for stacks comparison */ + MC_ignore_stack("e", "*"); + MC_ignore_stack("__ex_cleanup", "*"); + MC_ignore_stack("__ex_mctx_en", "*"); + MC_ignore_stack("__ex_mctx_me", "*"); + MC_ignore_stack("_log_ev", "*"); + MC_ignore_stack("_throw_ctx", "*"); + MC_ignore_stack("ctx", "*"); + + + if(raw_mem_set) + MC_SET_RAW_MEM; + +} + +void MC_modelcheck_safety(void) +{ + int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + + /* Check if MC is already initialized */ + if (initial_state_safety) + return; + + mc_time = xbt_new0(double, simix_process_maxpid); + + /* Initialize the data structures that must be persistent across every + iteration of the model-checker (in RAW memory) */ + + MC_SET_RAW_MEM; + + /* Initialize statistics */ + mc_stats = xbt_new0(s_mc_stats_t, 1); + mc_stats->state_size = 1; + + /* Create exploration stack */ + mc_stack_safety = xbt_fifo_new(); + + MC_UNSET_RAW_MEM; + + if(_surf_mc_stateful > 0){ + MC_init(); + }else{ + MC_init_memory_map_info(); + get_libsimgrid_plt_section(); + get_binary_plt_section(); + } + + MC_dpor_init(); + + MC_SET_RAW_MEM; + /* Save the initial state */ + initial_state_safety = xbt_new0(s_mc_global_t, 1); + initial_state_safety->snapshot = MC_take_snapshot(); + //MC_take_snapshot(initial_snapshot); + MC_UNSET_RAW_MEM; + if(raw_mem_set) MC_SET_RAW_MEM; + MC_dpor(); + + MC_exit(); } void MC_modelcheck_liveness(){ - raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); - MC_init_liveness(); + MC_init(); MC_SET_RAW_MEM; /* Initialize statistics */ mc_stats_pair = xbt_new0(s_mc_stats_pair_t, 1); - XBT_DEBUG("Creating stack"); - /* Create exploration stack */ mc_stack_liveness = xbt_fifo_new(); + initial_state_liveness = xbt_new0(s_mc_global_t, 1); + MC_UNSET_RAW_MEM; MC_ddfs_init(); @@ -249,6 +266,9 @@ void MC_modelcheck_liveness(){ MC_print_statistics_pairs(mc_stats_pair); xbt_free(mc_time); + if(raw_mem_set) + MC_SET_RAW_MEM; + } @@ -322,7 +342,7 @@ void MC_replay(xbt_fifo_t stack, int start) if(start == -1){ /* Restore the initial state */ - MC_restore_snapshot(initial_snapshot); + MC_restore_snapshot(initial_state_safety->snapshot); /* At the moment of taking the snapshot the raw heap was set, so restoring * it will set it back again, we have to unset it to continue */ MC_UNSET_RAW_MEM; @@ -377,7 +397,7 @@ void MC_replay(xbt_fifo_t stack, int start) void MC_replay_liveness(xbt_fifo_t stack, int all_stack) { - int raw_mem = (mmalloc_get_current_heap() == raw_heap); + initial_state_liveness->raw_mem_set = (mmalloc_get_current_heap() == raw_heap); int value; char *req_str; @@ -390,11 +410,12 @@ void MC_replay_liveness(xbt_fifo_t stack, int all_stack) XBT_DEBUG("**** Begin Replay ****"); /* Restore the initial state */ - MC_restore_snapshot(initial_state_liveness->initial_snapshot); + MC_restore_snapshot(initial_state_liveness->snapshot); + /* At the moment of taking the snapshot the raw heap was set, so restoring * it will set it back again, we have to unset it to continue */ - - MC_UNSET_RAW_MEM; + if(!initial_state_liveness->raw_mem_set) + MC_UNSET_RAW_MEM; if(all_stack){ @@ -480,7 +501,7 @@ void MC_replay_liveness(xbt_fifo_t stack, int all_stack) XBT_DEBUG("**** End Replay ****"); - if(raw_mem) + if(initial_state_liveness->raw_mem_set) MC_SET_RAW_MEM; else MC_UNSET_RAW_MEM; @@ -495,7 +516,7 @@ void MC_replay_liveness(xbt_fifo_t stack, int all_stack) void MC_dump_stack_safety(xbt_fifo_t stack) { - raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); MC_show_stack_safety(stack); @@ -578,7 +599,7 @@ void MC_show_stack_liveness(xbt_fifo_t stack){ void MC_dump_stack_liveness(xbt_fifo_t stack){ - raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); mc_pair_stateless_t pair; @@ -662,7 +683,7 @@ double MC_process_clock_get(smx_process_t process) void MC_automaton_load(const char *file){ - raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); MC_SET_RAW_MEM; @@ -680,7 +701,7 @@ void MC_automaton_load(const char *file){ void MC_automaton_new_propositional_symbol(const char* id, void* fct) { - raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); MC_SET_RAW_MEM; @@ -700,7 +721,7 @@ void MC_automaton_new_propositional_symbol(const char* id, void* fct) { void MC_ignore_heap(void *address, size_t size){ - raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); MC_SET_RAW_MEM; @@ -741,7 +762,7 @@ void MC_ignore_heap(void *address, size_t size){ void MC_ignore_data_bss(void *address, size_t size){ - raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); MC_SET_RAW_MEM; @@ -784,7 +805,7 @@ void MC_ignore_data_bss(void *address, size_t size){ var->address = address; var->size = size; - if(current_var->address > address) + if(current_var->address < address) xbt_dynar_insert_at(mc_data_bss_comparison_ignore, cursor + 1, &var); else xbt_dynar_insert_at(mc_data_bss_comparison_ignore, cursor, &var); @@ -799,7 +820,7 @@ void MC_ignore_data_bss(void *address, size_t size){ void MC_ignore_stack(const char *var_name, const char *frame){ - raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); MC_SET_RAW_MEM; @@ -864,7 +885,7 @@ void MC_ignore_stack(const char *var_name, const char *frame){ void MC_new_stack_area(void *stack, char *name, void* context, size_t size){ - raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); MC_SET_RAW_MEM; if(stacks_areas == NULL)