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"
10 namespace simgrid::mc::odpor {
12 void Execution::push_transition(const Transition* t)
15 throw std::invalid_argument("Unexpectedly received `nullptr`");
17 ClockVector max_clock_vector;
18 for (const Event& e : this->contents_) {
19 if (e.get_transition()->depends(t)) {
20 max_clock_vector = ClockVector::max(max_clock_vector, e.get_clock_vector());
23 // The entry in the vector for `t->aid_` is the size
24 // of the new stack, which will have a size one greater
25 // than that before we insert the new events
26 max_clock_vector[t->aid_] = this->size() + 1;
27 contents_.push_back(Event({t, max_clock_vector}));
30 void Execution::pop_latest()
35 std::unordered_set<Execution::EventHandle> Execution::get_racing_events_of(Execution::EventHandle target) const
37 std::unordered_set<Execution::EventHandle> racing_events;
38 std::unordered_set<Execution::EventHandle> disqualified_events;
40 // For each event of the execution
41 for (auto e_i = target; e_i > 0 && e_i != std::numeric_limits<Execution::EventHandle>::max(); e_i--) {
42 // We need `e_i -->_E target` as a necessary condition
43 if (not happens_before(e_i, target)) {
47 // Further, `proc(e_i) != proc(target)`
48 if (get_actor_with_handle(e_i) == get_actor_with_handle(target)) {
49 disqualified_events.insert(e_i);
53 // There could an event that "happens-between" the two events which would discount `e_i` as a race
54 for (auto e_j = e_i; e_j < target; e_j++) {
56 // 1. e_i --->_E e_j; and
57 // 2. disqualified_events.count(e_j) > 0
58 // then e_i --->_E target indirectly (either through
59 // e_j directly, or transitively through e_j)
60 if (happens_before(e_i, e_j) and disqualified_events.count(e_j) > 0) {
61 disqualified_events.insert(e_i);
66 // If `e_i` wasn't disqualified in the last round,
67 // it's in a race with `target`. After marking it
68 // as such, we ensure no other event `e` can happen-before
69 // it (since this would transitively make it the event
70 // which "happens-between" `target` and `e`)
71 if (disqualified_events.count(e_i) == 0) {
72 racing_events.insert(e_i);
73 disqualified_events.insert(e_i);
80 Execution Execution::get_prefix_up_to(Execution::EventHandle handle) const
82 return Execution(std::vector<Event>{contents_.begin(), contents_.begin() + handle});
85 std::optional<aid_t> Execution::get_first_ssdpor_initial_from(EventHandle e,
86 std::unordered_set<aid_t> disqualified_actors) const
88 // If this execution is empty, there are no initials
89 // relative to the last transition added to the execution
90 // since such a transition does not exist
95 // First, grab `E' := pre(e, E)` and determine what actor `p` is
96 // TODO: Instead of copying around these big structs, it
97 // would behoove us to incorporate some way to reference
98 // portions of an execution. For simplicity and for a
99 // "proof of concept" version, we opt to simply copy
100 // the contents instead of making a view into the execution
101 const auto next_E_p = get_latest_event_handle().value();
102 Execution E_prime_v = get_prefix_up_to(e);
103 std::vector<sdpor::Execution::EventHandle> v;
105 for (auto e_prime = e; e_prime <= next_E_p; ++e_prime) {
106 // Any event `e*` which occurs after `e` but which does not
107 // happen after `e` is a member of `v`. In addition to marking
108 // the event in `v`, we also "simulate" running the action `v`
110 if (not happens_before(e, e_prime) or e_prime == next_E_p) {
111 v.push_back(e_prime);
112 E_prime_v.push_transition(get_event_with_handle(e_prime).get_transition());
116 const EventHandle e_prime_in_E_prime = E_prime_v.get_latest_event_handle().value();
117 const aid_t q = E_prime_v.get_actor_with_handle(e_prime_in_E_prime);
118 if (disqualified_actors.count(q) > 0) {
121 const bool is_initial = std::none_of(
122 v.begin(), v.end(), [&](const auto& e_star) { return E_prime_v.happens_before(e_star, e_prime_in_E_prime); });
126 disqualified_actors.insert(q);
132 std::unordered_set<aid_t> Execution::get_ssdpor_initials_from(EventHandle e,
133 std::unordered_set<aid_t> disqualified) const
135 return std::unordered_set<aid_t>();
138 bool Execution::happens_before(Execution::EventHandle e1_handle, Execution::EventHandle e2_handle) const
140 // 1. "happens-before" is a subset of "occurs before"
141 if (e1_handle > e2_handle) {
145 // Each execution maintains a stack of clock vectors which are updated
146 // according to the procedure outlined in section 4 of the original DPOR paper
147 const Event& e2 = get_event_with_handle(e2_handle);
148 const aid_t proc_e1 = get_actor_with_handle(e1_handle);
149 return e1_handle <= e2.get_clock_vector().get(proc_e1).value_or(0);
152 } // namespace simgrid::mc::odpor