From e1e921c13508c418a7f26031f41b1fb3dc1376f3 Mon Sep 17 00:00:00 2001 From: Maxwell Pirtle Date: Fri, 5 May 2023 10:29:02 +0200 Subject: [PATCH] Fix two off-by-one errors with clock vectors Two errors were identified with managing clock vectors in the Execution class. The index assigned to the new transition was previously `size() + 1` when it should have read `size()`. Furthermore, the loop for checking "happens-between" events excluded event 0. Both issues are now resolved and a test with a race at the beginning was added as verification --- src/mc/explo/odpor/Execution.cpp | 7 +++---- src/mc/explo/odpor/Execution_test.cpp | 18 ++++++++++++++++++ 2 files changed, 21 insertions(+), 4 deletions(-) diff --git a/src/mc/explo/odpor/Execution.cpp b/src/mc/explo/odpor/Execution.cpp index fe84056636..da252f3b8c 100644 --- a/src/mc/explo/odpor/Execution.cpp +++ b/src/mc/explo/odpor/Execution.cpp @@ -21,9 +21,8 @@ void Execution::push_transition(const Transition* t) } } // The entry in the vector for `t->aid_` is the size - // of the new stack, which will have a size one greater - // than that before we insert the new events - max_clock_vector[t->aid_] = this->size() + 1; + // of the stack + max_clock_vector[t->aid_] = this->size(); contents_.push_back(Event({t, max_clock_vector})); } @@ -38,7 +37,7 @@ std::unordered_set Execution::get_racing_events_of(Execu std::unordered_set disqualified_events; // For each event of the execution - for (auto e_i = target; e_i > 0 && e_i != std::numeric_limits::max(); e_i--) { + for (auto e_i = target; e_i != std::numeric_limits::max(); e_i--) { // We need `e_i -->_E target` as a necessary condition if (not happens_before(e_i, target)) { continue; diff --git a/src/mc/explo/odpor/Execution_test.cpp b/src/mc/explo/odpor/Execution_test.cpp index 9033557ff8..b23384823a 100644 --- a/src/mc/explo/odpor/Execution_test.cpp +++ b/src/mc/explo/odpor/Execution_test.cpp @@ -196,4 +196,22 @@ TEST_CASE("simgrid::mc::odpor::Execution: Testing Racing Events and Initials") REQUIRE(initial_wrt_event2.value() == static_cast(3)); } } + + SECTION("Example 3: Testing 'Lock' Example") + { + const auto a1 = std::make_shared(Transition::Type::UNKNOWN, 2); + const auto a2 = std::make_shared(Transition::Type::UNKNOWN, 2); + const auto a3 = std::make_shared(Transition::Type::UNKNOWN, 2); + const auto a4 = std::make_shared(Transition::Type::UNKNOWN, 1); + const auto a5 = 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()); + execution.push_transition(a5.get()); + + REQUIRE(execution.get_racing_events_of(4) == std::unordered_set{0}); + } } \ No newline at end of file -- 2.20.1