Remove option model-checker/hash; This is always activated now.

diff --git a/ChangeLog b/ChangeLog
index 11be863..b67daea 100644 (file)
--- a/ChangeLog
+++ b/ChangeLog
@@ -5,6 +5,9 @@ SimGrid (3.23.3) NOT RELEASED YET (v3.24 expected September 23. 7:50 UTC)
 SMPI:
  - Fortran bindings for DVFS have been removed.
 
+Model-Checker:
+ - Option model-checker/hash was removed. This is always activated now.
+
 ----------------------------------------------------------------------------
 
 SimGrid (3.23.2) July 8. 2019

diff --git a/docs/source/Configuring_SimGrid.rst b/docs/source/Configuring_SimGrid.rst
index b980e4a..27cb2c6 100644 (file)
--- a/docs/source/Configuring_SimGrid.rst
+++ b/docs/source/Configuring_SimGrid.rst
@@ -112,7 +112,6 @@ Existing Configuration Items
 - **model-check/checkpoint:** :ref:`cfg=model-check/checkpoint`
 - **model-check/communications-determinism:** :ref:`cfg=model-check/communications-determinism`
 - **model-check/dot-output:** :ref:`cfg=model-check/dot-output`
-- **model-check/hash:** :ref:`cfg=model-checker/hash`
 - **model-check/max-depth:** :ref:`cfg=model-check/max-depth`
 - **model-check/property:** :ref:`cfg=model-check/property`
 - **model-check/reduction:** :ref:`cfg=model-check/reduction`
@@ -630,23 +629,6 @@ protected with guards: if the stack size is too small for your
 application, the stack will silently overflow on other parts of the
 memory (see :ref:`contexts/guard-size <cfg=contexts/guard-size>`).
 
-.. _cfg=model-checker/hash:
-
-State Hashing
-.............
-
-Usually most of the time of the model-checker is spent comparing states. This
-process is complicated and consumes a lot of bandwidth and cache.
-In order to speedup the state comparison, the experimental ``model-checker/hash``
-configuration item enables the computation of a hash summarizing as much
-information of the state as possible into a single value. This hash can be used
-to avoid most of the comparisons: the costly comparison is then only used when
-the hashes are identical.
-
-Currently most of the state is not included in the hash because the
-implementation was found to be buggy and this options is not as useful as
-it could be. For this reason, it is currently disabled by default.
-
 .. _cfg=model-check/replay:
 
 Replaying buggy execution paths out of the model-checker

diff --git a/src/mc/compare.cpp b/src/mc/compare.cpp
index aad1013..0c31ffd 100644 (file)
--- a/src/mc/compare.cpp
+++ b/src/mc/compare.cpp
@@ -1382,14 +1382,12 @@ int snapshot_compare(Snapshot* s1, Snapshot* s2)
 
   RemoteClient* process = &mc_model_checker->process();
 
-  if (_sg_mc_hash) {
-    if (s1->hash_ != s2->hash_) {
-      XBT_VERB("(%d - %d) Different hash: 0x%" PRIx64 "--0x%" PRIx64, s1->num_state_, s2->num_state_, s1->hash_,
-               s2->hash_);
-      return 1;
+  if (s1->hash_ != s2->hash_) {
+    XBT_VERB("(%d - %d) Different hash: 0x%" PRIx64 "--0x%" PRIx64, s1->num_state_, s2->num_state_, s1->hash_,
+             s2->hash_);
+    return 1;
     } else
       XBT_VERB("(%d - %d) Same hash: 0x%" PRIx64, s1->num_state_, s2->num_state_, s1->hash_);
-  }
 
   /* Compare enabled processes */
   if (s1->enabled_processes_ != s2->enabled_processes_) {

diff --git a/src/mc/mc_config.cpp b/src/mc/mc_config.cpp
index b1a70e3..8f60917 100644 (file)
--- a/src/mc/mc_config.cpp
+++ b/src/mc/mc_config.cpp
@@ -86,10 +86,6 @@ static simgrid::config::Flag<std::string> _sg_mc_reduce{
         xbt_die("configuration option model-check/reduction can only take 'none' or 'dpor' as a value");
     }};
 
-simgrid::config::Flag<bool> _sg_mc_hash{
-    "model-check/hash", "Whether to enable state hash for state comparison (experimental)", false,
-    [](bool) { _mc_cfg_cb_check("value to enable/disable the use of global hash to speedup state comparaison"); }};
-
 simgrid::config::Flag<int> _sg_mc_max_depth{"model-check/max-depth",
                                             {"model-check/max_depth"},
                                             "Maximal exploration depth (default: 1000)",

diff --git a/src/mc/mc_config.hpp b/src/mc/mc_config.hpp
index 4d17667..61d2c35 100644 (file)
--- a/src/mc/mc_config.hpp
+++ b/src/mc/mc_config.hpp
@@ -16,7 +16,6 @@ extern XBT_PUBLIC simgrid::config::Flag<std::string> _sg_mc_property_file;
 extern XBT_PUBLIC simgrid::config::Flag<bool> _sg_mc_comms_determinism;
 extern XBT_PUBLIC simgrid::config::Flag<bool> _sg_mc_send_determinism;
 extern XBT_PRIVATE simgrid::config::Flag<bool> _sg_mc_timeout;
-extern XBT_PRIVATE simgrid::config::Flag<bool> _sg_mc_hash;
 extern XBT_PRIVATE simgrid::config::Flag<int> _sg_mc_max_depth;
 extern "C" XBT_PUBLIC int _sg_mc_max_visited_states;
 extern XBT_PRIVATE simgrid::config::Flag<std::string> _sg_mc_dot_output_file;

diff --git a/src/mc/sosp/Snapshot.cpp b/src/mc/sosp/Snapshot.cpp
index bc72a2b..141d14a 100644 (file)
--- a/src/mc/sosp/Snapshot.cpp
+++ b/src/mc/sosp/Snapshot.cpp
@@ -217,8 +217,7 @@ Snapshot::Snapshot(int num_state, RemoteClient* process)
 
   if (_sg_mc_max_visited_states > 0 || not _sg_mc_property_file.get().empty()) {
     snapshot_stacks(process);
-    if (_sg_mc_hash)
-      hash_ = simgrid::mc::hash(*this);
+    hash_ = simgrid::mc::hash(*this);
   }
 
   snapshot_ignore_restore(this);