From da09e6cbf4e0213856897ac754430c7bf6beecee Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Thu, 15 Nov 2012 23:54:34 +0100 Subject: [PATCH] model-checker : factorize code for safety and liveness model-checking - same function for checkpointing : MC_take_snapshot - MC_init : dwarf parsing and init memory map info - add visited states storage for safety model checking --- src/include/mc/mc.h | 4 +- src/mc/mc_checkpoint.c | 74 ++++++++++++++-------------- src/mc/mc_dpor.c | 101 ++++++++++++++++++++++++++++++++------ src/mc/mc_global.c | 108 +++++++++++++++++++---------------------- src/mc/mc_liveness.c | 8 +-- src/mc/mc_private.h | 7 +-- src/simix/smx_smurf.c | 2 +- 7 files changed, 186 insertions(+), 118 deletions(-) diff --git a/src/include/mc/mc.h b/src/include/mc/mc.h index 04ab6f5d49..b4d9c713c5 100644 --- a/src/include/mc/mc.h +++ b/src/include/mc/mc.h @@ -35,10 +35,10 @@ void _mc_cfg_cb_stateful(const char *name, int pos); XBT_PUBLIC(void) MC_do_the_modelcheck_for_real(void); -XBT_PUBLIC(void) MC_init_safety(void); +XBT_PUBLIC(void) MC_init(void); XBT_PUBLIC(void) MC_exit(void); XBT_PUBLIC(void) MC_exit_liveness(void); -XBT_PUBLIC(void) MC_modelcheck(void); +XBT_PUBLIC(void) MC_modelcheck_safety(void); XBT_PUBLIC(void) MC_modelcheck_liveness(void); XBT_PUBLIC(void) MC_process_clock_add(smx_process_t, double); XBT_PUBLIC(double) MC_process_clock_get(smx_process_t); diff --git a/src/mc/mc_checkpoint.c b/src/mc/mc_checkpoint.c index c3e8bfac0c..df6c9c4f6b 100644 --- a/src/mc/mc_checkpoint.c +++ b/src/mc/mc_checkpoint.c @@ -76,42 +76,42 @@ static void MC_snapshot_add_region(mc_snapshot_t snapshot, int type, void *start return; } -void MC_take_snapshot(mc_snapshot_t snapshot) -{ - unsigned int i = 0; - s_map_region_t reg; - memory_map_t maps = get_memory_map(); - - /* Save the std heap and the writable mapped pages of libsimgrid */ - while (i < maps->mapsize) { - reg = maps->regions[i]; - if ((reg.prot & PROT_WRITE)){ - if (maps->regions[i].pathname == NULL){ - if (reg.start_addr == std_heap){ // only save the std heap (and not the raw one) - MC_snapshot_add_region(snapshot, 0, reg.start_addr, (char*)reg.end_addr - (char*)reg.start_addr); - } - i++; - } else { - if (!memcmp(basename(maps->regions[i].pathname), "libsimgrid", 10)){ - MC_snapshot_add_region(snapshot, 1, reg.start_addr, (char*)reg.end_addr - (char*)reg.start_addr); - i++; - reg = maps->regions[i]; - while(reg.pathname == NULL && (reg.prot & PROT_WRITE) && i < maps->mapsize){ - MC_snapshot_add_region(snapshot, 1, reg.start_addr, (char*)reg.end_addr - (char*)reg.start_addr); - i++; - reg = maps->regions[i]; - } - }else{ - i++; - } - } - }else{ - i++; - } - } - - free_memory_map(maps); -} +/* void MC_take_snapshot(mc_snapshot_t snapshot) */ +/* { */ +/* unsigned int i = 0; */ +/* s_map_region_t reg; */ +/* memory_map_t maps = get_memory_map(); */ + +/* /\* Save the std heap and the writable mapped pages of libsimgrid *\/ */ +/* while (i < maps->mapsize) { */ +/* reg = maps->regions[i]; */ +/* if ((reg.prot & PROT_WRITE)){ */ +/* if (maps->regions[i].pathname == NULL){ */ +/* if (reg.start_addr == std_heap){ // only save the std heap (and not the raw one) */ +/* MC_snapshot_add_region(snapshot, 0, reg.start_addr, (char*)reg.end_addr - (char*)reg.start_addr); */ +/* } */ +/* i++; */ +/* } else { */ +/* if (!memcmp(basename(maps->regions[i].pathname), "libsimgrid", 10)){ */ +/* MC_snapshot_add_region(snapshot, 1, reg.start_addr, (char*)reg.end_addr - (char*)reg.start_addr); */ +/* i++; */ +/* reg = maps->regions[i]; */ +/* while(reg.pathname == NULL && (reg.prot & PROT_WRITE) && i < maps->mapsize){ */ +/* MC_snapshot_add_region(snapshot, 1, reg.start_addr, (char*)reg.end_addr - (char*)reg.start_addr); */ +/* i++; */ +/* reg = maps->regions[i]; */ +/* } */ +/* }else{ */ +/* i++; */ +/* } */ +/* } */ +/* }else{ */ +/* i++; */ +/* } */ +/* } */ + +/* free_memory_map(maps); */ +/* } */ void MC_init_memory_map_info(){ @@ -171,7 +171,7 @@ void MC_init_memory_map_info(){ } -mc_snapshot_t MC_take_snapshot_liveness() +mc_snapshot_t MC_take_snapshot() { int raw_mem = (mmalloc_get_current_heap() == raw_heap); diff --git a/src/mc/mc_dpor.c b/src/mc/mc_dpor.c index 1238dfe71c..1d698bd651 100644 --- a/src/mc/mc_dpor.c +++ b/src/mc/mc_dpor.c @@ -8,6 +8,73 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_dpor, mc, "Logging specific to MC DPOR exploration"); +xbt_dynar_t visited_states; + +static int is_visited_state(void); + +static int is_visited_state(){ + + if(_surf_mc_stateful == 0) + return 0; + + int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + + MC_SET_RAW_MEM; + + mc_snapshot_t new_state = NULL; + new_state = MC_take_snapshot(); + + MC_UNSET_RAW_MEM; + + if(xbt_dynar_is_empty(visited_states)){ + + MC_SET_RAW_MEM; + xbt_dynar_push(visited_states, &new_state); + MC_UNSET_RAW_MEM; + + if(raw_mem_set) + MC_SET_RAW_MEM; + + return 0; + + }else{ + + MC_SET_RAW_MEM; + + unsigned int cursor = 0; + mc_snapshot_t state_test = NULL; + + xbt_dynar_foreach(visited_states, cursor, state_test){ + if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)) + XBT_DEBUG("****** Pair visited #%d ******", cursor + 1); + if(snapshot_compare(new_state, state_test, NULL, NULL) == 0){ + if(raw_mem_set) + MC_SET_RAW_MEM; + else + MC_UNSET_RAW_MEM; + + return 1; + } + } + + if(xbt_dynar_length(visited_states) == _surf_mc_stateful){ + mc_snapshot_t state_to_remove = NULL; + xbt_dynar_shift(visited_states, &state_to_remove); + MC_free_snapshot(state_to_remove); + } + + xbt_dynar_push(visited_states, &new_state); + + MC_UNSET_RAW_MEM; + + if(raw_mem_set) + MC_SET_RAW_MEM; + + return 0; + + } +} + /** * \brief Initialize the DPOR exploration algorithm */ @@ -21,7 +88,10 @@ void MC_dpor_init() /* Create the initial state and push it into the exploration stack */ MC_SET_RAW_MEM; + initial_state = MC_state_new(); + visited_states = xbt_dynar_new(sizeof(mc_snapshot_t), NULL); + MC_UNSET_RAW_MEM; XBT_DEBUG("**************************************************"); @@ -117,23 +187,26 @@ void MC_dpor(void) next_state = MC_state_new(); - xbt_swag_foreach(process, simix_global->process_list){ - if(MC_process_is_enabled(process)){ - XBT_DEBUG("Process %lu enabled with simcall : %d", process->pid, (&process->simcall)->call); + if(!is_visited_state()){ + + xbt_swag_foreach(process, simix_global->process_list){ + if(MC_process_is_enabled(process)){ + XBT_DEBUG("Process %lu enabled with simcall : %d", process->pid, (&process->simcall)->call); + } } - } - - /* Get an enabled process and insert it in the interleave set of the next state */ - xbt_swag_foreach(process, simix_global->process_list){ - if(MC_process_is_enabled(process)){ - MC_state_interleave_process(next_state, process); - break; + + /* Get an enabled process and insert it in the interleave set of the next state */ + xbt_swag_foreach(process, simix_global->process_list){ + if(MC_process_is_enabled(process)){ + MC_state_interleave_process(next_state, process); + break; + } + } + + if(_surf_mc_checkpoint && ((xbt_fifo_size(mc_stack_safety) + 1) % _surf_mc_checkpoint == 0)){ + next_state->system_state = MC_take_snapshot(); } - } - if(_surf_mc_checkpoint && ((xbt_fifo_size(mc_stack_safety) + 1) % _surf_mc_checkpoint == 0)){ - next_state->system_state = xbt_new0(s_mc_snapshot_t, 1); - MC_take_snapshot(next_state->system_state); } xbt_fifo_unshift(mc_stack_safety, next_state); diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index 016c3d2a00..19502f6e90 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -85,12 +85,12 @@ void _mc_cfg_cb_stateful(const char *name, int pos) { mc_state_t mc_current_state = NULL; char mc_replay_mode = FALSE; double *mc_time = NULL; -mc_snapshot_t initial_snapshot = NULL; /* Safety */ xbt_fifo_t mc_stack_safety = NULL; mc_stats_t mc_stats = NULL; +mc_global_t initial_state_safety = NULL; /* Liveness */ @@ -122,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 { @@ -135,60 +135,12 @@ void MC_do_the_modelcheck_for_real() { } } -/** - * \brief Initialize the model-checker data structures - */ -void MC_init_safety(void) -{ - - int 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_modelcheck(void) -{ - MC_init_safety(); - MC_dpor(); - MC_exit(); -} - -void MC_init_liveness(){ +void MC_init(){ int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); @@ -218,8 +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); - MC_UNSET_RAW_MEM; MC_init_memory_map_info(); @@ -233,22 +183,66 @@ void MC_init_liveness(){ } +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(); + + 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(){ 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(); @@ -333,7 +327,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; diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c index 2401f8f19f..ac829535e5 100644 --- a/src/mc/mc_liveness.c +++ b/src/mc/mc_liveness.c @@ -198,7 +198,7 @@ int reached(xbt_state_t st){ new_pair->automaton_state = st; new_pair->prop_ato = xbt_dynar_new(sizeof(int), NULL); new_pair->comparison_times = new_comparison_times(); - new_pair->system_state = MC_take_snapshot_liveness(); + new_pair->system_state = MC_take_snapshot(); /* Get values of propositional symbols */ int res; @@ -286,7 +286,7 @@ void set_pair_reached(xbt_state_t st){ pair->automaton_state = st; pair->prop_ato = xbt_dynar_new(sizeof(int), NULL); pair->comparison_times = new_comparison_times(); - pair->system_state = MC_take_snapshot_liveness(); + pair->system_state = MC_take_snapshot(); /* Get values of propositional symbols */ unsigned int cursor = 0; @@ -322,7 +322,7 @@ int visited(xbt_state_t st){ new_pair = xbt_new0(s_mc_pair_visited_t, 1); new_pair->automaton_state = st; new_pair->prop_ato = xbt_dynar_new(sizeof(int), NULL); - new_pair->system_state = MC_take_snapshot_liveness(); + new_pair->system_state = MC_take_snapshot(); /* Get values of propositional symbols */ int res; @@ -527,7 +527,7 @@ void MC_ddfs_init(void){ successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL); /* Save the initial state */ - initial_state_liveness->snapshot = MC_take_snapshot_liveness(); + initial_state_liveness->snapshot = MC_take_snapshot(); MC_UNSET_RAW_MEM; diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h index 3e881cd3c5..c76bb7a470 100644 --- a/src/mc/mc_private.h +++ b/src/mc/mc_private.h @@ -47,8 +47,8 @@ typedef struct s_mc_global_t{ int raw_mem_set; }s_mc_global_t, *mc_global_t; -void MC_take_snapshot(mc_snapshot_t); -mc_snapshot_t MC_take_snapshot_liveness(void); +//void MC_take_snapshot(mc_snapshot_t); +mc_snapshot_t MC_take_snapshot(void); void MC_restore_snapshot(mc_snapshot_t); void MC_free_snapshot(mc_snapshot_t); void snapshot_stack_free_voidp(void *s); @@ -202,11 +202,12 @@ typedef enum { } e_mc_reduce_t; extern e_mc_reduce_t mc_reduce_kind; +extern mc_global_t initial_state_safety; void MC_dpor_init(void); void MC_dpor(void); void MC_dpor_exit(void); -void MC_init_safety(void); +void MC_init(void); /********************************** Double-DFS for liveness property**************************************/ diff --git a/src/simix/smx_smurf.c b/src/simix/smx_smurf.c index 70c139337a..c049f29ea9 100644 --- a/src/simix/smx_smurf.c +++ b/src/simix/smx_smurf.c @@ -560,7 +560,7 @@ void SIMIX_simcall_pre(smx_simcall_t simcall, int value) #ifdef HAVE_MC case SIMCALL_MC_SNAPSHOT: - simcall->mc_snapshot.s = MC_take_snapshot_liveness(); + simcall->mc_snapshot.s = MC_take_snapshot(); SIMIX_simcall_answer(simcall); break; -- 2.20.1