#include "src/mc/explo/Exploration.hpp"
#include "src/mc/mc_config.hpp"
+#include <algorithm>
#include <boost/range/algorithm.hpp>
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_state, mc, "Logging specific to MC states");
return outgoing_transition_;
}
+
+std::unordered_set<aid_t> State::get_todo_actors() const
+{
+ std::unordered_set<aid_t> actors;
+ for (const auto& [aid, state] : get_actors_list()) {
+ if (state.is_todo()) {
+ actors.insert(aid);
+ }
+ }
+ return actors;
+}
+
} // namespace simgrid::mc
Snapshot* get_system_state() const { return system_state_.get(); }
void set_system_state(std::shared_ptr<Snapshot> state) { system_state_ = std::move(state); }
+ std::unordered_set<aid_t> get_todo_actors() const;
std::map<aid_t, Transition> const& get_sleep_set() const { return sleep_set_; }
void add_sleep_set(std::shared_ptr<Transition> t)
{
#include <cassert>
#include <cstdio>
+#include <algorithm>
#include <memory>
#include <string>
+#include <unordered_set>
#include <vector>
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_dfs, mc, "DFS exploration algorithm of the model-checker");
}
/* Actually answer the request: let's execute the selected request (MCed does one step) */
- state->execute_next(next, get_remote_app());
+ const auto executed_transition = state->execute_next(next, get_remote_app());
on_transition_execute_signal(state->get_transition_out().get(), get_remote_app());
// If there are processes to interleave and the maximum depth has not been
}
tmp_stack.pop_back();
}
+ } else if (reduction_mode_ == ReductionMode::sdpor) {
+ /**
+ * SDPOR Source Set Procedure:
+ */
+ execution_seq_.push_transition(executed_transition.get());
+
+ // To determine if the race is reversible, we have to ensure
+ // that actor `p` running `next_E_p` (viz. the event such that
+ // `racing_event -> (E_p) next_E_p` and no other event
+ // "happens-between" the two) is enabled in any equivalent
+ // execution where `racing_event` happens before `next_E_p`.
+ //
+ // Importantly, it is equivalent to checking if in ANY
+ // such equivalent execution sequence where `racing_event`
+ // happens-before `next_E_p` that `p` is enabled in `pre(racing_event, E.p)`.
+ // Thus it suffices to check THIS execution
+ xbt_assert(execution_seq_.get_latest_event_handle().has_value(),
+ "No events are contained in the SDPOR/OPDPOR execution "
+ "even though one was just added");
+ const aid_t p = executed_transition->aid_;
+ const auto next_E_p = execution_seq_.get_latest_event_handle().value();
+
+ for (const auto racing_event_handle : execution_seq_.get_racing_events_of(next_E_p)) {
+ // If the actor `p` is not enabled at s_[E'], it is not a *reversible* race
+ const std::shared_ptr<State> prev_state = stack_[racing_event_handle];
+ if (not prev_state->is_actor_enabled(p)) {
+ continue;
+ }
+
+ // This is a reversible race! First, grab `E' := pre(e, E)`
+ // TODO: Instead of copying around these big structs, it
+ // would behoove us to incorporate some way to reference
+ // portions of an execution. For simplicity and for a
+ // "proof of concept" version, we opt to simply copy
+ // the contents instead of making a view into the execution
+ const sdpor::Execution E_prime_v = execution_seq_.get_prefix_up_to(racing_event_handle);
+
+ // The vector `v` is constructed as `v := notdep(e, E)
+ std::vector<sdpor::Execution::EventHandle> v(execution_seq_.size());
+ std::unordered_set<aid_t> disqualified_actors = state->get_todo_actors();
+
+ for (auto e_prime = racing_event_handle; e_prime <= next_E_p; ++e_prime) {
+ // Any event `e` which occurs after `racing_event_handle` but which does not
+ // happen after `racing_event_handle` is a member of `v`
+ if (not E_prime_v.happens_before(racing_event_handle, e_prime) or e_prime == next_E_p) {
+ v.push_back(e_prime);
+ }
+ const aid_t q = E_prime_v.get_actor_with_handle(e_prime);
+ if (disqualified_actors.count(q) > 0) {
+ continue;
+ }
+
+ const bool is_initial = std::none_of(v.begin(), v.end(), [&E_prime_v, e_prime](const auto& e_star) {
+ return E_prime_v.happens_before(e_star, e_prime);
+ });
+ if (is_initial) {
+ if (not prev_state->is_actor_done(q)) {
+ prev_state->consider_one(q);
+ opened_states_.emplace_back(std::move(prev_state));
+ }
+ break;
+ } else {
+ disqualified_actors.insert(q);
+ }
+ }
+ }
}
// Before leaving that state, if the transition we just took can be taken multiple times, we
this->check_non_termination(next_state.get());
#if SIMGRID_HAVE_STATEFUL_MC
- /* Check whether we already explored next_state in the past (but only if interested in state-equality reduction) */
+ /* Check whether we already explored next_state in the past (but only if interested in state-equality reduction)
+ */
if (_sg_mc_max_visited_states > 0)
visited_state_ = visited_states_.addVisitedState(next_state->get_num(), next_state.get(), get_remote_app());
#endif
#include "src/mc/api/ClockVector.hpp"
#include "src/mc/api/State.hpp"
#include "src/mc/explo/Exploration.hpp"
+#include "src/mc/explo/odpor/Execution.hpp"
#if SIMGRID_HAVE_STATEFUL_MC
#include "src/mc/VisitedState.hpp"
#endif
+#include <deque>
#include <list>
#include <memory>
#include <set>
namespace simgrid::mc {
-using stack_t = std::list<std::shared_ptr<State>>;
+using stack_t = std::deque<std::shared_ptr<State>>;
class XBT_PRIVATE DFSExplorer : public Exploration {
XBT_DECLARE_ENUM_CLASS(ReductionMode, none, dpor, sdpor);
/** Stack representing the position in the exploration graph */
stack_t stack_;
+ /**
+ * Provides additional metadata about the position in the exploration graph
+ * which is used by SDPOR and ODPOR
+ */
+ odpor::Execution execution_seq_;
+
/** Per-actor clock vectors used to compute the "happens-before" relation */
std::unordered_map<aid_t, ClockVector> per_actor_clocks_;
+/* Copyright (c) 2008-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. */
+
+#include "src/mc/explo/odpor/Execution.hpp"
+
+namespace simgrid::mc::odpor {
+
+std::unordered_set<Execution::EventHandle> Execution::get_racing_events_of(Execution::EventHandle e1) const
+{
+ return {};
+}
+
+bool Execution::happens_before(Execution::EventHandle e1, Execution::EventHandle e2) const
+{
+ return true;
+}
+
+Execution Execution::get_prefix_up_to(Execution::EventHandle)
+{
+ return *this;
+}
+
+void Execution::pop_latest() {}
+
+void Execution::push_transition(const Transition*) {}
+
+} // namespace simgrid::mc::odpor
\ No newline at end of file
#define SIMGRID_MC_ODPOR_EXECUTION_HPP
#include "src/mc/api/ClockVector.hpp"
+#include "src/mc/explo/odpor/odpor_forward.hpp"
#include "src/mc/transition/Transition.hpp"
-#include <optonal>
+#include <list>
+#include <optional>
#include <unordered_set>
#include <vector>
std::pair<const Transition*, ClockVector> contents_;
public:
- Event() = default;
- Event(Event&&) = default;
- Event(const Event&) = default;
- Event& operator=(const Event&) = default;
- Event& operator=(const Event&&) = default;
+ Event() = default;
+ Event(Event&&) = default;
+ Event(const Event&) = default;
+ Event& operator=(const Event&) = default;
explicit Event(std::pair<const Transition*, ClockVector> pair) : contents_(std::move(pair)) {}
- const Transition* get_transition() const { return contents_.get<0>(); }
- const ClockVector& get_clock_vector() const { return contents_.get<1>(); }
-}
+ const Transition* get_transition() const { return std::get<0>(contents_); }
+ const ClockVector& get_clock_vector() const { return std::get<1>(contents_); }
+};
/**
* @brief An ordered sequence of transitions which describe
* the two concepts are analogous if not identical
*/
class Execution {
+private:
+ /**
+ * @brief The actual steps that are taken by the process
+ * during exploration, relative to the
+ */
+ std::vector<Event> contents_;
+
public:
- using Handle = decltype(contents_)::const_iterator;
+ using Handle = decltype(contents_)::const_iterator;
+ using EventHandle = uint32_t;
Execution() = default;
Execution(const Execution&) = default;
bool is_initial(aid_t p, const Hypothetical& w) const;
bool is_weak_initial(aid_t p, const Hypothetical& w) const;
+ const Event& get_event_with_handle(EventHandle handle) const { return contents_[handle]; }
+ aid_t get_actor_with_handle(EventHandle handle) const { return get_event_with_handle(handle).get_transition()->aid_; }
+
+ /**
+ * @brief Returns a set of IDs of events which are in
+ * "immediate conflict" (according to the definition given
+ * in the ODPOR paper) with one another
+ */
+ std::unordered_set<EventHandle> get_racing_events_of(EventHandle) const;
+
+ /**
+ * @brief Returns a handle to the newest event of the execution,
+ * if such an event exists
+ */
+ std::optional<EventHandle> get_latest_event_handle() const
+ {
+ return contents_.empty() ? std::nullopt : std::optional<EventHandle>{static_cast<EventHandle>(size() - 1)};
+ }
+
+ Execution get_prefix_up_to(EventHandle);
+
+ /**
+ * @brief Whether the event represented by `e1`
+ * "happens-before" the event represented by
+ * `e2` in the context of this execution
+ *
+ * In the terminology of the ODPOR paper,
+ * this function computes
+ *
+ * `e1 --->_E e2`
+ *
+ * where `E` is this execution
+ */
+ bool happens_before(EventHandle e1, EventHandle e2) const;
+
/**
* @brief Removes the last event of the execution,
* if such an event exists
*/
void push_transition(const Transition*);
- size_t size() const { return this->contents_.size(); }
- size_t size() const { return this->contents_.size(); }
-
-private:
- /**
- * @brief A pointer into the execution off of which this
- * execution extends computation
- *
- * Conceptually, the `prior`
- */
- std::optional<Handle> prior;
-
/**
- * @brief The actual steps that are taken by the process
- * during exploration, relative to the
+ * @brief The total number of steps contained in the execution
*/
- std::list<Event> contents_;
+ size_t size() const { return this->contents_.size(); }
};
} // namespace simgrid::mc::odpor
class Event;
class Execution;
-class ExecutionSequence;
class ExecutionView;
class WakeupTree;
} // namespace simgrid::mc::odpor
+namespace simgrid::mc {
+
+// Permit ODPOR or SDPOR to be used as namespaces
+// Many of the structures overlap, so it doesn't
+// make sense to some in one and not the other.
+// Having one for each algorithm makes the corresponding
+// code easier to read
+namespace sdpor = simgrid::mc::odpor;
+
+} // namespace simgrid::mc
+
#endif
