From: Martin Quinson Date: Wed, 15 May 2019 12:49:34 +0000 (+0200) Subject: Remove option 'model-check/record': paths are recorded in any cases X-Git-Tag: v3.22.4~127^2~11 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/ade29f42563cdc36cea26a7dd51fca288c160aa6?ds=sidebyside Remove option 'model-check/record': paths are recorded in any cases --- diff --git a/ChangeLog b/ChangeLog index a967110363..91fbb8ce94 100644 --- a/ChangeLog +++ b/ChangeLog @@ -12,6 +12,9 @@ SMPI: - MPI/IO is now supported over the Storage API (no files are written or read, storage is simulated). Supported calls are all synchronous ones. - MPI interface is now const correct for input parameters +Model-checker: + - Remove option 'model-check/record': Paths are recorded in any cases now. + Fixed bugs (GH=GitHub; FG=FramaGit): - FG#10: Can not use MSG_process_set_data from SMPI any more - FG#11: Auto-restart actors forget their on_exit behavior diff --git a/docs/source/Configuring_SimGrid.rst b/docs/source/Configuring_SimGrid.rst index 7a59994c84..ac9affccfb 100644 --- a/docs/source/Configuring_SimGrid.rst +++ b/docs/source/Configuring_SimGrid.rst @@ -110,7 +110,6 @@ Existing Configuration Items - **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/record:** :ref:`cfg=model-check/record` - **model-check/reduction:** :ref:`cfg=model-check/reduction` - **model-check/replay:** :ref:`cfg=model-check/replay` - **model-check/send-determinism:** :ref:`cfg=model-check/send-determinism` @@ -681,11 +680,10 @@ 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/record: .. _cfg=model-check/replay: -Recording and replaying verifications -..................................... +Replaying buggy execution paths out of the model-checker +........................................................ Debugging the problems reported by the model-checker is challenging: First, the application under verification cannot be debugged with gdb because the @@ -697,11 +695,7 @@ enabling the usage of classical debugging tools. When the model-checker finds an interesting path in the application execution graph (where a safety or liveness property is violated), it -can generate an identifier for this path. To enable this behavious the -``model-check/record`` must be set to **yes**, which is the case -by default. - -Here is an example of output: +generates an identifier for this path. Here is an example of output: .. code-block:: shell @@ -717,11 +711,11 @@ Here is an example of output: [ 0.000000] (0:@) Visited states = 68 [ 0.000000] (0:@) Executed transitions = 46 -This path can then be replayed outside of the model-checker (and even -in non-MC build of simgrid) by setting the ``model-check/replay`` item -to the given path. The other options should be the same (but the -model-checker should be disabled). Note that format and meaning of the -path may change between different releases. +The interesting line is ``Path = 1/3;1/4``, which means that you should use +`--cfg=model-check/replay:1/3;1/4`` to replay your application on the buggy +execution path. The other options should be the same (but the model-checker +should be disabled). Note that format and meaning of the path may change between +different releases. Configuring the User Code Virtualization ---------------------------------------- diff --git a/src/mc/mc_config.cpp b/src/mc/mc_config.cpp index ed3220ffad..584d0bae50 100644 --- a/src/mc/mc_config.cpp +++ b/src/mc/mc_config.cpp @@ -54,8 +54,6 @@ simgrid::config::Flag _sg_mc_timeout{ int _sg_do_model_check = 0; int _sg_mc_max_visited_states = 0; -simgrid::config::Flag _sg_do_model_check_record{"model-check/record", "Record the model-checking paths", true}; - simgrid::config::Flag _sg_mc_checkpoint{ "model-check/checkpoint", "Specify the amount of steps between checkpoints during stateful model-checking " "(default: 0 => stateless verification). If value=1, one checkpoint is saved for each " diff --git a/src/mc/mc_config.hpp b/src/mc/mc_config.hpp index 6ee0daf0fe..ffc0c2ed45 100644 --- a/src/mc/mc_config.hpp +++ b/src/mc/mc_config.hpp @@ -11,7 +11,6 @@ /********************************** Configuration of MC **************************************/ extern "C" XBT_PUBLIC int _sg_do_model_check; extern XBT_PUBLIC simgrid::config::Flag _sg_mc_record_path; -extern XBT_PRIVATE simgrid::config::Flag _sg_do_model_check_record; extern XBT_PRIVATE simgrid::config::Flag _sg_mc_checkpoint; extern XBT_PUBLIC simgrid::config::Flag _sg_mc_sparse_checkpoint; extern XBT_PUBLIC simgrid::config::Flag _sg_mc_ksm; diff --git a/src/mc/mc_record.cpp b/src/mc/mc_record.cpp index dd19a66a5d..115695c3dd 100644 --- a/src/mc/mc_record.cpp +++ b/src/mc/mc_record.cpp @@ -18,8 +18,7 @@ #include "src/mc/mc_state.hpp" #endif -XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_record, mc, - " Logging specific to MC record/replay facility"); +XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_record, mc, "Logging specific to MC record/replay facility"); namespace simgrid { namespace mc { @@ -99,10 +98,8 @@ std::string traceToString(simgrid::mc::RecordTrace const& trace) void dumpRecordPath() { - if (MC_record_is_active()) { - RecordTrace trace = mc_model_checker->getChecker()->getRecordTrace(); - XBT_INFO("Path = %s", traceToString(trace).c_str()); - } + RecordTrace trace = mc_model_checker->getChecker()->getRecordTrace(); + XBT_INFO("Path = %s", traceToString(trace).c_str()); } #endif diff --git a/src/mc/mc_record.hpp b/src/mc/mc_record.hpp index df5285e695..d4ead6f699 100644 --- a/src/mc/mc_record.hpp +++ b/src/mc/mc_record.hpp @@ -6,9 +6,8 @@ /** \file mc_record.hpp * * This file contains the MC replay/record functionnality. - * A MC path may be recorded by using ``-cfg=model-check/record:1`'`. - * The path is written in the log output and an be replayed with MC disabled - * (even with an non-MC build) with `--cfg=model-check/replay:$replayPath`. + * The recorded path is written in the log output and can be replayed with MC disabled + * (even with an non-MC build) using `--cfg=model-check/replay:$replayPath`. * * The same version of Simgrid should be used and the same arguments should be * passed to the application (without the MC specific arguments). @@ -39,13 +38,6 @@ XBT_PRIVATE void replay(const std::string& trace); } } -/** Whether the MC record mode is enabled - * - * The behaviour is not changed. The only real difference is that - * the path is writtent in the log when an interesting path is found. - */ -#define MC_record_is_active() _sg_do_model_check_record - // **** Data conversion #endif