From f96797fbc8f3a5f6b0d26fbf899ff25a75323f56 Mon Sep 17 00:00:00 2001 From: Martin Quinson Date: Wed, 10 Jul 2019 16:43:31 +0200 Subject: [PATCH] Remove option model-checker/hash; This is always activated now. --- ChangeLog | 3 +++ docs/source/Configuring_SimGrid.rst | 18 ------------------ src/mc/compare.cpp | 10 ++++------ src/mc/mc_config.cpp | 4 ---- src/mc/mc_config.hpp | 1 - src/mc/sosp/Snapshot.cpp | 3 +-- 6 files changed, 8 insertions(+), 31 deletions(-) diff --git a/ChangeLog b/ChangeLog index 11be8636b3..b67daea893 100644 --- 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 b980e4ad1a..27cb2c6e27 100644 --- 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=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 aad1013626..0c31ffd097 100644 --- 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 b1a70e34b5..8f60917531 100644 --- a/src/mc/mc_config.cpp +++ b/src/mc/mc_config.cpp @@ -86,10 +86,6 @@ static simgrid::config::Flag _sg_mc_reduce{ xbt_die("configuration option model-check/reduction can only take 'none' or 'dpor' as a value"); }}; -simgrid::config::Flag _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 _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 4d176678a0..61d2c35765 100644 --- a/src/mc/mc_config.hpp +++ b/src/mc/mc_config.hpp @@ -16,7 +16,6 @@ extern XBT_PUBLIC simgrid::config::Flag _sg_mc_property_file; extern XBT_PUBLIC simgrid::config::Flag _sg_mc_comms_determinism; extern XBT_PUBLIC simgrid::config::Flag _sg_mc_send_determinism; extern XBT_PRIVATE simgrid::config::Flag _sg_mc_timeout; -extern XBT_PRIVATE simgrid::config::Flag _sg_mc_hash; extern XBT_PRIVATE simgrid::config::Flag _sg_mc_max_depth; extern "C" XBT_PUBLIC int _sg_mc_max_visited_states; extern XBT_PRIVATE simgrid::config::Flag _sg_mc_dot_output_file; diff --git a/src/mc/sosp/Snapshot.cpp b/src/mc/sosp/Snapshot.cpp index bc72a2b751..141d14a9b1 100644 --- 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); -- 2.20.1