From ff420e1906d916322427488153e45bf82d5c03dd Mon Sep 17 00:00:00 2001 From: Arnaud Giersch Date: Wed, 18 Apr 2018 18:11:53 +0200 Subject: [PATCH] Convert MC config parameters to C++ API, and move their definitions to mc_config.cpp. --- src/mc/ModelChecker.cpp | 2 +- src/mc/Session.cpp | 2 +- src/mc/checker/LivenessChecker.cpp | 4 +- src/mc/checker/simgrid_mc.cpp | 2 +- src/mc/mc_checkpoint.cpp | 4 +- src/mc/mc_config.cpp | 206 +++++++++++++---------------- src/mc/mc_config.hpp | 43 ++---- src/mc/mc_global.cpp | 2 +- src/simgrid/sg_config.cpp | 59 --------- 9 files changed, 114 insertions(+), 210 deletions(-) diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp index 1d19d0650b..3ca696bef4 100644 --- a/src/mc/ModelChecker.cpp +++ b/src/mc/ModelChecker.cpp @@ -96,7 +96,7 @@ void ModelChecker::start() process_->init(); - if (not _sg_mc_dot_output_file.empty()) + if (not _sg_mc_dot_output_file.get().empty()) MC_init_dot_output(); setup_ignore(); diff --git a/src/mc/Session.cpp b/src/mc/Session.cpp index 0553d8932f..2190ad043e 100644 --- a/src/mc/Session.cpp +++ b/src/mc/Session.cpp @@ -122,7 +122,7 @@ void Session::logState() { mc_model_checker->getChecker()->logState(); - if (not _sg_mc_dot_output_file.empty()) { + if (not _sg_mc_dot_output_file.get().empty()) { fprintf(dot_output, "}\n"); fclose(dot_output); } diff --git a/src/mc/checker/LivenessChecker.cpp b/src/mc/checker/LivenessChecker.cpp index c1afd7a597..ee00b66ec6 100644 --- a/src/mc/checker/LivenessChecker.cpp +++ b/src/mc/checker/LivenessChecker.cpp @@ -345,8 +345,8 @@ void LivenessChecker::backtrack() void LivenessChecker::run() { - XBT_INFO("Check the liveness property %s", _sg_mc_property_file.c_str()); - MC_automaton_load(_sg_mc_property_file.c_str()); + XBT_INFO("Check the liveness property %s", _sg_mc_property_file.get().c_str()); + MC_automaton_load(_sg_mc_property_file.get().c_str()); XBT_DEBUG("Starting the liveness algorithm"); simgrid::mc::session->initialize(); diff --git a/src/mc/checker/simgrid_mc.cpp b/src/mc/checker/simgrid_mc.cpp index 13431d3899..a6e3159145 100644 --- a/src/mc/checker/simgrid_mc.cpp +++ b/src/mc/checker/simgrid_mc.cpp @@ -43,7 +43,7 @@ static std::unique_ptr createChecker(simgrid::mc::Session& { if (_sg_mc_comms_determinism || _sg_mc_send_determinism) return std::unique_ptr(simgrid::mc::createCommunicationDeterminismChecker(session)); - else if (_sg_mc_property_file.empty()) + else if (_sg_mc_property_file.get().empty()) return std::unique_ptr(simgrid::mc::createSafetyChecker(session)); else return std::unique_ptr(simgrid::mc::createLivenessChecker(session)); diff --git a/src/mc/mc_checkpoint.cpp b/src/mc/mc_checkpoint.cpp index 11ef27c0b9..bd1a8d719a 100644 --- a/src/mc/mc_checkpoint.cpp +++ b/src/mc/mc_checkpoint.cpp @@ -519,7 +519,7 @@ static std::vector get_current_fds(pid_t pid) // If dot_output enabled, do not handle the corresponding file if (dot_output != nullptr) { std::string link_basename = simgrid::xbt::Path(link).getBasename(); - if (link_basename == _sg_mc_dot_output_file) + if (link_basename == _sg_mc_dot_output_file.get()) continue; } @@ -561,7 +561,7 @@ std::shared_ptr take_snapshot(int num_state) snapshot->to_ignore = mc_model_checker->process().ignored_heap(); - if (_sg_mc_max_visited_states > 0 || not _sg_mc_property_file.empty()) { + if (_sg_mc_max_visited_states > 0 || not _sg_mc_property_file.get().empty()) { snapshot->stacks = take_snapshot_stacks(snapshot.get()); if (_sg_mc_hash) snapshot->hash = simgrid::mc::hash(*snapshot); diff --git a/src/mc/mc_config.cpp b/src/mc/mc_config.cpp index 5acdd2bbf5..fbe43122f6 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,103 @@ 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) */ +static simgrid::config::Flag _sg_mc_record_path{ + "model-check/replay", "Model-check path to replay (as reported by SimGrid when a violation is reported)", "", + [](const std::string& value) { MC_record_path = value; }}; - _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 diff --git a/src/mc/mc_config.hpp b/src/mc/mc_config.hpp index 8f88805574..0068a2c6e9 100644 --- a/src/mc/mc_config.hpp +++ b/src/mc/mc_config.hpp @@ -6,38 +6,23 @@ #ifndef MC_CONFIG_HPP #define MC_CONFIG_HPP -#include +#include /********************************** Configuration of MC **************************************/ extern "C" XBT_PUBLIC int _sg_do_model_check; -extern XBT_PRIVATE int _sg_do_model_check_record; -extern XBT_PRIVATE int _sg_mc_checkpoint; -extern XBT_PUBLIC int _sg_mc_sparse_checkpoint; -extern XBT_PUBLIC int _sg_mc_ksm; -extern XBT_PUBLIC std::string _sg_mc_property_file; -extern XBT_PRIVATE int _sg_mc_timeout; -extern XBT_PRIVATE int _sg_mc_hash; -extern XBT_PRIVATE int _sg_mc_max_depth; +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; +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_snapshot_fds; +extern XBT_PRIVATE simgrid::config::Flag _sg_mc_max_depth; extern "C" XBT_PUBLIC int _sg_mc_max_visited_states; -extern XBT_PRIVATE std::string _sg_mc_dot_output_file; -extern XBT_PUBLIC int _sg_mc_comms_determinism; -extern XBT_PUBLIC int _sg_mc_send_determinism; -extern XBT_PRIVATE int _sg_mc_snapshot_fds; -extern XBT_PRIVATE int _sg_mc_termination; - -XBT_PRIVATE void _mc_cfg_cb_reduce(const char* name); -XBT_PRIVATE void _mc_cfg_cb_checkpoint(const char* name); -XBT_PRIVATE void _mc_cfg_cb_sparse_checkpoint(const char* name); -XBT_PRIVATE void _mc_cfg_cb_ksm(const char* name); -XBT_PRIVATE void _mc_cfg_cb_property(const char* name); -XBT_PRIVATE void _mc_cfg_cb_timeout(const char* name); -XBT_PRIVATE void _mc_cfg_cb_snapshot_fds(const char* name); -XBT_PRIVATE void _mc_cfg_cb_hash(const char* name); -XBT_PRIVATE void _mc_cfg_cb_max_depth(const char* name); -XBT_PRIVATE void _mc_cfg_cb_visited(const char* name); -XBT_PRIVATE void _mc_cfg_cb_dot_output(const char* name); -XBT_PRIVATE void _mc_cfg_cb_comms_determinism(const char* name); -XBT_PRIVATE void _mc_cfg_cb_send_determinism(const char* name); -XBT_PRIVATE void _mc_cfg_cb_termination(const char* name); +extern XBT_PRIVATE simgrid::config::Flag _sg_mc_dot_output_file; +extern XBT_PRIVATE simgrid::config::Flag _sg_mc_termination; #endif diff --git a/src/mc/mc_global.cpp b/src/mc/mc_global.cpp index c0fbaa3eb3..ac4ccd4c99 100644 --- a/src/mc/mc_global.cpp +++ b/src/mc/mc_global.cpp @@ -76,7 +76,7 @@ FILE *dot_output = nullptr; void MC_init_dot_output() { - dot_output = fopen(_sg_mc_dot_output_file.c_str(), "w"); + dot_output = fopen(_sg_mc_dot_output_file.get().c_str(), "w"); if (dot_output == nullptr) { perror("Error open dot output file"); diff --git a/src/simgrid/sg_config.cpp b/src/simgrid/sg_config.cpp index 5999898c24..afb483b842 100644 --- a/src/simgrid/sg_config.cpp +++ b/src/simgrid/sg_config.cpp @@ -187,12 +187,6 @@ static void _sg_cfg_cb__network_model(const std::string& value) find_model_description(surf_network_model_description, value); } -#if SIMGRID_HAVE_MC -static void _sg_cfg_cb_model_check_record(const char *name) { - _sg_do_model_check_record = xbt_cfg_get_boolean(name); -} -#endif - static void _sg_cfg_cb_contexts_parallel_mode(const std::string& mode_name) { if (mode_name == "posix") { @@ -299,59 +293,6 @@ void sg_config_init(int *argc, char **argv) "default unless optim is set to lazy)", "no"); simgrid::config::alias("network/maxmin-selective-update", {"network/maxmin_selective_update"}); - /* Replay (this part is enabled even if MC it disabled) */ - simgrid::config::bindFlag(MC_record_path, "model-check/replay", - "Model-check path to replay (as reported by SimGrid when a violation is reported)"); - -#if SIMGRID_HAVE_MC - /* do model-checking-record */ - xbt_cfg_register_boolean("model-check/record", "no", _sg_cfg_cb_model_check_record, - "Record the model-checking paths"); - - xbt_cfg_register_int("model-check/checkpoint", 0, _mc_cfg_cb_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."); - - xbt_cfg_register_boolean("model-check/sparse-checkpoint", "no", _mc_cfg_cb_sparse_checkpoint, - "Use sparse per-page snapshots."); - xbt_cfg_register_boolean("model-check/ksm", "no", _mc_cfg_cb_ksm, "Kernel same-page merging"); - - xbt_cfg_register_string("model-check/property", "", _mc_cfg_cb_property, - "Name of the file containing the property, as formatted by the ltl2ba program."); - xbt_cfg_register_boolean("model-check/communications-determinism", "no", _mc_cfg_cb_comms_determinism, - "Whether to enable the detection of communication determinism"); - simgrid::config::alias("model-check/communications-determinism", {"model-check/communications_determinism"}); - - xbt_cfg_register_boolean("model-check/send-determinism", "no", _mc_cfg_cb_send_determinism, - "Enable/disable the detection of send-determinism in the communications schemes"); - simgrid::config::alias("model-check/send-determinism", {"model-check/send_determinism"}); - - /* Specify the kind of model-checking reduction */ - xbt_cfg_register_string("model-check/reduction", "dpor", _mc_cfg_cb_reduce, - "Specify the kind of exploration reduction (either none or DPOR)"); - xbt_cfg_register_boolean("model-check/timeout", "no", _mc_cfg_cb_timeout, - "Whether to enable timeouts for wait requests"); - - xbt_cfg_register_boolean("model-check/hash", "no", _mc_cfg_cb_hash, - "Whether to enable state hash for state comparison (experimental)"); - xbt_cfg_register_boolean("model-check/snapshot-fds", "no", _mc_cfg_cb_snapshot_fds, - "Whether file descriptors must be snapshoted (currently unusable)"); - simgrid::config::alias("model-check/snapshot-fds", {"model-check/snapshot_fds"}); - xbt_cfg_register_int("model-check/max-depth", 1000, _mc_cfg_cb_max_depth, - "Maximal exploration depth (default: 1000)"); - simgrid::config::alias("model-check/max-depth", {"model-check/max_depth"}); - xbt_cfg_register_int("model-check/visited", 0, _mc_cfg_cb_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."); - - xbt_cfg_register_string("model-check/dot-output", "", _mc_cfg_cb_dot_output, - "Name of dot output file corresponding to graph state"); - simgrid::config::alias("model-check/dot-output", {"model-check/dot_output"}); - xbt_cfg_register_boolean("model-check/termination", "no", _mc_cfg_cb_termination, - "Whether to enable non progressive cycle detection"); -#endif extern bool _sg_do_verbose_exit; simgrid::config::bindFlag(_sg_do_verbose_exit, "verbose-exit", "Activate the \"do nothing\" mode in Ctrl-C"); -- 2.20.1