From: Maxwell Pirtle Date: Thu, 16 Mar 2023 09:56:36 +0000 (+0100) Subject: Add full example for K-partial alternatives X-Git-Tag: v3.34~284^2~5 X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/9ee28948a83efbfd6b4d9d9e7b513932afa40c10 Add full example for K-partial alternatives --- diff --git a/src/mc/explo/udpor/Configuration.cpp b/src/mc/explo/udpor/Configuration.cpp index c7e125dcc4..7edc16ee44 100644 --- a/src/mc/explo/udpor/Configuration.cpp +++ b/src/mc/explo/udpor/Configuration.cpp @@ -145,15 +145,15 @@ std::optional Configuration::compute_k_partial_alternative_to(con // 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... + // into SimGrid which associated additonal data structures with each unfolding event. + // Since that is a rather complicated addition, we defer it to 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)) { + e_i->conflicts_with(e) and (not D.intersects(e_local_config)) and is_compatible_with(e_local_config)) { comb[i].push_back(e); } } @@ -165,7 +165,8 @@ std::optional Configuration::compute_k_partial_alternative_to(con // 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) + // NP-complete (although computing the k-partial alternative is polynomial in + // the number of events) const auto map_events = [](const std::vector& spikes) { std::vector events; for (const auto& event_in_spike : spikes) { diff --git a/src/mc/explo/udpor/Configuration_test.cpp b/src/mc/explo/udpor/Configuration_test.cpp index 8506dd47cb..cff61e7834 100644 --- a/src/mc/explo/udpor/Configuration_test.cpp +++ b/src/mc/explo/udpor/Configuration_test.cpp @@ -614,7 +614,10 @@ TEST_CASE("simgrid::mc::udpor:Configuration: Computing Full Alternatives in Read // e6 e10 // // Theses tests walk through exactly the configurations and sets of `D` that - // UDPOR should encounter as it walks the unfolding. + // UDPOR COULD encounter as it walks through the unfolding. Note that + // if there are multiple alternatives to any given configuration, UDPOR can + // continue searching any one of them. The sequence assumes UDPOR first picks `e1`, + // then `e4`, and then `e7` Unfolding U; auto e0 = std::make_unique(EventSet(), std::make_shared()); @@ -627,7 +630,7 @@ TEST_CASE("simgrid::mc::udpor:Configuration: Computing Full Alternatives in Read auto e2_handle = e2.get(); auto e3 = std::make_unique(EventSet({e1_handle}), std::make_shared()); - // auto e3_handle = e3.get(); + auto e3_handle = e3.get(); auto e4 = std::make_unique(EventSet({e0_handle}), std::make_shared()); auto e4_handle = e4.get(); @@ -636,21 +639,45 @@ TEST_CASE("simgrid::mc::udpor:Configuration: Computing Full Alternatives in Read auto e5_handle = e5.get(); auto e6 = std::make_unique(EventSet({e5_handle}), std::make_shared()); + auto e6_handle = e6.get(); auto e7 = std::make_unique(EventSet({e0_handle}), std::make_shared()); auto e7_handle = e7.get(); auto e8 = std::make_unique(EventSet({e4_handle, e7_handle}), std::make_shared()); + auto e8_handle = e8.get(); - auto e9 = std::make_unique(EventSet({e7_handle}), std::make_shared()); + auto e9 = std::make_unique(EventSet({e7_handle}), std::make_shared()); auto e9_handle = e9.get(); auto e10 = std::make_unique(EventSet({e9_handle}), std::make_shared()); + auto e10_handle = e10.get(); - SECTION("Alternative computation step 1") + SECTION("Alternative computation call 1") { - const EventSet D; + // During the first call to Alt(C, D + {e}), + // UDPOR believes `U` to be the following: + // + // e0 + // / / / + // e1 e4 e7 + // / + // / / + // e2 e3 + // + // C := {e0, e1, e2} and `Explore(C, D, A)` picked `e3` + // (since en(C') where C' := {e0, e1, e2, e3} is empty + // [so UDPOR will simply return when C' is reached]) + // + // Thus the computation is (since D is empty at first) + // + // Alt(C, D + {e}) --> Alt({e0, e1, e2}, {e3}) + // + // where U is given above. There are no alternatives in + // this case since `e4` and `e7` conflict with `e1` (so + // they cannot be added to C to form a configuration) const Configuration C{e0_handle, e1_handle, e2_handle}; + const EventSet D_plus_e{e3_handle}; REQUIRE(U.empty()); U.insert(std::move(e0)); @@ -660,14 +687,70 @@ TEST_CASE("simgrid::mc::udpor:Configuration: Computing Full Alternatives in Read U.insert(std::move(e4)); U.insert(std::move(e7)); - const auto alternative = C.compute_alternative_to(D, U); + const auto alternative = C.compute_alternative_to(D_plus_e, U); REQUIRE_FALSE(alternative.has_value()); } - SECTION("Alternative computation step 2") + SECTION("Alternative computation call 2") { - const EventSet D{e1_handle}; + // During the second call to Alt(C, D + {e}), + // UDPOR believes `U` to be the following: + // + // e0 + // / / / + // e1 e4 e7 + // / + // / / + // e2 e3 + // + // C := {e0, e1} and `Explore(C, D, A)` picked `e2`. + // + // Thus the computation is (since D is still empty) + // + // Alt(C, D + {e}) --> Alt({e0, e1}, {e2}) + // + // where U is given above. There are no alternatives in + // this case since `e4` and `e7` conflict with `e1` (so + // they cannot be added to C to form a configuration) and + // e3 is NOT in conflict with either e0 or e1 + const Configuration C{e0_handle, e1_handle}; + const EventSet D_plus_e{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_plus_e, U); + REQUIRE_FALSE(alternative.has_value()); + } + + SECTION("Alternative computation call 3") + { + // During the thrid call to Alt(C, D + {e}), + // UDPOR believes `U` to be the following: + // + // e0 + // / / / + // e1 e4 e7 + // / + // / / + // e2 e3 + // + // C := {e0} and `Explore(C, D, A)` picked `e1`. + // + // Thus the computation is (since D is still empty) + // + // Alt(C, D + {e}) --> Alt({e0}, {e1}) + // + // where U is given above. There are two alternatives in this case: + // {e0, e4} and {e0, e7}. Either one would be a valid choice for + // UDPOR, so we must check for the precense of either const Configuration C{e0_handle}; + const EventSet D_plus_e{e1_handle}; REQUIRE(U.empty()); U.insert(std::move(e0)); @@ -677,7 +760,7 @@ TEST_CASE("simgrid::mc::udpor:Configuration: Computing Full Alternatives in Read U.insert(std::move(e4)); U.insert(std::move(e7)); - const auto alternative = C.compute_alternative_to(D, U); + const auto alternative = C.compute_alternative_to(D_plus_e, U); REQUIRE(alternative.has_value()); // The first alternative that is found is the one that is chosen. Since @@ -686,4 +769,395 @@ TEST_CASE("simgrid::mc::udpor:Configuration: Computing Full Alternatives in Read REQUIRE((alternative.value().get_events() == EventSet({e0_handle, e4_handle}) or alternative.value().get_events() == EventSet({e0_handle, e7_handle}))); } + + SECTION("Alternative computation call 4") + { + // During the fourth call to Alt(C, D + {e}), + // UDPOR believes `U` to be the following: + // + // e0 + // / / / + // e1 e4 e7 + // / / // + // / / e5 e8 + // e2 e3 / + // e6 + // + // C := {e0, e4, e5} and `Explore(C, D, A)` picked `e6` + // (since en(C') where C' := {e0, e4, e5, e6} is empty + // [so UDPOR will simply return when C' is reached]) + // + // Thus the computation is (since D is {e1}) + // + // Alt(C, D + {e}) --> Alt({e0, e4, e5}, {e1, e6}) + // + // where U is given above. There are no alternatives in this + // case, since: + // + // 1.`e2/e3` are eliminated since their histories contain `e1` + // 2. `e7/e8` are eliminated because they conflict with `e5` + const Configuration C{e0_handle, e4_handle, e5_handle}; + const EventSet D_plus_e{e1_handle, e6_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(e6)); + U.insert(std::move(e7)); + U.insert(std::move(e8)); + + const auto alternative = C.compute_alternative_to(D_plus_e, U); + REQUIRE_FALSE(alternative.has_value()); + } + + SECTION("Alternative computation call 5") + { + // During the fifth call to Alt(C, D + {e}), + // UDPOR believes `U` to be the following: + // + // e0 + // / / / + // e1 e4 e7 + // / / // + // / / e5 e8 + // e2 e3 / + // e6 + // + // C := {e0, e4} and `Explore(C, D, A)` picked `e5` + // (since en(C') where C' := {e0, e4, e5, e6} is empty + // [so UDPOR will simply return when C' is reached]) + // + // Thus the computation is (since D is {e1}) + // + // Alt(C, D + {e}) --> Alt({e0, e4}, {e1, e5}) + // + // where U is given above. There is one alternative in this case, + // viz. {e0, e4, e7, e8}. + // + // To continue the search, UDPOR computes J / C which in this + // case gives {e7, e8}. Since `e8` is not in en(C), UDPOR will + // choose `e7` next and add `e5` to `D` + const Configuration C{e0_handle, e4_handle}; + const EventSet D_plus_e{e1_handle, e5_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(e6)); + U.insert(std::move(e7)); + U.insert(std::move(e8)); + + const auto alternative = C.compute_alternative_to(D_plus_e, U); + REQUIRE(alternative.has_value()); + REQUIRE(alternative.value().get_events() == EventSet({e0_handle, e4_handle, e7_handle, e8_handle})); + } + + SECTION("Alternative computation call 6") + { + // During the sixth call to Alt(C, D + {e}), + // UDPOR believes `U` to be the following: + // + // e0 + // / / / + // e1 e4 e7 + // / / // / + // / / e5 e8 e9 + // e2 e3 / + // e6 + // + // C := {e0, e4, e7} and `Explore(C, D, A)` picked `e8` + // (since en(C') where C' := {e0, e4, e7, e8} is empty + // [so UDPOR will simply return when C' is reached]) + // + // Thus the computation is (since D is {e1, e5} [see the last step]) + // + // Alt(C, D + {e}) --> Alt({e0, e4, e7}, {e1, e5, e8}) + // + // where U is given above. There are no alternatives in this case + // since all `e9` conflicts with `e4` and all other events of `U` + // are eliminated since their history intersects `D` + const Configuration C{e0_handle, e4_handle, e7_handle}; + const EventSet D_plus_e{e1_handle, e5_handle, e8_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(e6)); + U.insert(std::move(e7)); + U.insert(std::move(e8)); + U.insert(std::move(e9)); + + const auto alternative = C.compute_alternative_to(D_plus_e, U); + REQUIRE_FALSE(alternative.has_value()); + } + + SECTION("Alternative computation call 7") + { + // During the seventh call to Alt(C, D + {e}), + // UDPOR believes `U` to be the following: + // + // e0 + // / / / + // e1 e4 e7 + // / / // / + // / / e5 e8 e9 + // e2 e3 / + // e6 + // + // C := {e0, e4} and `Explore(C, D, A)` picked `e7` + // + // Thus the computation is (since D is {e1, e5} [see call 5]) + // + // Alt(C, D + {e}) --> Alt({e0, e4}, {e1, e5, e7}) + // + // where U is given above. There are no alternatives again in this case + // since all `e9` conflicts with `e4` and all other events of `U` + // are eliminated since their history intersects `D` + const Configuration C{e0_handle, e4_handle}; + const EventSet D_plus_e{e1_handle, e5_handle, e7_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(e6)); + U.insert(std::move(e7)); + U.insert(std::move(e8)); + U.insert(std::move(e9)); + + const auto alternative = C.compute_alternative_to(D_plus_e, U); + REQUIRE_FALSE(alternative.has_value()); + } + + SECTION("Alternative computation call 8") + { + // During the eigth call to Alt(C, D + {e}), + // UDPOR believes `U` to be the following: + // + // e0 + // / / / + // e1 e4 e7 + // / / // / + // / / e5 e8 e9 + // e2 e3 / + // e6 + // + // C := {e0} and `Explore(C, D, A)` picked `e4`. At this + // point, UDPOR finished its recursive search of {e0, e4} + // after having finished {e0, e1} prior. + // + // Thus the computation is (since D = {e1}) + // + // Alt(C, D + {e}) --> Alt({e0}, {e1, e4}) + // + // where U is given above. There is one alternative in this + // case, viz {e0, e7, e9} since + // 1. e9 conflicts with e4 in D + // 2. e7 conflicts with e1 in D + // 3. the set {e7, e9} is conflict-free since `e7 < e9` + // 4. all other events are eliminated since their histories + // intersect D + // + // UDPOR will continue its recursive search following `e7` + // and add `e4` to D + const Configuration C{e0_handle}; + const EventSet D_plus_e{e1_handle, e4_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(e6)); + U.insert(std::move(e7)); + U.insert(std::move(e8)); + U.insert(std::move(e9)); + + const auto alternative = C.compute_alternative_to(D_plus_e, U); + REQUIRE(alternative.has_value()); + REQUIRE(alternative.value().get_events() == EventSet({e0_handle, e7_handle, e9_handle})); + } + + SECTION("Alternative computation call 9") + { + // During the ninth call to Alt(C, D + {e}), + // UDPOR believes `U` to be the following: + // + // e0 + // / / / + // e1 e4 e7 + // / / // / + // / / e5 e8 e9 + // e2 e3 / / + // e6 e10 + // + // C := {e0, e7, e9} and `Explore(C, D, A)` picked `e10`. + // (since en(C') where C' := {e0, e7, e9, e10} is empty + // [so UDPOR will simply return when C' is reached]). + // + // Thus the computation is (since D = {e1, e4} [see the previous step]) + // + // Alt(C, D + {e}) --> Alt({e0}, {e1, e4, e10}) + // + // where U is given above. There are no alternatives in this case + const Configuration C{e0_handle, e7_handle, e9_handle}; + const EventSet D_plus_e{e1_handle, e4_handle, e10_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(e6)); + U.insert(std::move(e7)); + U.insert(std::move(e8)); + U.insert(std::move(e9)); + U.insert(std::move(e10)); + + const auto alternative = C.compute_alternative_to(D_plus_e, U); + REQUIRE_FALSE(alternative.has_value()); + } + + SECTION("Alternative computation call 10") + { + // During the tenth call to Alt(C, D + {e}), + // UDPOR believes `U` to be the following: + // + // e0 + // / / / + // e1 e4 e7 + // / / // / + // / / e5 e8 e9 + // e2 e3 / / + // e6 e10 + // + // C := {e0, e7} and `Explore(C, D, A)` picked `e9`. + // + // Thus the computation is (since D = {e1, e4} [see call 8]) + // + // Alt(C, D + {e}) --> Alt({e0}, {e1, e4, e9}) + // + // where U is given above. There are no alternatives in this case + const Configuration C{e0_handle, e7_handle}; + const EventSet D_plus_e{e1_handle, e4_handle, e9_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(e6)); + U.insert(std::move(e7)); + U.insert(std::move(e8)); + U.insert(std::move(e9)); + U.insert(std::move(e10)); + + const auto alternative = C.compute_alternative_to(D_plus_e, U); + REQUIRE_FALSE(alternative.has_value()); + } + + SECTION("Alternative computation call 11 (final call)") + { + // During the eleventh and final call to Alt(C, D + {e}), + // UDPOR believes `U` to be the following: + // + // e0 + // / / / + // e1 e4 e7 + // / / // / + // / / e5 e8 e9 + // e2 e3 / / + // e6 e10 + // + // C := {e0} and `Explore(C, D, A)` picked `e7`. + // + // Thus the computation is (since D = {e1, e4} [see call 8]) + // + // Alt(C, D + {e}) --> Alt({e0}, {e1, e4, e7}) + // + // where U is given above. There are no alternatives in this case: + // everyone is eliminated! + const Configuration C{e0_handle, e7_handle}; + const EventSet D_plus_e{e1_handle, e4_handle, e9_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(e6)); + U.insert(std::move(e7)); + U.insert(std::move(e8)); + U.insert(std::move(e9)); + U.insert(std::move(e10)); + + const auto alternative = C.compute_alternative_to(D_plus_e, U); + REQUIRE_FALSE(alternative.has_value()); + } + + SECTION("Alternative computation next") + { + SECTION("Followed {e0, e7} first") + { + const EventSet D{e1_handle, e7_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(e5)); + U.insert(std::move(e7)); + U.insert(std::move(e8)); + U.insert(std::move(e9)); + U.insert(std::move(e10)); + + const auto alternative = C.compute_alternative_to(D, U); + REQUIRE(alternative.has_value()); + + // In this case, only {e0, e4} is a valid alternative + REQUIRE(alternative.value().get_events() == EventSet({e0_handle, e4_handle, e5_handle})); + } + + SECTION("Followed {e0, e4} first") + { + const EventSet D{e1_handle, e4_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(e5)); + U.insert(std::move(e6)); + U.insert(std::move(e7)); + U.insert(std::move(e8)); + U.insert(std::move(e9)); + + const auto alternative = C.compute_alternative_to(D, U); + REQUIRE(alternative.has_value()); + + // In this case, only {e0, e7} is a valid alternative + REQUIRE(alternative.value().get_events() == EventSet({e0_handle, e7_handle, e9_handle})); + } + } } \ No newline at end of file diff --git a/src/mc/explo/udpor/EventSet.cpp b/src/mc/explo/udpor/EventSet.cpp index ea42f8b259..09cb66b061 100644 --- a/src/mc/explo/udpor/EventSet.cpp +++ b/src/mc/explo/udpor/EventSet.cpp @@ -137,6 +137,11 @@ bool EventSet::contains(const History& history) const return std::all_of(history.begin(), history.end(), [=](const UnfoldingEvent* e) { return this->contains(e); }); } +bool EventSet::intersects(const History& history) const +{ + return std::any_of(history.begin(), history.end(), [=](const UnfoldingEvent* e) { return this->contains(e); }); +} + bool EventSet::is_maximal() const { // A set of events is maximal if no event from diff --git a/src/mc/explo/udpor/EventSet.hpp b/src/mc/explo/udpor/EventSet.hpp index 37da51ab2d..54c00c8f47 100644 --- a/src/mc/explo/udpor/EventSet.hpp +++ b/src/mc/explo/udpor/EventSet.hpp @@ -54,6 +54,7 @@ public: bool empty() const; bool contains(const UnfoldingEvent*) const; bool contains(const History&) const; + bool intersects(const History&) const; bool is_subset_of(const EventSet&) const; bool operator==(const EventSet& other) const { return this->events_ == other.events_; }