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
Execution E_prime_v = get_prefix_up_to(e);
std::vector<sdpor::Execution::EventHandle> v;
+ // Note `e + 1` here: `notdep(e, E)` is defined as the
+ // set of events that *occur-after* but don't *happen-after* `e`
for (auto e_prime = e + 1; e_prime <= next_E_p; ++e_prime) {
// Any event `e*` which occurs after `e` but which does not
// happen after `e` is a member of `v`. In addition to marking
// 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 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;
- } else {
- disqualified_actors.insert(q);
+ 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);
+ }
}
}
return std::nullopt;
}
-std::unordered_set<aid_t> Execution::get_ssdpor_initials_from(EventHandle e,
- std::unordered_set<aid_t> disqualified) const
-{
- return std::unordered_set<aid_t>();
-}
-
bool Execution::happens_before(Execution::EventHandle e1_handle, Execution::EventHandle e2_handle) const
{
// 1. "happens-before" (-->_E) is a subset of "occurs before" (<_E)
