From: mlaurent Date: Wed, 8 Nov 2023 17:56:03 +0000 (+0100) Subject: Merge branch 'master' of https://framagit.org/simgrid/simgrid X-Git-Tag: v3.35~86 X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/861f43e45a240e3568c7db636d36d05ed3f70665?hp=3e9e2c3010b77637029ad9d6503de5ddccb38daa 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..b5929f3751 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(); diff --git a/src/mc/api/State.hpp b/src/mc/api/State.hpp index ca77b513a7..de11f78e88 100644 --- a/src/mc/api/State.hpp +++ b/src/mc/api/State.hpp @@ -144,7 +144,9 @@ public: */ void remove_subtree_using_current_out_transition(); 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 0fb95fd182..d279303a5f 100644 --- a/src/mc/explo/DFSExplorer.cpp +++ b/src/mc/explo/DFSExplorer.cpp @@ -81,7 +81,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(); } @@ -337,6 +337,8 @@ std::shared_ptr DFSExplorer::next_odpor_state() 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; } } @@ -356,15 +358,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) { - 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()) { 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..8b531ff7b0 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,9 @@ 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); + disqualified_events.insert(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..7a944a4dd7 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,8 +153,12 @@ 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 + // The only possibilities for e1 to satisfy the pre-condition are : + // - MUTEX_ASYNC_LOCK + + 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; } diff --git a/src/mc/explo/odpor/WakeupTree.cpp b/src/mc/explo/odpor/WakeupTree.cpp index 27d914a1f0..f7e0ea6040 100644 --- a/src/mc/explo/odpor/WakeupTree.cpp +++ b/src/mc/explo/odpor/WakeupTree.cpp @@ -13,6 +13,9 @@ #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 +24,18 @@ 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 diff --git a/src/mc/explo/odpor/WakeupTree.hpp b/src/mc/explo/odpor/WakeupTree.hpp index 8247a913b3..b4502f4951 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. 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