From: Marion Guthmuller Date: Tue, 24 Feb 2015 13:05:54 +0000 (+0100) Subject: model-checker : non-progressive cycle detection (enabled with --cfg=model-check/termi... X-Git-Tag: v3_12~751 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/d8710e879515b185393e2fa3a53d7377853cd25c?ds=sidebyside model-checker : non-progressive cycle detection (enabled with --cfg=model-check/termination:1) --- diff --git a/examples/smpi/CMakeLists.txt b/examples/smpi/CMakeLists.txt index 8effff1913..191d4e76b9 100644 --- a/examples/smpi/CMakeLists.txt +++ b/examples/smpi/CMakeLists.txt @@ -32,6 +32,10 @@ if(enable_smpi) add_executable(smpi_send_deterministic mc/send_deterministic.c) add_executable(smpi_non_deterministic mc/non_deterministic.c) add_executable(smpi_mutual_exclusion mc/mutual_exclusion.c) + add_executable(smpi_non_termination1 mc/non_termination1.c) + add_executable(smpi_non_termination2 mc/non_termination2.c) + add_executable(smpi_non_termination3 mc/non_termination3.c) + add_executable(smpi_non_termination4 mc/non_termination4.c) target_link_libraries(smpi_bugged1 simgrid) target_link_libraries(smpi_bugged2 simgrid) @@ -39,6 +43,10 @@ if(enable_smpi) target_link_libraries(smpi_send_deterministic simgrid) target_link_libraries(smpi_non_deterministic simgrid) target_link_libraries(smpi_mutual_exclusion simgrid) + target_link_libraries(smpi_non_termination1 simgrid) + target_link_libraries(smpi_non_termination2 simgrid) + target_link_libraries(smpi_non_termination3 simgrid) + target_link_libraries(smpi_non_termination4 simgrid) set_target_properties(smpi_bugged1 PROPERTIES RUNTIME_OUTPUT_DIRECTORY "./mc") set_target_properties(smpi_bugged2 PROPERTIES RUNTIME_OUTPUT_DIRECTORY "./mc") @@ -46,6 +54,10 @@ if(enable_smpi) set_target_properties(smpi_send_deterministic PROPERTIES RUNTIME_OUTPUT_DIRECTORY "./mc") set_target_properties(smpi_non_deterministic PROPERTIES RUNTIME_OUTPUT_DIRECTORY "./mc") set_target_properties(smpi_mutual_exclusion PROPERTIES RUNTIME_OUTPUT_DIRECTORY "./mc") + set_target_properties(smpi_non_termination1 PROPERTIES RUNTIME_OUTPUT_DIRECTORY "./mc") + set_target_properties(smpi_non_termination2 PROPERTIES RUNTIME_OUTPUT_DIRECTORY "./mc") + set_target_properties(smpi_non_termination3 PROPERTIES RUNTIME_OUTPUT_DIRECTORY "./mc") + set_target_properties(smpi_non_termination4 PROPERTIES RUNTIME_OUTPUT_DIRECTORY "./mc") endif() @@ -74,6 +86,10 @@ set(examples_src ${CMAKE_CURRENT_SOURCE_DIR}/mc/send_deterministic.c ${CMAKE_CURRENT_SOURCE_DIR}/mc/non_deterministic.c ${CMAKE_CURRENT_SOURCE_DIR}/mc/mutual_exclusion.c + ${CMAKE_CURRENT_SOURCE_DIR}/mc/non_termination1.c + ${CMAKE_CURRENT_SOURCE_DIR}/mc/non_termination2.c + ${CMAKE_CURRENT_SOURCE_DIR}/mc/non_termination3.c + ${CMAKE_CURRENT_SOURCE_DIR}/mc/non_termination4.c PARENT_SCOPE ) set(bin_files @@ -86,6 +102,7 @@ set(bin_files ${CMAKE_CURRENT_SOURCE_DIR}/mc/hostfile_send_deterministic ${CMAKE_CURRENT_SOURCE_DIR}/mc/hostfile_non_deterministic ${CMAKE_CURRENT_SOURCE_DIR}/mc/hostfile_mutual_exclusion + ${CMAKE_CURRENT_SOURCE_DIR}/mc/hostfile_non_termination PARENT_SCOPE ) set(txt_files diff --git a/src/include/mc/mc.h b/src/include/mc/mc.h index 2bfe7ad44b..e3fcd97a6e 100644 --- a/src/include/mc/mc.h +++ b/src/include/mc/mc.h @@ -51,6 +51,7 @@ extern int _sg_mc_comms_determinism; extern int _sg_mc_send_determinism; extern int _sg_mc_safety; extern int _sg_mc_liveness; +extern int _sg_mc_termination; extern xbt_dynar_t mc_heap_comparison_ignore; extern xbt_dynar_t stacks_areas; @@ -70,6 +71,7 @@ void _mc_cfg_cb_visited(const char *name, int pos); void _mc_cfg_cb_dot_output(const char *name, int pos); void _mc_cfg_cb_comms_determinism(const char *name, int pos); void _mc_cfg_cb_send_determinism(const char *name, int pos); +void _mc_cfg_cb_termination(const char *name, int pos); XBT_PUBLIC(void) MC_do_the_modelcheck_for_real(void); XBT_PUBLIC(void) MC_init(void); diff --git a/src/mc/mc_compare.cpp b/src/mc/mc_compare.cpp index 4745d3a4ee..2eb1d25999 100644 --- a/src/mc/mc_compare.cpp +++ b/src/mc/mc_compare.cpp @@ -366,6 +366,11 @@ int snapshot_compare(void *state1, void *state2) s2 = ((mc_visited_pair_t) state2)->graph_state->system_state; num1 = ((mc_visited_pair_t) state1)->num; num2 = ((mc_visited_pair_t) state2)->num; + }else if (_sg_mc_termination) { /* Non-progressive cycle MC */ + s1 = ((mc_state_t) state1)->system_state; + s2 = ((mc_state_t) state2)->system_state; + num1 = ((mc_state_t) state1)->num; + num2 = ((mc_state_t) state2)->num; } else { /* Safety or comm determinism MC */ s1 = ((mc_visited_state_t) state1)->system_state; s2 = ((mc_visited_state_t) state2)->system_state; diff --git a/src/mc/mc_config.c b/src/mc/mc_config.c index 07c9179889..5959b7f780 100644 --- a/src/mc/mc_config.c +++ b/src/mc/mc_config.c @@ -58,6 +58,7 @@ int _sg_mc_comms_determinism = 0; int _sg_mc_send_determinism = 0; int _sg_mc_safety = 0; int _sg_mc_liveness = 0; +int _sg_mc_termination = 0; void _mc_cfg_cb_reduce(const char *name, int pos) @@ -165,4 +166,14 @@ void _mc_cfg_cb_send_determinism(const char *name, int pos) mc_reduce_kind = e_mc_reduce_none; } +void _mc_cfg_cb_termination(const char *name, int pos) +{ + if (_sg_cfg_init_status && !_sg_do_model_check) { + xbt_die + ("You are specifying a value to enable/disable the detection of non progressive cycles 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."); + } + _sg_mc_termination = xbt_cfg_get_boolean(_sg_cfg_set, name); + mc_reduce_kind = e_mc_reduce_none; +} + #endif diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index 63ecd05968..59425b305f 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -173,7 +173,7 @@ void MC_init() MC_SET_STD_HEAP; - if (_sg_mc_visited > 0 || _sg_mc_liveness) { + if (_sg_mc_visited > 0 || _sg_mc_liveness || _sg_mc_termination) { /* 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", "*"); @@ -333,7 +333,10 @@ void MC_do_the_modelcheck_for_real() } else if (!_sg_mc_property_file || _sg_mc_property_file[0] == '\0') { if (mc_reduce_kind == e_mc_reduce_unset) mc_reduce_kind = e_mc_reduce_dpor; - XBT_INFO("Check a safety property"); + if(_sg_mc_termination) + XBT_INFO("Check non progressive cycles"); + else + XBT_INFO("Check a safety property"); MC_modelcheck_safety_init(); } else { if (mc_reduce_kind == e_mc_reduce_unset) @@ -690,6 +693,15 @@ void MC_show_deadlock(smx_simcall_t req) MC_print_statistics(mc_stats); } +void MC_show_non_termination(void){ + XBT_INFO("******************************************"); + XBT_INFO("*** NON-PROGRESSIVE CYCLE DETECTED ***"); + XBT_INFO("******************************************"); + XBT_INFO("Counter-example execution trace:"); + MC_dump_stack_safety(mc_stack); + MC_print_statistics(mc_stats); +} + void MC_show_stack_liveness(xbt_fifo_t stack) { diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h index 4a86245aeb..86b7e64837 100644 --- a/src/mc/mc_private.h +++ b/src/mc/mc_private.h @@ -56,6 +56,7 @@ void MC_replay_liveness(xbt_fifo_t stack); void MC_show_deadlock(smx_simcall_t req); void MC_show_stack_safety(xbt_fifo_t stack); void MC_dump_stack_safety(xbt_fifo_t stack); +void MC_show_non_termination(void); /** Stack (of `mc_state_t`) representing the current position of the * the MC in the exploration graph diff --git a/src/mc/mc_safety.c b/src/mc/mc_safety.c index 83460ff5da..38e0999740 100644 --- a/src/mc/mc_safety.c +++ b/src/mc/mc_safety.c @@ -15,6 +15,20 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_safety, mc, "Logging specific to MC safety verification "); +static int is_exploration_stack_state(mc_state_t current_state){ + + xbt_fifo_item_t item; + mc_state_t stack_state; + for(item = xbt_fifo_get_first_item(mc_stack); item != NULL; item = xbt_fifo_get_next_item(item)) { + stack_state = (mc_state_t) xbt_fifo_get_item_content(item); + if(snapshot_compare(stack_state, current_state) == 0){ + XBT_INFO("Non-progressive cycle : state %d -> state %d", stack_state->num, current_state->num); + return 1; + } + } + return 0; +} + /** * \brief Initialize the DPOR exploration algorithm */ @@ -118,6 +132,11 @@ void MC_modelcheck_safety(void) next_state = MC_state_new(); + if(_sg_mc_termination && is_exploration_stack_state(next_state)){ + MC_show_non_termination(); + return; + } + if ((visited_state = is_visited_state(next_state)) == NULL) { /* Get an enabled process and insert it in the interleave set of the next state */ diff --git a/src/mc/mc_state.c b/src/mc/mc_state.c index 84db3e8ec3..5830913ad5 100644 --- a/src/mc/mc_state.c +++ b/src/mc/mc_state.c @@ -71,7 +71,7 @@ mc_state_t MC_state_new() state->in_visited_states = 0; state->incomplete_comm_pattern = NULL; /* Stateful model checking */ - if(_sg_mc_checkpoint > 0 && mc_stats->expanded_states % _sg_mc_checkpoint == 0){ + if((_sg_mc_checkpoint > 0 && (mc_stats->expanded_states % _sg_mc_checkpoint == 0)) || _sg_mc_termination){ state->system_state = MC_take_snapshot(state->num); if(_sg_mc_comms_determinism || _sg_mc_send_determinism){ copy_incomplete_communications_pattern(state); diff --git a/src/simgrid/sg_config.c b/src/simgrid/sg_config.c index 544de00018..b2bda9fcef 100644 --- a/src/simgrid/sg_config.c +++ b/src/simgrid/sg_config.c @@ -712,6 +712,12 @@ void sg_config_init(int *argc, char **argv) "Specify the name of dot file corresponding to graph state", xbt_cfgelm_string, 1, 1, _mc_cfg_cb_dot_output, NULL); xbt_cfg_setdefault_string(_sg_cfg_set, "model-check/dot_output", ""); + + /* Enable/disable non progressive cycles detection with model-checking */ + xbt_cfg_register(&_sg_cfg_set, "model-check/termination", + "Enable/Disable non progressive cycle detection", + xbt_cfgelm_boolean, 1, 1, _mc_cfg_cb_termination, NULL); + xbt_cfg_setdefault_boolean(_sg_cfg_set, "model-check/termination", "no"); #endif /* do verbose-exit */