return outgoing_transition_;
}
-std::unordered_set<aid_t> State::get_todo_actors() const
+std::unordered_set<aid_t> State::get_backtrack_set() const
{
std::unordered_set<aid_t> actors;
for (const auto& [aid, state] : get_actors_list()) {
- if (state.is_todo()) {
+ if (state.is_todo() or state.is_done()) {
actors.insert(aid);
}
}
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;
+ /**
+ * @brief Computes the backtrack set for this state
+ * according to its definition in Simgrid.
+ *
+ * The backtrack set as it appears in DPOR, SDPOR, and ODPOR
+ * in SimGrid consists of those actors marked as `todo`
+ * (i.e. those that have yet to be explored) as well as those
+ * marked `done` (i.e. those that have already been explored)
+ * since the pseudcode in none of the above algorithms explicitly
+ * removes elements from the backtrack set. DPOR makes use
+ * explicitly of the `done` set, but we again note that the
+ * backtrack set still contains processes added to the done set.
+ */
+ std::unordered_set<aid_t> get_backtrack_set() const;
std::map<aid_t, Transition> const& get_sleep_set() const { return sleep_set_; }
void add_sleep_set(std::shared_ptr<Transition> t)
{
XBT_DEBUG("Replaced stack by %s", get_record_trace().to_string().c_str());
if (reduction_mode_ == ReductionMode::sdpor) {
- execution_seq_ = execution_seq_.get_prefix_up_to(stack_.size());
+ if (stack_.empty()) {
+ execution_seq_ = sdpor::Execution();
+ } else {
+ execution_seq_ = execution_seq_.get_prefix_up_to(stack_.size() - 1);
+ }
XBT_DEBUG("Additionally replaced corresponding SDPOR execution stack");
}
}
} else if (reduction_mode_ == ReductionMode::sdpor) {
/**
* SDPOR Source Set Procedure:
+ *
+ * Find "reversible races" in the current execution with respect
+ * to the latest action `p`. For each such race, determine one thread
+ * not contained in the backtrack set at the "race point" `r` which
+ * "represents" the trace formed by first executing everything after
+ * `r` and then `p` to flip the race
*/
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 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)) {
+ // 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
+ //
// 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
- 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;
- 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`.
- // In addition to marking the event in `v`, we also "simulate" running
- // the action `v` from E'.
- if (not execution_seq_.happens_before(racing_event_handle, e_prime) or e_prime == next_E_p) {
- v.push_back(e_prime);
- E_prime_v.push_transition(execution_seq_.get_event_with_handle(e_prime).get_transition());
- } else {
- continue;
- }
-
- xbt_assert(E_prime_v.get_latest_event_handle().has_value(),
- "No events are contained in the SDPOR/OPDPOR execution "
- "even though one was just added");
- const sdpor::Execution::EventHandle e_prime_in_E_prime = E_prime_v.get_latest_event_handle().value();
-
- const aid_t q = E_prime_v.get_actor_with_handle(e_prime_in_E_prime);
- if (disqualified_actors.count(q) > 0) {
- continue;
- }
-
- const bool is_initial = std::none_of(v.begin(), v.end(), [&](const auto& e_star) {
- return E_prime_v.happens_before(e_star, e_prime_in_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);
+ if (prev_state->is_actor_enabled(p)) {
+ // NOTE: To incorporate the idea of attempting to select the "best"
+ // backtrack point into SDPOR, instead of selecting the `first` initial,
+ // we should instead compute all choices and decide which is bes
+ const std::optional<aid_t> q =
+ execution_seq_.get_first_ssdpor_initial_from(racing_event_handle, prev_state->get_backtrack_set());
+ if (q.has_value()) {
+ prev_state->consider_one(q.value());
+ opened_states_.emplace_back(std::move(prev_state));
}
}
}
namespace simgrid::mc::odpor {
+void Execution::push_transition(const Transition* t)
+{
+ if (t == nullptr) {
+ throw std::invalid_argument("Unexpectedly received `nullptr`");
+ }
+ ClockVector max_clock_vector;
+ for (const Event& e : this->contents_) {
+ if (e.get_transition()->depends(t)) {
+ max_clock_vector = ClockVector::max(max_clock_vector, e.get_clock_vector());
+ }
+ }
+ // The entry in the vector for `t->aid_` is the size
+ // of the new stack, which will have a size one greater
+ // than that before we insert the new events
+ max_clock_vector[t->aid_] = this->size() + 1;
+ contents_.push_back(Event({t, max_clock_vector}));
+}
+
+void Execution::pop_latest()
+{
+ contents_.pop_back();
+}
+
std::unordered_set<Execution::EventHandle> Execution::get_racing_events_of(Execution::EventHandle target) const
{
std::unordered_set<Execution::EventHandle> racing_events;
return racing_events;
}
+Execution Execution::get_prefix_up_to(Execution::EventHandle handle) const
+{
+ return Execution(std::vector<Event>{contents_.begin(), contents_.begin() + handle});
+}
+
+std::optional<aid_t> Execution::get_first_ssdpor_initial_from(EventHandle e,
+ std::unordered_set<aid_t> disqualified_actors) const
+{
+ // If this execution is empty, there are no initials
+ // relative to the last transition added to the execution
+ // since such a transition does not exist
+ if (empty()) {
+ return std::nullopt;
+ }
+
+ // First, grab `E' := pre(e, E)` and determine what actor `p` is
+ // 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 auto next_E_p = get_latest_event_handle().value();
+ Execution E_prime_v = get_prefix_up_to(e);
+ std::vector<sdpor::Execution::EventHandle> v;
+
+ for (auto e_prime = e; e_prime <= next_E_p; ++e_prime) {
+ // Any event `e*` which occurs after `e` but which does not
+ // happen after `e` is a member of `v`. In addition to marking
+ // the event in `v`, we also "simulate" running the action `v`
+ // from E'
+ if (not happens_before(e, e_prime) or e_prime == next_E_p) {
+ v.push_back(e_prime);
+ E_prime_v.push_transition(get_event_with_handle(e_prime).get_transition());
+ } else {
+ continue;
+ }
+ const EventHandle e_prime_in_E_prime = E_prime_v.get_latest_event_handle().value();
+ const aid_t q = E_prime_v.get_actor_with_handle(e_prime_in_E_prime);
+ if (disqualified_actors.count(q) > 0) {
+ continue;
+ }
+ const bool is_initial = std::none_of(
+ v.begin(), v.end(), [&](const auto& e_star) { return E_prime_v.happens_before(e_star, e_prime_in_E_prime); });
+ if (is_initial) {
+ return q;
+ } else {
+ disqualified_actors.insert(q);
+ }
+ }
+ return std::nullopt;
+}
+
+std::unordered_set<aid_t> Execution::get_ssdpor_initials_from(EventHandle e,
+ std::unordered_set<aid_t> disqualified) const
+{
+ return std::unordered_set<aid_t>();
+}
+
bool Execution::happens_before(Execution::EventHandle e1_handle, Execution::EventHandle e2_handle) const
{
// 1. "happens-before" is a subset of "occurs before"
return e1_handle <= e2.get_clock_vector().get(proc_e1).value_or(0);
}
-Execution Execution::get_prefix_up_to(Execution::EventHandle handle)
-{
- if (handle == static_cast<Execution::EventHandle>(0)) {
- return Execution();
- }
- return Execution(std::vector<Event>{contents_.begin(), contents_.begin() + (handle - 1)});
-}
-
-void Execution::push_transition(const Transition* t)
-{
- if (t == nullptr) {
- throw std::invalid_argument("Unexpectedly received `nullptr`");
- }
- ClockVector max_clock_vector;
- for (const Event& e : this->contents_) {
- if (e.get_transition()->depends(t)) {
- max_clock_vector = ClockVector::max(max_clock_vector, e.get_clock_vector());
- }
- }
- // The entry in the vector for `t->aid_` is the size
- // of the new stack, which will have a size one greater
- // than that before we insert the new events
- max_clock_vector[t->aid_] = this->size() + 1;
- contents_.push_back(Event({t, max_clock_vector}));
-}
-
-void Execution::pop_latest()
-{
- contents_.pop_back();
-}
-
} // namespace simgrid::mc::odpor
\ No newline at end of file
Execution(const Execution&) = default;
Execution& operator=(Execution const&) = default;
Execution(Execution&&) = default;
+ Execution(ExecutionSequence&& seq);
+ Execution(const ExecutionSequence& seq);
- Execution(ExecutionSequence&& seq, std::optional<Handle> base = {});
- Execution(const ExecutionSequence& seq, std::optional<Handle> base = {});
+ size_t size() const { return this->contents_.size(); }
+ bool empty() const { return this->contents_.empty(); }
+
+ std::optional<aid_t> get_first_ssdpor_initial_from(EventHandle e, std::unordered_set<aid_t> disqualified) const;
+ std::unordered_set<aid_t> get_ssdpor_initials_from(EventHandle e, std::unordered_set<aid_t> disqualified) const;
- std::unordered_set<aid_t> get_initials_after(const Hypothetical& w) const;
- std::unordered_set<aid_t> get_weak_initials_after(const Hypothetical& w) const;
+
// std::unordered_set<aid_t> get_initials_after(const Hypothetical& w) const;
+
// std::unordered_set<aid_t> get_weak_initials_after(const Hypothetical& w) const;
- bool is_initial(aid_t p, const Hypothetical& w) const;
- bool is_weak_initial(aid_t p, const Hypothetical& w) const;
+ // std::unordered_set<aid_t> get_initials_after(const Hypothetical& w) const;
+ // std::unordered_set<aid_t> get_weak_initials_after(const Hypothetical& w) const;
+
+ // 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_; }
return contents_.empty() ? std::nullopt : std::optional<EventHandle>{static_cast<EventHandle>(size() - 1)};
}
- Execution get_prefix_up_to(EventHandle);
+ Execution get_prefix_up_to(EventHandle) const;
/**
* @brief Whether the event represented by `e1`
* actor which executed transition `t`.
*/
void push_transition(const Transition*);
-
- /**
- * @brief The total number of steps contained in the execution
- */
- size_t size() const { return this->contents_.size(); }
};
} // namespace simgrid::mc::odpor
