[mc] Make usage of state hash a runtime parameter (instead of compile-time)

"off" by default.

diff --git a/src/include/mc/mc.h b/src/include/mc/mc.h
index 0cf9f2d..298c779 100644 (file)
--- 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_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;
 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_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);
 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 2937f65..abd70f6 100644 (file)
--- 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(_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;
       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 b9ea20c..b872692 100644 (file)
--- 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;
   #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);
     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
 
      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;
 #endif
 
    return errors > 0 || hash_result;

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index c9cb9fd..78049ad 100644 (file)
--- 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_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;
 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);
 }
 
   _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.");
 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 dfabace..3ffc217 100644 (file)
--- 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);
 
 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_VERBOSE 1

-#define MC_USE_SNAPSHOT_HASH 1

 
 /********************************** DPOR for safety property **************************************/
 
 
 /********************************** DPOR for safety property **************************************/
 

diff --git a/src/simgrid/sg_config.c b/src/simgrid/sg_config.c
index b812c87..ad88f30 100644 (file)
--- 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");
 
                      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)",
     /* Set max depth exploration */
     xbt_cfg_register(&_sg_cfg_set, "model-check/max_depth",
                      "Specify the max depth of exploration (default : 1000)",