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 "src/mc/api/State.hpp"
8 #include "src/mc/explo/odpor/ReversibleRaceCalculator.hpp"
9 #include "xbt/asserts.h"
10 #include "xbt/string.hpp"
15 namespace simgrid::mc::odpor {
17 std::vector<std::string> get_textual_trace(const PartialExecution& w)
19 std::vector<std::string> trace;
20 for (const auto& t : w) {
21 const auto a = xbt::string_printf("Actor %ld: %s", t->aid_, t->to_string(true).c_str());
22 trace.push_back(std::move(a));
27 void Execution::push_transition(std::shared_ptr<Transition> t)
30 throw std::invalid_argument("Unexpectedly received `nullptr`");
32 ClockVector max_clock_vector;
33 for (const Event& e : this->contents_) {
34 if (e.get_transition()->depends(t.get())) {
35 max_clock_vector = ClockVector::max(max_clock_vector, e.get_clock_vector());
38 max_clock_vector[t->aid_] = this->size();
39 contents_.push_back(Event({std::move(t), max_clock_vector}));
42 std::vector<std::string> Execution::get_textual_trace() const
44 std::vector<std::string> trace;
45 for (const auto& t : this->contents_) {
47 xbt::string_printf("Actor %ld: %s", t.get_transition()->aid_, t.get_transition()->to_string(true).c_str());
48 trace.push_back(std::move(a));
53 std::unordered_set<Execution::EventHandle> Execution::get_racing_events_of(Execution::EventHandle target) const
55 std::unordered_set<Execution::EventHandle> racing_events;
56 std::unordered_set<Execution::EventHandle> disqualified_events;
58 // For each event of the execution
59 for (auto e_i = target; e_i != std::numeric_limits<Execution::EventHandle>::max(); e_i--) {
60 // We need `e_i -->_E target` as a necessary condition
61 if (not happens_before(e_i, target)) {
65 // Further, `proc(e_i) != proc(target)`
66 if (get_actor_with_handle(e_i) == get_actor_with_handle(target)) {
67 disqualified_events.insert(e_i);
71 // There could an event that "happens-between" the two events which would discount `e_i` as a race
72 for (auto e_j = e_i; e_j < target; e_j++) {
74 // 1. e_i --->_E e_j; and
75 // 2. disqualified_events.count(e_j) > 0
76 // then e_i --->_E target indirectly (either through
77 // e_j directly, or transitively through e_j)
78 if (disqualified_events.count(e_j) > 0 and happens_before(e_i, e_j)) {
79 disqualified_events.insert(e_i);
84 // If `e_i` wasn't disqualified in the last round,
85 // it's in a race with `target`. After marking it
86 // as such, we ensure no other event `e` can happen-before
87 // it (since this would transitively make it the event
88 // which "happens-between" `target` and `e`)
89 if (disqualified_events.count(e_i) == 0) {
90 racing_events.insert(e_i);
91 disqualified_events.insert(e_i);
98 std::unordered_set<Execution::EventHandle> Execution::get_reversible_races_of(EventHandle handle) const
100 std::unordered_set<EventHandle> reversible_races;
101 for (EventHandle race : get_racing_events_of(handle)) {
102 if (ReversibleRaceCalculator::is_race_reversible(*this, race, handle)) {
103 reversible_races.insert(race);
106 return reversible_races;
109 Execution Execution::get_prefix_before(Execution::EventHandle handle) const
111 return Execution(std::vector<Event>{contents_.begin(), contents_.begin() + handle});
114 std::optional<aid_t> Execution::get_first_sdpor_initial_from(EventHandle e,
115 std::unordered_set<aid_t> disqualified_actors) const
117 // If this execution is empty, there are no initials
118 // relative to the last transition added to the execution
119 // since such a transition does not exist
124 // To actually compute `I_[E'](v) ∩ backtrack(E')`, we must
125 // first compute `E'` and "move" in the direction of `v`.
126 // We perform a scan over `E` (this execution) and make
127 // note of any events which occur after `e` but don't
128 // "happen-after" `e` by pushing them onto `E'`. Note that
129 // correctness is still preserved in computing `v` "on-the-fly"
130 // to determine if an actor `q` is an initial for `E'` after `v`:
131 // only those events that "occur-before" `v`
132 // could happen-before `v` for any valid happens-before relation.
134 // First, grab `E' := pre(e, E)` and determine what actor `p` is
135 const auto next_E_p = get_latest_event_handle().value();
136 Execution E_prime_v = get_prefix_before(e);
137 std::vector<sdpor::Execution::EventHandle> v;
139 // Note `e + 1` here: `notdep(e, E)` is defined as the
140 // set of events that *occur-after* but don't *happen-after* `e`
141 for (auto e_prime = e + 1; e_prime <= next_E_p; ++e_prime) {
142 // Any event `e*` which occurs after `e` but which does not
143 // happen after `e` is a member of `v`. In addition to marking
144 // the event in `v`, we also "simulate" running the action `v`
146 if (not happens_before(e, e_prime) or e_prime == next_E_p) {
147 // First, push the transition onto the hypothetical execution
148 E_prime_v.push_transition(get_event_with_handle(e_prime).get_transition());
149 const EventHandle e_prime_in_E_prime_v = E_prime_v.get_latest_event_handle().value();
151 // When checking whether any event in `dom_[E'](v)` happens before
152 // `next_[E'](q)` below for thread `q`, we must consider that the
153 // events relative to `E` (this execution) are different than those
154 // relative to `E'.v`. Thus e.g. event `7` in `E` may be event `4`
155 // in `E'.v`. Since we are asking about "happens-before"
156 // `-->_[E'.v]` about `E'.v`, we must build `v` relative to `E'`
157 v.push_back(e_prime_in_E_prime_v);
159 // Note that we add `q` to v regardless of whether `q` itself has been
160 // disqualified since `q` may itself disqualify other actors
161 // (i.e. even if `q` is disqualified from being an initial, it
162 // is still contained in the sequence `v`)
163 const aid_t q = E_prime_v.get_actor_with_handle(e_prime_in_E_prime_v);
164 if (disqualified_actors.count(q) > 0) {
167 const bool is_initial = std::none_of(v.begin(), v.end(), [&](const auto& e_star) {
168 return E_prime_v.happens_before(e_star, e_prime_in_E_prime_v);
173 // If `q` is disqualified as a candidate, clearly
174 // no event occurring after `e_prime` in `E` executed
175 // by actor `q` will qualify since any (valid) happens-before
176 // relation orders actions taken by each actor
177 disqualified_actors.insert(q);
184 std::optional<PartialExecution> Execution::get_odpor_extension_from(EventHandle e, EventHandle e_prime,
185 const State& state_at_e) const
187 // `e` is assumed to be in a reversible race with `e_prime`.
188 // If `e > e_prime`, then `e` occurs-after `e_prime` which means
189 // `e` could not race with if
191 throw std::invalid_argument("ODPOR extensions can only be computed for "
192 "events in a reversible race, which is claimed, "
193 "yet the racing event 'occurs-after' the target");
201 Execution E_prime_v = get_prefix_before(e);
202 std::unordered_set<aid_t> disqualified_actors = state_at_e.get_sleeping_actors();
203 std::vector<sdpor::Execution::EventHandle> v_handles;
204 bool located_actor_in_initial = false;
206 // Note `e + 1` here: `notdep(e, E)` is defined as the
207 // set of events that *occur-after* but don't *happen-after* `e`
209 // SUBTLE NOTE: ODPOR requires us to compute `notdep(e, E)` EVEN THOUGH
210 // the race is between `e` and `e'`; that is, events occurring in `E`
211 // that "occur-after" `e'` may end up in the partial execution `v`.
213 // Observe that `notdep(e, E).proc(e')` will contain all transitions
214 // that don't happen-after `e` in the order they appear FOLLOWED BY
215 // THE **TRANSITION** ASSOCIATED WITH **`e'`**!!
217 // SUBTLE NOTE: Observe that any event that "happens-after" `e'`
218 // must necessarily "happen-after" `e` as well, since `e` and
219 // `e'` are presumed to be in a reversible race. Hence, we know that
220 // all events `e_star` that `e` "happens-before" cannot affect
221 // the enabledness of `e'`; furthermore, `e'` cannot affect the enabledness
222 // of any event independent with `e` that "occurs-after" `e'`
223 for (auto e_star = e + 1; e_star <= get_latest_event_handle().value(); ++e_star) {
224 // Any event `e*` which occurs after `e` but which does not
225 // happen after `e` is a member of `v`. In addition to marking
226 // the event in `v`, we also "simulate" running the action `v` from E'
227 // to be able to compute `--->[E'.v]`
228 if (not happens_before(e, e_star)) {
229 xbt_assert(e_star != e_prime,
230 "Invariant Violation: We claimed events %u and %u were in a reversible race, yet we also "
231 "claim that they do not happen-before one another. This is impossible: "
232 "are you sure that the two events are in a reversible race?",
234 E_prime_v.push_transition(get_event_with_handle(e_star).get_transition());
235 v.push_back(get_event_with_handle(e_star).get_transition());
237 const EventHandle e_star_in_E_prime_v = E_prime_v.get_latest_event_handle().value();
239 // When checking whether any event in `dom_[E'](v)` happens before
240 // `next_[E'](q)` below for thread `q`, we must consider that the
241 // events relative to `E` (this execution) are different than those
242 // relative to `E'.v`. Thus e.g. event `7` in `E` may be event `4`
243 // in `E'.v`. Since we are asking about "happens-before"
244 // `-->_[E'.v]` about `E'.v`, we must build `v` relative to `E'`
245 v_handles.push_back(e_star_in_E_prime_v);
247 if (located_actor_in_initial) {
248 // It suffices that we find one initial. If we've already found
249 // one, we simply need to finish building `v`
253 // Note that we add `q` to v regardless of whether `q` itself has been
254 // disqualified since `q` may itself disqualify other actors
255 // (i.e. even if `q` is disqualified from being an initial, it
256 // is still contained in the sequence `v`)
257 const aid_t q = E_prime_v.get_actor_with_handle(e_star_in_E_prime_v);
258 if (disqualified_actors.count(q) > 0) {
261 const bool is_initial = std::none_of(v_handles.begin(), v_handles.end(), [&](const auto& e_loc) {
262 return E_prime_v.happens_before(e_loc, e_star_in_E_prime_v);
265 located_actor_in_initial = true;
267 // If `q` is disqualified as a candidate, clearly
268 // no event occurring after `e_prime` in `E` executed
269 // by actor `q` will qualify since any (valid) happens-before
270 // relation orders actions taken by each actor
271 disqualified_actors.insert(q);
276 // Now we add `e_prime := <q, i>` to `E'.v` and repeat the same work
278 v.push_back(get_event_with_handle(e_prime).get_transition());
280 if (not located_actor_in_initial) {
281 // It's possible `proc(e_prime)` is an initial
282 E_prime_v.push_transition(get_event_with_handle(e_prime).get_transition());
283 const EventHandle e_prime_in_E_prime_v = E_prime_v.get_latest_event_handle().value();
284 v_handles.push_back(e_prime_in_E_prime_v);
286 const aid_t q = E_prime_v.get_actor_with_handle(e_prime_in_E_prime_v);
287 located_actor_in_initial = disqualified_actors.count(q) == 0 and
288 std::none_of(v_handles.begin(), v_handles.end(), [&](const auto& e_loc) {
289 return E_prime_v.happens_before(e_loc, e_prime_in_E_prime_v);
294 /** Some actor `p` in `v` is an initial for `E' := pre(e, E)`*/
295 if (located_actor_in_initial) {
299 const Execution pre_E_e = get_prefix_before(e);
300 const auto sleeping_actors = state_at_e.get_sleeping_actors();
302 // Otherwise, for each enabled actor also not in the sleep set, check if
303 // any of them are independent with this execution after `v`. This
304 // completes the check for weak initials
305 for (const auto& [aid, astate] : state_at_e.get_actors_list()) {
306 // TODO: We have to be able to react appropriately here when adding new
307 // types of transitions (multiple choices can be made :( )
308 if (astate.is_enabled() and sleeping_actors.count(aid) == 0 and
309 pre_E_e.is_independent_with_execution_of(v, astate.get_transition(0))) {
317 bool Execution::is_initial_after_execution_of(const PartialExecution& w, aid_t p) const
320 std::vector<EventHandle> w_handles;
321 for (const auto& w_i : w) {
322 // Take one step in the direction of `w`
323 E_w.push_transition(w_i);
325 // If that step happened to be executed by `p`,
326 // great: we know that `p` is contained in `w`.
327 // We now need to verify that it doens't "happen-after"
328 // any events which occur before it
329 if (w_i->aid_ == p) {
330 const auto p_handle = E_w.get_latest_event_handle().value();
331 return std::none_of(w_handles.begin(), w_handles.end(),
332 [&](const auto handle) { return E_w.happens_before(handle, p_handle); });
334 w_handles.push_back(E_w.get_latest_event_handle().value());
340 bool Execution::is_independent_with_execution_of(const PartialExecution& w, std::shared_ptr<Transition> next_E_p) const
342 // INVARIANT: Here, we assume that for any process `p_i` of `w`,
343 // the events of this execution followed by the execution of all
344 // actors occurring before `p_i` in `v` (`p_j`, `0 <= j < i`)
345 // are sufficient to enable `p_i`. This is fortunately the case
346 // with what ODPOR requires of us, viz. to ask the question about
347 // `v := notdep(e, E)` for some execution `E` and event `e` of
350 E_p_w.push_transition(std::move(next_E_p));
351 const auto p_handle = E_p_w.get_latest_event_handle().value();
353 // As we add events to `w`, verify that none
354 // of them "happen-after" the event associated with
355 // the step `next_E_p` (viz. p_handle)
356 for (const auto& w_i : w) {
357 E_p_w.push_transition(w_i);
358 const auto w_i_handle = E_p_w.get_latest_event_handle().value();
359 if (E_p_w.happens_before(p_handle, w_i_handle)) {
366 std::optional<PartialExecution> Execution::get_shortest_odpor_sq_subset_insertion(const PartialExecution& v,
367 const PartialExecution& w) const
369 // See section 4 of Abdulla. et al.'s 2017 ODPOR paper for details (specifically
370 // where the [iterative] computation of `v ~_[E] w` is described)
374 for (const auto& next_E_p : v) {
375 const aid_t p = next_E_p->aid_;
377 // Is `p in `I_[E](w)`?
378 if (E_v.is_initial_after_execution_of(w_now, p)) {
379 // Remove `p` from w and continue
381 // TODO: If `p` occurs in `w`, it had better refer to the same
382 // transition referenced by `v`. Unfortunately, we have two
383 // sources of truth here which can be manipulated at the same
384 // time as arguments to the function. If ODPOR works correctly,
385 // they should always refer to the same value; but as a sanity check,
386 // we have an assert that tests that at least the types are the same.
387 const auto action_by_p_in_w =
388 std::find_if(w_now.begin(), w_now.end(), [=](const auto& action) { return action->aid_ == p; });
389 xbt_assert(action_by_p_in_w != w_now.end(), "Invariant violated: actor `p` "
390 "is claimed to be an initial after `w` but is "
391 "not actually contained in `w`. This indicates that there "
392 "is a bug computing initials");
393 const auto& w_action = *action_by_p_in_w;
394 xbt_assert(w_action->type_ == next_E_p->type_,
395 "Invariant violated: `v` claims that actor `%ld` executes '%s' while "
396 "`w` claims that it executes '%s'. These two partial executions both "
397 "refer to `next_[E](p)`, which should be the same",
398 p, next_E_p->to_string(false).c_str(), w_action->to_string(false).c_str());
399 w_now.erase(action_by_p_in_w);
402 else if (E_v.is_independent_with_execution_of(w, next_E_p)) {
403 // INVARIANT: Note that it is impossible for `p` to be
404 // excluded from the set `I_[E](w)` BUT ALSO be contained in
405 // `w` itself if `E ⊢ p ◇ w` (intuitively, the fact that `E ⊢ p ◇ w`
406 // means that are able to move `p` anywhere in `w` IF it occurred, so
407 // if it really does occur we know it must then be an initial).
408 // We assert this is the case here
409 const auto action_by_p_in_w =
410 std::find_if(w_now.begin(), w_now.end(), [=](const auto& action) { return action->aid_ == p; });
411 xbt_assert(action_by_p_in_w == w_now.end(),
412 "Invariant violated: We claimed that actor `%ld` is not an initial "
413 "after `w`, yet it's independent with all actions of `w` AND occurs in `w`."
414 "This indicates that there is a bug computing initials",
417 // Neither of the two above conditions hold, so the relation fails
421 // Move one step forward in the direction of `v` and repeat
422 E_v.push_transition(next_E_p);
424 return std::optional<PartialExecution>{std::move(w_now)};
427 bool Execution::happens_before(Execution::EventHandle e1_handle, Execution::EventHandle e2_handle) const
429 // 1. "happens-before" (-->_E) is a subset of "occurs before" (<_E)
430 // and is an irreflexive relation
431 if (e1_handle >= e2_handle) {
435 // Each execution maintains a stack of clock vectors which are updated
436 // according to the procedure outlined in section 4 of the original DPOR paper
437 const Event& e2 = get_event_with_handle(e2_handle);
438 const aid_t proc_e1 = get_actor_with_handle(e1_handle);
440 if (const auto e1_in_e2_clock = e2.get_clock_vector().get(proc_e1); e1_in_e2_clock.has_value()) {
441 return e1_handle <= e1_in_e2_clock.value();
443 // If `e1` does not appear in e2's clock vector, this implies
444 // not only that the transitions associated with `e1` and `e2
445 // are independent, but further that there are no transitive
446 // dependencies between e1 and e2
450 } // namespace simgrid::mc::odpor