From: Gabriel Corona Date: Tue, 26 May 2015 13:58:12 +0000 (+0200) Subject: [mc][doc] Document the model-check/hash option X-Git-Tag: v3_12~655 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/2cd779436d49dabd1bcf6162a19c96f66d8cd7c8 [mc][doc] Document the model-check/hash option --- diff --git a/doc/doxygen/options.doc b/doc/doxygen/options.doc index 13b3f0dd20..34207f526f 100644 --- a/doc/doxygen/options.doc +++ b/doc/doxygen/options.doc @@ -426,7 +426,21 @@ protected with guards: if the stack size is too small for your application, the stack will silently overflow on other parts of the memory. -\subsection options_recordreplay Record/replay +\subsection options_modelchecking_hash Hashing of the state (experimental) + +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 \b 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. + +\subsection options_recordreplay Record/replay (experimental) As the model-checker keeps jumping at different places in the execution graph, it is difficult to understand what happens when trying to debug an application