From 7375674952af9a3836b0d7692a1a0894f758baab Mon Sep 17 00:00:00 2001 From: Maxwell Pirtle Date: Thu, 4 May 2023 09:33:25 +0200 Subject: [PATCH] Add first tests for "happens-before" The happens-before relation is used extensively by SDPOR and ODPOR during their computations for determining what executions should be searched next. This commit introduces the first round of tests for the happens-before relation on artificially constructed executions --- MANIFEST.in | 1 + src/mc/explo/odpor/Execution.cpp | 17 ++- src/mc/explo/odpor/Execution_test.cpp | 177 ++++++++++++++++++++++++++ tools/cmake/Tests.cmake | 1 + 4 files changed, 192 insertions(+), 4 deletions(-) create mode 100644 src/mc/explo/odpor/Execution_test.cpp diff --git a/MANIFEST.in b/MANIFEST.in index 5bcbb3499d..8912990be1 100644 --- a/MANIFEST.in +++ b/MANIFEST.in @@ -2191,6 +2191,7 @@ include src/mc/explo/LivenessChecker.cpp include src/mc/explo/LivenessChecker.hpp include src/mc/explo/odpor/Execution.cpp include src/mc/explo/odpor/Execution.hpp +include src/mc/explo/odpor/Execution_test.cpp include src/mc/explo/UdporChecker.cpp include src/mc/explo/UdporChecker.hpp include src/mc/explo/simgrid_mc.cpp diff --git a/src/mc/explo/odpor/Execution.cpp b/src/mc/explo/odpor/Execution.cpp index 1bc01d82fe..fe493cf194 100644 --- a/src/mc/explo/odpor/Execution.cpp +++ b/src/mc/explo/odpor/Execution.cpp @@ -102,7 +102,7 @@ std::optional Execution::get_first_ssdpor_initial_from(EventHandle e, Execution E_prime_v = get_prefix_up_to(e); std::vector v; - for (auto e_prime = e; e_prime <= next_E_p; ++e_prime) { + for (auto e_prime = e + 1; e_prime <= next_E_p; ++e_prime) { // Any event `e*` which occurs after `e` but which does not // happen after `e` is a member of `v`. In addition to marking // the event in `v`, we also "simulate" running the action `v` @@ -137,8 +137,9 @@ std::unordered_set Execution::get_ssdpor_initials_from(EventHandle e, bool Execution::happens_before(Execution::EventHandle e1_handle, Execution::EventHandle e2_handle) const { - // 1. "happens-before" is a subset of "occurs before" - if (e1_handle > e2_handle) { + // 1. "happens-before" (-->_E) is a subset of "occurs before" (<_E) + // and is an irreflexive relation + if (e1_handle >= e2_handle) { return false; } @@ -146,7 +147,15 @@ bool Execution::happens_before(Execution::EventHandle e1_handle, Execution::Even // according to the procedure outlined in section 4 of the original DPOR paper const Event& e2 = get_event_with_handle(e2_handle); const aid_t proc_e1 = get_actor_with_handle(e1_handle); - return e1_handle <= e2.get_clock_vector().get(proc_e1).value_or(0); + + if (const auto e1_in_e2_clock = e2.get_clock_vector().get(proc_e1); e1_in_e2_clock.has_value()) { + return e1_handle <= e1_in_e2_clock.value(); + } + // If `e1` does not appear in e2's clock vector, this implies + // not only that the transitions associated with `e1` and `e2 + // are independent, but further that there are no transitive + // dependencies between e1 and e2 + return false; } } // namespace simgrid::mc::odpor \ No newline at end of file diff --git a/src/mc/explo/odpor/Execution_test.cpp b/src/mc/explo/odpor/Execution_test.cpp new file mode 100644 index 0000000000..e69a4f9f1f --- /dev/null +++ b/src/mc/explo/odpor/Execution_test.cpp @@ -0,0 +1,177 @@ +/* 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/odpor/Execution.hpp" +#include "src/mc/explo/udpor/udpor_tests_private.hpp" +#include "src/mc/transition/TransitionComm.hpp" + +using namespace simgrid::mc; +using namespace simgrid::mc::odpor; +using namespace simgrid::mc::udpor; + +TEST_CASE("simgrid::mc::odpor::Execution: Constructing Executions") +{ + Execution execution; + REQUIRE(execution.empty()); + REQUIRE(execution.size() == 0); +} + +TEST_CASE("simgrid::mc::odpor::Execution: Testing Happens-Before") +{ + SECTION("Example 1") + { + // We check each permutation for happens before + // among the given actions added to the execution + const auto a1 = std::make_shared(Transition::Type::UNKNOWN, 1); + const auto a2 = std::make_shared(Transition::Type::UNKNOWN, 2); + const auto a3 = std::make_shared(Transition::Type::UNKNOWN, 3); + const auto a4 = std::make_shared(Transition::Type::UNKNOWN, 4); + + Execution execution; + execution.push_transition(a1.get()); + execution.push_transition(a2.get()); + execution.push_transition(a3.get()); + execution.push_transition(a4.get()); + + SECTION("Happens-before is irreflexive") + { + REQUIRE_FALSE(execution.happens_before(0, 0)); + REQUIRE_FALSE(execution.happens_before(1, 1)); + REQUIRE_FALSE(execution.happens_before(2, 2)); + REQUIRE_FALSE(execution.happens_before(3, 3)); + } + + SECTION("Happens-before values for each pair of events") + { + REQUIRE_FALSE(execution.happens_before(0, 1)); + REQUIRE_FALSE(execution.happens_before(0, 2)); + REQUIRE(execution.happens_before(0, 3)); + REQUIRE_FALSE(execution.happens_before(1, 2)); + REQUIRE_FALSE(execution.happens_before(1, 3)); + REQUIRE_FALSE(execution.happens_before(2, 3)); + } + + SECTION("Happens-before is a subset of 'occurs-before' ") + { + REQUIRE_FALSE(execution.happens_before(1, 0)); + REQUIRE_FALSE(execution.happens_before(2, 0)); + REQUIRE_FALSE(execution.happens_before(3, 0)); + REQUIRE_FALSE(execution.happens_before(2, 1)); + REQUIRE_FALSE(execution.happens_before(3, 1)); + REQUIRE_FALSE(execution.happens_before(3, 2)); + } + } + + SECTION("Example 2") + { + const auto a1 = std::make_shared(Transition::Type::UNKNOWN, 1); + const auto a2 = std::make_shared(Transition::Type::UNKNOWN, 3); + const auto a3 = std::make_shared(Transition::Type::UNKNOWN, 3); + const auto a4 = std::make_shared(Transition::Type::UNKNOWN, 3); + + // Notice that `a5` and `a6` are executed by the same actor; thus, although + // the actor is executing independent actions, each still "happen-before" + // the another + + Execution execution; + execution.push_transition(a1.get()); + execution.push_transition(a2.get()); + execution.push_transition(a3.get()); + execution.push_transition(a4.get()); + + SECTION("Happens-before is irreflexive") + { + REQUIRE_FALSE(execution.happens_before(0, 0)); + REQUIRE_FALSE(execution.happens_before(1, 1)); + REQUIRE_FALSE(execution.happens_before(2, 2)); + REQUIRE_FALSE(execution.happens_before(3, 3)); + } + + SECTION("Happens-before values for each pair of events") + { + REQUIRE_FALSE(execution.happens_before(0, 1)); + REQUIRE_FALSE(execution.happens_before(0, 2)); + REQUIRE_FALSE(execution.happens_before(0, 3)); + REQUIRE(execution.happens_before(1, 2)); + REQUIRE(execution.happens_before(1, 3)); + REQUIRE(execution.happens_before(2, 3)); + } + + SECTION("Happens-before is a subset of 'occurs-before'") + { + REQUIRE_FALSE(execution.happens_before(1, 0)); + REQUIRE_FALSE(execution.happens_before(2, 0)); + REQUIRE_FALSE(execution.happens_before(3, 0)); + REQUIRE_FALSE(execution.happens_before(2, 1)); + REQUIRE_FALSE(execution.happens_before(3, 1)); + REQUIRE_FALSE(execution.happens_before(3, 2)); + } + } +} + +TEST_CASE("simgrid::mc::odpor::Execution: Testing Racing Events Initials") +{ + SECTION("Example 1") + { + const auto a1 = std::make_shared(Transition::Type::UNKNOWN, 1); + const auto a2 = std::make_shared(Transition::Type::UNKNOWN, 2); + const auto a3 = std::make_shared(Transition::Type::UNKNOWN, 1); + const auto a4 = std::make_shared(Transition::Type::UNKNOWN, 1); + const auto a5 = std::make_shared(Transition::Type::UNKNOWN, 2); + + Execution execution; + execution.push_transition(a1.get()); + execution.push_transition(a2.get()); + execution.push_transition(a3.get()); + execution.push_transition(a4.get()); + execution.push_transition(a5.get()); + + // Nothing comes before event 0 + REQUIRE(execution.get_racing_events_of(0) == std::unordered_set{}); + + // Events 0 and 1 are independent + REQUIRE(execution.get_racing_events_of(1) == std::unordered_set{}); + + // 2 and 1 are executed by different actors and happen right after each other + REQUIRE(execution.get_racing_events_of(2) == std::unordered_set{1}); + + // Although a3 and a4 are dependent, they are executed by the same actor + REQUIRE(execution.get_racing_events_of(3) == std::unordered_set{}); + + // Event 4 is in a race with neither event 0 nor event 2 since those events + // "happen-before" event 3 with which event 4 races + // + // Furthermore, event 1 is run by the same actor and thus also is not in a race. + // Hence, only event 3 races with event 4 + REQUIRE(execution.get_racing_events_of(4) == std::unordered_set{3}); + } + + SECTION("Example 2: Events with multiple races") + { + const auto a1 = std::make_shared(Transition::Type::UNKNOWN, 1); + const auto a2 = std::make_shared(Transition::Type::UNKNOWN, 2); + const auto a3 = std::make_shared(Transition::Type::UNKNOWN, 1); + const auto a4 = std::make_shared(Transition::Type::UNKNOWN, 3); + + Execution execution; + execution.push_transition(a1.get()); + execution.push_transition(a2.get()); + execution.push_transition(a3.get()); + execution.push_transition(a4.get()); + + // Nothing comes before event 0 + REQUIRE(execution.get_racing_events_of(0) == std::unordered_set{}); + + // Events 0 and 1 are independent + REQUIRE(execution.get_racing_events_of(1) == std::unordered_set{}); + + // Event 2 is independent with event 1 and run by the same actor as event 0 + REQUIRE(execution.get_racing_events_of(2) == std::unordered_set{}); + + // All events are dependent with event 3, but event 0 "happens-before" event 2 + REQUIRE(execution.get_racing_events_of(3) == std::unordered_set{1, 2}); + } +} \ No newline at end of file diff --git a/tools/cmake/Tests.cmake b/tools/cmake/Tests.cmake index aab3aaba4a..625ce5e8bd 100644 --- a/tools/cmake/Tests.cmake +++ b/tools/cmake/Tests.cmake @@ -132,6 +132,7 @@ set(UNIT_TESTS src/xbt/unit-tests_main.cpp set(MC_UNIT_TESTS src/mc/sosp/Snapshot_test.cpp src/mc/sosp/PageStore_test.cpp + src/mc/explo/odpor/Execution_test.cpp src/mc/explo/udpor/EventSet_test.cpp src/mc/explo/udpor/Unfolding_test.cpp src/mc/explo/udpor/UnfoldingEvent_test.cpp -- 2.20.1