1 /* Copyright (c) 2008-2023. The SimGrid Team. All rights reserved. */
3 /* This program is free software; you can redistribute it and/or modify it
4 * under the terms of the license (GNU LGPL) which comes with this package. */
6 #include "src/mc/explo/odpor/Execution.hpp"
7 #include "xbt/asserts.h"
12 namespace simgrid::mc::odpor {
14 void Execution::push_transition(const Transition* t)
17 throw std::invalid_argument("Unexpectedly received `nullptr`");
19 ClockVector max_clock_vector;
20 for (const Event& e : this->contents_) {
21 if (e.get_transition()->depends(t)) {
22 max_clock_vector = ClockVector::max(max_clock_vector, e.get_clock_vector());
25 max_clock_vector[t->aid_] = this->size();
26 contents_.push_back(Event({t, max_clock_vector}));
29 std::unordered_set<Execution::EventHandle> Execution::get_racing_events_of(Execution::EventHandle target) const
31 std::unordered_set<Execution::EventHandle> racing_events;
32 std::unordered_set<Execution::EventHandle> disqualified_events;
34 // For each event of the execution
35 for (auto e_i = target; e_i != std::numeric_limits<Execution::EventHandle>::max(); e_i--) {
36 // We need `e_i -->_E target` as a necessary condition
37 if (not happens_before(e_i, target)) {
41 // Further, `proc(e_i) != proc(target)`
42 if (get_actor_with_handle(e_i) == get_actor_with_handle(target)) {
43 disqualified_events.insert(e_i);
47 // There could an event that "happens-between" the two events which would discount `e_i` as a race
48 for (auto e_j = e_i; e_j < target; e_j++) {
50 // 1. e_i --->_E e_j; and
51 // 2. disqualified_events.count(e_j) > 0
52 // then e_i --->_E target indirectly (either through
53 // e_j directly, or transitively through e_j)
54 if (happens_before(e_i, e_j) and disqualified_events.count(e_j) > 0) {
55 disqualified_events.insert(e_i);
60 // If `e_i` wasn't disqualified in the last round,
61 // it's in a race with `target`. After marking it
62 // as such, we ensure no other event `e` can happen-before
63 // it (since this would transitively make it the event
64 // which "happens-between" `target` and `e`)
65 if (disqualified_events.count(e_i) == 0) {
66 racing_events.insert(e_i);
67 disqualified_events.insert(e_i);
74 Execution Execution::get_prefix_before(Execution::EventHandle handle) const
76 return Execution(std::vector<Event>{contents_.begin(), contents_.begin() + handle});
79 std::optional<aid_t> Execution::get_first_sdpor_initial_from(EventHandle e,
80 std::unordered_set<aid_t> disqualified_actors) const
82 // If this execution is empty, there are no initials
83 // relative to the last transition added to the execution
84 // since such a transition does not exist
89 // To actually compute `I_[E'](v) ∩ backtrack(E')`, we must
90 // first compute `E'` and "move" in the direction of `v`.
91 // We perform a scan over `E` (this execution) and make
92 // note of any events which occur after `e` but don't
93 // "happen-after" `e` by pushing them onto `E'`. Note that
94 // correctness is still preserved in computing `v` "on-the-fly"
95 // to determine if an actor `q` is an initial for `E'` after `v`:
96 // only those events that "occur-before" `v`
97 // could happen-before `v` for any valid happens-before relation.
99 // First, grab `E' := pre(e, E)` and determine what actor `p` is
100 const auto next_E_p = get_latest_event_handle().value();
101 Execution E_prime_v = get_prefix_before(e);
102 std::vector<sdpor::Execution::EventHandle> v;
104 // Note `e + 1` here: `notdep(e, E)` is defined as the
105 // set of events that *occur-after* but don't *happen-after* `e`
106 for (auto e_prime = e + 1; e_prime <= next_E_p; ++e_prime) {
107 // Any event `e*` which occurs after `e` but which does not
108 // happen after `e` is a member of `v`. In addition to marking
109 // the event in `v`, we also "simulate" running the action `v`
111 if (not happens_before(e, e_prime) or e_prime == next_E_p) {
112 // First, push the transition onto the hypothetical execution
113 E_prime_v.push_transition(get_event_with_handle(e_prime).get_transition());
114 const EventHandle e_prime_in_E_prime_v = E_prime_v.get_latest_event_handle().value();
116 // When checking whether any event in `dom_[E'](v)` happens before
117 // `next_[E'](q)` below for thread `q`, we must consider that the
118 // events relative to `E` (this execution) are different than those
119 // relative to `E'.v`. Thus e.g. event `7` in `E` may be event `4`
120 // in `E'.v`. Since we are asking about "happens-before"
121 // `-->_[E'.v]` about `E'.v`, we must build `v` relative to `E'`
122 v.push_back(e_prime_in_E_prime_v);
124 // Note that we add `q` to v regardless of whether `q` itself has been
125 // disqualified since `q` may itself disqualify other actors
126 // (i.e. even if `q` is disqualified from being an initial, it
127 // is still contained in the sequence `v`)
128 const aid_t q = E_prime_v.get_actor_with_handle(e_prime_in_E_prime_v);
129 if (disqualified_actors.count(q) > 0) {
132 const bool is_initial = std::none_of(v.begin(), v.end(), [&](const auto& e_star) {
133 return E_prime_v.happens_before(e_star, e_prime_in_E_prime_v);
138 // If `q` is disqualified as a candidate, clearly
139 // no event occurring after `e_prime` in `E` executed
140 // by actor `q` will qualify since any (valid) happens-before
141 // relation orders actions taken by each actor
142 disqualified_actors.insert(q);
149 std::optional<PartialExecution> Execution::get_odpor_extension_from(EventHandle e, EventHandle e_prime,
150 std::unordered_set<aid_t> sleep_set,
151 std::unordered_set<aid_t> enabled_actors) const
153 // TODO: Implement this :(
157 bool Execution::is_initial_after_execution(const PartialExecution& w, aid_t p) const
160 std::vector<EventHandle> w_handles;
161 for (const auto& w_i : w) {
162 // Take one step in the direction of `w`
163 E_w.push_transition(w_i.get());
165 // If that step happened to be executed by `p`,
166 // great: we know that `p` is contained in `w`.
167 // We now need to verify that it doens't "happen-after"
168 // any events which occur before it
169 if (w_i->aid_ == p) {
170 const auto p_handle = E_w.get_latest_event_handle().value();
171 return std::none_of(w_handles.begin(), w_handles.end(),
172 [&](const auto handle) { return E_w.happens_before(handle, p_handle); });
174 w_handles.push_back(E_w.get_latest_event_handle().value());
180 bool Execution::is_independent_with_execution(const PartialExecution& w, const Transition* next_E_p) const
182 // INVARIANT: Here, we assume that for any process `p_i` of `w`,
183 // the events of this execution followed by the execution of all
184 // actors occurring before `p_i` in `v` (`p_j`, `0 <= j < i`)
185 // are sufficient to enable `p_i`. This is fortunately the case
186 // with what ODPOR requires of us, viz. to ask the question about
187 // `v := notdep(e, E)` for some execution `E` and event `e` of
190 E_p_w.push_transition(next_E_p);
191 const auto p_handle = E_p_w.get_latest_event_handle().value();
193 // As we add events to `w`, verify that none
194 // of them "happen-after" the event associated with
195 // the step `next_E_p` (viz. p_handle)
196 for (const auto& w_i : w) {
197 E_p_w.push_transition(w_i.get());
198 const auto w_i_handle = E_p_w.get_latest_event_handle().value();
199 if (E_p_w.happens_before(p_handle, w_i_handle)) {
206 std::optional<PartialExecution> Execution::get_shortest_odpor_sq_subset_insertion(const PartialExecution& v,
207 const PartialExecution& w) const
209 // See section 4 of Abdulla. et al.'s 2017 ODPOR paper for details (specifically
210 // where the [iterative] computation of `v ~_[E] w` is described)
214 for (const auto& next_p_E : v) {
215 const aid_t p = next_p_E->aid_;
217 // Is `p in `I_[E](w)`?
218 if (E_v.is_initial_after_execution(w_now, p)) {
219 // Remove `p` from w and continue
221 // TODO: If `p` occurs in `w`, it had better refer to the same
222 // transition referenced by `v`. Unfortunately, we have two
223 // sources of truth here which can be manipulated at the same
224 // time as arguments to the function. If ODPOR works correctly,
225 // they should always refer to the same value; but as a sanity check,
226 // we have an assert that tests that at least the types are the same.
227 const auto action_by_p_in_w =
228 std::find_if(w_now.begin(), w_now.end(), [=](const auto& action) { return action->aid_ == p; });
229 xbt_assert(action_by_p_in_w != w_now.end(), "Invariant violated: actor `p` "
230 "is claimed to be an initial after `w` but is "
231 "not actually contained in `w`. This indicates that there "
232 "is a bug computing initials");
233 const auto& w_action = *action_by_p_in_w;
234 xbt_assert(w_action->type_ == next_p_E->type_,
235 "Invariant violated: `v` claims that actor `%ld` executes '%s' while "
236 "`w` claims that it executes '%s'. These two partial executions both "
237 "refer to `next_[E](p)`, which should be the same",
238 p, next_p_E->to_string(false).c_str(), w_action->to_string(false).c_str());
239 w_now.erase(action_by_p_in_w);
242 else if (E_v.is_independent_with_execution(w, next_p_E.get())) {
243 // INVARIANT: Note that it is impossible for `p` to be
244 // excluded from the set `I_[E](w)` BUT ALSO be contained in
245 // `w` itself if `E ⊢ p ◇ w`. We assert this is the case here
246 const auto action_by_p_in_w =
247 std::find_if(w_now.begin(), w_now.end(), [=](const auto& action) { return action->aid_ == p; });
248 xbt_assert(action_by_p_in_w == w_now.end(),
249 "Invariant violated: We claimed that actor `%ld` is not an initial "
250 "after `w`, yet it's independent with all actions of `w` AND occurs in `w`."
251 "This indicates that there is a bug computing initials",
254 // Neither of the two above conditions hold, so the relation fails
258 // Move one step forward in the direction of `v` and repeat
259 E_v.push_transition(next_p_E.get());
262 // Construct, finally, v.w' by adding `v` to the front of
263 // what remains of `w` after removing `v` as above
264 for (auto it = v.rbegin(); it != v.rend(); ++it) {
265 w_now.push_front(*it);
268 return std::optional<PartialExecution>{std::move(w_now)};
271 bool Execution::happens_before(Execution::EventHandle e1_handle, Execution::EventHandle e2_handle) const
273 // 1. "happens-before" (-->_E) is a subset of "occurs before" (<_E)
274 // and is an irreflexive relation
275 if (e1_handle >= e2_handle) {
279 // Each execution maintains a stack of clock vectors which are updated
280 // according to the procedure outlined in section 4 of the original DPOR paper
281 const Event& e2 = get_event_with_handle(e2_handle);
282 const aid_t proc_e1 = get_actor_with_handle(e1_handle);
284 if (const auto e1_in_e2_clock = e2.get_clock_vector().get(proc_e1); e1_in_e2_clock.has_value()) {
285 return e1_handle <= e1_in_e2_clock.value();
287 // If `e1` does not appear in e2's clock vector, this implies
288 // not only that the transitions associated with `e1` and `e2
289 // are independent, but further that there are no transitive
290 // dependencies between e1 and e2
294 } // namespace simgrid::mc::odpor