- 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) {
+ XBT_DEBUG("ODPOR: Now considering all possible race with `%u`", 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()) {
+ switch (prev_state.insert_into_wakeup_tree(v.value(), execution_seq_.get_prefix_before(e))) {
+ case odpor::WakeupTree::InsertionResult::root: {
+ XBT_DEBUG("ODPOR: Reversible race with `%u`(%ld: %.20s) unaccounted for in the wakeup tree for "
+ "the execution prior to event `%u`(%ld: %.20s):",
+ e_prime, stack_[e_prime]->get_transition_out()->aid_,
+ stack_[e_prime]->get_transition_out()->to_string(true).c_str(), e,
+ prev_state.get_transition_out()->aid_,
+ prev_state.get_transition_out()->to_string(true).c_str());
+ 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;
+ }