X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/f9436b840852218b39dce22d6057b6f223168daa..d75fff3ccf9a0caf5d851cfd9dee6a2a0fe47864:/src/mc/mc_config.cpp diff --git a/src/mc/mc_config.cpp b/src/mc/mc_config.cpp index a288a173d0..b6dc36908b 100644 --- a/src/mc/mc_config.cpp +++ b/src/mc/mc_config.cpp @@ -1,186 +1,122 @@ -/* Copyright (c) 2008-2015. The SimGrid Team. - * All rights reserved. */ +/* Copyright (c) 2008-2022. The SimGrid Team. All rights reserved. */ /* This program is free software; you can redistribute it and/or modify it * under the terms of the license (GNU LGPL) which comes with this package. */ -#include -#include -#include +#include "src/mc/mc_config.hpp" +#include "src/mc/mc_replay.hpp" +#include -#include -#include "src/mc/mc_replay.h" - -#include +XBT_LOG_EXTERNAL_DEFAULT_CATEGORY(xbt_cfg); #if SIMGRID_HAVE_MC -#include "src/mc/mc_safety.h" -#include "src/mc/mc_private.h" -#endif - -#include "src/mc/mc_record.h" - -XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_config, mc, - "Configuration of MC"); +#include -#if SIMGRID_HAVE_MC -namespace simgrid { -namespace mc { -/* Configuration support */ -simgrid::mc::ReductionMode reduction_mode = simgrid::mc::ReductionMode::unset; -} -} -#endif - -#if !SIMGRID_HAVE_MC +#else #define _sg_do_model_check 0 #endif -int _sg_mc_timeout = 0; - -void _mc_cfg_cb_timeout(const char *name) +static void _mc_cfg_cb_check(const char* spec, bool more_check = true) { - if (_sg_cfg_init_status && !(_sg_do_model_check || MC_record_path)) - xbt_die("You are specifying a value to enable/disable timeout for wait requests after the initialization (through MSG_config?), but model-checking was not activated at config time (through bu the program was not runned under the model-checker (with simgrid-mc)). This won't work, sorry."); - - _sg_mc_timeout = xbt_cfg_get_boolean(name); + xbt_assert(_sg_cfg_init_status == 0 || _sg_do_model_check || not more_check, + "Specifying a %s is only allowed within the model-checker. Please use simgrid-mc.", spec); } +/* Replay (this part is enabled even if MC it disabled) */ +simgrid::config::Flag _sg_mc_record_path{ + "model-check/replay", "Model-check path to replay (as reported by SimGrid when a violation is reported)", "", + [](std::string_view value) { MC_record_path() = value; }}; + +simgrid::config::Flag _sg_mc_timeout{ + "model-check/timeout", "Whether to enable timeouts for wait requests", false, [](bool) { + _mc_cfg_cb_check("value to enable/disable timeout for wait requests", not MC_record_replay_is_active()); + }}; + #if SIMGRID_HAVE_MC int _sg_do_model_check = 0; -int _sg_do_model_check_record = 0; -int _sg_mc_checkpoint = 0; -int _sg_mc_sparse_checkpoint = 0; -int _sg_mc_ksm = 0; -char *_sg_mc_property_file = nullptr; -int _sg_mc_hash = 0; -int _sg_mc_max_depth = 1000; int _sg_mc_max_visited_states = 0; -char *_sg_mc_dot_output_file = nullptr; -int _sg_mc_comms_determinism = 0; -int _sg_mc_send_determinism = 0; -int _sg_mc_snapshot_fds = 0; -int _sg_mc_termination = 0; - -void _mc_cfg_cb_reduce(const char *name) -{ - if (_sg_cfg_init_status && !_sg_do_model_check) - xbt_die - ("You are specifying a reduction strategy after the initialization (through MSG_config?), but model-checking was not activated at config time (through bu the program was not runned under the model-checker (with simgrid-mc)). This won't work, sorry."); - - char *val = xbt_cfg_get_string(name); - if (not strcasecmp(val, "none")) - simgrid::mc::reduction_mode = simgrid::mc::ReductionMode::none; - else if (not strcasecmp(val, "dpor")) - simgrid::mc::reduction_mode = simgrid::mc::ReductionMode::dpor; - else - xbt_die("configuration option %s can only take 'none' or 'dpor' as a value", - name); -} - -void _mc_cfg_cb_checkpoint(const char *name) -{ - if (_sg_cfg_init_status && !_sg_do_model_check) - xbt_die - ("You are specifying a checkpointing value after the initialization (through MSG_config?), but model-checking was not activated at config time (through bu the program was not runned under the model-checker (with simgrid-mc)). This won't work, sorry."); - - _sg_mc_checkpoint = xbt_cfg_get_int(name); -} - -void _mc_cfg_cb_sparse_checkpoint(const char *name) { - if (_sg_cfg_init_status && !_sg_do_model_check) - xbt_die("You are specifying a checkpointing value after the initialization (through MSG_config?), but model-checking was not activated at config time (through bu the program was not runned under the model-checker (with simgrid-mc)). This won't work, sorry."); - - _sg_mc_sparse_checkpoint = xbt_cfg_get_boolean(name); -} - -void _mc_cfg_cb_ksm(const char *name) -{ - if (_sg_cfg_init_status && !_sg_do_model_check) - xbt_die("You are specifying a KSM value after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry."); - - _sg_mc_ksm = xbt_cfg_get_boolean(name); -} - -void _mc_cfg_cb_property(const char *name) -{ - if (_sg_cfg_init_status && !_sg_do_model_check) - xbt_die - ("You are specifying a property after the initialization (through MSG_config?), but model-checking was not activated at config time (through bu the program was not runned under the model-checker (with simgrid-mc)). This won't work, sorry."); - - _sg_mc_property_file = xbt_cfg_get_string(name); -} - -void _mc_cfg_cb_hash(const char *name) -{ - if (_sg_cfg_init_status && !_sg_do_model_check) - xbt_die - ("You are specifying a value to enable/disable the use of global hash to speedup state comparaison, but model-checking was not activated at config time (through bu the program was not runned under the model-checker (with simgrid-mc)). This won't work, sorry."); - - _sg_mc_hash = xbt_cfg_get_boolean(name); -} - -void _mc_cfg_cb_snapshot_fds(const char *name) -{ - if (_sg_cfg_init_status && !_sg_do_model_check) - xbt_die - ("You are specifying a value to enable/disable the use of FD snapshotting, but model-checking was not activated at config time (through bu the program was not runned under the model-checker (with simgrid-mc)). This won't work, sorry."); - - _sg_mc_snapshot_fds = xbt_cfg_get_boolean(name); -} - -void _mc_cfg_cb_max_depth(const char *name) -{ - if (_sg_cfg_init_status && !_sg_do_model_check) - xbt_die - ("You are specifying a max depth value after the initialization (through MSG_config?), but model-checking was not activated at config time (through bu the program was not runned under the model-checker (with simgrid-mc)). This won't work, sorry."); - - _sg_mc_max_depth = xbt_cfg_get_int(name); -} - -void _mc_cfg_cb_visited(const char *name) -{ - if (_sg_cfg_init_status && !_sg_do_model_check) - xbt_die - ("You are specifying a number of stored visited states after the initialization (through MSG_config?), but model-checking was not activated at config time (through bu the program was not runned under the model-checker (with simgrid-mc)). This won't work, sorry."); - _sg_mc_max_visited_states = xbt_cfg_get_int(name); -} - -void _mc_cfg_cb_dot_output(const char *name) -{ - if (_sg_cfg_init_status && !_sg_do_model_check) - xbt_die - ("You are specifying a file name for a dot output of graph state after the initialization (through MSG_config?), but model-checking was not activated at config time (through bu the program was not runned under the model-checker (with simgrid-mc)). This won't work, sorry."); - - _sg_mc_dot_output_file = xbt_cfg_get_string(name); -} - -void _mc_cfg_cb_comms_determinism(const char *name) +static simgrid::config::Flag cfg_mc_reduction{ + "model-check/reduction", "Specify the kind of exploration reduction (either none or DPOR)", "dpor", + [](std::string_view value) { + if (value != "none" && value != "dpor") + xbt_die("configuration option 'model-check/reduction' can only take 'none' or 'dpor' as a value"); + }}; + +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 " + "step => faster verification, but huge memory consumption; higher values are good " + "compromises between speed and memory consumption.", + 0, [](int) { _mc_cfg_cb_check("checkpointing value"); }}; + +simgrid::config::Flag _sg_mc_property_file{ + "model-check/property", "Name of the file containing the property, as formatted by the ltl2ba program.", "", + [](const std::string&) { _mc_cfg_cb_check("property"); }}; + +simgrid::config::Flag _sg_mc_comms_determinism{ + "model-check/communications-determinism", + "Whether to enable the detection of communication determinism", + false, + [](bool) { + _mc_cfg_cb_check("value to enable/disable the detection of determinism in the communications schemes"); + }}; + +simgrid::config::Flag _sg_mc_send_determinism{ + "model-check/send-determinism", + "Enable/disable the detection of send-determinism in the communications schemes", + false, + [](bool) { + _mc_cfg_cb_check("value to enable/disable the detection of send-determinism in the communications schemes"); + }}; + +simgrid::config::Flag _sg_mc_unfolding_checker{ + "model-check/unfolding-checker", + "Whether to enable the unfolding-based dynamic partial order reduction to MPI programs", false, [](bool) { + _mc_cfg_cb_check("value to to enable/disable the unfolding-based dynamic partial order reduction to MPI programs"); + }}; + +simgrid::config::Flag _sg_mc_buffering{ + "smpi/buffering", + "Buffering semantic to use for MPI (only used in MC)", + "infty", + {{"zero", "No system buffering: MPI_Send is blocking"}, + {"infty", "Infinite system buffering: MPI_Send returns immediately"}}, + [](std::string_view) { _mc_cfg_cb_check("buffering mode"); }}; + +simgrid::config::Flag _sg_mc_max_depth{"model-check/max-depth", + "Maximal exploration depth (default: 1000)", + 1000, + [](int) { _mc_cfg_cb_check("max depth value"); }}; + +static simgrid::config::Flag _sg_mc_max_visited_states__{ + "model-check/visited", + "Specify the number of visited state stored for state comparison reduction: any branch leading to a state that is " + "already stored is cut.\n" + "If value=5, the last 5 visited states are stored. If value=0 (the default), no state is stored and this reduction " + "technique is disabled.", + 0, [](int value) { + _mc_cfg_cb_check("number of stored visited states"); + _sg_mc_max_visited_states = value; + }}; + +simgrid::config::Flag _sg_mc_dot_output_file{ + "model-check/dot-output", + "Name of dot output file corresponding to graph state", + "", + [](const std::string&) { _mc_cfg_cb_check("file name for a dot output of graph state"); }}; + +simgrid::config::Flag _sg_mc_termination{ + "model-check/termination", "Whether to enable non progressive cycle detection", false, + [](bool) { _mc_cfg_cb_check("value to enable/disable the detection of non progressive cycles"); }}; + +bool simgrid::mc::cfg_use_DPOR() { - if (_sg_cfg_init_status && !_sg_do_model_check) - xbt_die - ("You are specifying a value to enable/disable the detection of determinism in the communications schemes after the initialization (through MSG_config?), but model-checking was not activated at config time (through bu the program was not runned under the model-checker (with simgrid-mc)). This won't work, sorry."); - - _sg_mc_comms_determinism = xbt_cfg_get_boolean(name); -} - -void _mc_cfg_cb_send_determinism(const char *name) -{ - if (_sg_cfg_init_status && !_sg_do_model_check) - xbt_die - ("You are specifying a value to enable/disable the detection of send-determinism in the communications schemes after the initialization (through MSG_config?), but model-checking was not activated at config time (through bu the program was not runned under the model-checker (with simgrid-mc)). This won't work, sorry."); - - _sg_mc_send_determinism = xbt_cfg_get_boolean(name); -} - -void _mc_cfg_cb_termination(const char *name) -{ - if (_sg_cfg_init_status && !_sg_do_model_check) - xbt_die - ("You are specifying a value to enable/disable the detection of non progressive cycles after the initialization (through MSG_config?), but model-checking was not activated at config time (through bu the program was not runned under the model-checker (with simgrid-mc)). This won't work, sorry."); - - _sg_mc_termination = xbt_cfg_get_boolean(name); + if (cfg_mc_reduction.get() == "dpor" && _sg_mc_max_visited_states__ > 0) { + XBT_INFO("Disabling DPOR since state-equality reduction is activated with 'model-check/visited'"); + return false; + } + return cfg_mc_reduction.get() == "dpor"; } #endif