From 5352b98fee2f44e66feb3a3fe9110782d98a779f Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Mon, 24 Feb 2014 18:39:18 +0100 Subject: [PATCH] model-checker : use separate configuration flags for comm determinism and send determinism detection --- src/include/mc/mc.h | 2 ++ src/mc/mc_dpor.c | 35 +++++++++++++++++++++++++++-------- src/mc/mc_global.c | 22 ++++++++++++++++------ src/simgrid/sg_config.c | 10 ++++++++-- 4 files changed, 53 insertions(+), 16 deletions(-) diff --git a/src/include/mc/mc.h b/src/include/mc/mc.h index 88bfb651bb..bbcdc2fd14 100644 --- a/src/include/mc/mc.h +++ b/src/include/mc/mc.h @@ -31,6 +31,7 @@ extern int _sg_mc_max_depth; extern int _sg_mc_visited; extern char* _sg_mc_dot_output_file; extern int _sg_mc_comms_determinism; +extern int _sg_mc_send_determinism; extern xbt_dynar_t mc_heap_comparison_ignore; extern xbt_dynar_t stacks_areas; @@ -47,6 +48,7 @@ void _mc_cfg_cb_max_depth(const char *name, int pos); 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); XBT_PUBLIC(void) MC_do_the_modelcheck_for_real(void); diff --git a/src/mc/mc_dpor.c b/src/mc/mc_dpor.c index d0b158d7f3..1fa1f26fc0 100644 --- a/src/mc/mc_dpor.c +++ b/src/mc/mc_dpor.c @@ -92,7 +92,6 @@ static void deterministic_pattern(xbt_dynar_t initial_pattern, xbt_dynar_t patte recv_index = 0; current_process++; } - // XBT_DEBUG("Communication-deterministic : %d, Send-deterministic : %d", initial_state_safety->comm_deterministic, initial_state_safety->send_deterministic); } static int complete_comm_pattern(xbt_dynar_t list, mc_comm_pattern_t pattern){ @@ -517,7 +516,7 @@ void MC_dpor(void) xbt_free(key); MC_UNSET_RAW_MEM; - if(_sg_mc_comms_determinism){ + if(_sg_mc_comms_determinism || _sg_mc_send_determinism){ if(req->call == SIMCALL_COMM_ISEND) comm_pattern = 1; else if(req->call == SIMCALL_COMM_IRECV) @@ -527,7 +526,7 @@ void MC_dpor(void) /* Answer the request */ SIMIX_simcall_pre(req, value); /* After this call req is no longer usefull */ - if(_sg_mc_comms_determinism){ + if(_sg_mc_comms_determinism || _sg_mc_send_determinism){ MC_SET_RAW_MEM; if(comm_pattern != 0){ if(!initial_state_safety->initial_communications_pattern_done) @@ -632,16 +631,36 @@ void MC_dpor(void) MC_SET_RAW_MEM; - if(_sg_mc_comms_determinism){ - if(!initial_state_safety->initial_communications_pattern_done){ - //print_communications_pattern(initial_communications_pattern); - }else{ + if(_sg_mc_comms_determinism || _sg_mc_send_determinism){ + if(initial_state_safety->initial_communications_pattern_done){ if(interleave_size == 0){ /* if (interleave_size > 0), process interleaved but not enabled => "incorrect" path, determinism not evaluated */ //print_communications_pattern(communications_pattern); deterministic_pattern(initial_communications_pattern, communications_pattern); + if(initial_state_safety->comm_deterministic == 0 && _sg_mc_comms_determinism){ + XBT_INFO("****************************************************"); + XBT_INFO("***** Non-deterministic communications pattern *****"); + XBT_INFO("****************************************************"); + XBT_INFO("Initial communications pattern:"); + print_communications_pattern(initial_communications_pattern); + XBT_INFO("Communications pattern counter-example:"); + print_communications_pattern(communications_pattern); + MC_print_statistics(mc_stats); + return; + }else if(initial_state_safety->send_deterministic == 0 && _sg_mc_send_determinism){ + XBT_INFO("****************************************************"); + XBT_INFO("***** Non-send-deterministic communications pattern *****"); + XBT_INFO("****************************************************"); + XBT_INFO("Initial communications pattern:"); + print_communications_pattern(initial_communications_pattern); + XBT_INFO("Communications pattern counter-example:"); + print_communications_pattern(communications_pattern); + MC_print_statistics(mc_stats); + return; + } } + }else{ + initial_state_safety->initial_communications_pattern_done = 1; } - initial_state_safety->initial_communications_pattern_done = 1; } /* Trash the current state, no longer needed */ diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index f92085fc14..7528e5b9d2 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -35,6 +35,7 @@ int _sg_mc_max_depth=1000; int _sg_mc_visited=0; char *_sg_mc_dot_output_file = NULL; int _sg_mc_comms_determinism=0; +int _sg_mc_send_determinism=0; int user_max_depth_reached = 0; @@ -107,6 +108,13 @@ void _mc_cfg_cb_comms_determinism(const char *name, int pos) { _sg_mc_comms_determinism= xbt_cfg_get_boolean(_sg_cfg_set, name); } +void _mc_cfg_cb_send_determinism(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 send-determinism in the communications schemes 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_send_determinism= xbt_cfg_get_boolean(_sg_cfg_set, name); +} + /* MC global data structures */ mc_state_t mc_current_state = NULL; char mc_replay_mode = FALSE; @@ -1247,7 +1255,7 @@ void MC_replay(xbt_fifo_t stack, int start) xbt_free(key); } } - if(_sg_mc_comms_determinism) + if(_sg_mc_comms_determinism || _sg_mc_send_determinism) xbt_dynar_reset(communications_pattern); MC_UNSET_RAW_MEM; @@ -1279,7 +1287,7 @@ void MC_replay(xbt_fifo_t stack, int start) } } - if(_sg_mc_comms_determinism){ + if(_sg_mc_comms_determinism || _sg_mc_send_determinism){ if(req->call == SIMCALL_COMM_ISEND) comm_pattern = 1; else if(req->call == SIMCALL_COMM_IRECV) @@ -1288,7 +1296,7 @@ void MC_replay(xbt_fifo_t stack, int start) SIMIX_simcall_pre(req, value); - if(_sg_mc_comms_determinism){ + if(_sg_mc_comms_determinism || _sg_mc_send_determinism){ MC_SET_RAW_MEM; if(comm_pattern != 0){ get_comm_pattern(communications_pattern, req, comm_pattern); @@ -1577,9 +1585,11 @@ void MC_print_statistics(mc_stats_t stats) fprintf(dot_output, "}\n"); fclose(dot_output); } - if(initial_state_safety != NULL && _sg_mc_comms_determinism){ - XBT_INFO("Communication-deterministic : %s", !initial_state_safety->comm_deterministic ? "No" : "Yes"); - XBT_INFO("Send-deterministic : %s", !initial_state_safety->send_deterministic ? "No" : "Yes"); + if(initial_state_safety != NULL){ + if(_sg_mc_comms_determinism) + XBT_INFO("Communication-deterministic : %s", !initial_state_safety->comm_deterministic ? "No" : "Yes"); + if (_sg_mc_send_determinism) + XBT_INFO("Send-deterministic : %s", !initial_state_safety->send_deterministic ? "No" : "Yes"); } MC_UNSET_RAW_MEM; } diff --git a/src/simgrid/sg_config.c b/src/simgrid/sg_config.c index 4886b39b2e..dafa40683d 100644 --- a/src/simgrid/sg_config.c +++ b/src/simgrid/sg_config.c @@ -574,12 +574,18 @@ void sg_config_init(int *argc, char **argv) xbt_cfgelm_string, 0, 1, _mc_cfg_cb_property, NULL); xbt_cfg_setdefault_string(_sg_cfg_set, "model-check/property", ""); - /* do determinism model-checking */ - xbt_cfg_register(&_sg_cfg_set, "model-check/communications_determinism", + /* do communications determinism model-checking */ + xbt_cfg_register(&_sg_cfg_set, "model-check/communications_determinism", "Enable/disable the detection of determinism in the communications schemes", xbt_cfgelm_boolean, 0, 1, _mc_cfg_cb_comms_determinism, NULL); xbt_cfg_setdefault_boolean(_sg_cfg_set, "model-check/communications_determinism", "no"); + /* do send determinism model-checking */ + xbt_cfg_register(&_sg_cfg_set, "model-check/send_determinism", + "Enable/disable the detection of send-determinism in the communications schemes", + xbt_cfgelm_boolean, 0, 1, _mc_cfg_cb_send_determinism, NULL); + xbt_cfg_setdefault_boolean(_sg_cfg_set, "model-check/send_determinism", "no"); + /* Specify the kind of model-checking reduction */ xbt_cfg_register(&_sg_cfg_set, "model-check/reduction", "Specify the kind of exploration reduction (either none or DPOR)", -- 2.20.1