From eb3ad7bf1f83d355e938a83cf02f78bc898eefbb Mon Sep 17 00:00:00 2001 From: Gabriel Corona Date: Tue, 11 Feb 2014 13:38:04 +0100 Subject: [PATCH] [mc] Make usage of state hash a runtime parameter (instead of compile-time) "off" by default. --- src/include/mc/mc.h | 2 ++ src/mc/mc_checkpoint.c | 2 +- src/mc/mc_compare.c | 16 +++++++++------- src/mc/mc_global.c | 8 ++++++++ src/mc/mc_private.h | 3 +-- src/simgrid/sg_config.c | 6 ++++++ 6 files changed, 27 insertions(+), 10 deletions(-) diff --git a/src/include/mc/mc.h b/src/include/mc/mc.h index 0cf9f2d17c..298c779903 100644 --- a/src/include/mc/mc.h +++ b/src/include/mc/mc.h @@ -26,6 +26,7 @@ extern int _sg_do_model_check; extern int _sg_mc_checkpoint; extern char* _sg_mc_property_file; extern int _sg_mc_timeout; +extern int _sg_mc_hash; extern int _sg_mc_max_depth; extern int _sg_mc_visited; extern char* _sg_mc_dot_output_file; @@ -40,6 +41,7 @@ void _mc_cfg_cb_reduce(const char *name, int pos); 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_hash(const char *name, int pos); 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); diff --git a/src/mc/mc_checkpoint.c b/src/mc/mc_checkpoint.c index 2937f65471..abd70f6fe8 100644 --- a/src/mc/mc_checkpoint.c +++ b/src/mc/mc_checkpoint.c @@ -517,7 +517,7 @@ mc_snapshot_t MC_take_snapshot(int num_state){ if(_sg_mc_visited > 0 || strcmp(_sg_mc_property_file,"")){ snapshot->stacks = MC_take_snapshot_stacks(&snapshot, snapshot->regions[0]->data); - if(MC_USE_SNAPSHOT_HASH && snapshot->stacks!=NULL) { + if(_sg_mc_hash && snapshot->stacks!=NULL) { snapshot->hash = mc_hash_processes_state(num_state, snapshot->stacks); } else { snapshot->hash = 0; diff --git a/src/mc/mc_compare.c b/src/mc/mc_compare.c index b9ea20c69a..b872692b7a 100644 --- a/src/mc/mc_compare.c +++ b/src/mc/mc_compare.c @@ -391,7 +391,7 @@ int snapshot_compare(void *state1, void *state2){ #endif int hash_result = 0; - if(MC_USE_SNAPSHOT_HASH) { + if(_sg_mc_hash) { hash_result = (s1->hash != s2->hash); if(hash_result) { XBT_VERB("(%d - %d) Different hash : 0x%" PRIx64 "--0x%" PRIx64, num1, num2, s1->hash, s2->hash); @@ -608,13 +608,15 @@ int snapshot_compare(void *state1, void *state2){ XBT_VERB("(%d - %d) No difference found", num1, num2); #endif -#if defined(MC_DEBUG) && defined(MC_VERBOSE) && MC_USE_SNAPSHOT_HASH - // * false positive SHOULD be avoided. - // * There MUST not be any false negative. +#if defined(MC_DEBUG) && defined(MC_VERBOSE) + if(_sg_mc_hash) { + // * false positive SHOULD be avoided. + // * There MUST not be any false negative. - XBT_VERB("(%d - %d) State equality hash test is %s %s", num1, num2, - (hash_result!=0) == (errors!=0) ? "true" : "false", - !hash_result ? "positive" : "negative"); + XBT_VERB("(%d - %d) State equality hash test is %s %s", num1, num2, + (hash_result!=0) == (errors!=0) ? "true" : "false", + !hash_result ? "positive" : "negative"); + } #endif return errors > 0 || hash_result; diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index c9cb9fdb02..78049adec6 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -30,6 +30,7 @@ int _sg_do_model_check = 0; int _sg_mc_checkpoint=0; char* _sg_mc_property_file=NULL; int _sg_mc_timeout=0; +int _sg_mc_hash=0; int _sg_mc_max_depth=1000; int _sg_mc_visited=0; char *_sg_mc_dot_output_file = NULL; @@ -70,6 +71,13 @@ void _mc_cfg_cb_timeout(const char *name, int pos) { _sg_mc_timeout= xbt_cfg_get_boolean(_sg_cfg_set, name); } +void _mc_cfg_cb_hash(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 use of global hash to speedup state comparaison, but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry."); + } + _sg_mc_hash= xbt_cfg_get_boolean(_sg_cfg_set, name); +} + void _mc_cfg_cb_max_depth(const char *name, int pos) { if (_sg_cfg_init_status && !_sg_do_model_check) { xbt_die("You are specifying a max depth value 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."); diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h index dfabace050..3ffc21772b 100644 --- a/src/mc/mc_private.h +++ b/src/mc/mc_private.h @@ -261,9 +261,8 @@ int snapshot_compare(void *state1, void *state2); int SIMIX_pre_mc_compare_snapshots(smx_simcall_t simcall, mc_snapshot_t s1, mc_snapshot_t s2); void print_comparison_times(void); -//#define MC_DEBUG 1 +#define MC_DEBUG 1 #define MC_VERBOSE 1 -#define MC_USE_SNAPSHOT_HASH 1 /********************************** DPOR for safety property **************************************/ diff --git a/src/simgrid/sg_config.c b/src/simgrid/sg_config.c index b812c87d55..ad88f30f75 100644 --- a/src/simgrid/sg_config.c +++ b/src/simgrid/sg_config.c @@ -586,6 +586,12 @@ void sg_config_init(int *argc, char **argv) xbt_cfgelm_boolean, 0, 1, _mc_cfg_cb_timeout, NULL); xbt_cfg_setdefault_boolean(_sg_cfg_set, "model-check/timeout", "no"); + /* Enable/disable global hash computation with model-checking */ + xbt_cfg_register(&_sg_cfg_set, "model-check/hash", + "Enable/Disable state hash for state comparison", + xbt_cfgelm_boolean, 0, 1, _mc_cfg_cb_hash, NULL); + xbt_cfg_setdefault_boolean(_sg_cfg_set, "model-check/hash", "no"); + /* Set max depth exploration */ xbt_cfg_register(&_sg_cfg_set, "model-check/max_depth", "Specify the max depth of exploration (default : 1000)", -- 2.20.1