From 2ef958bf49890e4ac8fbe179f1d339b923fb67a8 Mon Sep 17 00:00:00 2001 From: Martin Quinson Date: Thu, 9 Nov 2023 11:53:21 +0100 Subject: [PATCH] Cleanup work to make is_race_reversible() a method of Transition That's someone less efficient as we need to retrieve the other's transition in all cases where most Transition kind can compute the answer without the other transition, but that should be more readable. --- .../explo/odpor/ReversibleRaceCalculator.cpp | 104 +++++++++--------- .../explo/odpor/ReversibleRaceCalculator.hpp | 38 +++---- 2 files changed, 72 insertions(+), 70 deletions(-) diff --git a/src/mc/explo/odpor/ReversibleRaceCalculator.cpp b/src/mc/explo/odpor/ReversibleRaceCalculator.cpp index a7de9b92ec..d35c167d67 100644 --- a/src/mc/explo/odpor/ReversibleRaceCalculator.cpp +++ b/src/mc/explo/odpor/ReversibleRaceCalculator.cpp @@ -29,7 +29,7 @@ bool ReversibleRaceCalculator::is_race_reversible(const Execution& E, Execution: Execution::EventHandle e2) { using Action = Transition::Type; - using Handler = std::function; + using Handler = std::function; using HandlerMap = std::unordered_map; const static HandlerMap handlers = { @@ -53,9 +53,10 @@ bool ReversibleRaceCalculator::is_race_reversible(const Execution& E, Execution: {Action::TESTANY, &ReversibleRaceCalculator::is_race_reversible_TestAny}, {Action::WAITANY, &ReversibleRaceCalculator::is_race_reversible_WaitAny}}; - const auto* e2_action = E.get_transition_for_handle(e2); - if (const auto handler = handlers.find(e2_action->type_); handler != handlers.end()) { - return handler->second(E, e1, e2_action); + const auto* other_transition = E.get_transition_for_handle(e1); + const auto* t2 = E.get_transition_for_handle(e2); + if (const auto handler = handlers.find(t2->type_); handler != handlers.end()) { + return handler->second(E, other_transition, t2); } else { xbt_die("There is currently no specialized computation for the transition " "'%s' for computing reversible races in ODPOR, so the model checker cannot " @@ -63,12 +64,12 @@ bool ReversibleRaceCalculator::is_race_reversible(const Execution& E, Execution: "that the transition be supported in SimGrid using ODPPR and consider " "using the other model-checking algorithms supported by SimGrid instead " "in the meantime", - e2_action->to_string().c_str()); + t2->to_string().c_str()); } } -bool ReversibleRaceCalculator::is_race_reversible_ActorJoin(const Execution&, Execution::EventHandle /*e1*/, - const Transition* /*e2*/) +bool ReversibleRaceCalculator::is_race_reversible_ActorJoin(const Execution&, const Transition* /*other_transition*/, + const Transition* /*t2*/) { // ActorJoin races with another event iff its target `T` is the same as // the actor executing the other transition. Clearly, then, we could not join @@ -76,138 +77,139 @@ bool ReversibleRaceCalculator::is_race_reversible_ActorJoin(const Execution&, Ex return false; } -bool ReversibleRaceCalculator::is_race_reversible_BarrierAsyncLock(const Execution&, Execution::EventHandle /*e1*/, - const Transition* /*e2*/) +bool ReversibleRaceCalculator::is_race_reversible_BarrierAsyncLock(const Execution&, + const Transition* /*other_transition*/, + const Transition* /*t2*/) { // BarrierAsyncLock is always enabled return true; } -bool ReversibleRaceCalculator::is_race_reversible_BarrierWait(const Execution& E, Execution::EventHandle e1, - const Transition* /*e2*/) +bool ReversibleRaceCalculator::is_race_reversible_BarrierWait(const Execution& E, const Transition* other_transition, + const Transition* /*t2*/) { // If the other event is a barrier lock event, then we // are not reversible; otherwise we are reversible. - const auto e1_action = E.get_transition_for_handle(e1)->type_; - return e1_action != Transition::Type::BARRIER_ASYNC_LOCK; + const auto other_action = other_transition->type_; + return other_action != Transition::Type::BARRIER_ASYNC_LOCK; } -bool ReversibleRaceCalculator::is_race_reversible_CommRecv(const Execution&, Execution::EventHandle /*e1*/, - const Transition* /*e2*/) +bool ReversibleRaceCalculator::is_race_reversible_CommRecv(const Execution&, const Transition* /*other_transition*/, + const Transition* /*t2*/) { // CommRecv is always enabled return true; } -bool ReversibleRaceCalculator::is_race_reversible_CommSend(const Execution&, Execution::EventHandle /*e1*/, - const Transition* /*e2*/) +bool ReversibleRaceCalculator::is_race_reversible_CommSend(const Execution&, const Transition* /*other_transition*/, + const Transition* /*t2*/) { // CommSend is always enabled return true; } -bool ReversibleRaceCalculator::is_race_reversible_CommWait(const Execution& E, Execution::EventHandle e1, - const Transition* /*e2*/) +bool ReversibleRaceCalculator::is_race_reversible_CommWait(const Execution& E, const Transition* other_transition, + const Transition* /*t2*/) { // If the other event is a communication event, then we // are not reversible; otherwise we are reversible. - const auto e1_action = E.get_transition_for_handle(e1)->type_; - return e1_action != Transition::Type::COMM_ASYNC_SEND && e1_action != Transition::Type::COMM_ASYNC_RECV; + const auto other_action = other_transition->type_; + return other_action != Transition::Type::COMM_ASYNC_SEND && other_action != Transition::Type::COMM_ASYNC_RECV; } -bool ReversibleRaceCalculator::is_race_reversible_CommTest(const Execution&, Execution::EventHandle /*e1*/, - const Transition* /*e2*/) +bool ReversibleRaceCalculator::is_race_reversible_CommTest(const Execution&, const Transition* /*other_transition*/, + const Transition* /*t2*/) { // CommTest is always enabled return true; } -bool ReversibleRaceCalculator::is_race_reversible_MutexAsyncLock(const Execution&, Execution::EventHandle /*e1*/, - const Transition* /*e2*/) +bool ReversibleRaceCalculator::is_race_reversible_MutexAsyncLock(const Execution&, + const Transition* /*other_transition*/, + const Transition* /*t2*/) { // MutexAsyncLock is always enabled return true; } -bool ReversibleRaceCalculator::is_race_reversible_MutexTest(const Execution&, Execution::EventHandle /*e1*/, - const Transition* /*e2*/) +bool ReversibleRaceCalculator::is_race_reversible_MutexTest(const Execution&, const Transition* /*other_transition*/, + const Transition* /*t2*/) { // MutexTest is always enabled return true; } -bool ReversibleRaceCalculator::is_race_reversible_MutexTrylock(const Execution&, Execution::EventHandle /*e1*/, - const Transition* /*e2*/) +bool ReversibleRaceCalculator::is_race_reversible_MutexTrylock(const Execution&, const Transition* /*other_transition*/, + const Transition* /*t2*/) { // MutexTrylock is always enabled return true; } -bool ReversibleRaceCalculator::is_race_reversible_MutexUnlock(const Execution&, Execution::EventHandle /*e1*/, - const Transition* /*e2*/) +bool ReversibleRaceCalculator::is_race_reversible_MutexUnlock(const Execution&, const Transition* /*other_transition*/, + const Transition* /*t2*/) { // MutexUnlock is always enabled return true; } -bool ReversibleRaceCalculator::is_race_reversible_MutexWait(const Execution& E, Execution::EventHandle e1, - const Transition* /*e2*/) +bool ReversibleRaceCalculator::is_race_reversible_MutexWait(const Execution& E, const Transition* /*other_transition*/, + const Transition* /*t2*/) { // TODO: for now we over approximate the reversibility return true; } -bool ReversibleRaceCalculator::is_race_reversible_SemAsyncLock(const Execution&, Execution::EventHandle /*e1*/, - const Transition* /*e2*/) +bool ReversibleRaceCalculator::is_race_reversible_SemAsyncLock(const Execution&, const Transition* /*other_transition*/, + const Transition* /*t2*/) { // SemAsyncLock is always enabled return true; } -bool ReversibleRaceCalculator::is_race_reversible_SemUnlock(const Execution&, Execution::EventHandle /*e1*/, - const Transition* /*e2*/) +bool ReversibleRaceCalculator::is_race_reversible_SemUnlock(const Execution&, const Transition* /*other_transition*/, + const Transition* /*t2*/) { // SemUnlock is always enabled return true; } -bool ReversibleRaceCalculator::is_race_reversible_SemWait(const Execution& E, Execution::EventHandle e1, - const Transition* /*e2*/) +bool ReversibleRaceCalculator::is_race_reversible_SemWait(const Execution& E, const Transition* other_transition, + const Transition* /*t2*/) { - const auto e1_transition = E.get_transition_for_handle(e1); - if (e1_transition->type_ == Transition::Type::SEM_UNLOCK && - static_cast(e1_transition)->get_capacity() <= 1) { + if (other_transition->type_ == Transition::Type::SEM_UNLOCK && + static_cast(other_transition)->get_capacity() <= 1) { return false; } - xbt_assert(false, "SEM_WAIT that is dependent with a SEM_UNLOCK should not be reversible. FixMe"); + xbt_die("SEM_WAIT that is dependent with a SEM_UNLOCK should not be reversible. FixMe"); return true; } -bool ReversibleRaceCalculator::is_race_reversible_ObjectAccess(const Execution&, Execution::EventHandle /*e1*/, - const Transition* /*e2*/) +bool ReversibleRaceCalculator::is_race_reversible_ObjectAccess(const Execution&, const Transition* /*other_transition*/, + const Transition* /*t2*/) { // Object access is always enabled return true; } -bool ReversibleRaceCalculator::is_race_reversible_Random(const Execution&, Execution::EventHandle /*e1*/, - const Transition* /*e2*/) +bool ReversibleRaceCalculator::is_race_reversible_Random(const Execution&, const Transition* /*other_transition*/, + const Transition* /*t2*/) { // Random is always enabled return true; } -bool ReversibleRaceCalculator::is_race_reversible_TestAny(const Execution&, Execution::EventHandle /*e1*/, - const Transition* /*e2*/) +bool ReversibleRaceCalculator::is_race_reversible_TestAny(const Execution&, const Transition* /*other_transition*/, + const Transition* /*t2*/) { // TestAny is always enabled return true; } -bool ReversibleRaceCalculator::is_race_reversible_WaitAny(const Execution&, Execution::EventHandle /*e1*/, - const Transition* /*e2*/) +bool ReversibleRaceCalculator::is_race_reversible_WaitAny(const Execution&, const Transition* /*other_transition*/, + const Transition* /*t2*/) { // TODO: We need to check if any of the transitions // waited on occurred before `e1` diff --git a/src/mc/explo/odpor/ReversibleRaceCalculator.hpp b/src/mc/explo/odpor/ReversibleRaceCalculator.hpp index 88c6839bb0..1c6781482a 100644 --- a/src/mc/explo/odpor/ReversibleRaceCalculator.hpp +++ b/src/mc/explo/odpor/ReversibleRaceCalculator.hpp @@ -30,25 +30,25 @@ namespace simgrid::mc::odpor { * is only sensible in the context of a race */ class ReversibleRaceCalculator final { - static bool is_race_reversible_ActorJoin(const Execution&, Execution::EventHandle e1, const Transition* e2); - static bool is_race_reversible_BarrierAsyncLock(const Execution&, Execution::EventHandle e1, const Transition* e2); - static bool is_race_reversible_BarrierWait(const Execution&, Execution::EventHandle e1, const Transition* e2); - static bool is_race_reversible_CommRecv(const Execution&, Execution::EventHandle e1, const Transition* e2); - static bool is_race_reversible_CommSend(const Execution&, Execution::EventHandle e1, const Transition* e2); - static bool is_race_reversible_CommWait(const Execution&, Execution::EventHandle e1, const Transition* e2); - static bool is_race_reversible_CommTest(const Execution&, Execution::EventHandle e1, const Transition* e2); - static bool is_race_reversible_MutexAsyncLock(const Execution&, Execution::EventHandle e1, const Transition* e2); - static bool is_race_reversible_MutexTest(const Execution&, Execution::EventHandle e1, const Transition* e2); - static bool is_race_reversible_MutexTrylock(const Execution&, Execution::EventHandle e1, const Transition* e2); - static bool is_race_reversible_MutexUnlock(const Execution&, Execution::EventHandle e1, const Transition* e2); - static bool is_race_reversible_MutexWait(const Execution&, Execution::EventHandle e1, const Transition* e2); - static bool is_race_reversible_SemAsyncLock(const Execution&, Execution::EventHandle e1, const Transition* e2); - static bool is_race_reversible_SemUnlock(const Execution&, Execution::EventHandle e1, const Transition* e2); - static bool is_race_reversible_SemWait(const Execution&, Execution::EventHandle e1, const Transition* e2); - static bool is_race_reversible_ObjectAccess(const Execution&, Execution::EventHandle e1, const Transition* e2); - static bool is_race_reversible_Random(const Execution&, Execution::EventHandle e1, const Transition* e2); - static bool is_race_reversible_TestAny(const Execution&, Execution::EventHandle e1, const Transition* e2); - static bool is_race_reversible_WaitAny(const Execution&, Execution::EventHandle e1, const Transition* e2); + static bool is_race_reversible_ActorJoin(const Execution&, const Transition* t1, const Transition* t2); + static bool is_race_reversible_BarrierAsyncLock(const Execution&, const Transition* t1, const Transition* t2); + static bool is_race_reversible_BarrierWait(const Execution&, const Transition* t1, const Transition* t2); + static bool is_race_reversible_CommRecv(const Execution&, const Transition* t1, const Transition* t2); + static bool is_race_reversible_CommSend(const Execution&, const Transition* t1, const Transition* t2); + static bool is_race_reversible_CommWait(const Execution&, const Transition* t1, const Transition* t2); + static bool is_race_reversible_CommTest(const Execution&, const Transition* t1, const Transition* t2); + static bool is_race_reversible_MutexAsyncLock(const Execution&, const Transition* t1, const Transition* t2); + static bool is_race_reversible_MutexTest(const Execution&, const Transition* t1, const Transition* t2); + static bool is_race_reversible_MutexTrylock(const Execution&, const Transition* t1, const Transition* t2); + static bool is_race_reversible_MutexUnlock(const Execution&, const Transition* t1, const Transition* t2); + static bool is_race_reversible_MutexWait(const Execution&, const Transition* t1, const Transition* t2); + static bool is_race_reversible_SemAsyncLock(const Execution&, const Transition* t1, const Transition* t2); + static bool is_race_reversible_SemUnlock(const Execution&, const Transition* t1, const Transition* t2); + static bool is_race_reversible_SemWait(const Execution&, const Transition* t1, const Transition* t2); + static bool is_race_reversible_ObjectAccess(const Execution&, const Transition* t1, const Transition* t2); + static bool is_race_reversible_Random(const Execution&, const Transition* t1, const Transition* t2); + static bool is_race_reversible_TestAny(const Execution&, const Transition* t1, const Transition* t2); + static bool is_race_reversible_WaitAny(const Execution&, const Transition* t1, const Transition* t2); public: static bool is_race_reversible(const Execution&, Execution::EventHandle e1, Execution::EventHandle e2); -- 2.20.1