namespace simgrid::mc::odpor {
-using ProcessSequence = std::list<aid_t>;
-using ExecutionSequence = std::list<const State*>;
-using Hypothetical = ExecutionSequence;
-
/**
* @brief The occurrence of a transition in an execution
+ *
+ * An execution is set of *events*, where each element represents
+ * the occurrence or execution of the `i`th step of a particular
+ * actor `j`
*/
class Event {
std::pair<const Transition*, ClockVector> contents_;
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 std::get<0>(contents_); }
* In addition to representing an actual steps taken,
* an execution keeps track of the "happens-before"
* relation among the transitions in the execution
- * by following the procedure outlined in the
- * original DPOR paper with clock vectors
+ * by following the procedure outlined in section 4 of the
+ * original DPOR paper with clock vectors.
+ * As new transitions are added to the execution, clock vectors are
+ * computed as appropriate and associated with the corresponding position
+ * in the execution. This allows us to determine “happens-before” in
+ * constant-time between points in the execution (called events
+ * [which is unfortunately the same name used in UDPOR for a slightly
+ * different concept]), albeit for an up-front cost of traversing the
+ * execution stack. The happens-before relation is important in many
+ * places in SDPOR and ODPOR.
*
* @note: For more nuanced happens-before relations, clock
* vectors may not always suffice. Clock vectors work
Execution(const Execution&) = default;
Execution& operator=(Execution const&) = default;
Execution(Execution&&) = default;
- Execution(ExecutionSequence&& seq);
- Execution(const ExecutionSequence& seq);
size_t size() const { return this->contents_.size(); }
bool empty() const { return this->contents_.empty(); }
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;
+ /**
+ * @brief Computes the "core" portion the SDPOR algorithm,
+ * viz. the intersection of the backtracking set and the
+ * set of initials with respect to the *last* event added
+ * to the execution
+ *
+ * The "core" portion of the SDPOR algorithm is found on
+ * lines 6-9 of the pseudocode:
+ *
+ * 6 | let E' := pre(E, e)
+ * 7 | let v := notdep(e, E).p
+ * 8 | if I_[E'](v) ∩ backtrack(E') = empty then
+ * 9 | --> add some q in I_[E'](v) to backtrack(E')
+ *
+ * This method computes all of the lines simultaneously,
+ * returning some actor `q` if it passes line 8 and exists.
+ * The event `e` and the set `backtrack(E')` are the provided
+ * arguments to the method.
+ *
+ * @param e the event with respect to which to determine
+ * whether a backtrack point needs to be added for the
+ * prefix corresponding to the execution prior to `e`
+ *
+ * @param backtrack_set The set of actors which should
+ * not be considered for selection as an SDPOR initial.
+ * While this set need not necessarily correspond to the
+ * backtrack set `backtrack(E')`, doing so provides what
+ * is expected for SDPOR
+ *
+ * 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 explicitly 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> backtrack_set) 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_after_execution(const PartialExecution& w, aid_t p) const;
+ bool is_independent_with_execution(const PartialExecution& w, const Transition* next_E_p) const;
- // bool is_initial(aid_t p, const Hypothetical& w) const;
- // bool is_weak_initial(aid_t p, const Hypothetical& w) const;
+ /**
+ * @brief For a given sequence of actors `v` and a sequence of transitions `w`,
+ * computes the sequence, if any, that should be inserted as a child a WakeupTree for
+ * this execution
+ */
+ std::optional<PartialExecution> get_shortest_odpor_sq_subset_insertion(const PartialExecution& v,
+ const PartialExecution& w) 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;
/**
*/
bool happens_before(EventHandle e1, EventHandle e2) const;
- /**
- * @brief Removes the last event of the execution,
- * if such an event exists
- *
- * @note: When you remove events from an execution, any views
- * of the execution referring to those removed events
- * become invalidated
- */
- void pop_latest();
-
/**
* @brief Extends the execution by one more step
*
