X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/452237878ed316508bdfa05e3af625f549628842..6f5199d14e3f1b6505d3e264257bfe64bd991ca7:/src/mc/mc_config.cpp diff --git a/src/mc/mc_config.cpp b/src/mc/mc_config.cpp index 5acdd2bbf5..4aebb9bd62 100644 --- a/src/mc/mc_config.cpp +++ b/src/mc/mc_config.cpp @@ -34,8 +34,6 @@ simgrid::mc::ReductionMode reduction_mode = simgrid::mc::ReductionMode::unset; #define _sg_do_model_check 0 #endif -int _sg_mc_timeout = 0; - static void _mc_cfg_cb_check(const char* spec, bool more_check = true) { if (_sg_cfg_init_status && not _sg_do_model_check && more_check) @@ -44,123 +42,102 @@ static void _mc_cfg_cb_check(const char* spec, bool more_check = true) spec); } -void _mc_cfg_cb_timeout(const char *name) -{ - _mc_cfg_cb_check("value to enable/disable timeout for wait requests", MC_record_path.empty()); +/* 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)", ""}; - _sg_mc_timeout = xbt_cfg_get_boolean(name); -} +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", MC_record_path.empty()); }}; #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; -std::string _sg_mc_property_file; -int _sg_mc_hash = 0; -int _sg_mc_max_depth = 1000; int _sg_mc_max_visited_states = 0; -std::string _sg_mc_dot_output_file; -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) -{ - _mc_cfg_cb_check("reduction strategy"); - - std::string val = xbt_cfg_get_string(name); - if (val == "none") - simgrid::mc::reduction_mode = simgrid::mc::ReductionMode::none; - else if (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) -{ - _mc_cfg_cb_check("checkpointing value"); - - _sg_mc_checkpoint = xbt_cfg_get_int(name); -} - -void _mc_cfg_cb_sparse_checkpoint(const char *name) { - _mc_cfg_cb_check("checkpointing value"); - - _sg_mc_sparse_checkpoint = xbt_cfg_get_boolean(name); -} - -void _mc_cfg_cb_ksm(const char *name) -{ - _mc_cfg_cb_check("KSM value"); - - _sg_mc_ksm = xbt_cfg_get_boolean(name); -} - -void _mc_cfg_cb_property(const char *name) -{ - _mc_cfg_cb_check("property"); - - _sg_mc_property_file = xbt_cfg_get_string(name); -} - -void _mc_cfg_cb_hash(const char *name) -{ - _mc_cfg_cb_check("value to enable/disable the use of global hash to speedup state comparaison"); - - _sg_mc_hash = xbt_cfg_get_boolean(name); -} - -void _mc_cfg_cb_snapshot_fds(const char *name) -{ - _mc_cfg_cb_check("value to enable/disable the use of FD snapshotting"); - - _sg_mc_snapshot_fds = xbt_cfg_get_boolean(name); -} - -void _mc_cfg_cb_max_depth(const char *name) -{ - _mc_cfg_cb_check("max depth value"); - - _sg_mc_max_depth = xbt_cfg_get_int(name); -} - -void _mc_cfg_cb_visited(const char *name) -{ - _mc_cfg_cb_check("number of stored visited states"); - - _sg_mc_max_visited_states = xbt_cfg_get_int(name); -} - -void _mc_cfg_cb_dot_output(const char *name) -{ - _mc_cfg_cb_check("file name for a dot output of graph state"); - _sg_mc_dot_output_file = xbt_cfg_get_string(name); -} - -void _mc_cfg_cb_comms_determinism(const char *name) -{ - _mc_cfg_cb_check("value to enable/disable the detection of determinism in the communications schemes"); - - _sg_mc_comms_determinism = xbt_cfg_get_boolean(name); -} - -void _mc_cfg_cb_send_determinism(const char *name) -{ - _mc_cfg_cb_check("value to enable/disable the detection of send-determinism in the communications schemes"); - - _sg_mc_send_determinism = xbt_cfg_get_boolean(name); -} - -void _mc_cfg_cb_termination(const char *name) -{ - _mc_cfg_cb_check("value to enable/disable the detection of non progressive cycles"); - - _sg_mc_termination = xbt_cfg_get_boolean(name); -} +simgrid::config::Flag _sg_do_model_check_record{"model-check/record", "Record the model-checking paths", false}; + +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_sparse_checkpoint{"model-check/sparse-checkpoint", "Use sparse per-page snapshots.", + false, [](bool) { _mc_cfg_cb_check("checkpointing value"); }}; + +simgrid::config::Flag _sg_mc_ksm{"model-check/ksm", "Kernel same-page merging", false, + [](bool) { _mc_cfg_cb_check("KSM 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", + {"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", + {"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"); + }}; + +static simgrid::config::Flag _sg_mc_reduce{ + "model-check/reduction", "Specify the kind of exploration reduction (either none or DPOR)", "dpor", + [](const std::string& value) { + _mc_cfg_cb_check("reduction strategy"); + + if (value == "none") + simgrid::mc::reduction_mode = simgrid::mc::ReductionMode::none; + else if (value == "dpor") + simgrid::mc::reduction_mode = simgrid::mc::ReductionMode::dpor; + else + 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_snapshot_fds{ + "model-check/snapshot-fds", + {"model-check/snapshot_fds"}, + "Whether file descriptors must be snapshoted (currently unusable)", + false, + [](bool) { _mc_cfg_cb_check("value to enable/disable the use of FD snapshotting"); }}; + +simgrid::config::Flag _sg_mc_max_depth{"model-check/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. If value=5, the " + "last 5 visited states are stored. If value=0 (the default), all states are stored.", + 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", + {"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"); }}; #endif