* under the terms of the license (GNU LGPL) which comes with this package. */
#include "src/mc/explo/odpor/Execution.hpp"
-#include <exception>
+#include "xbt/asserts.h"
+#include <algorithm>
#include <limits>
+#include <vector>
namespace simgrid::mc::odpor {
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 new stack, which will have a size one greater
- // than that before we insert the new events
- max_clock_vector[t->aid_] = this->size() + 1;
+ max_clock_vector[t->aid_] = this->size();
contents_.push_back(Event({t, max_clock_vector}));
}
-void Execution::pop_latest()
-{
- contents_.pop_back();
-}
-
std::unordered_set<Execution::EventHandle> Execution::get_racing_events_of(Execution::EventHandle target) const
{
std::unordered_set<Execution::EventHandle> racing_events;
std::unordered_set<Execution::EventHandle> disqualified_events;
// For each event of the execution
- for (auto e_i = target; e_i > 0 && e_i != std::numeric_limits<Execution::EventHandle>::max(); e_i--) {
+ for (auto e_i = target; e_i != std::numeric_limits<Execution::EventHandle>::max(); e_i--) {
// We need `e_i -->_E target` as a necessary condition
if (not happens_before(e_i, target)) {
continue;
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;
}
+ // To actually compute `I_[E'](v) ∩ backtrack(E')`, we must
+ // first compute `E'` and "move" in the direction of `v`.
+ // We perform a scan over `E` (this execution) and make
+ // note of any events which occur after `e` but don't
+ // "happen-after" `e` by pushing them onto `E'`. Note that
+ // correctness is still preserved in computing `v` "on-the-fly"
+ // to determine if an actor `q` is an initial for `E'` after `v`:
+ // only those events that "occur-before" `v`
+ // could happen-before `v` for any valid happens-before relation.
+
// First, grab `E' := pre(e, E)` and determine what actor `p` is
- // TODO: Instead of copying around these big structs, it
- // would behoove us to incorporate some way to reference
- // portions of an execution. For simplicity and for a
- // "proof of concept" version, we opt to simply copy
- // the contents instead of making a view into the execution
const auto next_E_p = get_latest_event_handle().value();
Execution E_prime_v = get_prefix_up_to(e);
std::vector<sdpor::Execution::EventHandle> v;
// the event in `v`, we also "simulate" running the action `v`
// from E'
if (not happens_before(e, e_prime) or e_prime == next_E_p) {
- v.push_back(e_prime);
+ // First, push the transition onto the hypothetical execution
E_prime_v.push_transition(get_event_with_handle(e_prime).get_transition());
- } else {
- continue;
- }
- const EventHandle e_prime_in_E_prime = E_prime_v.get_latest_event_handle().value();
- const aid_t q = E_prime_v.get_actor_with_handle(e_prime_in_E_prime);
- if (disqualified_actors.count(q) > 0) {
- continue;
+ const EventHandle e_prime_in_E_prime_v = E_prime_v.get_latest_event_handle().value();
+
+ // When checking whether any event in `dom_[E'](v)` happens before
+ // `next_[E'](q)` below for thread `q`, we must consider that the
+ // events relative to `E` (this execution) are different than those
+ // relative to `E'.v`. Thus e.g. event `7` in `E` may be event `4`
+ // in `E'.v`. Since we are asking about "happens-before"
+ // `-->_[E'.v]` about `E'.v`, we must build `v` relative to `E'`
+ v.push_back(e_prime_in_E_prime_v);
+
+ // Note that we add `q` to v regardless of whether `q` itself has been
+ // disqualified since `q` may itself disqualify other actors
+ // (i.e. even if `q` is disqualified from being an initial, it
+ // is still contained in the sequence `v`)
+ const aid_t q = E_prime_v.get_actor_with_handle(e_prime_in_E_prime_v);
+ if (disqualified_actors.count(q) > 0) {
+ continue;
+ }
+ const bool is_initial = std::none_of(v.begin(), v.end(), [&](const auto& e_star) {
+ return E_prime_v.happens_before(e_star, e_prime_in_E_prime_v);
+ });
+ if (is_initial) {
+ return q;
+ } else {
+ // If `q` is disqualified as a candidate, clearly
+ // no event occurring after `e_prime` in `E` executed
+ // by actor `q` will qualify since any (valid) happens-before
+ // relation orders actions taken by each actor
+ disqualified_actors.insert(q);
+ }
}
- const bool is_initial = std::none_of(
- v.begin(), v.end(), [&](const auto& e_star) { return E_prime_v.happens_before(e_star, e_prime_in_E_prime); });
- if (is_initial) {
- return q;
+ }
+ return std::nullopt;
+}
+
+bool Execution::is_initial_after_execution(const PartialExecution& w, aid_t p) const
+{
+ auto E_w = *this;
+ std::vector<EventHandle> w_handles;
+ for (const auto& w_i : w) {
+ // Take one step in the direction of `w`
+ E_w.push_transition(w_i.get());
+
+ // If that step happened to be executed by `p`,
+ // great: we know that `p` is contained in `w`.
+ // We now need to verify that it doens't "happen-after"
+ // any events which occur before it
+ if (w_i->aid_ == p) {
+ const auto p_handle = E_w.get_latest_event_handle().value();
+ return std::none_of(w_handles.begin(), w_handles.end(),
+ [&](const auto handle) { return E_w.happens_before(handle, p_handle); });
} else {
- disqualified_actors.insert(q);
+ w_handles.push_back(E_w.get_latest_event_handle().value());
}
}
- return std::nullopt;
+ return false;
}
-std::unordered_set<aid_t> Execution::get_ssdpor_initials_from(EventHandle e,
- std::unordered_set<aid_t> disqualified) const
+bool Execution::is_independent_with_execution(const PartialExecution& w, const Transition* next_E_p) const
{
- return std::unordered_set<aid_t>();
+ // INVARIANT: Here, we assume that for any process `p_i` of `w`,
+ // the events of this execution followed by the execution of all
+ // actors occurring before `p_i` in `v` (`p_j`, `0 <= j < i`)
+ // are sufficient to enable `p_i`. This is fortunately the case
+ // with what ODPOR requires of us, viz. to ask the question about
+ // `v := notdep(e, E)` for some execution `E` and event `e` of
+ // that execution.
+ auto E_p_w = *this;
+ E_p_w.push_transition(next_E_p);
+ const auto p_handle = E_p_w.get_latest_event_handle().value();
+
+ // As we add events to `w`, verify that none
+ // of them "happen-after" the event associated with
+ // the step `next_E_p` (viz. p_handle)
+ for (const auto& w_i : w) {
+ E_p_w.push_transition(w_i.get());
+ const auto w_i_handle = E_p_w.get_latest_event_handle().value();
+ if (E_p_w.happens_before(p_handle, w_i_handle)) {
+ return false;
+ }
+ }
+ return true;
+}
+
+std::optional<PartialExecution> Execution::get_shortest_odpor_sq_subset_insertion(const PartialExecution& v,
+ const PartialExecution& w) const
+{
+ // See section 4 of Abdulla. et al.'s 2017 ODPOR paper for details (specifically
+ // where the [iterative] computation of `v ~_[E] w` is described)
+ auto E_v = *this;
+ auto w_now = w;
+
+ for (const auto& next_p_E : v) {
+ const aid_t p = next_p_E->aid_;
+
+ // Is `p in `I_[E](w)`?
+ if (E_v.is_initial_after_execution(w_now, p)) {
+ // Remove `p` from w and continue
+
+ // TODO: If `p` occurs in `w`, it had better refer to the same
+ // transition referenced by `v`. Unfortunately, we have two
+ // sources of truth here which can be manipulated at the same
+ // time as arguments to the function. If ODPOR works correctly,
+ // they should always refer to the same value; but as a sanity check,
+ // we have an assert that tests that at least the types are the same.
+ const auto action_by_p_in_w =
+ std::find_if(w_now.begin(), w_now.end(), [=](const auto& action) { return action->aid_ == p; });
+ xbt_assert(action_by_p_in_w != w_now.end(), "Invariant violated: actor `p` "
+ "is claimed to be an initial after `w` but is "
+ "not actually contained in `w`. This indicates that there "
+ "is a bug computing initials");
+ const auto& w_action = *action_by_p_in_w;
+ xbt_assert(w_action->type_ == next_p_E->type_,
+ "Invariant violated: `v` claims that actor `%ld` executes '%s' while "
+ "`w` claims that it executes '%s'. These two partial executions both "
+ "refer to `next_[E](p)`, which should be the same",
+ p, next_p_E->to_string(false).c_str(), w_action->to_string(false).c_str());
+ w_now.erase(action_by_p_in_w);
+ }
+ // Is `E ⊢ p ◇ w`?
+ else if (E_v.is_independent_with_execution(w, next_p_E.get())) {
+ // INVARIANT: Note that it is impossible for `p` to be
+ // excluded from the set `I_[E](w)` BUT ALSO be contained in
+ // `w` itself if `E ⊢ p ◇ w`. We assert this is the case here
+ const auto action_by_p_in_w =
+ std::find_if(w_now.begin(), w_now.end(), [=](const auto& action) { return action->aid_ == p; });
+ xbt_assert(action_by_p_in_w == w_now.end(),
+ "Invariant violated: We claimed that actor `%ld` is not an initial "
+ "after `w`, yet it's independent with all actions of `w` AND occurs in `w`."
+ "This indicates that there is a bug computing initials",
+ p);
+ } else {
+ // Neither of the two above conditions hold, so the relation fails
+ return std::nullopt;
+ }
+
+ // Move one step forward in the direction of `v` and repeat
+ E_v.push_transition(next_p_E.get());
+ }
+
+ // Construct, finally, v.w' by adding `v` to the front of
+ // what remains of `w` after removing `v` as above
+ for (auto it = v.rbegin(); it != v.rend(); ++it) {
+ w_now.push_front(*it);
+ }
+
+ return std::optional<PartialExecution>{std::move(w_now)};
}
bool Execution::happens_before(Execution::EventHandle e1_handle, Execution::EventHandle e2_handle) const
