#include "src/mc/api/State.hpp"
#include "src/mc/api/strategy/BasicStrategy.hpp"
-#include "src/mc/api/strategy/WaitStrategy.hpp"
+#include "src/mc/api/strategy/MaxMatchComm.hpp"
+#include "src/mc/api/strategy/MinMatchComm.hpp"
+#include "src/mc/api/strategy/UniformStrategy.hpp"
#include "src/mc/explo/Exploration.hpp"
#include "src/mc/mc_config.hpp"
State::State(RemoteApp& remote_app) : num_(++expended_states_)
{
XBT_VERB("Creating a guide for the state");
+
+ srand(_sg_mc_random_seed);
+
if (_sg_mc_strategy == "none")
strategy_ = std::make_shared<BasicStrategy>();
- else if (_sg_mc_strategy == "nb_wait")
- strategy_ = std::make_shared<WaitStrategy>();
+ else if (_sg_mc_strategy == "max_match_comm")
+ strategy_ = std::make_shared<MaxMatchComm>();
+ else if (_sg_mc_strategy == "min_match_comm")
+ strategy_ = std::make_shared<MinMatchComm>();
+ else if (_sg_mc_strategy == "uniform")
+ strategy_ = std::make_shared<UniformStrategy>();
else
THROW_IMPOSSIBLE;
State::State(RemoteApp& remote_app, std::shared_ptr<State> parent_state)
: incoming_transition_(parent_state->get_transition_out()), num_(++expended_states_), parent_state_(parent_state)
{
- if (_sg_mc_strategy == "none")
+
+ if (_sg_mc_strategy == "none")
strategy_ = std::make_shared<BasicStrategy>();
- else if (_sg_mc_strategy == "nb_wait")
- strategy_ = std::make_shared<WaitStrategy>();
+ else if (_sg_mc_strategy == "max_match_comm")
+ strategy_ = std::make_shared<MaxMatchComm>();
+ else if (_sg_mc_strategy == "min_match_comm")
+ strategy_ = std::make_shared<MinMatchComm>();
+ else if (_sg_mc_strategy == "uniform")
+ strategy_ = std::make_shared<UniformStrategy>();
else
THROW_IMPOSSIBLE;
- *strategy_ = *(parent_state->strategy_);
+ strategy_->copy_from(parent_state_->strategy_.get());
remote_app.get_actors_status(strategy_->actors_to_run_);
namespace simgrid::mc {
-/** Basic MC guiding class which corresponds to no guide at all (random choice) */
+/** Basic MC guiding class which corresponds to no guide. When asked for different states
+ * it will follow a depth first search politics to minize the number of opened states. */
class BasicStrategy : public Strategy {
+ int depth_ = 100000; // Arbitrary starting point. next_transition must return a positiv value to work with threshold in DFSExplorer
+
public:
+ void copy_from(const Strategy* strategy) override
+ {
+ const BasicStrategy* cast_strategy = static_cast<BasicStrategy const*>(strategy);
+ xbt_assert(cast_strategy != nullptr);
+ depth_ = cast_strategy->depth_ - 1;
+ xbt_assert(depth_ > 0, "The exploration reached a depth greater than 100000. We will stop here to prevent weird interaction with DFSExplorer.");
+ }
BasicStrategy() = default;
~BasicStrategy() override = default;
- BasicStrategy(const BasicStrategy&) = delete;
- BasicStrategy& operator=(const BasicStrategy&)
- { /* nothing to copy over while cloning */
- return *this;
- }
std::pair<aid_t, int> next_transition() const override
{
continue;
}
- return std::make_pair(aid, 1);
+ return std::make_pair(aid, depth_);
}
- return std::make_pair(-1, 0);
+ return std::make_pair(-1, depth_);
}
void execute_next(aid_t aid, RemoteApp& app) override { return; }
--- /dev/null
+/* Copyright (c) 2007-2023. 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_WAITSTRATEGY_HPP
+#define SIMGRID_MC_WAITSTRATEGY_HPP
+
+#include "src/mc/transition/TransitionComm.hpp"
+
+namespace simgrid::mc {
+
+/** Wait MC guiding class that aims at minimizing the number of in-fly communication.
+ * When possible, it will try to match corresponding in-fly communications. */
+class MaxMatchComm : public Strategy {
+
+ /** Stores for each mailbox what kind of transition is waiting on it.
+ * Negative number means that much recv are waiting on that mailbox, while
+ * a positiv number means that much send are waiting there. */
+ std::map<unsigned, int> mailbox_;
+ int value_of_state_ = 0; // used to valuate the state. Corresponds to the number of in-fly communications
+ // The two next values are used to save the operation we execute so the next strategy can update its field accordingly
+ Transition::Type last_transition_;
+ unsigned last_mailbox_ = 0;
+
+public:
+ void copy_from(const Strategy* strategy) override
+ {
+ const MaxMatchComm* cast_strategy = static_cast<MaxMatchComm const*>(strategy);
+ xbt_assert(cast_strategy != nullptr);
+ for (auto& [id, val] : cast_strategy->mailbox_)
+ mailbox_[id] = val;
+ if (cast_strategy->last_transition_ == Transition::Type::COMM_ASYNC_RECV)
+ mailbox_[cast_strategy->last_mailbox_]--;
+ if (cast_strategy->last_transition_ == Transition::Type::COMM_ASYNC_SEND)
+ mailbox_[cast_strategy->last_mailbox_]++;
+
+ for (auto const& [_, val] : mailbox_)
+ value_of_state_ += std::abs(val);
+ }
+ MaxMatchComm() = default;
+ ~MaxMatchComm() override = default;
+
+ std::pair<aid_t, int> next_transition() const override
+ {
+ std::pair<aid_t, int> if_no_match = std::make_pair(-1, 0);
+ for (auto const& [aid, actor] : actors_to_run_) {
+ if (not actor.is_todo() || not actor.is_enabled() || actor.is_done())
+ continue;
+
+ const Transition* transition = actor.get_transition(actor.get_times_considered());
+
+ const CommRecvTransition* cast_recv = static_cast<CommRecvTransition const*>(transition);
+ if (cast_recv != nullptr and mailbox_.count(cast_recv->get_mailbox()) > 0 and
+ mailbox_.at(cast_recv->get_mailbox()) > 0)
+ return std::make_pair(aid, value_of_state_ - 1); // This means we have waiting send corresponding to this recv
+
+ const CommSendTransition* cast_send = static_cast<CommSendTransition const*>(transition);
+ if (cast_send != nullptr and mailbox_.count(cast_send->get_mailbox()) > 0 and
+ mailbox_.at(cast_send->get_mailbox()) < 0)
+ return std::make_pair(aid, value_of_state_ - 1); // This means we have waiting recv corresponding to this send
+
+ if (if_no_match.first == -1)
+ if_no_match = std::make_pair(aid, value_of_state_);
+ }
+ return if_no_match;
+ }
+
+ void execute_next(aid_t aid, RemoteApp& app) override
+ {
+ const Transition* transition = actors_to_run_.at(aid).get_transition(actors_to_run_.at(aid).get_times_considered());
+ last_transition_ = transition->type_;
+
+ const CommRecvTransition* cast_recv = static_cast<CommRecvTransition const*>(transition);
+ if (cast_recv != nullptr)
+ last_mailbox_ = cast_recv->get_mailbox();
+
+ const CommSendTransition* cast_send = static_cast<CommSendTransition const*>(transition);
+ if (cast_send != nullptr)
+ last_mailbox_ = cast_send->get_mailbox();
+ }
+
+ void consider_best() override
+ {
+ for (auto& [aid, actor] : actors_to_run_)
+ if (actor.is_todo())
+ return;
+
+ for (auto& [aid, actor] : actors_to_run_) {
+ if (not actor.is_enabled() || actor.is_done())
+ continue;
+
+ const Transition* transition = actor.get_transition(actor.get_times_considered());
+
+ const CommRecvTransition* cast_recv = static_cast<CommRecvTransition const*>(transition);
+ if (cast_recv != nullptr and mailbox_.count(cast_recv->get_mailbox()) > 0 and
+ mailbox_.at(cast_recv->get_mailbox()) > 0) {
+ actor.mark_todo();
+ return;
+ }
+
+ const CommSendTransition* cast_send = static_cast<CommSendTransition const*>(transition);
+ if (cast_send != nullptr and mailbox_.count(cast_send->get_mailbox()) > 0 and
+ mailbox_.at(cast_send->get_mailbox()) < 0) {
+ actor.mark_todo();
+ return;
+ }
+ }
+ for (auto& [_, actor] : actors_to_run_) {
+ if (actor.is_enabled() and not actor.is_done()) {
+ actor.mark_todo();
+ return;
+ }
+ }
+ }
+};
+
+} // namespace simgrid::mc
+
+#endif
--- /dev/null
+/* Copyright (c) 2007-2023. 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_MINWAITTAKEN_HPP
+#define SIMGRID_MC_MINWAITTAKEN_HPP
+
+#include "src/mc/transition/TransitionComm.hpp"
+
+namespace simgrid::mc {
+
+/** Wait MC guiding class that aims at maximizing the number of in-fly communication.
+ * When possible, it will try not to match communications. */
+class MinMatchComm : public Strategy {
+
+
+ /** Stores for each mailbox what kind of transition is waiting on it.
+ * Negative number means that much recv are waiting on that mailbox, while
+ * a positiv number means that much send are waiting there. */
+ std::map<unsigned, int> mailbox_;
+ int value_of_state_ = 100000; // used to valuate the state. Corresponds to the number of in-fly communications
+ // The two next values are used to save the operation we execute so the next strategy can update its field accordingly
+ Transition::Type last_transition_;
+ unsigned last_mailbox_ = 0;
+
+public:
+ void copy_from(const Strategy* strategy) override
+ {
+ const MinMatchComm* cast_strategy = static_cast<MinMatchComm const*>(strategy);
+ xbt_assert(cast_strategy != nullptr);
+ for (auto& [id, val] : cast_strategy->mailbox_)
+ mailbox_[id] = val;
+ if (cast_strategy->last_transition_ == Transition::Type::COMM_ASYNC_RECV)
+ mailbox_[cast_strategy->last_mailbox_]--;
+ if (cast_strategy->last_transition_ == Transition::Type::COMM_ASYNC_SEND)
+ mailbox_[cast_strategy->last_mailbox_]++;
+
+ for (auto const& [_, val] : mailbox_)
+ value_of_state_ -= std::abs(val);
+ if (value_of_state_ < 0)
+ value_of_state_ = 0;
+ }
+ MinMatchComm() = default;
+ ~MinMatchComm() override = default;
+
+ std::pair<aid_t, int> next_transition() const override
+ {
+ std::pair<aid_t, int> if_no_match = std::make_pair(-1, 0);
+ for (auto const& [aid, actor] : actors_to_run_) {
+ if (not actor.is_todo() || not actor.is_enabled() || actor.is_done())
+ continue;
+
+ const Transition* transition = actor.get_transition(actor.get_times_considered());
+
+ const CommRecvTransition* cast_recv = static_cast<CommRecvTransition const*>(transition);
+ if (cast_recv != nullptr and mailbox_.count(cast_recv->get_mailbox()) > 0 and
+ mailbox_.at(cast_recv->get_mailbox()) <= 0)
+ return std::make_pair(aid, value_of_state_ - 1); // This means we don't have waiting recv corresponding to this recv
+
+ const CommSendTransition* cast_send = static_cast<CommSendTransition const*>(transition);
+ if (cast_send != nullptr and mailbox_.count(cast_send->get_mailbox()) > 0 and
+ mailbox_.at(cast_send->get_mailbox()) >= 0)
+ return std::make_pair(aid, value_of_state_ - 1); // This means we don't have waiting recv corresponding to this send
+
+ if (if_no_match.first == -1)
+ if_no_match = std::make_pair(aid, value_of_state_);
+ }
+ return if_no_match;
+ }
+
+ void execute_next(aid_t aid, RemoteApp& app) override
+ {
+ const Transition* transition = actors_to_run_.at(aid).get_transition(actors_to_run_.at(aid).get_times_considered());
+ last_transition_ = transition->type_;
+
+ const CommRecvTransition* cast_recv = static_cast<CommRecvTransition const*>(transition);
+ if (cast_recv != nullptr)
+ last_mailbox_ = cast_recv->get_mailbox();
+
+ const CommSendTransition* cast_send = static_cast<CommSendTransition const*>(transition);
+ if (cast_send != nullptr)
+ last_mailbox_ = cast_send->get_mailbox();
+ }
+
+ void consider_best() override
+ {
+ for (auto& [aid, actor] : actors_to_run_)
+ if (actor.is_todo())
+ return;
+
+ for (auto& [aid, actor] : actors_to_run_) {
+ if (not actor.is_enabled() || actor.is_done())
+ continue;
+
+ const Transition* transition = actor.get_transition(actor.get_times_considered());
+
+ const CommRecvTransition* cast_recv = static_cast<CommRecvTransition const*>(transition);
+ if (cast_recv != nullptr and mailbox_.count(cast_recv->get_mailbox()) > 0 and
+ mailbox_.at(cast_recv->get_mailbox()) <= 0) {
+ actor.mark_todo();
+ return;
+ }
+
+ const CommSendTransition* cast_send = static_cast<CommSendTransition const*>(transition);
+ if (cast_send != nullptr and mailbox_.count(cast_send->get_mailbox()) > 0 and
+ mailbox_.at(cast_send->get_mailbox()) >= 0) {
+ actor.mark_todo();
+ return;
+ }
+ }
+ for (auto& [_, actor] : actors_to_run_) {
+ if (actor.is_enabled() and not actor.is_done()) {
+ actor.mark_todo();
+ return;
+ }
+ }
+ }
+};
+
+} // namespace simgrid::mc
+
+#endif
class Strategy {
protected:
- /** State's exploration status by actor. Not all the actors are there, only the ones that are ready-to-run in this
- * state */
+ /** State's exploration status by actor. All actors should be present, eventually disabled for now. */
std::map<aid_t, ActorState> actors_to_run_;
public:
- Strategy() = default;
- virtual ~Strategy() = default;
- Strategy(const Strategy&) = delete;
- Strategy& operator=(const Strategy&)
- { /* nothing to copy over while cloning */
- return *this;
- }
+ virtual void copy_from(const Strategy*) = 0;
+ Strategy() = default;
+ virtual ~Strategy() = default;
virtual std::pair<aid_t, int> next_transition() const = 0;
virtual void execute_next(aid_t aid, RemoteApp& app) = 0;
- virtual void consider_best() = 0;
// Mark the first enabled and not yet done transition as todo
// If there's already a transition marked as todo, does nothing
+ virtual void consider_best() = 0;
+
+ // Mark aid as todo. If it makes no sense, ie. if it is already done or not enabled,
+ // raise an error
void consider_one(aid_t aid)
{
xbt_assert(actors_to_run_.at(aid).is_enabled() and not actors_to_run_.at(aid).is_done(),
"Tried to mark as TODO actor %ld but it is either not enabled or already done", aid);
actors_to_run_.at(aid).mark_todo();
}
- // Matk as todo all actors enabled that are not done yet
+ // Mark as todo all actors enabled that are not done yet and return the number
+ // of marked actors
unsigned long consider_all()
{
unsigned long count = 0;
--- /dev/null
+/* Copyright (c) 2007-2023. 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_UNIFORMSTRATEGY_HPP
+#define SIMGRID_MC_UNIFORMSTRATEGY_HPP
+
+#include "src/mc/transition/Transition.hpp"
+
+namespace simgrid::mc {
+
+/** Guiding strategy that valuate states randomly */
+class UniformStrategy : public Strategy {
+ std::map<aid_t, int> valuation;
+
+public:
+ UniformStrategy()
+ {
+ for (long aid = 0; aid < 10; aid++)
+ valuation[aid] = rand() % 1000;
+ }
+ void copy_from(const Strategy* strategy) override
+ {
+ for (auto& [aid, _] : actors_to_run_)
+ valuation[aid] = rand() % 1000;
+ }
+
+ std::pair<aid_t, int> next_transition() const override
+ {
+ int possibilities = 0;
+
+ // Consider only valid actors
+ for (auto const& [aid, actor] : actors_to_run_) {
+ if (actor.is_todo() and (not actor.is_done()) and actor.is_enabled())
+ possibilities++;
+ }
+
+ int chosen;
+ if (possibilities == 0)
+ return std::make_pair(-1, 100000);
+ if (possibilities == 1)
+ chosen = 0;
+ else
+ chosen = rand() % possibilities;
+
+ for (auto const& [aid, actor] : actors_to_run_) {
+ if ((not actor.is_todo()) or actor.is_done() or (not actor.is_enabled()))
+ continue;
+ if (chosen == 0) {
+ return std::make_pair(aid, valuation.at(aid));
+ }
+ chosen--;
+ }
+
+ return std::make_pair(-1, 100000);
+ }
+
+ void execute_next(aid_t aid, RemoteApp& app) override {}
+
+ void consider_best() override
+ {
+
+ int possibilities = 0;
+ // Consider only valid actors
+ // If some actor are already considered as todo, skip
+ for (auto const& [aid, actor] : actors_to_run_) {
+ if (valuation.count(aid) == 0)
+ for (auto& [aid, _] : actors_to_run_)
+ valuation[aid] = rand() % 1000;
+ if (actor.is_todo())
+ return;
+ if (actor.is_enabled() and not actor.is_done())
+ possibilities++;
+ }
+
+ int chosen;
+ if (possibilities == 0)
+ return;
+ if (possibilities == 1)
+ chosen = 0;
+ else
+ chosen = rand() % possibilities;
+
+ for (auto& [aid, actor] : actors_to_run_) {
+ if (not actor.is_enabled() or actor.is_done())
+ continue;
+ if (chosen == 0) {
+ actor.mark_todo();
+ return;
+ }
+ chosen--;
+ }
+ THROW_IMPOSSIBLE; // One actor should be marked as todo before
+ }
+};
+
+} // namespace simgrid::mc
+
+#endif
+++ /dev/null
-/* Copyright (c) 2007-2023. 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_WAITSTRATEGY_HPP
-#define SIMGRID_MC_WAITSTRATEGY_HPP
-
-#include "Strategy.hpp"
-#include "src/mc/transition/Transition.hpp"
-
-namespace simgrid::mc {
-
-/** Wait MC guiding class that aims at minimizing the number of in-fly communication.
- * When possible, it will try to take the wait transition. */
-class WaitStrategy : public Strategy {
- int taken_wait_ = 0;
- bool taking_wait_ = false;
-
-public:
- WaitStrategy() = default;
- ~WaitStrategy() override = default;
- WaitStrategy(const WaitStrategy&) = delete;
- WaitStrategy& operator=(const WaitStrategy& guide)
- {
- taken_wait_ = guide.taken_wait_;
- return *this;
- }
-
- bool is_transition_wait(Transition::Type type) const
- {
- return type == Transition::Type::WAITANY or type == Transition::Type::BARRIER_WAIT or
- type == Transition::Type::MUTEX_WAIT or type == Transition::Type::SEM_WAIT;
- }
-
- std::pair<aid_t, int> next_transition() const override
- {
- std::pair<aid_t, int> if_no_wait = std::make_pair(-1, 0);
- for (auto const& [aid, actor] : actors_to_run_) {
- if (not actor.is_todo() || not actor.is_enabled() || actor.is_done())
- continue;
- if (is_transition_wait(actor.get_transition(actor.get_times_considered())->type_))
- return std::make_pair(aid, -(taken_wait_ + 1));
- if_no_wait = std::make_pair(aid, -taken_wait_);
- }
- return if_no_wait;
- }
-
- /** If we are taking a wait transition, and last transition wasn't a wait, we need to increment the number
- * of wait taken. On the opposite, if we took a wait before, and now we are taking another transition, we need
- * to decrease the count. */
- void execute_next(aid_t aid, RemoteApp& app) override
- {
- auto const& actor = actors_to_run_.at(aid);
- if ((not taking_wait_) and is_transition_wait(actor.get_transition(actor.get_times_considered())->type_)) {
- taken_wait_++;
- taking_wait_ = true;
- return;
- }
- if (taking_wait_ and (not is_transition_wait(actor.get_transition(actor.get_times_considered())->type_))) {
- taken_wait_--;
- taking_wait_ = false;
- return;
- }
- }
-
- void consider_best() override
- {
- aid_t aid = next_transition().first;
- if (auto actor = actors_to_run_.find(aid); actor != actors_to_run_.end()) {
- actor->second.mark_todo();
- return;
- }
- for (auto& [_, actor] : actors_to_run_) {
- if (actor.is_todo())
- return;
- if (actor.is_enabled() and not actor.is_done()) {
- actor.mark_todo();
- return;
- }
- }
- }
-};
-
-} // namespace simgrid::mc
-
-#endif
continue;
if (valid != current)
*valid = std::move(*current);
- if (best == end(opened_states_) || prio > best_prio) {
+ if (best == end(opened_states_) || prio < best_prio) {
best_prio = prio;
best = valid;
}
"model-check/strategy",
"Specify the the kind of heuristic to use for guided model-checking",
"none",
- {{"none", "No specific strategy: simply pick the first available transistion."},
- {"nb_wait", "Take any enabled wait transition, to reduce the distance between an async and its wait."}}};
+ {{"none", "No specific strategy: simply pick the first available transistion and act as a DFS."},
+ {"max_match_comm", "Try to minimize the number of in-fly communication by appairing matching send and receive."},
+ {"min_match_comm", "Try to maximize the number of in-fly communication by not appairing matching send and receive."},
+ {"uniform", "No specific strategy: choices are made randomly based on a uniform sampling."}
+ }};
+
+simgrid::config::Flag<int> _sg_mc_random_seed{"model-check/rand-seed",
+ "give a specific random seed to initialize the uniform distribution", 0,
+ [](int) { _mc_cfg_cb_check("Random seed"); }};
#if SIMGRID_HAVE_STATEFUL_MC
simgrid::config::Flag<int> _sg_mc_checkpoint{
extern XBT_PUBLIC simgrid::config::Flag<bool> _sg_mc_unfolding_checker;
extern XBT_PRIVATE simgrid::config::Flag<bool> _sg_mc_timeout;
extern XBT_PRIVATE simgrid::config::Flag<int> _sg_mc_max_depth;
+extern XBT_PRIVATE simgrid::config::Flag<int> _sg_mc_random_seed;
extern "C" XBT_PUBLIC int _sg_mc_max_visited_states;
extern XBT_PRIVATE simgrid::config::Flag<std::string> _sg_mc_dot_output_file;
extern XBT_PRIVATE simgrid::config::Flag<bool> _sg_mc_termination;
src/mc/mc_record.cpp
src/mc/api/strategy/BasicStrategy.hpp
+ src/mc/api/strategy/MaxMatchComm.hpp
+ src/mc/api/strategy/MinMatchComm.hpp
src/mc/api/strategy/Strategy.hpp
- src/mc/api/strategy/WaitStrategy.hpp
+ src/mc/api/strategy/UniformStrategy.hpp
src/xbt/mmalloc/mm_interface.c
)
