From: Maxwell Pirtle Date: Fri, 24 Mar 2023 10:21:13 +0000 (+0100) Subject: Add first steps for ex(C) for CommWait X-Git-Tag: v3.34~153^2~10 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/afbb946d52d6d23ea7c9b83ee6c0ba50ce5d9972 Add first steps for ex(C) for CommWait Computing the extension sets of a `CommWait` action turns out to be a bit more involved than I anticipated. In particular, we must determine whether or not the transition is enabled at some point in the past. This requires us to find the event which created the communication on which the `CommWait` waits and perform a couple checks on that event. The current implementation is not complete and is missing several important steps, but it's a step in the right direction. Additionally, some Sonar errors were fixed. --- diff --git a/src/mc/explo/UdporChecker.cpp b/src/mc/explo/UdporChecker.cpp index 492b808554..15cc3ec9fb 100644 --- a/src/mc/explo/UdporChecker.cpp +++ b/src/mc/explo/UdporChecker.cpp @@ -135,34 +135,6 @@ EventSet UdporChecker::compute_exC(const Configuration& C, const State& stateC, return exC; } -EventSet UdporChecker::compute_exC_by_enumeration(const Configuration& C, const std::shared_ptr action) -{ - // Here we're computing the following: - // - // U{ : K is maximal, `a` depends on all of K, `a` enabled at config(K) } - // - // where `a` is the `action` given to us. Note that `a` is presumed to be enabled - EventSet incremental_exC; - - for (auto begin = - maximal_subsets_iterator(C, {[&](const UnfoldingEvent* e) { return e->is_dependent_with(action.get()); }}); - begin != maximal_subsets_iterator(); ++begin) { - const EventSet& maximal_subset = *begin; - - // Determining if `a` is enabled here might not be possible while looking at `a` opaquely - // We leave the implementation as-is to ensure that any addition would be simple - // if it were ever added - const bool enabled_at_config_k = false; - - if (enabled_at_config_k) { - auto event = std::make_unique(maximal_subset, action); - const auto handle = unfolding.insert(std::move(event)); - incremental_exC.insert(handle); - } - } - return incremental_exC; -} - EventSet UdporChecker::compute_enC(const Configuration& C, const EventSet& exC) const { EventSet enC; @@ -211,7 +183,13 @@ std::unique_ptr UdporChecker::record_current_state() const UnfoldingEvent* UdporChecker::select_next_unfolding_event(const EventSet& A, const EventSet& enC) { - if (!enC.empty()) { + if (enC.empty()) { + throw std::invalid_argument("There are no unfolding events to select. " + "Are you sure that you checked that en(C) was not " + "empty before attempting to select an event from it?"); + } + + if (A.empty()) { return *(enC.begin()); } diff --git a/src/mc/explo/UdporChecker.hpp b/src/mc/explo/UdporChecker.hpp index d7377d1129..6e907a3c13 100644 --- a/src/mc/explo/UdporChecker.hpp +++ b/src/mc/explo/UdporChecker.hpp @@ -108,14 +108,6 @@ private: * @returns the extension set `ex(C)` of `C` */ EventSet compute_exC(const Configuration& C, const State& stateC, const EventSet& prev_exC); - - /** - * @brief Computes a portion of the extension set of a configuration given - * some action `action` by directly enumerating all maximal subsets of C - * (i.e. without specializations based on the action) - */ - EventSet compute_exC_by_enumeration(const Configuration& C, const std::shared_ptr action); - EventSet compute_enC(const Configuration& C, const EventSet& exC) const; /** diff --git a/src/mc/explo/udpor/ExtensionSetCalculator.cpp b/src/mc/explo/udpor/ExtensionSetCalculator.cpp index 757441c74c..704866f3e9 100644 --- a/src/mc/explo/udpor/ExtensionSetCalculator.cpp +++ b/src/mc/explo/udpor/ExtensionSetCalculator.cpp @@ -48,60 +48,142 @@ EventSet ExtensionSetCalculator::partially_extend_CommSend(const Configuration& { EventSet exC; - // TODO: if this is the first action by the actor, no such previous event exists. - // How do we react here? Do we say we're dependent with the root event? const auto send_action = std::static_pointer_cast(std::move(action)); + const auto pre_event_a_C = C.pre_event(send_action->aid_); const unsigned sender_mailbox = send_action->get_mailbox(); - const auto pre_event_a_C = C.pre_event(send_action->aid_).value(); // 1. Create `e' := ` and add `e'` to `ex(C)` - const auto e_prime = U->discover_event(EventSet({pre_event_a_C}), send_action); - exC.insert(e_prime); + // NOTE: If `preEvt(a, C)` doesn't exist, we're effectively asking + // about `config({})` + if (pre_event_a_C.has_value()) { + const auto e_prime = U->discover_event(EventSet({pre_event_a_C.value()}), send_action); + exC.insert(e_prime); + } else { + const auto e_prime = U->discover_event(EventSet(), send_action); + exC.insert(e_prime); + } // 2. foreach e ∈ C s.t. λ(e) ∈ {AsyncSend(m, _), TestAny(Com)} where // Com contains a matching c' = AsyncReceive(m, _) with a for (const auto e : C) { const bool transition_type_check = [&]() { if (const auto* async_send = dynamic_cast(e->get_transition()); - e != nullptr && async_send->get_mailbox() == sender_mailbox) { - return true; - } else if (const auto* e_test_any = dynamic_cast(e->get_transition()); - e_test_any != nullptr) { - // TODO: Check if there's a way to find a matching AsyncReceive -> matching when? in the history? - return true; + async_send != nullptr) { + return async_send->get_mailbox() == sender_mailbox; } + // TODO: Add `TestAny` dependency return false; }(); if (transition_type_check) { - const EventSet K = EventSet({e, pre_event_a_C}).get_largest_maximal_subset(); + const EventSet K = EventSet({e, pre_event_a_C.value_or(e)}).get_largest_maximal_subset(); - // TODO: How do we compute D_K(a, b)? There's a specialized - // function for each case it appears, but I don't see where - // `config(K)` comes in - if (false) { + // TODO: Check D_K(a, lambda(e)) + if (true) { const auto e_prime = U->discover_event(std::move(K), send_action); exC.insert(e_prime); } } } + // TODO: Add `TestAny` dependency case return exC; } EventSet ExtensionSetCalculator::partially_extend_CommRecv(const Configuration& C, Unfolding* U, - const std::shared_ptr recv_action) + const std::shared_ptr action) { - return EventSet(); + EventSet exC; + + // TODO: if this is the first action by the actor, no such previous event exists. + // How do we react here? Do we say we're dependent with the root event? + const auto recv_action = std::static_pointer_cast(std::move(action)); + const unsigned recv_mailbox = recv_action->get_mailbox(); + const auto pre_event_a_C = C.pre_event(recv_action->aid_); + + // 1. Create `e' := ` and add `e'` to `ex(C)` + if (pre_event_a_C.has_value()) { + const auto e_prime = U->discover_event(EventSet({pre_event_a_C.value()}), recv_action); + exC.insert(e_prime); + } else { + const auto e_prime = U->discover_event(EventSet(), recv_action); + exC.insert(e_prime); + } + + // 2. foreach e ∈ C s.t. λ(e) ∈ {AsyncSend(m, _), TestAny(Com)} where + // Com contains a matching c' = AsyncReceive(m, _) with a + for (const auto e : C) { + const bool transition_type_check = [&]() { + if (const auto* async_recv = dynamic_cast(e->get_transition()); + async_recv != nullptr && async_recv->get_mailbox() == recv_mailbox) { + return true; + } + // TODO: Add `TestAny` dependency + return false; + }(); + + if (transition_type_check) { + const EventSet K = EventSet({e, pre_event_a_C.value_or(e)}).get_largest_maximal_subset(); + + // TODO: Check D_K(a, lambda(e)) + if (true) { + const auto e_prime = U->discover_event(std::move(K), recv_action); + exC.insert(e_prime); + } + } + } + + // TODO: Add `TestAny` dependency case + return exC; } -EventSet ExtensionSetCalculator::partially_extend_CommWait(const Configuration&, Unfolding* U, - std::shared_ptr wait_action) +EventSet ExtensionSetCalculator::partially_extend_CommWait(const Configuration& C, Unfolding* U, + std::shared_ptr action) { - return EventSet(); + EventSet exC; + + const auto wait_action = std::static_pointer_cast(std::move(action)); + const auto pre_event_a_C = C.pre_event(wait_action->aid_); + + // 1. if `a` is enabled at state(config({preEvt(a,C)})), then + // create `e' := ` and add `e'` to `ex(C)` + // + // First, if `pre_event_a_C == std::nullopt`, then there is nothing to + // do: `CommWait` will never be enabled in the empty configuration (at + // least two actions must be executed before) + if (pre_event_a_C.has_value(); const auto unwrapped_pre_event = pre_event_a_C.value()) { + + // Determine the _issuer_ of the communication of the `CommWait` event + // in `C`. The issuer of the `CommWait` in `C` is the event in `C` + // whose transition is the `CommRecv` or `CommSend` whose resutling + // communication this `CommWait` waits on + const auto issuer = std::find_if(C.begin(), C.end(), [=](const UnfoldingEvent* e) { return false; }); + xbt_assert(issuer != C.end(), + "Invariant violation! A (supposedly) enabled `CommWait` transition " + "waiting on commiunication %lu should not be enabled: the receive/send " + "transition which generated the communication is not an action taken " + "to reach state(C) (the state of the configuration), which should " + "be an impossibility if `%s` is enabled. Please report this as " + "a bug in SimGrid's UDPOR implementation", + wait_action->get_comm(), wait_action->to_string(false).c_str()); + + // A necessary condition is that the issuer be present in + // config({preEvt(a, C)}); otherwise, the `CommWait` could not + // be enabled since the communication on which it waits would not + // have been created for it! + if (const auto config_pre_event = History(unwrapped_pre_event); config_pre_event.contains(*issuer)) { + // If the issuer is a `CommRecv` (resp. `CommSend`), then we check that there + // are at least as many `CommSend` (resp. `CommRecv`) transitions in `config_pre_event` + // as needed to reach the receive/send number that is `issuer`. + //... + //... + } + } + + return exC; } -EventSet ExtensionSetCalculator::partially_extend_CommTest(const Configuration&, Unfolding* U, +EventSet ExtensionSetCalculator::partially_extend_CommTest(const Configuration& C, Unfolding* U, std::shared_ptr test_action) { return EventSet(); diff --git a/src/mc/explo/udpor/maximal_subsets_iterator.hpp b/src/mc/explo/udpor/maximal_subsets_iterator.hpp index 7d0ab46565..9f6b473091 100644 --- a/src/mc/explo/udpor/maximal_subsets_iterator.hpp +++ b/src/mc/explo/udpor/maximal_subsets_iterator.hpp @@ -38,7 +38,8 @@ public: using node_filter_function = std::function; using topological_order_position = std::vector::const_iterator; - maximal_subsets_iterator() = default; + maximal_subsets_iterator() = default; + maximal_subsets_iterator(maximal_subsets_iterator&&) noexcept = default; explicit maximal_subsets_iterator(const Configuration& config, std::optional filter = std::nullopt, std::optional maximum_subset_size = std::nullopt) @@ -74,6 +75,11 @@ private: public: using topological_order_position = maximal_subsets_iterator::topological_order_position; + bookkeeper() = default; + bookkeeper(bookkeeper&&) = default; + bookkeeper& operator=(bookkeeper&) = default; + bookkeeper& operator=(bookkeeper&&) = default; + void mark_included_in_maximal_set(const UnfoldingEvent*); void mark_removed_from_maximal_set(const UnfoldingEvent*); topological_order_position find_next_candidate_event(topological_order_position first, diff --git a/src/xbt/utils/iter/iterator_wrapping.hpp b/src/xbt/utils/iter/iterator_wrapping.hpp index e865995c86..6e44299e85 100644 --- a/src/xbt/utils/iter/iterator_wrapping.hpp +++ b/src/xbt/utils/iter/iterator_wrapping.hpp @@ -48,7 +48,7 @@ private: friend constexpr iterator_wrapping make_iterator_wrapping_explicit(Arguments... args); public: - iterator_wrapping(Args&&... begin_iteration) : m_args(std::forward>(begin_iteration)...) {} + iterator_wrapping(Args&&... begin_iteration) : m_args(ref_or_value_t(begin_iteration)...) {} iterator_wrapping(const iterator_wrapping&) = delete; iterator_wrapping(iterator_wrapping&&) = delete; iterator_wrapping& operator=(const iterator_wrapping&) = delete; @@ -70,7 +70,7 @@ constexpr iterator_wrapping make_iterator_wrapping(Args&&... template constexpr iterator_wrapping make_iterator_wrapping_explicit(Args... args) { - return iterator_wrapping(std::forward(args)...); + return iterator_wrapping(args...); } } // namespace simgrid::xbt diff --git a/src/xbt/utils/iter/powerset.hpp b/src/xbt/utils/iter/powerset.hpp index 1ce6a93f11..11879a4ea5 100644 --- a/src/xbt/utils/iter/powerset.hpp +++ b/src/xbt/utils/iter/powerset.hpp @@ -29,7 +29,11 @@ namespace simgrid::xbt { template struct powerset_iterator : public boost::iterator_facade, const std::vector, boost::forward_traversal_tag> { - powerset_iterator() = default; + powerset_iterator() = default; + powerset_iterator(powerset_iterator&) noexcept = default; + powerset_iterator(powerset_iterator&&) noexcept = default; + powerset_iterator& operator=(powerset_iterator&&) noexcept = default; + powerset_iterator& operator=(const powerset_iterator&) noexcept = default; explicit powerset_iterator(Iterator begin, Iterator end = Iterator()); private: @@ -75,8 +79,8 @@ template const std::vector& powerset_iterator void powerset_iterator::increment() { - if (!current_subset_iter.has_value() || !current_subset_iter_end.has_value() || - !current_subset_iter.has_value() || !iterator_end.has_value()) { + if (!current_subset_iter.has_value() || !current_subset_iter_end.has_value() || !current_subset_iter.has_value() || + !iterator_end.has_value()) { return; // We've traversed all subsets at this point, or we're the "last" iterator }