}
*/
-Exploration* create_communication_determinism_checker(const std::vector<char*>& args)
+Exploration* create_communication_determinism_checker(const std::vector<char*>& args, bool with_dpor)
{
CommDetExtension::EXTENSION_ID = simgrid::mc::Exploration::extension_create<CommDetExtension>();
StateCommDet::EXTENSION_ID = simgrid::mc::State::extension_create<StateCommDet>();
XBT_DEBUG("********* Start communication determinism verification *********");
- auto base = new DFSExplorer(args);
+ auto base = new DFSExplorer(args, with_dpor);
auto extension = new CommDetExtension(*base);
DFSExplorer::on_exploration_start([extension](RemoteApp&) {
// Backtrack if we reached the maximum depth
if (stack_.size() > (std::size_t)_sg_mc_max_depth) {
- if (reductionMode_ == ReductionMode::dpor) {
+ if (reduction_mode_ == ReductionMode::dpor) {
XBT_ERROR("/!\\ Max depth of %d reached! THIS WILL PROBABLY BREAK the dpor reduction /!\\",
_sg_mc_max_depth.get());
XBT_ERROR("/!\\ If bad things happen, disable dpor with --cfg=model-check/reduction:none /!\\");
for (auto const& [aid, _] : next_state->get_actors_list()) {
if (next_state->is_actor_enabled(aid)) {
next_state->mark_todo(aid);
- if (reductionMode_ == ReductionMode::dpor)
+ if (reduction_mode_ == ReductionMode::dpor)
break; // With DPOR, we take the first enabled transition
}
}
while (not stack_.empty()) {
std::unique_ptr<State> state = std::move(stack_.back());
stack_.pop_back();
- if (reductionMode_ == ReductionMode::dpor) {
+ if (reduction_mode_ == ReductionMode::dpor) {
aid_t issuer_id = state->get_transition()->aid_;
for (auto i = stack_.rbegin(); i != stack_.rend(); ++i) {
State* prev_state = i->get();
}
}
-DFSExplorer::DFSExplorer(const std::vector<char*>& args) : Exploration(args)
+DFSExplorer::DFSExplorer(const std::vector<char*>& args, bool with_dpor) : Exploration(args)
{
- reductionMode_ = reduction_mode;
- if (_sg_mc_termination)
- reductionMode_ = ReductionMode::none;
- else if (reductionMode_ == ReductionMode::unset)
- reductionMode_ = ReductionMode::dpor;
-
- if (_sg_mc_termination)
- XBT_INFO("Check non progressive cycles");
+ if (with_dpor)
+ reduction_mode_ = ReductionMode::dpor;
else
- XBT_INFO("Start a DFS exploration. Reduction is: %s.",
- (reductionMode_ == ReductionMode::none ? "none"
- : (reductionMode_ == ReductionMode::dpor ? "dpor" : "unknown")));
+ reduction_mode_ = ReductionMode::none;
- XBT_DEBUG("Starting the DFS exploration");
+ if (_sg_mc_termination) {
+ if (with_dpor) {
+ XBT_INFO("Check non progressive cycles (turning DPOR off)");
+ reduction_mode_ = ReductionMode::none;
+ } else {
+ XBT_INFO("Check non progressive cycles");
+ }
+ } else
+ XBT_INFO("Start a DFS exploration. Reduction is: %s.", to_c_str(reduction_mode_));
auto initial_state = std::make_unique<State>(get_remote_app());
for (auto const& [aid, _] : initial_state->get_actors_list()) {
if (initial_state->is_actor_enabled(aid)) {
initial_state->mark_todo(aid);
- if (reductionMode_ == ReductionMode::dpor) {
+ if (reduction_mode_ == ReductionMode::dpor) {
XBT_DEBUG("Actor %ld is TODO, DPOR is ON so let's go for this one.", aid);
break;
}
stack_.push_back(std::move(initial_state));
}
-Exploration* create_dfs_exploration(const std::vector<char*>& args)
+Exploration* create_dfs_exploration(const std::vector<char*>& args, bool with_dpor)
{
- return new DFSExplorer(args);
+ return new DFSExplorer(args, with_dpor);
}
} // namespace simgrid::mc
#include "src/mc/VisitedState.hpp"
#include "src/mc/explo/Exploration.hpp"
-#include "src/mc/mc_safety.hpp"
#include <list>
#include <memory>
namespace simgrid::mc {
class XBT_PRIVATE DFSExplorer : public Exploration {
- ReductionMode reductionMode_ = ReductionMode::unset;
+ XBT_DECLARE_ENUM_CLASS(ReductionMode, none, dpor);
+
+ ReductionMode reduction_mode_;
long backtrack_count_ = 0;
static xbt::signal<void(RemoteApp&)> on_exploration_start_signal;
static xbt::signal<void(RemoteApp&)> on_log_state_signal;
public:
- explicit DFSExplorer(const std::vector<char*>& args);
+ explicit DFSExplorer(const std::vector<char*>& args, bool with_dpor);
void run() override;
RecordTrace get_record_trace() override;
std::vector<std::string> get_textual_trace() override;
// External constructors so that the types (and the types of their content) remain hidden
XBT_PUBLIC Exploration* create_liveness_checker(const std::vector<char*>& args);
-XBT_PUBLIC Exploration* create_dfs_exploration(const std::vector<char*>& args);
-XBT_PUBLIC Exploration* create_communication_determinism_checker(const std::vector<char*>& args);
+XBT_PUBLIC Exploration* create_dfs_exploration(const std::vector<char*>& args, bool with_dpor);
+XBT_PUBLIC Exploration* create_communication_determinism_checker(const std::vector<char*>& args, bool with_dpor);
XBT_PUBLIC Exploration* create_udpor_checker(const std::vector<char*>& args);
// FIXME: kill this template and use lambdas in boost::range_equal
XBT_LOG_EXTERNAL_DEFAULT_CATEGORY(mc);
+using namespace simgrid::mc;
+
int main(int argc, char** argv)
{
xbt_assert(argc >= 2, "Missing arguments");
#endif
sg_config_init(&argc, argv);
- simgrid::mc::Exploration* explo;
+ std::unique_ptr<Exploration> explo;
+
if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
- explo = simgrid::mc::create_communication_determinism_checker(argv_copy);
+ explo = std::unique_ptr<Exploration>(create_communication_determinism_checker(argv_copy, cfg_use_DPOR()));
else if (_sg_mc_unfolding_checker)
- explo = simgrid::mc::create_udpor_checker(argv_copy);
+ explo = std::unique_ptr<Exploration>(create_udpor_checker(argv_copy));
else if (_sg_mc_property_file.get().empty())
- explo = simgrid::mc::create_dfs_exploration(argv_copy);
+ explo = std::unique_ptr<Exploration>(create_dfs_exploration(argv_copy, cfg_use_DPOR()));
else
- explo = simgrid::mc::create_liveness_checker(argv_copy);
-
- std::unique_ptr<simgrid::mc::Exploration> checker{explo};
+ explo = std::unique_ptr<Exploration>(create_liveness_checker(argv_copy));
try {
- checker->run();
- } catch (const simgrid::mc::DeadlockError&) {
+ explo->run();
+ } catch (const DeadlockError&) {
return SIMGRID_MC_EXIT_DEADLOCK;
- } catch (const simgrid::mc::TerminationError&) {
+ } catch (const TerminationError&) {
return SIMGRID_MC_EXIT_NON_TERMINATION;
- } catch (const simgrid::mc::LivenessError&) {
+ } catch (const LivenessError&) {
return SIMGRID_MC_EXIT_LIVENESS;
}
return SIMGRID_MC_EXIT_SUCCESS;
#include <simgrid/sg_config.hpp>
#if SIMGRID_HAVE_MC
-#include "src/mc/mc_safety.hpp"
#include <string_view>
-#endif
-#if SIMGRID_HAVE_MC
-namespace simgrid::mc {
-/* Configuration support */
-simgrid::mc::ReductionMode reduction_mode = simgrid::mc::ReductionMode::unset;
-} // namespace simgrid::mc
#else
#define _sg_do_model_check 0
#endif
static void _mc_cfg_cb_check(const char* spec, bool more_check = true)
{
xbt_assert(_sg_cfg_init_status == 0 || _sg_do_model_check || not more_check,
- "You are specifying a %s after the initialization (through MSG_config?), but the program was not run "
- "under the model-checker (with simgrid-mc)). This won't work, sorry.",
- spec);
+ "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) */
int _sg_do_model_check = 0;
int _sg_mc_max_visited_states = 0;
+static simgrid::config::Flag<std::string> 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");
+ }};
+
+bool simgrid::mc::cfg_use_DPOR()
+{
+ return cfg_mc_reduction.get() == "dpor";
+}
+
simgrid::config::Flag<int> _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 "
{"infty", "Infinite system buffering: MPI_Send returns immediately"}},
[](std::string_view) { _mc_cfg_cb_check("buffering mode"); }};
-static simgrid::config::Flag<std::string> _sg_mc_reduce{
- "model-check/reduction", "Specify the kind of exploration reduction (either none or DPOR)", "dpor",
- [](std::string_view 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<int> _sg_mc_max_depth{"model-check/max-depth",
"Maximal exploration depth (default: 1000)",
1000,
#include <xbt/config.hpp>
/********************************** Configuration of MC **************************************/
+namespace simgrid::mc {
+bool cfg_use_DPOR(); // "model-check/reduction" == "DPOR"
+};
+
extern "C" XBT_PUBLIC int _sg_do_model_check;
extern XBT_PUBLIC simgrid::config::Flag<std::string> _sg_mc_buffering;
extern XBT_PRIVATE simgrid::config::Flag<int> _sg_mc_checkpoint;
#include "src/mc/inspect/mc_unw.hpp"
#include "src/mc/mc_config.hpp"
#include "src/mc/mc_private.hpp"
-#include "src/mc/mc_safety.hpp"
#include "src/mc/remote/AppSide.hpp"
#include "src/mc/sosp/Snapshot.hpp"
+++ /dev/null
-/* Copyright (c) 2007-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. */
-
-#ifndef SIMGRID_MC_SAFETY_HPP
-#define SIMGRID_MC_SAFETY_HPP
-
-#include "xbt/base.h"
-
-namespace simgrid::mc {
-
-enum class ReductionMode {
- unset,
- none,
- dpor,
-};
-
-extern XBT_PRIVATE simgrid::mc::ReductionMode reduction_mode;
-} // namespace simgrid::mc
-
-#endif
src/mc/mc_forward.hpp
src/mc/mc_private.hpp
src/mc/mc_record.cpp
- src/mc/mc_safety.hpp
src/mc/udpor_global.cpp
src/mc/udpor_global.hpp
