D.insert(e);
constexpr unsigned K = 10;
- if (auto J_minus_C = compute_k_partial_alternative(D, C, K); J_minus_C.has_value()) {
+ if (auto J = C.compute_k_partial_alternative_to(D, this->unfolding, K); J.has_value()) {
+
// Before searching the "right half", we need to make
// sure the program actually reflects the fact
// that we are searching again from `stateC` (the recursive
restore_program_state_to(*stateC);
// Explore(C, D + {e}, J \ C)
- explore(C, D, std::move(J_minus_C.value()), std::move(stateC), std::move(prev_exC));
+ auto J_minus_C = J.value().get_events().subtracting(C.get_events());
+ explore(C, D, std::move(J_minus_C), std::move(stateC), std::move(prev_exC));
}
// D <-- D - {e}
return nullptr;
}
-std::vector<const UnfoldingEvent*> UdporChecker::pick_k_partial_alternative_events(const EventSet& D,
- const unsigned k) const
-{
- const unsigned size = std::min(k, static_cast<unsigned>(D.size()));
- std::vector<const UnfoldingEvent*> D_hat(size);
-
- // Potentially select intelligently here (e.g. perhaps pick events
- // with transitions that we know are totally independent)...
- //
- // For now, simply pick the first `k` events (any subset suffices)
- std::copy_n(D.begin(), size, D_hat.begin());
- return D_hat;
-}
-
-std::optional<EventSet> UdporChecker::compute_k_partial_alternative(const EventSet& D, const Configuration& C,
- const unsigned k) const
-{
- // 1. Select k (of |D|, whichever is smaller) arbitrary events e_1, ..., e_k from D
- const auto D_hat = pick_k_partial_alternative_events(D, k);
-
- // 2. Build a U-comb <s_1, ..., s_k> of size k, where spike `s_i` contains
- // all events in conflict with `e_i`
- //
- // 3. EXCEPT those events e' for which [e'] + C is not a configuration or
- // [e'] intersects D
- //
- // NOTE: This is an expensive operation as we must traverse the entire unfolding
- // and compute `C.is_compatible_with(History)` for every event in the structure :/.
- // A later performance improvement would be to incorporate the work of Nguyen et al.
- // into SimGrid. Since that is a rather complicated addition, we defer to the addition
- // for a later time...
- Comb comb(k);
-
- for (const auto* e : this->unfolding) {
- for (unsigned i = 0; i < k; i++) {
- const auto& e_i = D_hat[i];
- if (const auto e_local_config = History(e);
- e_i->conflicts_with(e) and (not D.contains(e_local_config)) and C.is_compatible_with(e_local_config)) {
- comb[i].push_back(e);
- }
- }
- }
-
- // 4. Find any such combination <e_1', ..., e_k'> in comb satisfying
- // ~(e_i' # e_j') for i != j
- //
- // NOTE: This is a VERY expensive operation: it enumerates all possible
- // ways to select an element from each spike. Unfortunately there's no
- // way around the enumeration, as computing a full alternative in general is
- // NP-complete (although computing the k-partial alternative is polynomial in n)
- const auto map_events = [](const std::vector<Spike::const_iterator>& spikes) {
- std::vector<const UnfoldingEvent*> events;
- for (const auto& event_in_spike : spikes) {
- events.push_back(*event_in_spike);
- }
- return EventSet(std::move(events));
- };
- const auto alternative =
- std::find_if(comb.combinations_begin(), comb.combinations_end(),
- [&map_events](const auto& vector) { return map_events(vector).is_conflict_free(); });
-
- // No such alternative exists
- if (alternative == comb.combinations_end()) {
- return std::nullopt;
- }
-
- // 5. J := [e_1] + [e_2] + ... + [e_k] is a k-partial alternative
- // NOTE: This function computes J / C, which is what is actually used in UDPOR
- return History(map_events(*alternative)).get_event_diff_with(C);
-}
-
void UdporChecker::clean_up_explore(const UnfoldingEvent* e, const Configuration& C, const EventSet& D)
{
const EventSet C_union_D = C.get_events().make_union(D);
EventSet compute_enC(const Configuration& C, const EventSet& exC) const;
- std::optional<EventSet> compute_k_partial_alternative(const EventSet& D, const Configuration& C,
- const unsigned k) const;
- std::vector<const UnfoldingEvent*> pick_k_partial_alternative_events(const EventSet& D, const unsigned k) const;
-
/**
*
*/
namespace simgrid::mc::udpor {
-class Spike : public std::vector<const UnfoldingEvent*> {
-public:
- Spike(unsigned cap) : std::vector<const UnfoldingEvent*>() { reserve(cap); }
-};
+using Spike = std::vector<const UnfoldingEvent*>;
class Comb {
public:
- explicit Comb(unsigned k) : k(k) {}
+ explicit Comb(unsigned k) : k(k), spikes(k) {}
Comb(const Comb& other) = default;
Comb(Comb&& other) = default;
Comb& operator=(const Comb& other) = default;
* under the terms of the license (GNU LGPL) which comes with this package. */
#include "src/mc/explo/udpor/Configuration.hpp"
+#include "src/mc/explo/udpor/Comb.hpp"
#include "src/mc/explo/udpor/History.hpp"
+#include "src/mc/explo/udpor/Unfolding.hpp"
#include "src/mc/explo/udpor/UnfoldingEvent.hpp"
#include "src/mc/explo/udpor/maximal_subsets_iterator.hpp"
#include "xbt/asserts.h"
}
}
+Configuration::Configuration(const History& history) : Configuration(history.get_all_events()) {}
+
void Configuration::add_event(const UnfoldingEvent* e)
{
if (e == nullptr) {
}
}
+bool Configuration::is_compatible_with(const UnfoldingEvent* e) const
+{
+ return not e->conflicts_with(*this);
+}
+
bool Configuration::is_compatible_with(const History& history) const
{
return std::none_of(history.begin(), history.end(),
return minimally_reproducible_events;
}
+std::optional<Configuration> Configuration::compute_alternative_to(const EventSet& D, const Unfolding& U) const
+{
+ // A full alternative can be computed by checking against everything in D
+ return compute_k_partial_alternative_to(D, U, D.size());
+}
+
+std::optional<Configuration> Configuration::compute_k_partial_alternative_to(const EventSet& D, const Unfolding& U,
+ size_t k) const
+{
+ // 1. Select k (of |D|, whichever is smaller) arbitrary events e_1, ..., e_k from D
+ const auto D_hat = [&]() {
+ const size_t size = std::min(k, D.size());
+ std::vector<const UnfoldingEvent*> D_hat(size);
+ // Potentially select intelligently here (e.g. perhaps pick events
+ // with transitions that we know are totally independent)...
+ //
+ // For now, simply pick the first `k` events (any subset suffices)
+ std::copy_n(D.begin(), size, D_hat.begin());
+ return D_hat;
+ }();
+
+ // 2. Build a U-comb <s_1, ..., s_k> of size k, where spike `s_i` contains
+ // all events in conflict with `e_i`
+ //
+ // 3. EXCEPT those events e' for which [e'] + C is not a configuration or
+ // [e'] intersects D
+ //
+ // NOTE: This is an expensive operation as we must traverse the entire unfolding
+ // and compute `C.is_compatible_with(History)` for every event in the structure :/.
+ // A later performance improvement would be to incorporate the work of Nguyen et al.
+ // into SimGrid. Since that is a rather complicated addition, we defer to the addition
+ // for a later time...
+ Comb comb(k);
+
+ for (const auto* e : U) {
+ for (unsigned i = 0; i < k; i++) {
+ const UnfoldingEvent* e_i = D_hat[i];
+ if (const auto e_local_config = History(e);
+ e_i->conflicts_with(e) and (not D.contains(e_local_config)) and is_compatible_with(e_local_config)) {
+ comb[i].push_back(e);
+ }
+ }
+ }
+
+ // 4. Find any such combination <e_1', ..., e_k'> in comb satisfying
+ // ~(e_i' # e_j') for i != j
+ //
+ // NOTE: This is a VERY expensive operation: it enumerates all possible
+ // ways to select an element from each spike. Unfortunately there's no
+ // way around the enumeration, as computing a full alternative in general is
+ // NP-complete (although computing the k-partial alternative is polynomial in n)
+ const auto map_events = [](const std::vector<Spike::const_iterator>& spikes) {
+ std::vector<const UnfoldingEvent*> events;
+ for (const auto& event_in_spike : spikes) {
+ events.push_back(*event_in_spike);
+ }
+ return EventSet(std::move(events));
+ };
+ const auto alternative =
+ std::find_if(comb.combinations_begin(), comb.combinations_end(),
+ [&map_events](const auto& vector) { return map_events(vector).is_conflict_free(); });
+
+ // No such alternative exists
+ if (alternative == comb.combinations_end()) {
+ return std::nullopt;
+ }
+
+ // 5. J := [e_1] + [e_2] + ... + [e_k] is a k-partial alternative
+ return Configuration(History(map_events(*alternative)));
+}
+
} // namespace simgrid::mc::udpor
#include "src/mc/explo/udpor/EventSet.hpp"
#include "src/mc/explo/udpor/udpor_forward.hpp"
+#include <optional>
+
namespace simgrid::mc::udpor {
class Configuration {
explicit Configuration(const UnfoldingEvent* event);
explicit Configuration(const EventSet& events);
+ explicit Configuration(const History& history);
explicit Configuration(std::initializer_list<const UnfoldingEvent*> events);
auto begin() const { return this->events_.begin(); }
*/
void add_event(const UnfoldingEvent* e);
+ /**
+ * @brief Whether or not the given event can be added to
+ * this configuration while keeping the set of events causally closed
+ * and conflict-free
+ */
bool is_compatible_with(const UnfoldingEvent* e) const;
/**
- * @brief Whether or not the events in the given history
- * could be added to this configuration while preserving
- * the configuration property
+ * @brief Whether or not the events in the given history can be added to
+ * this configuration while keeping the set of events causally closed
+ * and conflict-free
*/
bool is_compatible_with(const History& history) const;
+ std::optional<Configuration> compute_alternative_to(const EventSet& D, const Unfolding& U) const;
+ std::optional<Configuration> compute_k_partial_alternative_to(const EventSet& D, const Unfolding& U, size_t k) const;
+
/**
* @brief Orders the events of the configuration such that
* "more recent" events (i.e. those that are farther down in
* of the events returned by this method is equal to the set of events
* in this configuration
*
- * @returns the smallest set of events whose events generates this configuration
- * (denoted `config(E)`)
+ * @returns the smallest set of events whose events generates
+ * this configuration (denoted `config(E)`)
*/
EventSet get_minimally_reproducible_events() const;
#include "src/mc/explo/udpor/Configuration.hpp"
#include "src/mc/explo/udpor/EventSet.hpp"
#include "src/mc/explo/udpor/History.hpp"
+#include "src/mc/explo/udpor/Unfolding.hpp"
#include "src/mc/explo/udpor/UnfoldingEvent.hpp"
#include "src/mc/explo/udpor/maximal_subsets_iterator.hpp"
#include "src/mc/explo/udpor/udpor_tests_private.hpp"
// Iteration with events directly should now also be finished
REQUIRE(first_events == last);
}
+}
+
+TEST_CASE("simgrid::mc::udpor:Configuration: Computing Full Alternatives in Reader/Writer Example")
+{
+ // The following tests concern the given event structure that is given as
+ // an example in figure 1 of the original UDPOR paper.
+ // e0
+ // / / /
+ // e1 e4 e7
+ // / / // /
+ // / / e5 e8 e9
+ // e2 e3 / /
+ // e6 e10
+ //
+ // Theses tests walk through exactly the configurations and sets of `D` that
+ // UDPOR should encounter as it walks the unfolding.
+ Unfolding U;
+
+ auto e0 = std::make_unique<UnfoldingEvent>(EventSet(), std::make_shared<ConditionallyDependentAction>());
+ auto e0_handle = e0.get();
+
+ auto e1 = std::make_unique<UnfoldingEvent>(EventSet({e0_handle}), std::make_shared<DependentAction>());
+ auto e1_handle = e1.get();
+
+ auto e2 = std::make_unique<UnfoldingEvent>(EventSet({e1_handle}), std::make_shared<ConditionallyDependentAction>());
+ auto e2_handle = e2.get();
+
+ auto e3 = std::make_unique<UnfoldingEvent>(EventSet({e1_handle}), std::make_shared<ConditionallyDependentAction>());
+ // auto e3_handle = e3.get();
+
+ auto e4 = std::make_unique<UnfoldingEvent>(EventSet({e0_handle}), std::make_shared<ConditionallyDependentAction>());
+ auto e4_handle = e4.get();
+
+ auto e5 = std::make_unique<UnfoldingEvent>(EventSet({e4_handle}), std::make_shared<DependentAction>());
+ auto e5_handle = e5.get();
+
+ auto e6 = std::make_unique<UnfoldingEvent>(EventSet({e5_handle}), std::make_shared<ConditionallyDependentAction>());
+
+ auto e7 = std::make_unique<UnfoldingEvent>(EventSet({e0_handle}), std::make_shared<ConditionallyDependentAction>());
+ auto e7_handle = e7.get();
+
+ auto e8 = std::make_unique<UnfoldingEvent>(EventSet({e4_handle, e7_handle}), std::make_shared<DependentAction>());
+
+ auto e9 = std::make_unique<UnfoldingEvent>(EventSet({e7_handle}), std::make_shared<ConditionallyDependentAction>());
+ auto e9_handle = e9.get();
+
+ auto e10 = std::make_unique<UnfoldingEvent>(EventSet({e9_handle}), std::make_shared<ConditionallyDependentAction>());
+
+ SECTION("Alternative computation step 1")
+ {
+ const EventSet D;
+ const Configuration C{e0_handle, e1_handle, e2_handle};
+
+ REQUIRE(U.empty());
+ U.insert(std::move(e0));
+ U.insert(std::move(e1));
+ U.insert(std::move(e2));
+ U.insert(std::move(e3));
+ U.insert(std::move(e4));
+ U.insert(std::move(e7));
+
+ const auto alternative = C.compute_alternative_to(D, U);
+ REQUIRE_FALSE(alternative.has_value());
+ }
+
+ SECTION("Alternative computation step 2")
+ {
+ const EventSet D{e1_handle};
+ const Configuration C{e0_handle};
+
+ REQUIRE(U.empty());
+ U.insert(std::move(e0));
+ U.insert(std::move(e1));
+ U.insert(std::move(e2));
+ U.insert(std::move(e3));
+ U.insert(std::move(e4));
+ U.insert(std::move(e7));
+
+ const auto alternative = C.compute_alternative_to(D, U);
+ REQUIRE(alternative.has_value());
+
+ // The first alternative that is found is the one that is chosen. Since
+ // traversal over the elements of an unordered_set<> are not guaranteed,
+ // both {e0, e4} and {e0, e7} are valid alternatives
+ REQUIRE((alternative.value().get_events() == EventSet({e0_handle, e4_handle}) or
+ alternative.value().get_events() == EventSet({e0_handle, e7_handle})));
+ }
}
\ No newline at end of file
bool contains_event_equivalent_to(const UnfoldingEvent* e) const;
auto begin() const { return this->event_handles.begin(); }
- auto end() const { return this->event_handles.begin(); }
+ auto end() const { return this->event_handles.end(); }
auto cbegin() const { return this->event_handles.cbegin(); }
auto cend() const { return this->event_handles.cend(); }
size_t size() const { return this->global_events_.size(); }
#include "src/mc/explo/udpor/Unfolding.hpp"
#include "src/mc/explo/udpor/udpor_tests_private.hpp"
+using namespace simgrid::mc;
using namespace simgrid::mc::udpor;
TEST_CASE("simgrid::mc::udpor::Unfolding: Creating an unfolding")
TEST_CASE("simgrid::mc::udpor::Unfolding: Checking for semantically equivalent events")
{
Unfolding unfolding;
- auto e1 = std::make_unique<UnfoldingEvent>(EventSet(), std::make_shared<IndependentAction>());
- auto e2 = std::make_unique<UnfoldingEvent>(EventSet(), std::make_shared<IndependentAction>());
+ auto e1 = std::make_unique<UnfoldingEvent>(
+ EventSet(), std::make_shared<IndependentAction>(Transition::Type::BARRIER_ASYNC_LOCK, 6, 2));
+ auto e2 = std::make_unique<UnfoldingEvent>(
+ EventSet(), std::make_shared<IndependentAction>(Transition::Type::BARRIER_ASYNC_LOCK, 6, 2));
- // e1 and e2 are semantically equivalent
+ // e1 and e2 are equivalent
REQUIRE(*e1 == *e2);
-}
\ No newline at end of file
+
+ const auto e1_handle = e1.get();
+ const auto e2_handle = e2.get();
+ unfolding.insert(std::move(e1));
+
+ REQUIRE(unfolding.contains_event_equivalent_to(e1_handle));
+ REQUIRE(unfolding.contains_event_equivalent_to(e2_handle));
+}
+
+TEST_CASE("simgrid::mc::udpor::Unfolding: Checking all immediate conflicts restricted to an unfolding") {}
\ No newline at end of file
