/**
* SDPOR Source Set Procedure:
*
- * Find "reversible races" in the current execution with respect
+ * Find "reversible races" in the current execution `E` 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
+ * `r` that doesn't depend on it (`v := notdep(r, E)`) and then `p` to
+ * flip the race.
+ *
+ * The intuition is that some subsequence of `v` may enable `p`, so
+ * we want to be sure that search "in that direction"
*/
execution_seq_.push_transition(executed_transition.get());
// 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());
+ execution_seq_.get_first_sdpor_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));
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 stack
max_clock_vector[t->aid_] = this->size();
contents_.push_back(Event({t, max_clock_vector}));
}
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
+std::optional<aid_t> Execution::get_first_sdpor_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
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" (-->_E) is a subset of "occurs before" (<_E)
auto begin() const { return this->contents_.begin(); }
auto end() const { return this->contents_.end(); }
- 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;
+ /**
+ * @brief Computes the "core" portion the SDPOR algorithm,
+ * viz. the intersection of the backtracking set and the
+ * set of initials with respect to the end
+ *
+ * See the SDPOR algorithm pseudocode in [1] for more
+ * details for the context of the function.
+ *
+ * @invariant: This method assumes that events `e` and
+ * `e' := get_latest_event_handle()` are in a *reversible* race
+ * as is the case in SDPOR
+ *
+ * @returns an actor not contained in `disqualified` which
+ * can serve as an initial to reverse the race between `e`
+ * and `e'`
+ */
+ std::optional<aid_t> get_first_sdpor_initial_from(EventHandle e, std::unordered_set<aid_t> disqualified) const;
+ /**
+ * @brief Determines the event associated with
+ * the given handle `handle`
+ */
const Event& get_event_with_handle(EventHandle handle) const { return contents_[handle]; }
+
+ /**
+ * @brief Determines the actor associated with
+ * the given event handle `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
+ * @brief Returns a set of events which are in
* "immediate conflict" (according to the definition given
- * in the ODPOR paper) with one another
+ * in the ODPOR paper) with the given event
+ *
+ * Two events `e` and `e'` in an execution `E` are said to
+ * race iff
+ *
+ * 1. `proc(e) != proc(e')`; that is, the events correspond to
+ * the execution of different actors
+ * 2. `e -->_E e'` and there is no `e''` in `E` such that
+ * `e -->_E e''` and `e'' -->_E e'`; that is, the two events
+ * "happen-before" one another in `E` and no other event in
+ * `E` "happens-between" `e` and `e'`
+ *
+ * @param handle the event with respect to which races are
+ * computed
+ * @returns a set of event handles from which race with `handle`
*/
- std::unordered_set<EventHandle> get_racing_events_of(EventHandle) const;
+ std::unordered_set<EventHandle> get_racing_events_of(EventHandle handle) const;
/**
* @brief Returns a handle to the newest event of the execution,
return contents_.empty() ? std::nullopt : std::optional<EventHandle>{static_cast<EventHandle>(size() - 1)};
}
+ /**
+ * @brief Computes `pre(e, E)` as described in ODPOR [1]
+ *
+ * The execution `pre(e, E)` for an event `e` in an
+ * execution `E` is the contiguous prefix of events
+ * `E' <= E` up to by excluding the event `e` itself.
+ * The prefix intuitively represents the "history" of
+ * causes that permitted event `e` to exist (roughly
+ * speaking)
+ */
Execution get_prefix_up_to(EventHandle) const;
/**
// Since e2 -->_E e3, actor 3 is not an initial for E' := pre(1, execution)
// with respect to `v`. e2, however, has nothing happening before it in dom_E(v),
// so it is an initial of E' wrt. `v`
- const auto initial_wrt_event1 = execution.get_first_s
sdpor_initial_from(1, std::unordered_set<aid_t>{});
+ const auto initial_wrt_event1 = execution.get_first_sdpor_initial_from(1, std::unordered_set<aid_t>{});
REQUIRE(initial_wrt_event1.has_value());
REQUIRE(initial_wrt_event1.value() == static_cast<aid_t>(1));
}
// First, note that v := notdep(1, execution).p == {}.{e3} == {e3}
// e3 has nothing happening before it in dom_E(v), so it is an initial
// of E' wrt. `v`
- const auto initial_wrt_event2 = execution.get_first_s
sdpor_initial_from(2, std::unordered_set<aid_t>{});
+ const auto initial_wrt_event2 = execution.get_first_sdpor_initial_from(2, std::unordered_set<aid_t>{});
REQUIRE(initial_wrt_event2.has_value());
REQUIRE(initial_wrt_event2.value() == static_cast<aid_t>(3));
}
