From: Maxwell Pirtle Date: Thu, 25 May 2023 08:25:07 +0000 (+0200) Subject: Fix two minor bugs in the ODPOR implementation X-Git-Tag: v3.34~68^2~15 X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/9513f2fee2b19db92ef287098fa7707d30cdce84 Fix two minor bugs in the ODPOR implementation This commit fixes the following two bugs: 1. When seeding a wakeup tree for the first time, we forgot to add a `break` statement to ensure that only one such enabled thread were placed into the wakeup tree. Before all such enabled threads were inserted which amounted to what would have been a brute-force search :(. 2. When determining whether a sequence is a candidate for insertion into a wakeup tree, we may need to check, for all enabled actors in a given state, whether those actors' next steps are independent with the sequence theretofore constructed. This additional step peforms the work needed to check whether those actors are contained in the set of *weak* initials. The method corresponds to line 6 of the pseudocode of the ODPOR algorithm --- diff --git a/src/mc/api/State.cpp b/src/mc/api/State.cpp index 1680ca07cf..c8059b5fe5 100644 --- a/src/mc/api/State.cpp +++ b/src/mc/api/State.cpp @@ -220,6 +220,7 @@ void State::seed_wakeup_tree_if_needed(const odpor::Execution& prior) for (unsigned times = 0; times < actor.get_max_considered(); ++times) { wakeup_tree_.insert(prior, odpor::PartialExecution{actor.get_transition(times)}); } + break; // Only one actor gets inserted (see pseudocode) } } } @@ -235,26 +236,31 @@ void State::sprout_tree_from_parent_state() "parent with an empty wakeup tree. This indicates either that ODPOR " "actor selection in State.cpp is incorrect, or that the code " "deciding when to make subtrees in ODPOR is incorrect"); - - // TODO: This assert should even be bolstered to check that the - // the transitions themselves are identical -- not only just - // that the actors are the same. When we have to consider - // multiple paths for a transition, things get trickier - xbt_assert(parent_state_->get_transition_out()->aid_ == min_process_node.value()->get_actor(), - "We tried to make a subtree from a parent state who claimed to have executed %ld " - "but whose wakeup tree indicates it should have executed %ld. This indicates " + xbt_assert((parent_state_->get_transition_out()->aid_ == min_process_node.value()->get_actor()) && + (parent_state_->get_transition_out()->type_ == min_process_node.value()->get_action()->type_), + "We tried to make a subtree from a parent state who claimed to have executed `%s` " + "but whose wakeup tree indicates it should have executed `%s`. This indicates " "that exploration is not following ODPOR. Are you sure you're choosing actors " "to schedule from the wakeup tree?", - parent_state_->get_transition_out()->aid_, min_process_node.value()->get_actor()); + parent_state_->get_transition_out()->to_string(false).c_str(), + min_process_node.value()->get_action()->to_string(false).c_str()); this->wakeup_tree_ = odpor::WakeupTree::make_subtree_rooted_at(min_process_node.value()); } void State::remove_subtree_using_current_out_transition() { if (auto out_transition = get_transition_out(); out_transition != nullptr) { - // TODO: Add invariant check here + if (const auto min_process_node = wakeup_tree_.get_min_single_process_node(); min_process_node.has_value()) { + xbt_assert((out_transition->aid_ == min_process_node.value()->get_actor()) && + (out_transition->type_ == min_process_node.value()->get_action()->type_), + "We tried to make a subtree from a parent state who claimed to have executed `%s` " + "but whose wakeup tree indicates it should have executed `%s`. This indicates " + "that exploration is not following ODPOR. Are you sure you're choosing actors " + "to schedule from the wakeup tree?", + out_transition->to_string(false).c_str(), + min_process_node.value()->get_action()->to_string(false).c_str()); + } } - wakeup_tree_.remove_min_single_process_subtree(); } diff --git a/src/mc/api/State.hpp b/src/mc/api/State.hpp index a015de9fef..7f0290baa1 100644 --- a/src/mc/api/State.hpp +++ b/src/mc/api/State.hpp @@ -122,6 +122,11 @@ public: { sleep_set_.insert_or_assign(t->aid_, Transition(t->type_, t->aid_, t->times_considered_)); } + bool is_actor_sleeping(aid_t actor) const + { + return std::find_if(sleep_set_.begin(), sleep_set_.end(), [=](const auto& pair) { return pair.first == actor; }) != + sleep_set_.end(); + } /** * @brief Inserts an arbitrary enabled actor into the wakeup tree diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp index cdc31dfc28..af2d8ba442 100644 --- a/src/mc/explo/DFSExplorer.cpp +++ b/src/mc/explo/DFSExplorer.cpp @@ -186,6 +186,11 @@ void DFSExplorer::run() // in case we want to consider multiple states (eg. during backtrack) const aid_t next = reduction_mode_ == ReductionMode::odpor ? state->next_odpor_transition() : std::get<0>(state->next_transition_guided()); + xbt_assert(!state->is_actor_sleeping(next), + "We decided to schedule an actor (%ld) that is in the sleep set " + "of the current state. By definition, this should be impossible; " + "and yet it happened, somehow...", + next); if (next < 0) { // If there is no more transition in the current state, backtrack. XBT_VERB("%lu actors remain, but none of them need to be interleaved (depth %zu).", state->get_actor_count(), diff --git a/src/mc/explo/odpor/Execution.cpp b/src/mc/explo/odpor/Execution.cpp index 6b84b0f861..3aa3df602b 100644 --- a/src/mc/explo/odpor/Execution.cpp +++ b/src/mc/explo/odpor/Execution.cpp @@ -53,7 +53,7 @@ std::unordered_set Execution::get_racing_events_of(Execu // 2. disqualified_events.count(e_j) > 0 // then e_i --->_E target indirectly (either through // e_j directly, or transitively through e_j) - if (happens_before(e_i, e_j) and disqualified_events.count(e_j) > 0) { + if (disqualified_events.count(e_j) > 0 and happens_before(e_i, e_j)) { disqualified_events.insert(e_i); break; } @@ -283,7 +283,8 @@ std::optional Execution::get_odpor_extension_from(EventHandle for (const auto& [aid, astate] : state_at_e.get_actors_list()) { // TODO: We have to be able to react appropriately here when adding new // types of transitions (multiple choices can be made :( ) - if (sleeping_actors.count(aid) == 0 and pre_E_e.is_independent_with_execution_of(v, astate.get_transition(0))) { + if (astate.is_enabled() and sleeping_actors.count(aid) == 0 and + pre_E_e.is_independent_with_execution_of(v, astate.get_transition(0))) { return v; } }