From: Marion Guthmuller Date: Thu, 15 Nov 2012 16:08:26 +0000 (+0100) Subject: model-checker : store last visited states during exploration X-Git-Tag: v3_9_rc1~91^2~87 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/c6189d1b7b02cda083791afc98f7e632100424d5?hp=5b1e363f764347ddf3e895a6b58529c2036a1f24 model-checker : store last visited states during exploration - new cfg flag : model-check/stateful -> indicates how many visited states stored (default value : 10) - if a state has been already visited, backtracking --- diff --git a/src/include/mc/mc.h b/src/include/mc/mc.h index defe37f7f7..04ab6f5d49 100644 --- a/src/include/mc/mc.h +++ b/src/include/mc/mc.h @@ -31,6 +31,7 @@ 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_max_depth(const char *name, int pos); +void _mc_cfg_cb_stateful(const char *name, int pos); XBT_PUBLIC(void) MC_do_the_modelcheck_for_real(void); diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index c351065cf2..b382d7abb4 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -71,6 +71,14 @@ void _mc_cfg_cb_max_depth(const char *name, int pos) { 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 */ diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c index e534750edb..778c88e9ba 100644 --- a/src/mc/mc_liveness.c +++ b/src/mc/mc_liveness.c @@ -11,6 +11,7 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc, "Logging specific to algorithms for liveness properties verification"); xbt_dynar_t reached_pairs; +xbt_dynar_t visited_pairs; xbt_dynar_t successors; int create_dump(int pair) @@ -308,6 +309,91 @@ void set_pair_reached(xbt_state_t st){ } +int visited(xbt_state_t st){ + + if(_surf_mc_stateful == 0) + return 0; + + int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + + MC_SET_RAW_MEM; + + mc_pair_visited_t new_pair = NULL; + 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(); + + /* Get values of propositional symbols */ + int res; + int_f_void_t f; + unsigned int cursor = 0; + xbt_propositional_symbol_t ps = NULL; + xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){ + f = (int_f_void_t)ps->function; + res = (*f)(); + xbt_dynar_push_as(new_pair->prop_ato, int, res); + } + + MC_UNSET_RAW_MEM; + + if(xbt_dynar_is_empty(visited_pairs)){ + + MC_SET_RAW_MEM; + /* New pair visited */ + xbt_dynar_push(visited_pairs, &new_pair); + MC_UNSET_RAW_MEM; + + if(raw_mem_set) + MC_SET_RAW_MEM; + + return 0; + + }else{ + + MC_SET_RAW_MEM; + + cursor = 0; + mc_pair_visited_t pair_test = NULL; + + xbt_dynar_foreach(visited_pairs, cursor, pair_test){ + if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)) + XBT_DEBUG("****** Pair visited #%d ******", cursor + 1); + if(automaton_state_compare(pair_test->automaton_state, st) == 0){ + if(propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){ + if(snapshot_compare(new_pair->system_state, pair_test->system_state, NULL, NULL) == 0){ + if(raw_mem_set) + MC_SET_RAW_MEM; + else + MC_UNSET_RAW_MEM; + + return 1; + } + }else{ + XBT_INFO("Different values of propositional symbols"); + } + }else{ + XBT_INFO("Different automaton state"); + } + } + + if(xbt_dynar_length(visited_pairs) == _surf_mc_stateful){ + xbt_dynar_remove_at(visited_pairs, 0, NULL); + } + + /* New pair visited */ + xbt_dynar_push(visited_pairs, &new_pair); + + MC_UNSET_RAW_MEM; + + if(raw_mem_set) + MC_SET_RAW_MEM; + + return 0; + + } +} + void MC_pair_delete(mc_pair_t pair){ xbt_free(pair->graph_state->proc_status); xbt_free(pair->graph_state); @@ -356,6 +442,19 @@ int MC_automaton_evaluate_label(xbt_exp_label_t l){ /********************* Double-DFS stateless *******************/ +void pair_visited_free(mc_pair_visited_t pair){ + if(pair){ + pair->automaton_state = NULL; + xbt_dynar_free(&(pair->prop_ato)); + MC_free_snapshot(pair->system_state); + xbt_free(pair); + } +} + +void pair_visited_free_voidp(void *p){ + pair_visited_free((mc_pair_visited_t) * (void **) p); +} + void pair_stateless_free(mc_pair_stateless_t pair){ xbt_free(pair->graph_state->system_state); xbt_free(pair->graph_state->proc_status); @@ -415,6 +514,7 @@ void MC_ddfs_init(void){ } reached_pairs = xbt_dynar_new(sizeof(mc_pair_reached_t), pair_reached_free_voidp); + visited_pairs = xbt_dynar_new(sizeof(mc_pair_visited_t), pair_visited_free_voidp); successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL); /* Save the initial state */ @@ -605,56 +705,80 @@ void MC_ddfs(int search_cycle){ }else{ - XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id); + if(visited(pair_succ->automaton_state)){ - XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs)); + XBT_DEBUG("Next pair already visited !"); + break; + + }else{ - MC_SET_RAW_MEM; - xbt_fifo_unshift(mc_stack_liveness, pair_succ); - MC_UNSET_RAW_MEM; + XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id); + + XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs)); + + MC_SET_RAW_MEM; + xbt_fifo_unshift(mc_stack_liveness, pair_succ); + MC_UNSET_RAW_MEM; - MC_ddfs(search_cycle); + MC_ddfs(search_cycle); + + } } }else{ - MC_SET_RAW_MEM; - xbt_fifo_unshift(mc_stack_liveness, pair_succ); - MC_UNSET_RAW_MEM; - - MC_ddfs(search_cycle); + if(visited(pair_succ->automaton_state)){ + + XBT_DEBUG("Next pair already visited !"); + break; + + }else{ + + MC_SET_RAW_MEM; + xbt_fifo_unshift(mc_stack_liveness, pair_succ); + MC_UNSET_RAW_MEM; + + MC_ddfs(search_cycle); + } } }else{ + + if(visited(pair_succ->automaton_state)){ + + XBT_DEBUG("Next pair already visited !"); + break; + + }else{ - if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){ + if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){ - XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id); + XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id); - set_pair_reached(pair_succ->automaton_state); + set_pair_reached(pair_succ->automaton_state); - search_cycle = 1; + search_cycle = 1; - XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs)); + XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs)); - } + } - MC_SET_RAW_MEM; - xbt_fifo_unshift(mc_stack_liveness, pair_succ); - MC_UNSET_RAW_MEM; + MC_SET_RAW_MEM; + xbt_fifo_unshift(mc_stack_liveness, pair_succ); + MC_UNSET_RAW_MEM; - MC_ddfs(search_cycle); + MC_ddfs(search_cycle); + + } } - /* Restore system before checking others successors */ if(cursor != (xbt_dynar_length(successors) - 1)) MC_replay_liveness(mc_stack_liveness, 1); - - + } if(MC_state_interleave_size(current_pair->graph_state) > 0){ diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h index d0e2162efd..2f42914aa3 100644 --- a/src/mc/mc_private.h +++ b/src/mc/mc_private.h @@ -249,18 +249,27 @@ typedef struct s_mc_pair_reached{ mc_comparison_times_t comparison_times; }s_mc_pair_reached_t, *mc_pair_reached_t; +typedef struct s_mc_pair_visited{ + xbt_state_t automaton_state; + xbt_dynar_t prop_ato; + mc_snapshot_t system_state; +}s_mc_pair_visited_t, *mc_pair_visited_t; + int MC_automaton_evaluate_label(xbt_exp_label_t l); mc_pair_t new_pair(mc_snapshot_t sn, mc_state_t sg, xbt_state_t st); mc_comparison_times_t new_comparison_times(void); int reached(xbt_state_t st); void set_pair_reached(xbt_state_t st); +int visited(xbt_state_t st); int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2, mc_comparison_times_t ct1, mc_comparison_times_t ct2); void MC_pair_delete(mc_pair_t pair); void MC_exit_liveness(void); mc_state_t MC_state_pair_new(void); void pair_reached_free(mc_pair_reached_t pair); void pair_reached_free_voidp(void *p); +void pair_visited_free(mc_pair_visited_t pair); +void pair_visited_free_voidp(void *p); void MC_init_liveness(void); void MC_init_memory_map_info(void); void MC_print_comparison_times_statistics(mc_comparison_times_t ct); @@ -288,6 +297,7 @@ extern int _surf_mc_checkpoint; extern char* _surf_mc_property_file; extern int _surf_mc_timeout; extern int _surf_mc_max_depth; +extern int _surf_mc_stateful; /****** Core dump ******/ diff --git a/src/surf/surf_config.c b/src/surf/surf_config.c index cda623d550..32b361afb0 100644 --- a/src/surf/surf_config.c +++ b/src/surf/surf_config.c @@ -528,9 +528,16 @@ void surf_config_init(int *argc, char **argv) /* Set max depth exploration */ default_value_int = 1000; xbt_cfg_register(&_surf_cfg_set, "model-check/max_depth", - "Specify the max depth of exploration", + "Specify the max depth of exploration (default : 1000)", xbt_cfgelm_int, &default_value, 0, 1, _mc_cfg_cb_max_depth, NULL); + + /* Set number of visited state stored in stateful mode */ + default_value_int = 10; + xbt_cfg_register(&_surf_cfg_set, "model-check/stateful", + "Specify the number of visited state stored in stateful mode. The default value is 10 which means that we only keep in memory the last 10 visited states", + xbt_cfgelm_int, &default_value, 0, 1, + _mc_cfg_cb_stateful, NULL); #endif /* do verbose-exit */ diff --git a/src/xbt/xbt_main.c b/src/xbt/xbt_main.c index 2ca9580227..c1ebcf465f 100644 --- a/src/xbt/xbt_main.c +++ b/src/xbt/xbt_main.c @@ -34,6 +34,7 @@ int _surf_mc_checkpoint=0; char* _surf_mc_property_file=NULL; int _surf_mc_timeout=0; int _surf_mc_max_depth=1000; +int _surf_mc_stateful=10; /* Declare xbt_preinit and xbt_postexit as constructor/destructor of the library. * This is crude and rather compiler-specific, unfortunately.