[mc] Code for evaluation of the impact of the hash

Generate log for evaluating the result of the test:
* true positive;
* true negative;
* false negative (there must not be any of them);
* false positive (should be minimised).

diff --git a/src/mc/mc_compare.c b/src/mc/mc_compare.c
index 1405e25..b9ea20c 100644 (file)
--- a/src/mc/mc_compare.c
+++ b/src/mc/mc_compare.c
@@ -390,10 +390,14 @@ int snapshot_compare(void *state1, void *state2){
     xbt_os_walltimer_start(timer);
   #endif
 
+  int hash_result = 0;
   if(MC_USE_SNAPSHOT_HASH) {
-    if(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);
+#ifndef MC_DEBUG
       return 1;
+#endif
     } else {
       XBT_VERB("(%d - %d) Same hash : 0x%" PRIx64, num1, num2, s1->hash);
     }
@@ -598,10 +602,22 @@ int snapshot_compare(void *state1, void *state2){
   #endif
 
 #ifdef MC_VERBOSE
-   if(errors==0)
+   if(errors || hash_result)
+     XBT_VERB("(%d - %d) Difference found", num1, num2);
+   else
      XBT_VERB("(%d - %d) No difference found", num1, num2);
 #endif
-  return errors > 0;
+
+#if defined(MC_DEBUG) && defined(MC_VERBOSE) && MC_USE_SNAPSHOT_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");
+#endif
+
+   return errors > 0 || hash_result;
   
 }
 

diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h
index f4c4cae..dfabace 100644 (file)
--- a/src/mc/mc_private.h
+++ b/src/mc/mc_private.h
@@ -263,7 +263,7 @@ void print_comparison_times(void);
 
 //#define MC_DEBUG 1
 #define MC_VERBOSE 1
-
+#define MC_USE_SNAPSHOT_HASH 1
 
 /********************************** DPOR for safety property **************************************/
 
@@ -502,7 +502,5 @@ bool mc_address_test(mc_address_set_t p, const void* value);
  * */
 uint64_t mc_hash_processes_state(int num_state, xbt_dynar_t stacks);
 
-#define MC_USE_SNAPSHOT_HASH 1
-
 #endif