From fcba745e5cc75f24b063641b26fd0fc03bf697e3 Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Thu, 15 Nov 2012 17:27:01 +0100 Subject: [PATCH] model-checker : cleanups in verification of current heap --- src/mc/mc_checkpoint.c | 8 ++++---- src/mc/mc_compare.c | 20 +++++++++++--------- src/mc/mc_dpor.c | 12 ++---------- src/mc/mc_global.c | 37 ++++++++++++++++++++----------------- src/mc/mc_liveness.c | 20 ++++++++++---------- src/mc/mc_private.h | 5 ++--- 6 files changed, 49 insertions(+), 53 deletions(-) diff --git a/src/mc/mc_checkpoint.c b/src/mc/mc_checkpoint.c index e9830d5138..c3e8bfac0c 100644 --- a/src/mc/mc_checkpoint.c +++ b/src/mc/mc_checkpoint.c @@ -115,7 +115,7 @@ void MC_take_snapshot(mc_snapshot_t snapshot) void MC_init_memory_map_info(){ - raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); MC_SET_RAW_MEM; @@ -174,8 +174,8 @@ void MC_init_memory_map_info(){ mc_snapshot_t MC_take_snapshot_liveness() { - raw_mem_set = (mmalloc_get_current_heap() == raw_heap); - + int raw_mem = (mmalloc_get_current_heap() == raw_heap); + MC_SET_RAW_MEM; mc_snapshot_t snapshot = xbt_new0(s_mc_snapshot_t, 1); @@ -251,7 +251,7 @@ mc_snapshot_t MC_take_snapshot_liveness() MC_UNSET_RAW_MEM; - if(raw_mem_set) + if(raw_mem) MC_SET_RAW_MEM; return snapshot; diff --git a/src/mc/mc_compare.c b/src/mc/mc_compare.c index 0974d9902f..cc5a4a6024 100644 --- a/src/mc/mc_compare.c +++ b/src/mc/mc_compare.c @@ -165,16 +165,18 @@ void heap_equality_free_voidp(void *e){ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2, mc_comparison_times_t ct1, mc_comparison_times_t ct2){ - raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + int raw_mem = (mmalloc_get_current_heap() == raw_heap); MC_SET_RAW_MEM; - + int errors = 0, i = 0; if(s1->num_reg != s2->num_reg){ if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_verbose)){ XBT_VERB("Different num_reg (s1 = %u, s2 = %u)", s1->num_reg, s2->num_reg); } + if(!raw_mem) + MC_UNSET_RAW_MEM; return 1; } @@ -239,7 +241,7 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2, mc_comparison_times_t c xbt_dynar_push_as(ct2->snapshot_comparison_times, double, xbt_os_timer_elapsed(global_timer)); xbt_os_timer_free(global_timer); - if(!raw_mem_set) + if(!raw_mem) MC_UNSET_RAW_MEM; return 1; @@ -289,7 +291,7 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2, mc_comparison_times_t c xbt_dynar_push_as(ct2->snapshot_comparison_times, double, xbt_os_timer_elapsed(global_timer)); xbt_os_timer_free(global_timer); - if(!raw_mem_set) + if(!raw_mem) MC_UNSET_RAW_MEM; return 1; @@ -332,7 +334,7 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2, mc_comparison_times_t c xbt_dynar_push_as(ct2->snapshot_comparison_times, double, xbt_os_timer_elapsed(global_timer)); xbt_os_timer_free(global_timer); - if(!raw_mem_set) + if(!raw_mem) MC_UNSET_RAW_MEM; return 1; } @@ -374,7 +376,7 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2, mc_comparison_times_t c xbt_dynar_push_as(ct2->snapshot_comparison_times, double, xbt_os_timer_elapsed(global_timer)); xbt_os_timer_free(global_timer); - if(!raw_mem_set) + if(!raw_mem) MC_UNSET_RAW_MEM; return 1; } @@ -422,7 +424,7 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2, mc_comparison_times_t c xbt_dynar_push_as(ct2->snapshot_comparison_times, double, xbt_os_timer_elapsed(global_timer)); xbt_os_timer_free(global_timer); - if(!raw_mem_set) + if(!raw_mem) MC_UNSET_RAW_MEM; return 1; } @@ -477,7 +479,7 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2, mc_comparison_times_t c xbt_dynar_push_as(ct2->snapshot_comparison_times, double, xbt_os_timer_elapsed(global_timer)); xbt_os_timer_free(global_timer); - if(!raw_mem_set) + if(!raw_mem) MC_UNSET_RAW_MEM; return 1; @@ -503,7 +505,7 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2, mc_comparison_times_t c } xbt_os_timer_free(global_timer); - if(!raw_mem_set) + if(!raw_mem) MC_UNSET_RAW_MEM; return errors > 0; diff --git a/src/mc/mc_dpor.c b/src/mc/mc_dpor.c index ccc3db80a2..5587e6a4e4 100644 --- a/src/mc/mc_dpor.c +++ b/src/mc/mc_dpor.c @@ -14,7 +14,7 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_dpor, mc, void MC_dpor_init() { - raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); mc_state_t initial_state = NULL; smx_process_t process; @@ -62,8 +62,6 @@ void MC_dpor_init() void MC_dpor(void) { - raw_mem_set = (mmalloc_get_current_heap() == raw_heap); - char *req_str; int value; smx_simcall_t req = NULL, prev_req = NULL; @@ -222,13 +220,7 @@ void MC_dpor(void) } } MC_print_statistics(mc_stats); - MC_UNSET_RAW_MEM; - - if(raw_mem_set) - MC_SET_RAW_MEM; - else - MC_UNSET_RAW_MEM; - + MC_UNSET_RAW_MEM; return; } diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index b382d7abb4..016c3d2a00 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -86,7 +86,6 @@ 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 */ @@ -142,7 +141,7 @@ void MC_do_the_modelcheck_for_real() { void MC_init_safety(void) { - raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); /* Check if MC is already initialized */ if (initial_snapshot) @@ -191,7 +190,7 @@ void MC_modelcheck(void) 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); @@ -236,7 +235,7 @@ void MC_init_liveness(){ 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(); @@ -258,6 +257,9 @@ void MC_modelcheck_liveness(){ MC_print_statistics_pairs(mc_stats_pair); xbt_free(mc_time); + if(raw_mem_set) + MC_SET_RAW_MEM; + } @@ -386,7 +388,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; @@ -399,11 +401,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){ @@ -489,7 +492,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; @@ -504,7 +507,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); @@ -587,7 +590,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; @@ -671,7 +674,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; @@ -689,7 +692,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; @@ -709,7 +712,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; @@ -750,7 +753,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; @@ -808,7 +811,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; @@ -873,7 +876,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) diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c index 778c88e9ba..3dc68fc370 100644 --- a/src/mc/mc_liveness.c +++ b/src/mc/mc_liveness.c @@ -188,7 +188,7 @@ mc_comparison_times_t new_comparison_times(){ int reached(xbt_state_t st){ - raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); MC_SET_RAW_MEM; @@ -276,7 +276,7 @@ int reached(xbt_state_t st){ void set_pair_reached(xbt_state_t st){ - raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); MC_SET_RAW_MEM; @@ -491,7 +491,7 @@ void pair_reached_free_voidp(void *p){ void MC_ddfs_init(void){ - raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + initial_state_liveness->raw_mem_set = (mmalloc_get_current_heap() == raw_heap); XBT_INFO("**************************************************"); XBT_INFO("Double-DFS init"); @@ -518,7 +518,7 @@ void MC_ddfs_init(void){ successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL); /* Save the initial state */ - initial_state_liveness->initial_snapshot = MC_take_snapshot_liveness(); + initial_state_liveness->snapshot = MC_take_snapshot_liveness(); MC_UNSET_RAW_MEM; @@ -534,7 +534,7 @@ void MC_ddfs_init(void){ MC_UNSET_RAW_MEM; if(cursor != 0){ - MC_restore_snapshot(initial_state_liveness->initial_snapshot); + MC_restore_snapshot(initial_state_liveness->snapshot); MC_UNSET_RAW_MEM; } @@ -551,7 +551,7 @@ void MC_ddfs_init(void){ set_pair_reached(state); if(cursor != 0){ - MC_restore_snapshot(initial_state_liveness->initial_snapshot); + MC_restore_snapshot(initial_state_liveness->snapshot); MC_UNSET_RAW_MEM; } @@ -561,7 +561,7 @@ void MC_ddfs_init(void){ } } - if(raw_mem_set) + if(initial_state_liveness->raw_mem_set) MC_SET_RAW_MEM; else MC_UNSET_RAW_MEM; @@ -572,7 +572,7 @@ void MC_ddfs_init(void){ void MC_ddfs(int search_cycle){ - raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + //initial_state_liveness->raw_mem_set = (mmalloc_get_current_heap() == raw_heap); smx_process_t process; mc_pair_stateless_t current_pair = NULL; @@ -929,7 +929,7 @@ void MC_ddfs(int search_cycle){ } MC_UNSET_RAW_MEM; - if(raw_mem_set) - MC_SET_RAW_MEM; + /*if(initial_state_liveness->raw_mem_set) + MC_SET_RAW_MEM;*/ } diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h index 2f42914aa3..3e881cd3c5 100644 --- a/src/mc/mc_private.h +++ b/src/mc/mc_private.h @@ -43,7 +43,8 @@ typedef struct s_mc_snapshot_stack{ }s_mc_snapshot_stack_t, *mc_snapshot_stack_t; typedef struct s_mc_global_t{ - mc_snapshot_t initial_snapshot; + mc_snapshot_t snapshot; + int raw_mem_set; }s_mc_global_t, *mc_global_t; void MC_take_snapshot(mc_snapshot_t); @@ -159,8 +160,6 @@ extern void *raw_heap; #define MC_SET_RAW_MEM mmalloc_set_current_heap(raw_heap) #define MC_UNSET_RAW_MEM mmalloc_set_current_heap(std_heap) -extern int raw_mem_set; - /******************************* MEMORY MAPPINGS ***************************/ /* These functions and data structures implements a binary interface for */ /* the proc maps ascii interface */ -- 2.20.1