From bc2253e2c879ee28ae5153f1d56497ab802aeea9 Mon Sep 17 00:00:00 2001 From: mlaurent Date: Thu, 9 Nov 2023 10:26:22 +0100 Subject: [PATCH] Discard the wakeup tree when ODPOR reaches a disabled transition --- src/mc/api/State.cpp | 5 +++ src/mc/api/State.hpp | 1 + src/mc/explo/DFSExplorer.cpp | 35 +++++++++++++------ .../explo/odpor/ReversibleRaceCalculator.cpp | 14 ++++---- src/mc/explo/odpor/WakeupTree.cpp | 15 ++++++-- src/mc/explo/odpor/WakeupTree.hpp | 2 ++ src/mc/transition/TransitionSynchro.cpp | 12 +++++-- 7 files changed, 60 insertions(+), 24 deletions(-) diff --git a/src/mc/api/State.cpp b/src/mc/api/State.cpp index b5929f3751..6190f25414 100644 --- a/src/mc/api/State.cpp +++ b/src/mc/api/State.cpp @@ -270,6 +270,11 @@ void State::remove_subtree_using_current_out_transition() wakeup_tree_.remove_min_single_process_subtree(); } + void State::remove_subtree_at_aid(const aid_t proc) { + wakeup_tree_.remove_subtree_at_aid(proc); + + } + odpor::WakeupTree::InsertionResult State::insert_into_wakeup_tree(const odpor::PartialExecution& pe, const odpor::Execution& E) { diff --git a/src/mc/api/State.hpp b/src/mc/api/State.hpp index de11f78e88..3988504ec2 100644 --- a/src/mc/api/State.hpp +++ b/src/mc/api/State.hpp @@ -143,6 +143,7 @@ public: * `N` running actor `p` of this state's wakeup tree */ void remove_subtree_using_current_out_transition(); + void remove_subtree_at_aid(aid_t proc); bool has_empty_tree() const { return this->wakeup_tree_.empty(); } std::string string_of_wut() const { return this->wakeup_tree_.string_of_whole_tree(); } diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp index d279303a5f..ee49e31d9b 100644 --- a/src/mc/explo/DFSExplorer.cpp +++ b/src/mc/explo/DFSExplorer.cpp @@ -136,9 +136,29 @@ void DFSExplorer::run() const aid_t next = reduction_mode_ == ReductionMode::odpor ? state->next_odpor_transition() : std::get<0>(state->next_transition_guided()); - if (next < 0 || not state->is_actor_enabled(next)) { - // If there is no more transition in the current state (or if ODPOR picked an actor that is not enabled -- - // ReversibleRace is an overapproximation), backtrace + if (next < 0) { + // If there is no more transition in the current state ), backtrace + XBT_VERB("%lu actors remain, but none of them need to be interleaved (depth %zu).", state->get_actor_count(), + stack_.size() + 1); + + if (state->get_actor_count() == 0) { + get_remote_app().finalize_app(); + XBT_VERB("Execution came to an end at %s (state: %ld, depth: %zu)", get_record_trace().to_string().c_str(), + state->get_num(), stack_.size()); + } + + this->backtrack(); + continue; + } + if (not state->is_actor_enabled(next)) { + // if ODPOR picked an actor that is not enabled -- ReversibleRace is an overapproximation + xbt_assert(reduction_mode_ == ReductionMode::odpor, + "Only ODPOR should be fool enough to try to execute a disabled transition"); + XBT_VERB("Preventing ODPOR exploration from executing a disabled transition. The reversibility of the race " + "must have been overapproximated"); + + state->remove_subtree_at_aid(next); + state->add_sleep_set(state->get_actors_list().at(next).get_transition()); XBT_VERB("%lu actors remain, but none of them need to be interleaved (depth %zu).", state->get_actor_count(), stack_.size() + 1); @@ -336,11 +356,6 @@ std::shared_ptr DFSExplorer::next_odpor_state() XBT_DEBUG("\tPerformed ODPOR 'clean-up'. Sleep set has:"); for (const auto& [aid, transition] : state->get_sleep_set()) XBT_DEBUG("\t <%ld,%s>", aid, transition->to_string().c_str()); - if (not state->has_empty_tree()) { - XBT_DEBUG("\t found the following non-empty WuT:\n" - "%s", state->string_of_wut().c_str()); - return state; - } } return nullptr; } @@ -358,8 +373,8 @@ void DFSExplorer::backtrack() * ("eventually looks like C", viz. the `~_E` relation) */ for (auto e_prime = static_cast(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: 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()) { diff --git a/src/mc/explo/odpor/ReversibleRaceCalculator.cpp b/src/mc/explo/odpor/ReversibleRaceCalculator.cpp index 7a944a4dd7..d1b7b2a693 100644 --- a/src/mc/explo/odpor/ReversibleRaceCalculator.cpp +++ b/src/mc/explo/odpor/ReversibleRaceCalculator.cpp @@ -153,13 +153,9 @@ bool ReversibleRaceCalculator::is_race_reversible_MutexUnlock(const Execution&, bool ReversibleRaceCalculator::is_race_reversible_MutexWait(const Execution& E, Execution::EventHandle e1, const Transition* /*e2*/) { - // The only possibilities for e1 to satisfy the pre-condition are : - // - MUTEX_ASYNC_LOCK + // TODO: for now we over approximate the reversibility - - const auto e1_action = E.get_transition_for_handle(e1)->type_; - xbt_assert(e1_action == Transition::Type::MUTEX_UNLOCK); - return e1_action != Transition::Type::MUTEX_ASYNC_LOCK && e1_action != Transition::Type::MUTEX_UNLOCK; + return true; } bool ReversibleRaceCalculator::is_race_reversible_SemAsyncLock(const Execution&, Execution::EventHandle /*e1*/, @@ -179,11 +175,13 @@ bool ReversibleRaceCalculator::is_race_reversible_SemUnlock(const Execution&, Ex bool ReversibleRaceCalculator::is_race_reversible_SemWait(const Execution& E, Execution::EventHandle e1, const Transition* /*e2*/) { - // Reversible with everynbody but unlock which creates a free token + const auto e1_transition = E.get_transition_for_handle(e1); if (e1_transition->type_ == Transition::Type::SEM_UNLOCK && - static_cast(e1_transition)->get_capacity() <= 1) + static_cast(e1_transition)->get_capacity() <= 1) { return false; + } + xbt_assert(false, "SEM_WAIT that is dependent with a SEM_UNLOCK should not be reversible. FixMe"); return true; } diff --git a/src/mc/explo/odpor/WakeupTree.cpp b/src/mc/explo/odpor/WakeupTree.cpp index f7e0ea6040..73b2171894 100644 --- a/src/mc/explo/odpor/WakeupTree.cpp +++ b/src/mc/explo/odpor/WakeupTree.cpp @@ -15,7 +15,6 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_wut, mc, "Logging specific to ODPOR WakeupTrees"); - namespace simgrid::mc::odpor { void WakeupTreeNode::add_child(WakeupTreeNode* node) @@ -29,8 +28,9 @@ std::string WakeupTreeNode::string_of_whole_tree(int indentation_level) const std::string tabulations = ""; for (int i = 0; i < indentation_level; i++) tabulations += " "; - std::string final_string = action_ == nullptr ? "<>\n" : - tabulations + "Actor " + std::to_string(action_->aid_) + ": " + action_->to_string(true) + "\n"; + std::string final_string = action_ == nullptr ? "<>\n" + : tabulations + "Actor " + std::to_string(action_->aid_) + ": " + + action_->to_string(true) + "\n"; for (auto node : children_) final_string += node->string_of_whole_tree(indentation_level + 1); return final_string; @@ -159,6 +159,15 @@ void WakeupTree::remove_subtree_rooted_at(WakeupTreeNode* root) } } +void WakeupTree::remove_subtree_at_aid(aid_t proc) +{ + for (const auto& child : root_->get_ordered_children()) + if (child->get_actor() == proc) { + this->remove_subtree_rooted_at(child); + break; + } +} + void WakeupTree::remove_min_single_process_subtree() { if (const auto node = get_min_single_process_node(); node.has_value()) { diff --git a/src/mc/explo/odpor/WakeupTree.hpp b/src/mc/explo/odpor/WakeupTree.hpp index b4502f4951..def2840e0f 100644 --- a/src/mc/explo/odpor/WakeupTree.hpp +++ b/src/mc/explo/odpor/WakeupTree.hpp @@ -169,6 +169,8 @@ public: */ void remove_min_single_process_subtree(); + void remove_subtree_at_aid(aid_t proc); + /** * @brief Whether or not this tree is considered empty * diff --git a/src/mc/transition/TransitionSynchro.cpp b/src/mc/transition/TransitionSynchro.cpp index 469c71cbac..f98a352af3 100644 --- a/src/mc/transition/TransitionSynchro.cpp +++ b/src/mc/transition/TransitionSynchro.cpp @@ -109,10 +109,11 @@ bool MutexTransition::depends(const Transition* o) const std::string SemaphoreTransition::to_string(bool verbose) const { if (type_ == Type::SEM_ASYNC_LOCK || type_ == Type::SEM_UNLOCK) - return xbt::string_printf("%s(semaphore: %u, capacity: %u)", Transition::to_c_str(type_), capacity_, sem_); + return xbt::string_printf("%s(semaphore: %u, capacity: %u)", Transition::to_c_str(type_), sem_, capacity_); if (type_ == Type::SEM_WAIT) - return xbt::string_printf("%s(semaphore: %u, capacity: %u, granted: %s)", Transition::to_c_str(type_), capacity_, - sem_, granted_ ? "yes" : "no"); + return xbt::string_printf("%s(semaphore: %u, capacity: %u, granted: %s)", Transition::to_c_str(type_), sem_, + capacity_, + granted_ ? "yes" : "no"); THROW_IMPOSSIBLE; } SemaphoreTransition::SemaphoreTransition(aid_t issuer, int times_considered, Type type, std::stringstream& stream) @@ -146,6 +147,10 @@ bool SemaphoreTransition::depends(const Transition* o) const if (type_ == Type::SEM_UNLOCK && other->type_ == Type::SEM_UNLOCK) return false; + // UNLCOK indep with a WAIT if the semaphore had enought capacity anyway + if (type_ == Type::SEM_UNLOCK && capacity_ > 1 && other->type_ == Type::SEM_WAIT ) + return false; + // WAIT indep WAIT: // if both enabled (may happen in the initial value is sufficient), the ordering has no impact on the result. // If only one enabled, the other won't be enabled by the first one. @@ -153,6 +158,7 @@ bool SemaphoreTransition::depends(const Transition* o) const if (type_ == Type::SEM_WAIT && other->type_ == Type::SEM_WAIT) return false; + return true; // Other semaphore cases are dependent } -- 2.20.1