From 718cf4ba4da6d6032f60d8c4c432807b9c018185 Mon Sep 17 00:00:00 2001 From: Gabriel Corona Date: Mon, 10 Feb 2014 15:02:13 +0100 Subject: [PATCH] [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). --- src/mc/mc_compare.c | 22 +++++++++++++++++++--- src/mc/mc_private.h | 4 +--- 2 files changed, 20 insertions(+), 6 deletions(-) diff --git a/src/mc/mc_compare.c b/src/mc/mc_compare.c index 1405e259ea..b9ea20c69a 100644 --- 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 f4c4caef9f..dfabace050 100644 --- 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 -- 2.30.2