From cddc05516f6bb5cb50d472ac61079cdee0243d20 Mon Sep 17 00:00:00 2001 From: Maxwell Pirtle Date: Wed, 8 Mar 2023 13:12:00 +0100 Subject: [PATCH] Add conflict-free invariant check to Configuration When adding events to a configuration, we want to ensure that the configuration remains both a) causally closed and b) conflict-free. The latter required that the tests be modified as they effectively assumed that the transitions associated with each event were independent of one another. Since the `Transition` base class is dependent by default, this was at odds with the assumptions --- src/mc/explo/udpor/Configuration.cpp | 12 ++- src/mc/explo/udpor/Configuration.hpp | 2 + src/mc/explo/udpor/Configuration_test.cpp | 117 +++++++++++---------- src/mc/explo/udpor/EventSet_test.cpp | 23 +--- src/mc/explo/udpor/UnfoldingEvent.cpp | 12 +++ src/mc/explo/udpor/udpor_forward.hpp | 2 +- src/mc/explo/udpor/udpor_tests_private.hpp | 40 +++++++ 7 files changed, 124 insertions(+), 84 deletions(-) create mode 100644 src/mc/explo/udpor/udpor_tests_private.hpp diff --git a/src/mc/explo/udpor/Configuration.cpp b/src/mc/explo/udpor/Configuration.cpp index a1b7924edb..8e2cb8521e 100644 --- a/src/mc/explo/udpor/Configuration.cpp +++ b/src/mc/explo/udpor/Configuration.cpp @@ -36,12 +36,18 @@ void Configuration::add_event(const UnfoldingEvent* e) return; } + // Preserves the property that the configuration is conflict-free + if (e->conflicts_with(*this)) { + throw std::invalid_argument("The newly added event conflicts with the events already " + "contained in the configuration. Adding this event violates " + "the property that a configuration is conflict-free"); + } + this->events_.insert(e); this->newest_event = e; - // Preserves the property that the configuration is valid - History history(e); - if (!this->events_.contains(history)) { + // Preserves the property that the configuration is causally closed + if (auto history = History(e); !this->events_.contains(history)) { throw std::invalid_argument("The newly added event has dependencies " "which are missing from this configuration"); } diff --git a/src/mc/explo/udpor/Configuration.hpp b/src/mc/explo/udpor/Configuration.hpp index 3b344dda00..a27b9a6a8a 100644 --- a/src/mc/explo/udpor/Configuration.hpp +++ b/src/mc/explo/udpor/Configuration.hpp @@ -23,6 +23,8 @@ public: auto begin() const { return this->events_.begin(); } auto end() const { return this->events_.end(); } + auto cbegin() const { return this->events_.cbegin(); } + auto cend() const { return this->events_.cend(); } bool contains(const UnfoldingEvent* e) const { return this->events_.contains(e); } const EventSet& get_events() const { return this->events_; } diff --git a/src/mc/explo/udpor/Configuration_test.cpp b/src/mc/explo/udpor/Configuration_test.cpp index af975fc467..48eeb4e1fd 100644 --- a/src/mc/explo/udpor/Configuration_test.cpp +++ b/src/mc/explo/udpor/Configuration_test.cpp @@ -9,6 +9,7 @@ #include "src/mc/explo/udpor/History.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" #include @@ -24,11 +25,11 @@ TEST_CASE("simgrid::mc::udpor::Configuration: Constructing Configurations") // e3 // / / // e4 e5 - UnfoldingEvent e1; - UnfoldingEvent e2{&e1}; - UnfoldingEvent e3{&e2}; - UnfoldingEvent e4{&e3}; - UnfoldingEvent e5{&e3}; + UnfoldingEvent e1(EventSet(), std::make_shared()); + UnfoldingEvent e2(EventSet({&e1}), std::make_shared()); + UnfoldingEvent e3(EventSet({&e2}), std::make_shared()); + UnfoldingEvent e4(EventSet({&e3}), std::make_shared()); + UnfoldingEvent e5(EventSet({&e3}), std::make_shared()); SECTION("Creating a configuration without events") { @@ -37,7 +38,7 @@ TEST_CASE("simgrid::mc::udpor::Configuration: Constructing Configurations") REQUIRE(C.get_latest_event() == nullptr); } - SECTION("Creating a configuration with events") + SECTION("Creating a configuration with events (test violation of being causally closed)") { // 5 choose 0 = 1 test REQUIRE_NOTHROW(Configuration({&e1})); @@ -93,10 +94,10 @@ TEST_CASE("simgrid::mc::udpor::Configuration: Adding Events") // / // / / // e3 e4 - UnfoldingEvent e1; - UnfoldingEvent e2{&e1}; - UnfoldingEvent e3{&e2}; - UnfoldingEvent e4{&e2}; + UnfoldingEvent e1(EventSet(), std::make_shared()); + UnfoldingEvent e2(EventSet({&e1}), std::make_shared()); + UnfoldingEvent e3(EventSet({&e2}), std::make_shared()); + UnfoldingEvent e4(EventSet({&e2}), std::make_shared()); REQUIRE_THROWS_AS(Configuration().add_event(nullptr), std::invalid_argument); REQUIRE_THROWS_AS(Configuration().add_event(&e2), std::invalid_argument); @@ -136,10 +137,10 @@ TEST_CASE("simgrid::mc::udpor::Configuration: Topological Sort Order") // e3 // / // e4 - UnfoldingEvent e1; - UnfoldingEvent e2{&e1}; - UnfoldingEvent e3{&e2}; - UnfoldingEvent e4{&e3}; + UnfoldingEvent e1(EventSet(), std::make_shared()); + UnfoldingEvent e2(EventSet({&e1}), std::make_shared()); + UnfoldingEvent e3(EventSet({&e2}), std::make_shared()); + UnfoldingEvent e4(EventSet({&e3}), std::make_shared()); SECTION("Topological ordering for entire set") { @@ -194,12 +195,12 @@ TEST_CASE("simgrid::mc::udpor::Configuration: Topological Sort Order More Compli // e4 e6 // / // e5 - UnfoldingEvent e1; - UnfoldingEvent e2{&e1}; - UnfoldingEvent e3{&e2}; - UnfoldingEvent e4{&e3}; - UnfoldingEvent e5{&e4}; - UnfoldingEvent e6{&e3}; + UnfoldingEvent e1(EventSet(), std::make_shared()); + UnfoldingEvent e2(EventSet({&e1}), std::make_shared()); + UnfoldingEvent e3(EventSet({&e2}), std::make_shared()); + UnfoldingEvent e4(EventSet({&e3}), std::make_shared()); + UnfoldingEvent e5(EventSet({&e4}), std::make_shared()); + UnfoldingEvent e6(EventSet({&e3}), std::make_shared()); SECTION("Topological ordering for subsets") { @@ -303,18 +304,18 @@ TEST_CASE("simgrid::mc::udpor::Configuration: Topological Sort Order Very Compli // / / / // / / / // [ e12 ] - UnfoldingEvent e1; - UnfoldingEvent e2{&e1}; - UnfoldingEvent e8{&e1}; - UnfoldingEvent e3{&e2}; - UnfoldingEvent e4{&e3}; - UnfoldingEvent e5{&e4}; - UnfoldingEvent e6{&e4}; - UnfoldingEvent e7{&e2, &e8}; - UnfoldingEvent e9{&e6, &e7}; - UnfoldingEvent e10{&e7}; - UnfoldingEvent e11{&e8}; - UnfoldingEvent e12{&e5, &e9, &e10}; + UnfoldingEvent e1(EventSet(), std::make_shared()); + UnfoldingEvent e2(EventSet({&e1}), std::make_shared()); + UnfoldingEvent e8(EventSet({&e1}), std::make_shared()); + UnfoldingEvent e3(EventSet({&e2}), std::make_shared()); + UnfoldingEvent e4(EventSet({&e3}), std::make_shared()); + UnfoldingEvent e5(EventSet({&e4}), std::make_shared()); + UnfoldingEvent e6(EventSet({&e4}), std::make_shared()); + UnfoldingEvent e7(EventSet({&e2, &e8}), std::make_shared()); + UnfoldingEvent e9(EventSet({&e6, &e7}), std::make_shared()); + UnfoldingEvent e10(EventSet({&e7}), std::make_shared()); + UnfoldingEvent e11(EventSet({&e8}), std::make_shared()); + UnfoldingEvent e12(EventSet({&e5, &e9, &e10}), std::make_shared()); Configuration C{&e1, &e2, &e3, &e4, &e5, &e6, &e7, &e8, &e9, &e10, &e11, &e12}; SECTION("Test every combination of the maximal configuration (forward graph)") @@ -405,14 +406,14 @@ TEST_CASE("simgrid::mc::udpor::maximal_subsets_iterator: Basic Testing of Maxima // e3 e6 // / / / // e4 e7 e8 - UnfoldingEvent e1; - UnfoldingEvent e2{&e1}; - UnfoldingEvent e3{&e2}; - UnfoldingEvent e4{&e3}; - UnfoldingEvent e5{&e1}; - UnfoldingEvent e6{&e5}; - UnfoldingEvent e7{&e6}; - UnfoldingEvent e8{&e6}; + UnfoldingEvent e1(EventSet(), std::make_shared()); + UnfoldingEvent e2(EventSet({&e1}), std::make_shared()); + UnfoldingEvent e3(EventSet({&e2}), std::make_shared()); + UnfoldingEvent e4(EventSet({&e3}), std::make_shared()); + UnfoldingEvent e5(EventSet({&e1}), std::make_shared()); + UnfoldingEvent e6(EventSet({&e5}), std::make_shared()); + UnfoldingEvent e7(EventSet({&e6}), std::make_shared()); + UnfoldingEvent e8(EventSet({&e6}), std::make_shared()); SECTION("Iteration over an empty configuration yields only the empty set") { @@ -538,24 +539,24 @@ TEST_CASE("simgrid::mc::udpor::maximal_subsets_iterator: Stress Test for Maximal // | e11 e12 e13 e14 e15 // | / / / / / / // +-> e16 e17 e18 - UnfoldingEvent e1; - UnfoldingEvent e2{&e1}; - UnfoldingEvent e3{&e1}; - UnfoldingEvent e4{&e2}; - UnfoldingEvent e5{&e2}; - UnfoldingEvent e6{&e3}; - UnfoldingEvent e7{&e3}; - UnfoldingEvent e8{&e4}; - UnfoldingEvent e9{&e4, &e5, &e6}; - UnfoldingEvent e10{&e6, &e7}; - UnfoldingEvent e11{&e8}; - UnfoldingEvent e12{&e8}; - UnfoldingEvent e13{&e9}; - UnfoldingEvent e14{&e9}; - UnfoldingEvent e15{&e10}; - UnfoldingEvent e16{&e5, &e11}; - UnfoldingEvent e17{&e12, &e13, &e14}; - UnfoldingEvent e18{&e14, &e15}; + UnfoldingEvent e1(EventSet(), std::make_shared()); + UnfoldingEvent e2(EventSet({&e1}), std::make_shared()); + UnfoldingEvent e3(EventSet({&e1}), std::make_shared()); + UnfoldingEvent e4(EventSet({&e2}), std::make_shared()); + UnfoldingEvent e5(EventSet({&e2}), std::make_shared()); + UnfoldingEvent e6(EventSet({&e3}), std::make_shared()); + UnfoldingEvent e7(EventSet({&e3}), std::make_shared()); + UnfoldingEvent e8(EventSet({&e4}), std::make_shared()); + UnfoldingEvent e9(EventSet({&e4, &e5, &e6}), std::make_shared()); + UnfoldingEvent e10(EventSet({&e6, &e7}), std::make_shared()); + UnfoldingEvent e11(EventSet({&e8}), std::make_shared()); + UnfoldingEvent e12(EventSet({&e8}), std::make_shared()); + UnfoldingEvent e13(EventSet({&e9}), std::make_shared()); + UnfoldingEvent e14(EventSet({&e9}), std::make_shared()); + UnfoldingEvent e15(EventSet({&e10}), std::make_shared()); + UnfoldingEvent e16(EventSet({&e5, &e11}), std::make_shared()); + UnfoldingEvent e17(EventSet({&e12, &e13, &e14}), std::make_shared()); + UnfoldingEvent e18(EventSet({&e14, &e15}), std::make_shared()); Configuration C{&e1, &e2, &e3, &e4, &e5, &e6, &e7, &e8, &e9, &e10, &e11, &e12, &e13, &e14, &e15, &e16, &e17, &e18}; SECTION("Every subset iterated over is maximal") diff --git a/src/mc/explo/udpor/EventSet_test.cpp b/src/mc/explo/udpor/EventSet_test.cpp index de0822aedf..62109a4e3c 100644 --- a/src/mc/explo/udpor/EventSet_test.cpp +++ b/src/mc/explo/udpor/EventSet_test.cpp @@ -6,9 +6,9 @@ #include "src/3rd-party/catch.hpp" #include "src/mc/explo/udpor/EventSet.hpp" #include "src/mc/explo/udpor/UnfoldingEvent.hpp" +#include "src/mc/explo/udpor/udpor_tests_private.hpp" #include "src/mc/transition/Transition.hpp" -using namespace simgrid::mc; using namespace simgrid::mc::udpor; TEST_CASE("simgrid::mc::udpor::EventSet: Initial conditions when creating sets") @@ -761,27 +761,6 @@ TEST_CASE("simgrid::mc::udpor::EventSet: Moving into a collection") TEST_CASE("simgrid::mc::udpor::EventSet: Checking conflicts") { - struct IndependentAction : public Transition { - // Independent with everyone else - bool depends(const Transition* other) const override { return false; } - }; - - struct DependentAction : public Transition { - // Dependent with everyone else (except IndependentAction) - bool depends(const Transition* other) const override - { - return dynamic_cast(other) == nullptr; - } - }; - - struct ConditionallyDependentAction : public Transition { - // Dependent only with DependentAction (i.e. not itself) - bool depends(const Transition* other) const override - { - return dynamic_cast(other) != nullptr; - } - }; - // The following tests concern the given event structure: // e1 // / / diff --git a/src/mc/explo/udpor/UnfoldingEvent.cpp b/src/mc/explo/udpor/UnfoldingEvent.cpp index bd49e863e9..83e1d7dba3 100644 --- a/src/mc/explo/udpor/UnfoldingEvent.cpp +++ b/src/mc/explo/udpor/UnfoldingEvent.cpp @@ -74,6 +74,18 @@ bool UnfoldingEvent::conflicts_with(const UnfoldingEvent* other) const return false; } +bool UnfoldingEvent::conflicts_with(const Configuration& config) const +{ + // A configuration is itself already conflict-free. Thus, it is + // simply a matter of testing whether or not the transition associated + // with the event is dependent with any already in `config` that are + // OUTSIDE this event's history (in an unfolding, events only conflict + // if they are not related) + const EventSet potential_conflicts = config.get_events().subtracting(get_history()); + return std::any_of(potential_conflicts.cbegin(), potential_conflicts.cend(), + [&](const UnfoldingEvent* e) { return this->has_conflicting_transition_with(e); }); +} + bool UnfoldingEvent::has_conflicting_transition_with(const UnfoldingEvent* other) const { return associated_transition->depends(other->associated_transition.get()); diff --git a/src/mc/explo/udpor/udpor_forward.hpp b/src/mc/explo/udpor/udpor_forward.hpp index 865df169af..1cbdb2e0e5 100644 --- a/src/mc/explo/udpor/udpor_forward.hpp +++ b/src/mc/explo/udpor/udpor_forward.hpp @@ -3,7 +3,7 @@ /* 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. */ -/** @file mc_forward.hpp +/** @file udpor_forward.hpp * * Forward definitions for MC types specific to UDPOR */ diff --git a/src/mc/explo/udpor/udpor_tests_private.hpp b/src/mc/explo/udpor/udpor_tests_private.hpp new file mode 100644 index 0000000000..6e1a23345b --- /dev/null +++ b/src/mc/explo/udpor/udpor_tests_private.hpp @@ -0,0 +1,40 @@ +/* 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. */ + +/** @file udpor_tests_private.hpp + * + * A private header file for tests involving events in + * configurations + */ + +#ifndef SIMGRID_MC_UDPOR_TEST_PRIVATE_HPP +#define SIMGRID_MC_UDPOR_TEST_PRIVATE_HPP + +namespace simgrid::mc::udpor { + +struct IndependentAction : public Transition { + // Independent with everyone else + bool depends(const Transition* other) const override { return false; } +}; + +struct DependentAction : public Transition { + // Dependent with everyone else (except IndependentAction) + bool depends(const Transition* other) const override + { + return dynamic_cast(other) == nullptr; + } +}; + +struct ConditionallyDependentAction : public Transition { + // Dependent only with DependentAction (i.e. not itself) + bool depends(const Transition* other) const override + { + return dynamic_cast(other) != nullptr; + } +}; + +} // namespace simgrid::mc::udpor + +#endif -- 2.20.1