From: Maxwell Pirtle Date: Mon, 17 Apr 2023 08:38:29 +0000 (+0200) Subject: Add preliminary basic tests for ex(C) computation X-Git-Tag: v3.34~39^2~10 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/f1dd25cad1bee0eb04a01e8d94b5776c5e8aeb44?ds=sidebyside Add preliminary basic tests for ex(C) computation Testing the correctness of the computation for extension sets is critical, as extension sets guide the entire UDPOR search. Unfortunately it is also very difficult to create tests for computing the extension sets... --- diff --git a/MANIFEST.in b/MANIFEST.in index 0caa0f9991..296c687d9b 100644 --- a/MANIFEST.in +++ b/MANIFEST.in @@ -2228,6 +2228,7 @@ include src/mc/explo/udpor/Configuration_test.cpp include src/mc/explo/udpor/EventSet.cpp include src/mc/explo/udpor/EventSet.hpp include src/mc/explo/udpor/EventSet_test.cpp +include src/mc/explo/udpor/ExtensionSet_test.cpp include src/mc/explo/udpor/ExtensionSetCalculator.cpp include src/mc/explo/udpor/ExtensionSetCalculator.hpp include src/mc/explo/udpor/History.cpp diff --git a/src/mc/explo/udpor/EventSet.cpp b/src/mc/explo/udpor/EventSet.cpp index b644448a84..0485cd8fa8 100644 --- a/src/mc/explo/udpor/EventSet.cpp +++ b/src/mc/explo/udpor/EventSet.cpp @@ -110,6 +110,11 @@ bool EventSet::contains(const UnfoldingEvent* e) const return this->events_.find(e) != this->events_.end(); } +bool EventSet::contains_equivalent_to(const UnfoldingEvent* e) const +{ + return std::find_if(begin(), end(), [=](const UnfoldingEvent* e_in_set) { return *e == *e_in_set; }) != end(); +} + bool EventSet::is_subset_of(const EventSet& other) const { // If there is some element not contained in `other`, then diff --git a/src/mc/explo/udpor/EventSet.hpp b/src/mc/explo/udpor/EventSet.hpp index ddd875d7ad..67314f6041 100644 --- a/src/mc/explo/udpor/EventSet.hpp +++ b/src/mc/explo/udpor/EventSet.hpp @@ -28,18 +28,9 @@ public: EventSet& operator=(EventSet&&) = default; EventSet(EventSet&&) = default; explicit EventSet(Configuration&& config); - explicit EventSet(std::vector&& raw_events) : events_(raw_events.begin(), raw_events.end()) - { - xbt_assert(std::none_of(events_.begin(), events_.end(), [](const auto* e) { return e == nullptr; }), "Oh no"); - } - explicit EventSet(std::unordered_set&& raw_events) : events_(raw_events) - { - xbt_assert(std::none_of(events_.begin(), events_.end(), [](const auto* e) { return e == nullptr; }), "Oh no"); - } - explicit EventSet(std::initializer_list event_list) : events_(std::move(event_list)) - { - xbt_assert(std::none_of(events_.begin(), events_.end(), [](const auto* e) { return e == nullptr; }), "Oh no"); - } + explicit EventSet(std::vector&& raw_events) : events_(raw_events.begin(), raw_events.end()) {} + explicit EventSet(std::unordered_set&& raw_events) : events_(raw_events) {} + explicit EventSet(std::initializer_list event_list) : events_(std::move(event_list)) {} auto begin() const { return this->events_.begin(); } auto end() const { return this->events_.end(); } @@ -63,8 +54,10 @@ public: size_t size() const; bool empty() const; + bool contains(const UnfoldingEvent*) const; bool contains(const History&) const; + bool contains_equivalent_to(const UnfoldingEvent*) const; bool intersects(const EventSet&) const; bool intersects(const History&) const; bool is_subset_of(const EventSet&) const; diff --git a/src/mc/explo/udpor/ExtensionSet_test.cpp b/src/mc/explo/udpor/ExtensionSet_test.cpp new file mode 100644 index 0000000000..dcd5533e2a --- /dev/null +++ b/src/mc/explo/udpor/ExtensionSet_test.cpp @@ -0,0 +1,69 @@ +/* Copyright (c) 2017-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. */ + +#include "src/3rd-party/catch.hpp" +#include "src/mc/explo/udpor/Configuration.hpp" +#include "src/mc/explo/udpor/ExtensionSetCalculator.hpp" +#include "src/mc/explo/udpor/History.hpp" +#include "src/mc/explo/udpor/Unfolding.hpp" + +using namespace simgrid::mc; +using namespace simgrid::mc::udpor; + +TEST_CASE("simgrid::mc::udpor: Testing Computation with AsyncSend/AsyncReceive Only") +{ + // This test checks that the unfolding constructed for the very + // simple program described below is extended correctly. Each + // step of UDPOR is observed to ensure that computations are carried + // out correctly. The program described is simply: + // + // 1 2 + // AsyncSend(m) AsyncRecv(m) + // + const int times_considered = 0; + const int tag = 0; + const unsigned mbox = 0; + const uintptr_t comm = 0; + + Unfolding U; + + SECTION("Computing ex({⊥}) with 1: AsyncSend") + { + // Consider the extension with `1: AsyncSend(m)` + Configuration C; + aid_t issuer = 1; + const uintptr_t sbuff = 0; + const size_t size = 100; + + const auto async_send = + std::make_shared(issuer, times_considered, comm, mbox, sbuff, size, tag); + const auto incremental_exC = ExtensionSetCalculator::partially_extend(C, &U, async_send); + + // Check that the events have been added to `U` + REQUIRE(U.size() == 1); + + // Make assertions about the contents of ex(C) + UnfoldingEvent e(EventSet(), async_send); + REQUIRE(incremental_exC.contains_equivalent_to(&e)); + } + + SECTION("Computing ex({⊥}) with 2: AsyncRecv") + { + // Consider the extension with `2: AsyncRecv(m)` + Configuration C; + aid_t issuer = 2; + const uintptr_t rbuff = 0; + + const auto async_recv = std::make_shared(issuer, times_considered, comm, mbox, rbuff, tag); + const auto incremental_exC = ExtensionSetCalculator::partially_extend(C, &U, async_recv); + + // Check that the events have been added to `U` + REQUIRE(U.size() == 1); + + // Make assertions about the contents of ex(C) + UnfoldingEvent e(EventSet(), async_recv); + REQUIRE(incremental_exC.contains_equivalent_to(&e)); + } +} \ No newline at end of file diff --git a/src/mc/transition/TransitionComm.cpp b/src/mc/transition/TransitionComm.cpp index 42837a5d99..54c27f6aca 100644 --- a/src/mc/transition/TransitionComm.cpp +++ b/src/mc/transition/TransitionComm.cpp @@ -94,6 +94,15 @@ bool CommTestTransition::depends(const Transition* other) const return false; // Comm transitions are INDEP with non-comm transitions } +CommRecvTransition::CommRecvTransition(aid_t issuer, int times_considered, uintptr_t comm_, unsigned mbox_, + uintptr_t rbuff_, int tag_) + : Transition(Type::COMM_ASYNC_RECV, issuer, times_considered) + , comm_(comm_) + , mbox_(mbox_) + , rbuff_(rbuff_) + , tag_(tag_) +{ +} CommRecvTransition::CommRecvTransition(aid_t issuer, int times_considered, std::stringstream& stream) : Transition(Type::COMM_ASYNC_RECV, issuer, times_considered) { @@ -148,6 +157,16 @@ bool CommRecvTransition::depends(const Transition* other) const return false; // Comm transitions are INDEP with non-comm transitions } +CommSendTransition::CommSendTransition(aid_t issuer, int times_considered, uintptr_t comm_, unsigned mbox_, + uintptr_t sbuff_, size_t size_, int tag_) + : Transition(Type::COMM_ASYNC_SEND, issuer, times_considered) + , comm_(comm_) + , mbox_(mbox_) + , sbuff_(sbuff_) + , size_(size_) + , tag_(tag_) +{ +} CommSendTransition::CommSendTransition(aid_t issuer, int times_considered, std::stringstream& stream) : Transition(Type::COMM_ASYNC_SEND, issuer, times_considered) { diff --git a/src/mc/transition/TransitionComm.hpp b/src/mc/transition/TransitionComm.hpp index f652d035c7..c212509531 100644 --- a/src/mc/transition/TransitionComm.hpp +++ b/src/mc/transition/TransitionComm.hpp @@ -92,6 +92,7 @@ class CommRecvTransition : public Transition { int tag_; public: + CommRecvTransition(aid_t issuer, int times_considered, uintptr_t comm_, unsigned mbox_, uintptr_t rbuff_, int tag_); CommRecvTransition(aid_t issuer, int times_considered, std::stringstream& stream); std::string to_string(bool verbose) const override; bool depends(const Transition* other) const override; @@ -114,6 +115,8 @@ class CommSendTransition : public Transition { int tag_; public: + CommSendTransition(aid_t issuer, int times_considered, uintptr_t comm_, unsigned mbox_, uintptr_t sbuff_, + size_t size_, int tag_); CommSendTransition(aid_t issuer, int times_considered, std::stringstream& stream); std::string to_string(bool verbose) const override; bool depends(const Transition* other) const override; diff --git a/tools/cmake/Tests.cmake b/tools/cmake/Tests.cmake index 6c71e1d107..6023103a61 100644 --- a/tools/cmake/Tests.cmake +++ b/tools/cmake/Tests.cmake @@ -138,8 +138,8 @@ set(STATEFUL_MC_UNIT_TESTS src/mc/sosp/Snapshot_test.cpp src/mc/sosp/PageStore_test.cpp src/mc/explo/udpor/Unfolding_test.cpp src/mc/explo/udpor/UnfoldingEvent_test.cpp - src/mc/explo/udpor/EventSet_test.cpp + src/mc/explo/udpor/ExtensionSet_test.cpp src/mc/explo/udpor/History_test.cpp src/mc/explo/udpor/Configuration_test.cpp)