From 61a8bb9423361cde6dfc57a00815e5fc99320ca4 Mon Sep 17 00:00:00 2001 From: Maxwell Pirtle Date: Thu, 2 Mar 2023 09:28:34 +0100 Subject: [PATCH] Add first implementation of maximal_subsets_iterator The maximal_subsets_iterator traverses the subsets of events of a configuration `C` which are maximal, viz. those subsets of `C` which are causally-free. --- MANIFEST.in | 2 + src/mc/explo/udpor/Configuration_test.cpp | 2 + src/mc/explo/udpor/UnfoldingEvent.cpp | 6 + src/mc/explo/udpor/UnfoldingEvent.hpp | 2 +- .../explo/udpor/maximal_subsets_iterator.cpp | 116 ++++++++++++++++++ .../explo/udpor/maximal_subsets_iterator.hpp | 105 ++++++++++++++++ tools/cmake/DefinePackages.cmake | 2 + 7 files changed, 234 insertions(+), 1 deletion(-) create mode 100644 src/mc/explo/udpor/maximal_subsets_iterator.cpp create mode 100644 src/mc/explo/udpor/maximal_subsets_iterator.hpp diff --git a/MANIFEST.in b/MANIFEST.in index 97c352873a..add0e16c11 100644 --- a/MANIFEST.in +++ b/MANIFEST.in @@ -2163,6 +2163,8 @@ include src/mc/explo/udpor/EventSet_test.cpp include src/mc/explo/udpor/History.cpp include src/mc/explo/udpor/History.hpp include src/mc/explo/udpor/History_test.cpp +include src/mc/explo/udpor/maximal_subsets_iterator.cpp +include src/mc/explo/udpor/maximal_subsets_iterator.hpp include src/mc/explo/udpor/Unfolding.cpp include src/mc/explo/udpor/Unfolding.hpp include src/mc/explo/udpor/UnfoldingEvent.cpp diff --git a/src/mc/explo/udpor/Configuration_test.cpp b/src/mc/explo/udpor/Configuration_test.cpp index 9a5a756b08..f9d025ea83 100644 --- a/src/mc/explo/udpor/Configuration_test.cpp +++ b/src/mc/explo/udpor/Configuration_test.cpp @@ -358,4 +358,6 @@ TEST_CASE("simgrid::mc::udpor::Configuration: Topological Sort Order Very Compli events_seen.insert(e); }); } + + SECTION("Test that the topological ordering contains only the events of the configuration") {} } \ No newline at end of file diff --git a/src/mc/explo/udpor/UnfoldingEvent.cpp b/src/mc/explo/udpor/UnfoldingEvent.cpp index ee6de7cba1..5ca2229d04 100644 --- a/src/mc/explo/udpor/UnfoldingEvent.cpp +++ b/src/mc/explo/udpor/UnfoldingEvent.cpp @@ -4,6 +4,7 @@ * under the terms of the license (GNU LGPL) which comes with this package. */ #include "src/mc/explo/udpor/UnfoldingEvent.hpp" +#include "src/mc/explo/udpor/History.hpp" namespace simgrid::mc::udpor { @@ -34,4 +35,9 @@ bool UnfoldingEvent::operator==(const UnfoldingEvent& other) const return this->immediate_causes == other.immediate_causes; } +EventSet UnfoldingEvent::get_history() +{ + return History(this).get_all_events(); +} + } // namespace simgrid::mc::udpor diff --git a/src/mc/explo/udpor/UnfoldingEvent.hpp b/src/mc/explo/udpor/UnfoldingEvent.hpp index 4468b210c5..edd7eece88 100644 --- a/src/mc/explo/udpor/UnfoldingEvent.hpp +++ b/src/mc/explo/udpor/UnfoldingEvent.hpp @@ -26,7 +26,7 @@ public: UnfoldingEvent& operator=(UnfoldingEvent const&) = default; UnfoldingEvent(UnfoldingEvent&&) = default; - EventSet get_history() const; + EventSet get_history(); bool in_history_of(const UnfoldingEvent* otherEvent) const; bool conflicts_with(const UnfoldingEvent* otherEvent) const; diff --git a/src/mc/explo/udpor/maximal_subsets_iterator.cpp b/src/mc/explo/udpor/maximal_subsets_iterator.cpp new file mode 100644 index 0000000000..a96287d6d6 --- /dev/null +++ b/src/mc/explo/udpor/maximal_subsets_iterator.cpp @@ -0,0 +1,116 @@ +#include "src/mc/explo/udpor/maximal_subsets_iterator.hpp" +#include "src/mc/explo/udpor/UnfoldingEvent.hpp" +#include "xbt/asserts.h" + +#include + +namespace simgrid::mc::udpor { + +void maximal_subsets_iterator::increment() +{ + // Until we discover otherwise, we default to being done + auto next_event_ref = topological_ordering.end(); + + while (not backtrack_points.empty()) { + // This is an iterator which points to the latest event `e` that + // was added to what is currently the maximal set + const auto latest_event_ref = backtrack_points.top(); + + // Look for the next event to test with what we currently + // have based on the conflicts we've already kept track of. + // + // NOTE: We only need to search FROM `e` and not + // from the beginning of the topological sort. The fact that the + // set is topologically ordered ensures that removing `e` + // will not change whether or not to now allow someone before `e` + // in the ordering (otherwise, they would have to be in `e`'s history + // and therefore would come after `e`) + next_event_ref = bookkeeper.find_next_event(latest_event_ref, topological_ordering.end()); + + // If we can't find another event to add after `e`, + // then we retry after first removing the latest event. + // This effectively tests "check now with all combinations that + // exclude the latest event". + // + // Note: it is important to remove the element FIRST before performing + // the second search, as removal may enable dependencies of `e` to be selected + if (next_event_ref == topological_ordering.end()) { + remove_element_from_current_maximal_set(*latest_event_ref); + backtrack_points.pop(); + + // We begin the search AFTER the event we popped: we only want + // to consider those events that could be added AFTER `e` and + // not `e` itself again + next_event_ref = bookkeeper.find_next_event(latest_event_ref + 1, topological_ordering.end()); + + // If we finally found some event, we can stop + if (next_event_ref != topological_ordering.end()) { + break; + } + } + } + + // If after all of the backtracking we still have no luck, we've finished + if (next_event_ref == topological_ordering.end()) { + return; + } + + // Otherwise we found some other event `e'` which is not in conflict with anything + // that currently exists in `current_maximal_set`. Add it in and perform + // some more bookkeeping + UnfoldingEvent* next_event = *next_event_ref; + add_element_to_current_maximal_set(next_event); + backtrack_points.push(next_event_ref); +} + +void maximal_subsets_iterator::add_element_to_current_maximal_set(UnfoldingEvent* e) +{ + current_maximal_set.insert(e); + bookkeeper.mark_included_in_maximal_set(e); +} + +void maximal_subsets_iterator::remove_element_from_current_maximal_set(UnfoldingEvent* e) +{ + current_maximal_set.remove(e); + bookkeeper.mark_removed_from_maximal_set(e); +} + +maximal_subsets_iterator::topological_order_position +maximal_subsets_iterator::bookkeeper::find_next_event(topological_order_position first, + topological_order_position last) const +{ + return std::find_if(first, last, [&](UnfoldingEvent* e) { return is_candidate_event(e); }); +} + +bool maximal_subsets_iterator::bookkeeper::is_candidate_event(UnfoldingEvent* e) const +{ + if (const auto e_count = event_counts.find(e); e_count != event_counts.end()) { + return e_count->second == 0; + } + return true; +} + +void maximal_subsets_iterator::bookkeeper::mark_included_in_maximal_set(UnfoldingEvent* e) +{ + const auto e_history = e->get_history(); + for (const auto e_hist : e_history) { + event_counts[e_hist]++; + } +} + +void maximal_subsets_iterator::bookkeeper::mark_removed_from_maximal_set(UnfoldingEvent* e) +{ + const auto e_history = e->get_history(); + for (const auto e_hist : e_history) { + xbt_assert(event_counts.find(e_hist) != event_counts.end(), + "Invariant Violation: Attempted to remove an event which was not previously added"); + xbt_assert(event_counts[e_hist] > 0, "Invariant Violation: An event `e` had a count of `0` at this point " + "of the bookkeeping, which means that it is a candidate maximal event. " + "Yet some event that `e'` which contains `e` in its history was removed " + "first. This incidates that the topological sorting of events of the " + "configuration has failed and should be investigated first"); + event_counts[e_hist]--; + } +} + +} // namespace simgrid::mc::udpor \ No newline at end of file diff --git a/src/mc/explo/udpor/maximal_subsets_iterator.hpp b/src/mc/explo/udpor/maximal_subsets_iterator.hpp new file mode 100644 index 0000000000..b51144ec09 --- /dev/null +++ b/src/mc/explo/udpor/maximal_subsets_iterator.hpp @@ -0,0 +1,105 @@ +/* Copyright (c) 2007-2023. The SimGrid Team. All rights reserved. */ + +/* This program is free software; you can redistribute it and/or modify it + * under the terms of the license (GNU LGPL) which comes with this package. */ + +#ifndef SIMGRID_MC_UDPOR_MAXIMAL_SUBSETS_ITERATOR_HPP +#define SIMGRID_MC_UDPOR_MAXIMAL_SUBSETS_ITERATOR_HPP + +#include "src/mc/explo/udpor/Configuration.hpp" + +#include +#include +#include +#include + +namespace simgrid::mc::udpor { + +/** + * @brief An iterator over the tree of sets of maximal events that + * can be generated from a given configuration + * + * This iterator traverses all possible sets of maximal events that + * can be formed from a configuration, each of which satisfy a predicate. + * + * Iteration over the maximal events of a configuration is an important + * step in computing the extension set of a configuration for an action + * whose identity is not "exploitable" (i.e. one whose type information cannot + * help us narrow down our search). + */ +struct maximal_subsets_iterator + : public boost::iterator_facade { +public: + // A function which answers the question "do I need to consider maximal sets + // that contain this node?" + using node_filter_function = std::function; + + maximal_subsets_iterator(); + maximal_subsets_iterator(const Configuration& config) + : maximal_subsets_iterator( + config, [](const UnfoldingEvent*) constexpr { return true; }) + { + } + + maximal_subsets_iterator(const Configuration& config, node_filter_function filter) + : config({config}) + , topological_ordering(config.get_topologically_sorted_events_of_reverse_graph()) + , filter(filter) + { + // The idea here is that initially, no work has been done; but we want + // it to be the case that the iterator points at the very first + // element in the list. Effectively, we want to take the first step + if (not topological_ordering.empty()) { + auto earliest_element_iter = topological_ordering.begin(); + // add_element_to_current_maximal_set(*earliest_element_iter); + backtrack_points.push(earliest_element_iter); + } + } + +private: + using topological_order_position = std::vector::const_iterator; + const std::optional> config; + const std::vector topological_ordering; + const std::optional filter; + + EventSet current_maximal_set = EventSet(); + std::stack backtrack_points; + + /** + * @brief A small class which provides functionality for managing + * the "counts" as the iterator proceeds forward in time + * + * As an instance of the `maximal_subsets_iterator` traverses + * the configuration, it keeps track of how many events + * further down in the causality tree have been signaled as in-conflict + * with events that are its current maximal event set (i.e. + * its `current_maximal_set`) + */ + struct bookkeeper { + private: + using topological_order_position = maximal_subsets_iterator::topological_order_position; + std::unordered_map event_counts; + + bool is_candidate_event(UnfoldingEvent*) const; + + public: + void mark_included_in_maximal_set(UnfoldingEvent*); + void mark_removed_from_maximal_set(UnfoldingEvent*); + + topological_order_position find_next_event(topological_order_position first, topological_order_position last) const; + } bookkeeper; + + void add_element_to_current_maximal_set(UnfoldingEvent*); + void remove_element_from_current_maximal_set(UnfoldingEvent*); + + // boost::iterator_facade<...> interface to implement + void increment(); + bool equal(const maximal_subsets_iterator& other) const { return current_maximal_set == other.current_maximal_set; } + const EventSet& dereference() const { return current_maximal_set; } + + // Allows boost::iterator_facade<...> to function properly + friend class boost::iterator_core_access; +}; + +} // namespace simgrid::mc::udpor +#endif diff --git a/tools/cmake/DefinePackages.cmake b/tools/cmake/DefinePackages.cmake index f420c1cdeb..8e7b1acb09 100644 --- a/tools/cmake/DefinePackages.cmake +++ b/tools/cmake/DefinePackages.cmake @@ -533,6 +533,8 @@ set(MC_SRC src/mc/explo/udpor/EventSet.hpp src/mc/explo/udpor/History.cpp src/mc/explo/udpor/History.hpp + src/mc/explo/udpor/maximal_subsets_iterator.cpp + src/mc/explo/udpor/maximal_subsets_iterator.hpp src/mc/explo/udpor/UnfoldingEvent.cpp src/mc/explo/udpor/UnfoldingEvent.hpp src/mc/explo/udpor/Unfolding.cpp -- 2.20.1