- for (auto e_prime = static_cast<odpor::Execution::EventHandle>(0); e_prime <= last_event; e_prime++) {
- for (const auto e : execution_seq_.get_racing_events_of(e_prime)) {
- // To determine if the race is reversible, we have to ensure
- // that actor `p` running `e_i` (viz. the event such that
- // `racing_event -> (E_p) e_i` and no other event
- // "happens-between" the two) is enabled in any equivalent
- // execution where `racing_event` happens before `e_i`.
- //
- // Importantly, it is equivalent to checking if in ANY
- // such equivalent execution sequence where `racing_event`
- // happens-before `next_E_p` that `p` is enabled in `pre(racing_event, E.p)`.
- // Thus it suffices to check THIS execution
- //
- // If the actor `p` is not enabled at s_[E'], it is not a *reversible* race
- const aid_t p = execution_seq_.get_actor_with_handle(e_prime);
- const std::shared_ptr<State> prev_state = stack_[e];
- if (prev_state->is_actor_enabled(p)) {
- const std::optional<odpor::PartialExecution> v = execution_seq_.get_odpor_extension_from(
- e, e_prime, prev_state->get_sleeping_set(), prev_state->get_enabled_actors());
- if (v.has_value()) {
- prev_state->mark_path_interesting_for_odpor(v.value(), execution_seq_.get_prefix_before(e));
+ for (auto e_prime = static_cast<odpor::Execution::EventHandle>(0); e_prime <= last_event.value(); ++e_prime) {
+ for (const auto e : execution_seq_.get_reversible_races_of(e_prime)) {
+ XBT_DEBUG("ODPOR: Reversible race detected between events `%u` and `%u`", e, e_prime);
+ State& prev_state = *stack_[e];
+ if (const auto v = execution_seq_.get_odpor_extension_from(e, e_prime, prev_state); v.has_value()) {
+ const auto result = prev_state.insert_into_wakeup_tree(v.value(), execution_seq_.get_prefix_before(e));
+ switch (result) {
+ case odpor::WakeupTree::InsertionResult::root: {
+ XBT_DEBUG("ODPOR: Reversible race with `%u` unaccounted for in the wakeup tree for "
+ "the execution prior to event `%u`:",
+ e_prime, e);
+ break;
+ }
+ case odpor::WakeupTree::InsertionResult::interior_node: {
+ XBT_DEBUG("ODPOR: Reversible race with `%u` partially accounted for in the wakeup tree for "
+ "the execution prior to event `%u`:",
+ e_prime, e);
+ break;
+ }
+ case odpor::WakeupTree::InsertionResult::leaf: {
+ XBT_DEBUG("ODPOR: Reversible race with `%u` accounted for in the wakeup tree for "
+ "the execution prior to event `%u`:",
+ e_prime, e);
+ break;
+ }