From: mlaurent Date: Thu, 9 Nov 2023 09:34:39 +0000 (+0100) Subject: Merge branch 'master' of https://framagit.org/simgrid/simgrid X-Git-Tag: v3.35~83 X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/9fc682676a33abb6a4cc527c09a34db3c33e5711?hp=d259b3370ea354bf2a4fb3e292a086b7a2f52ff7 Merge branch 'master' of https://framagit.org/simgrid/simgrid --- diff --git a/src/mc/api/State.cpp b/src/mc/api/State.cpp index afd89041ba..6190f25414 100644 --- a/src/mc/api/State.cpp +++ b/src/mc/api/State.cpp @@ -25,7 +25,6 @@ State::State(RemoteApp& remote_app) : num_(++expended_states_) { XBT_VERB("Creating a guide for the state"); - if (_sg_mc_strategy == "none") strategy_ = std::make_shared(); else if (_sg_mc_strategy == "max_match_comm") @@ -33,10 +32,9 @@ State::State(RemoteApp& remote_app) : num_(++expended_states_) else if (_sg_mc_strategy == "min_match_comm") strategy_ = std::make_shared(); else if (_sg_mc_strategy == "uniform") { - xbt::random::set_mersenne_seed(_sg_mc_random_seed); + xbt::random::set_mersenne_seed(_sg_mc_random_seed); strategy_ = std::make_shared(); - } - else + } else THROW_IMPOSSIBLE; remote_app.get_actors_status(strategy_->actors_to_run_); @@ -51,7 +49,7 @@ State::State(RemoteApp& remote_app, std::shared_ptr parent_state) strategy_ = std::make_shared(); else if (_sg_mc_strategy == "min_match_comm") strategy_ = std::make_shared(); - else if (_sg_mc_strategy == "uniform") + else if (_sg_mc_strategy == "uniform") strategy_ = std::make_shared(); else THROW_IMPOSSIBLE; @@ -201,6 +199,9 @@ void State::seed_wakeup_tree_if_needed(const odpor::Execution& prior) { // TODO: It would be better not to have such a flag. if (has_initialized_wakeup_tree) { + XBT_DEBUG("Reached a node with the following initialized WuT:"); + XBT_DEBUG("\n%s", wakeup_tree_.string_of_whole_tree().c_str()); + return; } // TODO: Note that the next action taken by the actor may be updated @@ -225,6 +226,11 @@ void State::seed_wakeup_tree_if_needed(const odpor::Execution& prior) void State::sprout_tree_from_parent_state() { + + XBT_DEBUG("Initializing Wut with parent one:"); + XBT_DEBUG("\n%s", parent_state_->wakeup_tree_.string_of_whole_tree().c_str()); + + xbt_assert(parent_state_ != nullptr, "Attempting to construct a wakeup tree for the root state " "(or what appears to be, rather for state without a parent defined)"); const auto min_process_node = parent_state_->wakeup_tree_.get_min_single_process_node(); @@ -264,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 ca77b513a7..3988504ec2 100644 --- a/src/mc/api/State.hpp +++ b/src/mc/api/State.hpp @@ -143,8 +143,11 @@ 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(); } + /** * @brief */ diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp index a7c9dcf021..8d85325ef7 100644 --- a/src/mc/explo/DFSExplorer.cpp +++ b/src/mc/explo/DFSExplorer.cpp @@ -83,7 +83,7 @@ void DFSExplorer::log_state() // override XBT_INFO("DFS exploration ended. %ld unique states visited; %lu backtracks (%lu transition replays, %lu states " "visited overall)", State::get_expanded_states(), backtrack_count_, Transition::get_replayed_transitions(), - visited_states_count_); + visited_states_count_); Exploration::log_state(); } @@ -138,6 +138,7 @@ 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 (next >= 0) { // Actor is not enabled, then XBT_INFO("Reduction %s wants to execute a disabled transition %s. If it's ODPOR, ReversibleRace is suboptimal.", @@ -147,6 +148,9 @@ void DFSExplorer::run() XBT_INFO("Current trace:"); for (auto elm : get_textual_trace()) XBT_ERROR("%s", elm.c_str()); + // Remove the disabled transition from the wakeup tree so that ODPOR doesn't try it again + state->remove_subtree_at_aid(next); + state->add_sleep_set(state->get_actors_list().at(next).get_transition()); } } // If there is no more transition in the current state (or if ODPOR picked an actor that is not enabled -- @@ -348,9 +352,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()) { - return state; - } } return nullptr; } @@ -368,15 +369,19 @@ 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: 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` unaccounted for in the wakeup tree for " - "the execution prior to event `%u`:", - e_prime, e); + 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: { diff --git a/src/mc/explo/odpor/Execution.cpp b/src/mc/explo/odpor/Execution.cpp index 162425d2f4..536c3f05a6 100644 --- a/src/mc/explo/odpor/Execution.cpp +++ b/src/mc/explo/odpor/Execution.cpp @@ -12,6 +12,8 @@ #include #include +XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_odpor_execution, mc_dfs, "ODPOR exploration algorithm of the model-checker"); + namespace simgrid::mc::odpor { std::vector get_textual_trace(const PartialExecution& w) @@ -64,18 +66,22 @@ std::vector Execution::get_textual_trace() const std::unordered_set Execution::get_racing_events_of(Execution::EventHandle target) const { std::unordered_set racing_events; + // This keep tracks of events that happens-before the target std::unordered_set disqualified_events; // For each event of the execution for (auto e_i = target; e_i != std::numeric_limits::max(); e_i--) { // We need `e_i -->_E target` as a necessary condition if (not happens_before(e_i, target)) { + XBT_DEBUG("ODPOR_RACING_EVENTS with `%u` : `%u` discarded because `%u` --\\-->_E `%u`", target, e_i, e_i, target); continue; } // Further, `proc(e_i) != proc(target)` if (get_actor_with_handle(e_i) == get_actor_with_handle(target)) { disqualified_events.insert(e_i); + XBT_DEBUG("ODPOR_RACING_EVENTS with `%u` : `%u` disqualified because proc(`%u`)=proc(`%u`)", target, e_i, e_i, + target); continue; } @@ -87,6 +93,8 @@ std::unordered_set Execution::get_racing_events_of(Execu // then e_i --->_E target indirectly (either through // e_j directly, or transitively through e_j) if (disqualified_events.count(e_j) > 0 && happens_before(e_i, e_j)) { + XBT_DEBUG("ODPOR_RACING_EVENTS with `%u` : `%u` disqualified because `%u` happens-between `%u`-->`%u`-->`%u`)", + target, e_i, e_j, e_i, e_j, target); disqualified_events.insert(e_i); break; } @@ -98,6 +106,8 @@ std::unordered_set Execution::get_racing_events_of(Execu // it (since this would transitively make it the event // which "happens-between" `target` and `e`) if (disqualified_events.count(e_i) == 0) { + XBT_DEBUG("ODPOR_RACING_EVENTS with `%u` : `%u` is a valid racing event", + target, e_i); racing_events.insert(e_i); disqualified_events.insert(e_i); } diff --git a/src/mc/explo/odpor/ReversibleRaceCalculator.cpp b/src/mc/explo/odpor/ReversibleRaceCalculator.cpp index f449d6a363..d1b7b2a693 100644 --- a/src/mc/explo/odpor/ReversibleRaceCalculator.cpp +++ b/src/mc/explo/odpor/ReversibleRaceCalculator.cpp @@ -13,8 +13,18 @@ #include #include +XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_odpor_reversible_race, mc_dfs, "ODPOR exploration algorithm of the model-checker"); + namespace simgrid::mc::odpor { +/** + The reversible race detector should only be used if we already have the assumption + e1 <* e2 (see Source set: a foundation for ODPOR). In particular this means that : + - e1 -->_E e2 + - proc(e1) != proc(e2) + - there is no event e3 s.t. e1 --> e3 --> e2 +*/ + bool ReversibleRaceCalculator::is_race_reversible(const Execution& E, Execution::EventHandle e1, Execution::EventHandle e2) { @@ -143,9 +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*/) { - // TODO: Get the semantics correct here - const auto e1_action = E.get_transition_for_handle(e1)->type_; - return e1_action != Transition::Type::MUTEX_ASYNC_LOCK && e1_action != Transition::Type::MUTEX_UNLOCK; + // TODO: for now we over approximate the reversibility + + return true; } bool ReversibleRaceCalculator::is_race_reversible_SemAsyncLock(const Execution&, Execution::EventHandle /*e1*/, @@ -165,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 27d914a1f0..73b2171894 100644 --- a/src/mc/explo/odpor/WakeupTree.cpp +++ b/src/mc/explo/odpor/WakeupTree.cpp @@ -13,6 +13,8 @@ #include #include +XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_wut, mc, "Logging specific to ODPOR WakeupTrees"); + namespace simgrid::mc::odpor { void WakeupTreeNode::add_child(WakeupTreeNode* node) @@ -21,6 +23,19 @@ void WakeupTreeNode::add_child(WakeupTreeNode* node) node->parent_ = this; } +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"; + for (auto node : children_) + final_string += node->string_of_whole_tree(indentation_level + 1); + return final_string; +} + PartialExecution WakeupTreeNode::get_sequence() const { // TODO: Prevent having to compute this at the node level @@ -85,6 +100,11 @@ std::optional WakeupTree::get_min_single_process_node() const return this->root_->children_.front(); } +std::string WakeupTree::string_of_whole_tree() const +{ + return root_->string_of_whole_tree(0); +} + WakeupTree WakeupTree::make_subtree_rooted_at(WakeupTreeNode* root) { // Perform a BFS search to perform a deep copy of the portion @@ -139,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 8247a913b3..def2840e0f 100644 --- a/src/mc/explo/odpor/WakeupTree.hpp +++ b/src/mc/explo/odpor/WakeupTree.hpp @@ -72,6 +72,8 @@ public: std::shared_ptr get_action() const { return action_; } const std::list& get_ordered_children() const { return children_; } + std::string string_of_whole_tree(int indentation_level) const; + /** Insert a node `node` as a new child of this node */ void add_child(WakeupTreeNode* node); }; @@ -152,6 +154,8 @@ public: std::vector get_single_process_texts() const; + std::string string_of_whole_tree() const; + /** * @brief Remove the subtree of the smallest (with respect * to the tree's "<" relation) single-process node. @@ -165,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/TransitionAny.cpp b/src/mc/transition/TransitionAny.cpp index 3ea33cca38..48e061730c 100644 --- a/src/mc/transition/TransitionAny.cpp +++ b/src/mc/transition/TransitionAny.cpp @@ -59,7 +59,7 @@ std::string WaitAnyTransition::to_string(bool verbose) const auto res = xbt::string_printf("WaitAny{ "); for (auto const* t : transitions_) res += t->to_string(verbose); - res += " }"; + res += " } (times considered = " + std::to_string(times_considered_) + ")"; return res; } bool WaitAnyTransition::depends(const Transition* other) const 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 }