From: Martin Quinson Date: Mon, 13 Nov 2023 22:54:15 +0000 (+0100) Subject: MC: move the reversible_race logic to the Transition class X-Git-Tag: v3.35~54 X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/7e625e5e848a284b522d69ec28cb111f1f88515b MC: move the reversible_race logic to the Transition class --- diff --git a/MANIFEST.in b/MANIFEST.in index 718a59eced..ec75cbf48f 100644 --- a/MANIFEST.in +++ b/MANIFEST.in @@ -2242,8 +2242,6 @@ include src/mc/explo/odpor/ClockVector_test.cpp 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/odpor/ReversibleRaceCalculator.cpp -include src/mc/explo/odpor/ReversibleRaceCalculator.hpp include src/mc/explo/odpor/WakeupTree.cpp include src/mc/explo/odpor/WakeupTree.hpp include src/mc/explo/odpor/WakeupTreeIterator.cpp diff --git a/src/mc/explo/odpor/Execution.cpp b/src/mc/explo/odpor/Execution.cpp index 42ff35ec86..0694161cd2 100644 --- a/src/mc/explo/odpor/Execution.cpp +++ b/src/mc/explo/odpor/Execution.cpp @@ -5,7 +5,6 @@ #include "src/mc/explo/odpor/Execution.hpp" #include "src/mc/api/State.hpp" -#include "src/mc/explo/odpor/ReversibleRaceCalculator.hpp" #include "xbt/asserts.h" #include "xbt/string.hpp" #include @@ -118,8 +117,11 @@ std::unordered_set Execution::get_racing_events_of(Execu std::unordered_set Execution::get_reversible_races_of(EventHandle handle) const { std::unordered_set reversible_races; + const auto* this_transition = get_transition_for_handle(handle); for (EventHandle race : get_racing_events_of(handle)) { - if (ReversibleRaceCalculator::is_race_reversible(*this, race, handle)) { + const auto* other_transition = get_transition_for_handle(race); + + if (this_transition->reversible_race(other_transition)) { reversible_races.insert(race); } } diff --git a/src/mc/explo/odpor/ReversibleRaceCalculator.cpp b/src/mc/explo/odpor/ReversibleRaceCalculator.cpp deleted file mode 100644 index e3cccc761a..0000000000 --- a/src/mc/explo/odpor/ReversibleRaceCalculator.cpp +++ /dev/null @@ -1,220 +0,0 @@ -/* Copyright (c) 2008-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/mc/explo/odpor/ReversibleRaceCalculator.hpp" -#include "src/mc/explo/odpor/Execution.hpp" -#include "src/mc/transition/Transition.hpp" -#include "src/mc/transition/TransitionSynchro.hpp" - -#include -#include -#include -#include - -XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_odpor_reversible_race, mc_dfs, "ODPOR exploration algorithm of the model-checker"); - -namespace simgrid::mc::odpor { - -/** - The reversible race detector should only be used if we already have the assumption - e1 <* e2 (see Source set: a foundation for ODPOR). In particular this means that : - - e1 -->_E e2 - - proc(e1) != proc(e2) - - there is no event e3 s.t. e1 --> e3 --> e2 -*/ - -bool ReversibleRaceCalculator::is_race_reversible(const Execution& E, Execution::EventHandle e1, - Execution::EventHandle e2) -{ - using Action = Transition::Type; - using Handler = std::function; - using HandlerMap = std::unordered_map; - - const static HandlerMap handlers = { - {Action::ACTOR_JOIN, &ReversibleRaceCalculator::is_race_reversible_ActorJoin}, - {Action::BARRIER_ASYNC_LOCK, &ReversibleRaceCalculator::is_race_reversible_BarrierAsyncLock}, - {Action::BARRIER_WAIT, &ReversibleRaceCalculator::is_race_reversible_BarrierWait}, - {Action::COMM_ASYNC_SEND, &ReversibleRaceCalculator::is_race_reversible_CommSend}, - {Action::COMM_ASYNC_RECV, &ReversibleRaceCalculator::is_race_reversible_CommRecv}, - {Action::COMM_TEST, &ReversibleRaceCalculator::is_race_reversible_CommTest}, - {Action::COMM_WAIT, &ReversibleRaceCalculator::is_race_reversible_CommWait}, - {Action::MUTEX_ASYNC_LOCK, &ReversibleRaceCalculator::is_race_reversible_MutexAsyncLock}, - {Action::MUTEX_TEST, &ReversibleRaceCalculator::is_race_reversible_MutexTest}, - {Action::MUTEX_TRYLOCK, &ReversibleRaceCalculator::is_race_reversible_MutexTrylock}, - {Action::MUTEX_UNLOCK, &ReversibleRaceCalculator::is_race_reversible_MutexUnlock}, - {Action::MUTEX_WAIT, &ReversibleRaceCalculator::is_race_reversible_MutexWait}, - {Action::OBJECT_ACCESS, &ReversibleRaceCalculator::is_race_reversible_ObjectAccess}, - {Action::RANDOM, &ReversibleRaceCalculator::is_race_reversible_Random}, - {Action::SEM_ASYNC_LOCK, &ReversibleRaceCalculator::is_race_reversible_SemAsyncLock}, - {Action::SEM_UNLOCK, &ReversibleRaceCalculator::is_race_reversible_SemUnlock}, - {Action::SEM_WAIT, &ReversibleRaceCalculator::is_race_reversible_SemWait}, - {Action::TESTANY, &ReversibleRaceCalculator::is_race_reversible_TestAny}, - {Action::WAITANY, &ReversibleRaceCalculator::is_race_reversible_WaitAny}}; - - 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 " - "determine how to proceed. Please submit a bug report requesting " - "that the transition be supported in SimGrid using ODPPR and consider " - "using the other model-checking algorithms supported by SimGrid instead " - "in the meantime", - t2->to_string().c_str()); - } -} - -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 - // on that actor `T` and then run a transition by `T`, so no race is reversible - return false; -} - -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, 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 other_action = other_transition->type_; - return other_action != Transition::Type::BARRIER_ASYNC_LOCK; -} - -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&, const Transition* /*other_transition*/, - const Transition* /*t2*/) -{ - // CommSend is always enabled - return true; -} - -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 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&, const Transition* /*other_transition*/, - const Transition* /*t2*/) -{ - // CommTest is always enabled - return true; -} - -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&, const Transition* /*other_transition*/, - const Transition* /*t2*/) -{ - // MutexTest is always enabled - return true; -} - -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&, const Transition* /*other_transition*/, - const Transition* /*t2*/) -{ - // MutexUnlock is always enabled - return true; -} - -bool ReversibleRaceCalculator::is_race_reversible_MutexWait(const Execution& E, const Transition* /*other_transition*/, - const Transition* /*t2*/) -{ - // Only an Unlock can be dependent with a Wait - // and in this case, that Unlock enabled the wait - // Not reversible - return false; -} - -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&, const Transition* /*other_transition*/, - const Transition* /*t2*/) -{ - // SemUnlock is always enabled - return true; -} - -bool ReversibleRaceCalculator::is_race_reversible_SemWait(const Execution& E, const Transition* other_transition, - const Transition* /*t2*/) -{ - - if (other_transition->type_ == Transition::Type::SEM_UNLOCK && - static_cast(other_transition)->get_capacity() <= 1) { - return false; - } - 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&, const Transition* /*other_transition*/, - const Transition* /*t2*/) -{ - // Object access is always enabled - return true; -} - -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&, const Transition* /*other_transition*/, - const Transition* /*t2*/) -{ - // TestAny is always enabled - return true; -} - -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` - return true; // Let's overapproximate to not miss branches -} - -} // namespace simgrid::mc::odpor diff --git a/src/mc/explo/odpor/ReversibleRaceCalculator.hpp b/src/mc/explo/odpor/ReversibleRaceCalculator.hpp deleted file mode 100644 index 1c6781482a..0000000000 --- a/src/mc/explo/odpor/ReversibleRaceCalculator.hpp +++ /dev/null @@ -1,58 +0,0 @@ -/* 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. */ - -#ifndef SIMGRID_MC_ODPOR_REVERSIBLE_RACE_CALCULATOR_HPP -#define SIMGRID_MC_ODPOR_REVERSIBLE_RACE_CALCULATOR_HPP - -#include "src/mc/explo/odpor/Execution.hpp" -#include "src/mc/explo/odpor/odpor_forward.hpp" -#include "src/mc/transition/Transition.hpp" -#include "src/mc/transition/TransitionActor.hpp" -#include "src/mc/transition/TransitionAny.hpp" -#include "src/mc/transition/TransitionComm.hpp" -#include "src/mc/transition/TransitionObjectAccess.hpp" -#include "src/mc/transition/TransitionRandom.hpp" -#include "src/mc/transition/TransitionSynchro.hpp" - -#include - -namespace simgrid::mc::odpor { - -/** - * @brief Computes whether a race between two events - * in a given execution is a reversible race. - * - * @note: All of the methods assume that there is - * indeed a race between the two events in the - * execution; indeed, the question the method answers - * is only sensible in the context of a race - */ -class ReversibleRaceCalculator final { - 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); -}; - -} // namespace simgrid::mc::odpor -#endif diff --git a/src/mc/transition/Transition.hpp b/src/mc/transition/Transition.hpp index 9a840246c4..246b3f0ba2 100644 --- a/src/mc/transition/Transition.hpp +++ b/src/mc/transition/Transition.hpp @@ -7,6 +7,7 @@ #define SIMGRID_MC_TRANSITION_HPP #include "simgrid/forward.h" // aid_t +#include "xbt/ex.h" #include "xbt/utility.hpp" // XBT_DECLARE_ENUM_CLASS #include @@ -23,7 +24,7 @@ namespace simgrid::mc { * calls. */ class Transition { - /* Textual representation of the transition, to display backtraces */ + /* Global statistics */ static unsigned long executed_transitions_; static unsigned long replayed_transitions_; @@ -84,6 +85,21 @@ public: virtual bool depends(const Transition* other) const { return true; } + /** + The reversible race detector should only be used if we already have the assumption + this <* other (see Source set: a foundation for ODPOR). In particular this means that : + - this -->_E other + - proc(this) != proc(other) + - there is no event e s.t. this --> e --> other + + @note: It is safe to assume that there is indeed a race between the two events in the execution; + indeed, the question the method answers is only sensible in the context of a race + */ + virtual bool reversible_race(const Transition* other) const + { + xbt_die("%s unimplemented for %s", __func__, to_c_str(type_)); + } + /* Returns the total amount of transitions executed so far (for statistics) */ static unsigned long get_executed_transitions() { return executed_transitions_; } /* Returns the total amount of transitions replayed so far while backtracing (for statistics) */ diff --git a/src/mc/transition/TransitionActor.cpp b/src/mc/transition/TransitionActor.cpp index 70608f14da..16a17a3d09 100644 --- a/src/mc/transition/TransitionActor.cpp +++ b/src/mc/transition/TransitionActor.cpp @@ -47,6 +47,19 @@ bool ActorJoinTransition::depends(const Transition* other) const return false; } +bool ActorJoinTransition::reversible_race(const Transition* other) const +{ + switch (type_) { + case Type::ACTOR_JOIN: + // 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 + // on that actor `T` and then run a transition by `T`, so no race is reversible + return false; + default: + xbt_die("Unexpected transition type %s", to_c_str(type_)); + } +} + ActorSleepTransition::ActorSleepTransition(aid_t issuer, int times_considered, std::stringstream& stream) : Transition(Type::ACTOR_SLEEP, issuer, times_considered) { @@ -66,4 +79,14 @@ bool ActorSleepTransition::depends(const Transition* other) const return false; } +bool ActorSleepTransition::reversible_race(const Transition* other) const +{ + switch (type_) { + case Type::ACTOR_SLEEP: + return true; // Always enabled + default: + xbt_die("Unexpected transition type %s", to_c_str(type_)); + } +} + } // namespace simgrid::mc diff --git a/src/mc/transition/TransitionActor.hpp b/src/mc/transition/TransitionActor.hpp index 34df4417eb..68cc89f502 100644 --- a/src/mc/transition/TransitionActor.hpp +++ b/src/mc/transition/TransitionActor.hpp @@ -23,6 +23,7 @@ public: ActorJoinTransition(aid_t issuer, int times_considered, std::stringstream& stream); std::string to_string(bool verbose) const override; bool depends(const Transition* other) const override; + bool reversible_race(const Transition* other) const override; bool get_timeout() const { return timeout_; } /** Target ID */ @@ -35,6 +36,7 @@ public: ActorSleepTransition(aid_t issuer, int times_considered, std::stringstream& stream); std::string to_string(bool verbose) const override; bool depends(const Transition* other) const override; + bool reversible_race(const Transition* other) const override; }; } // namespace simgrid::mc diff --git a/src/mc/transition/TransitionAny.cpp b/src/mc/transition/TransitionAny.cpp index 48e061730c..580fb44389 100644 --- a/src/mc/transition/TransitionAny.cpp +++ b/src/mc/transition/TransitionAny.cpp @@ -43,6 +43,16 @@ bool TestAnyTransition::depends(const Transition* other) const return transitions_[times_considered_]->depends(other); } +bool TestAnyTransition::reversible_race(const Transition* other) const +{ + switch (type_) { + case Type::TESTANY: + return true; // TestAny is always enabled + default: + xbt_die("Unexpected transition type %s", to_c_str(type_)); + } +} + WaitAnyTransition::WaitAnyTransition(aid_t issuer, int times_considered, std::stringstream& stream) : Transition(Type::WAITANY, issuer, times_considered) { @@ -69,5 +79,15 @@ bool WaitAnyTransition::depends(const Transition* other) const return true; return transitions_[times_considered_]->depends(other); } +bool WaitAnyTransition::reversible_race(const Transition* other) const +{ + switch (type_) { + case Type::WAITANY: + // TODO: We need to check if any of the transitions waited on occurred before `e1` + return true; // Let's overapproximate to not miss branches + default: + xbt_die("Unexpected transition type %s", to_c_str(type_)); + } +} } // namespace simgrid::mc diff --git a/src/mc/transition/TransitionAny.hpp b/src/mc/transition/TransitionAny.hpp index 96a721226c..35cbf4e391 100644 --- a/src/mc/transition/TransitionAny.hpp +++ b/src/mc/transition/TransitionAny.hpp @@ -23,6 +23,7 @@ public: TestAnyTransition(aid_t issuer, int times_considered, std::stringstream& stream); std::string to_string(bool verbose) const override; bool depends(const Transition* other) const override; + bool reversible_race(const Transition* other) const override; Transition* get_current_transition() const { return transitions_.at(times_considered_); } bool result() const @@ -41,6 +42,7 @@ public: WaitAnyTransition(aid_t issuer, int times_considered, std::stringstream& stream); std::string to_string(bool verbose) const override; bool depends(const Transition* other) const override; + bool reversible_race(const Transition* other) const override; Transition* get_current_transition() const { return transitions_.at(times_considered_); } }; diff --git a/src/mc/transition/TransitionComm.cpp b/src/mc/transition/TransitionComm.cpp index 3cbf62ac81..19d8ebfde9 100644 --- a/src/mc/transition/TransitionComm.cpp +++ b/src/mc/transition/TransitionComm.cpp @@ -56,6 +56,18 @@ bool CommWaitTransition::depends(const Transition* other) const return false; // Comm transitions are INDEP with non-comm transitions } + +bool CommWaitTransition::reversible_race(const Transition* other) const +{ + switch (type_) { + case Type::COMM_WAIT: + // If the other event is a communication event, then we are not reversible; otherwise we are reversible. + return other->type_ != Transition::Type::COMM_ASYNC_SEND && other->type_ != Transition::Type::COMM_ASYNC_RECV; + default: + xbt_die("Unexpected transition type %s", to_c_str(type_)); + } +} + CommTestTransition::CommTestTransition(aid_t issuer, int times_considered, unsigned comm_, aid_t sender_, aid_t receiver_, unsigned mbox_) : Transition(Type::COMM_TEST, issuer, times_considered) @@ -76,6 +88,7 @@ std::string CommTestTransition::to_string(bool verbose) const { return xbt::string_printf("TestComm(from %ld to %ld, mbox=%u)", sender_, receiver_, mbox_); } + bool CommTestTransition::depends(const Transition* other) const { if (other->type_ < type_) @@ -99,6 +112,16 @@ bool CommTestTransition::depends(const Transition* other) const return false; // Comm transitions are INDEP with non-comm transitions } +bool CommTestTransition::reversible_race(const Transition* other) const +{ + switch (type_) { + case Type::COMM_TEST: + return true; // CommTest is always enabled + default: + xbt_die("Unexpected transition type %s", to_c_str(type_)); + } +} + CommRecvTransition::CommRecvTransition(aid_t issuer, int times_considered, unsigned comm_, unsigned mbox_, int tag_) : Transition(Type::COMM_ASYNC_RECV, issuer, times_considered), comm_(comm_), mbox_(mbox_), tag_(tag_) { @@ -164,6 +187,16 @@ bool CommRecvTransition::depends(const Transition* other) const return false; // Comm transitions are INDEP with non-comm transitions } +bool CommRecvTransition::reversible_race(const Transition* other) const +{ + switch (type_) { + case Type::COMM_ASYNC_RECV: + return true; // CommRecv is always enabled + default: + xbt_die("Unexpected transition type %s", to_c_str(type_)); + } +} + CommSendTransition::CommSendTransition(aid_t issuer, int times_considered, unsigned comm_, unsigned mbox_, int tag_) : Transition(Type::COMM_ASYNC_SEND, issuer, times_considered), comm_(comm_), mbox_(mbox_), tag_(tag_) { @@ -230,4 +263,14 @@ bool CommSendTransition::depends(const Transition* other) const return false; // Comm transitions are INDEP with non-comm transitions } +bool CommSendTransition::reversible_race(const Transition* other) const +{ + switch (type_) { + case Type::COMM_ASYNC_SEND: + return true; // CommSend is always enabled + default: + xbt_die("Unexpected transition type %s", to_c_str(type_)); + } +} + } // namespace simgrid::mc diff --git a/src/mc/transition/TransitionComm.hpp b/src/mc/transition/TransitionComm.hpp index a3a59babe1..1e9d0748cf 100644 --- a/src/mc/transition/TransitionComm.hpp +++ b/src/mc/transition/TransitionComm.hpp @@ -35,6 +35,7 @@ public: CommWaitTransition(aid_t issuer, int times_considered, std::stringstream& stream); std::string to_string(bool verbose) const override; bool depends(const Transition* other) const override; + bool reversible_race(const Transition* other) const override; bool get_timeout() const { return timeout_; } /** ID of the corresponding Communication object in the application, or 0 if unknown */ @@ -60,6 +61,7 @@ public: CommTestTransition(aid_t issuer, int times_considered, std::stringstream& stream); std::string to_string(bool verbose) const override; bool depends(const Transition* other) const override; + bool reversible_race(const Transition* other) const override; /** ID of the corresponding Communication object in the application, or 0 if unknown */ unsigned get_comm() const { return comm_; } @@ -81,6 +83,7 @@ public: 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; + bool reversible_race(const Transition* other) const override; /** ID of the corresponding Communication object in the application (or 0 if unknown)*/ unsigned get_comm() const { return comm_; } @@ -100,6 +103,7 @@ public: 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; + bool reversible_race(const Transition* other) const override; /** ID of the corresponding Communication object in the application, or 0 if unknown */ unsigned get_comm() const { return comm_; } diff --git a/src/mc/transition/TransitionObjectAccess.cpp b/src/mc/transition/TransitionObjectAccess.cpp index 0936359886..33b4163012 100644 --- a/src/mc/transition/TransitionObjectAccess.cpp +++ b/src/mc/transition/TransitionObjectAccess.cpp @@ -46,4 +46,14 @@ bool ObjectAccessTransition::depends(const Transition* o) const return false; } +bool ObjectAccessTransition::reversible_race(const Transition* other) const +{ + switch (type_) { + case Type::OBJECT_ACCESS: + return true; // Object access is always enabled + default: + xbt_die("Unexpected transition type %s", to_c_str(type_)); + } +} + } // namespace simgrid::mc diff --git a/src/mc/transition/TransitionObjectAccess.hpp b/src/mc/transition/TransitionObjectAccess.hpp index 4ca7ff8250..f9d7bc299e 100644 --- a/src/mc/transition/TransitionObjectAccess.hpp +++ b/src/mc/transition/TransitionObjectAccess.hpp @@ -22,6 +22,7 @@ public: ObjectAccessTransition(aid_t issuer, int times_considered, std::stringstream& stream); std::string to_string(bool verbose) const override; bool depends(const Transition* other) const override; + bool reversible_race(const Transition* other) const override; }; } // namespace simgrid::mc diff --git a/src/mc/transition/TransitionRandom.cpp b/src/mc/transition/TransitionRandom.cpp index d117a5712f..81eab72a0d 100644 --- a/src/mc/transition/TransitionRandom.cpp +++ b/src/mc/transition/TransitionRandom.cpp @@ -23,4 +23,14 @@ RandomTransition::RandomTransition(aid_t issuer, int times_considered, std::stri xbt_assert(stream >> min_ >> max_); } +bool RandomTransition::reversible_race(const Transition* other) const +{ + switch (type_) { + case Type::RANDOM: + return true; // Random is always enabled + default: + xbt_die("Unexpected transition type %s", to_c_str(type_)); + } +} + } // namespace simgrid::mc diff --git a/src/mc/transition/TransitionRandom.hpp b/src/mc/transition/TransitionRandom.hpp index 374d69def4..27d9757a27 100644 --- a/src/mc/transition/TransitionRandom.hpp +++ b/src/mc/transition/TransitionRandom.hpp @@ -24,6 +24,7 @@ public: return aid_ == other->aid_; } // Independent with any other transition + bool reversible_race(const Transition* other) const override; }; } // namespace simgrid::mc diff --git a/src/mc/transition/TransitionSynchro.cpp b/src/mc/transition/TransitionSynchro.cpp index b1bea23de0..3d0e0cd794 100644 --- a/src/mc/transition/TransitionSynchro.cpp +++ b/src/mc/transition/TransitionSynchro.cpp @@ -4,6 +4,8 @@ * under the terms of the license (GNU LGPL) which comes with this package. */ #include "src/mc/transition/TransitionSynchro.hpp" +#include "src/mc/mc_forward.hpp" +#include "src/mc/transition/TransitionObjectAccess.hpp" #include "xbt/asserts.h" #include "xbt/ex.h" #include "xbt/string.hpp" @@ -50,6 +52,19 @@ bool BarrierTransition::depends(const Transition* o) const return false; // barriers are INDEP with non-barrier transitions } +bool BarrierTransition::reversible_race(const Transition* other) const +{ + switch (type_) { + case Type::BARRIER_ASYNC_LOCK: + return true; // BarrierAsyncLock is always enabled + case Type::BARRIER_WAIT: + // If the other event is a barrier lock event, then we are not reversible; + // otherwise we are reversible. + return other->type_ != Transition::Type::BARRIER_ASYNC_LOCK; + default: + xbt_die("Unexpected transition type %s", to_c_str(type_)); + } +} std::string MutexTransition::to_string(bool verbose) const { @@ -112,6 +127,25 @@ bool MutexTransition::depends(const Transition* o) const return false; // mutexes are INDEP with non-mutex transitions } +bool SemaphoreTransition::reversible_race(const Transition* other) const +{ + switch (type_) { + case Type::SEM_ASYNC_LOCK: + return true; // SemAsyncLock is always enabled + case Type::SEM_UNLOCK: + return true; // SemUnlock is always enabled + case Type::SEM_WAIT: + if (other->type_ == Transition::Type::SEM_UNLOCK && + static_cast(other)->get_capacity() <= 1) { + return false; + } + xbt_die("SEM_WAIT that is dependent with a SEM_UNLOCK should not be reversible. FixMe"); + return true; + default: + xbt_die("Unexpected transition type %s", to_c_str(type_)); + } +} + std::string SemaphoreTransition::to_string(bool verbose) const { if (type_ == Type::SEM_ASYNC_LOCK || type_ == Type::SEM_UNLOCK) @@ -169,4 +203,26 @@ bool SemaphoreTransition::depends(const Transition* o) const return false; // semaphores are INDEP with non-semaphore transitions } +bool MutexTransition::reversible_race(const Transition* other) const +{ + switch (type_) { + case Type::MUTEX_ASYNC_LOCK: + return true; // MutexAsyncLock is always enabled + case Type::MUTEX_TEST: + return true; // MutexTest is always enabled + case Type::MUTEX_TRYLOCK: + return true; // MutexTrylock is always enabled + case Type::MUTEX_UNLOCK: + return true; // MutexUnlock is always enabled + + case Type::MUTEX_WAIT: + // Only an Unlock can be dependent with a Wait + // and in this case, that Unlock enabled the wait + // Not reversible + return false; + default: + xbt_die("Unexpected transition type %s", to_c_str(type_)); + } +} + } // namespace simgrid::mc diff --git a/src/mc/transition/TransitionSynchro.hpp b/src/mc/transition/TransitionSynchro.hpp index a4ea7e3ab1..d8b7d030eb 100644 --- a/src/mc/transition/TransitionSynchro.hpp +++ b/src/mc/transition/TransitionSynchro.hpp @@ -19,6 +19,7 @@ public: std::string to_string(bool verbose) const override; BarrierTransition(aid_t issuer, int times_considered, Type type, std::stringstream& stream); bool depends(const Transition* other) const override; + bool reversible_race(const Transition* other) const override; }; class MutexTransition : public Transition { @@ -29,6 +30,7 @@ public: std::string to_string(bool verbose) const override; MutexTransition(aid_t issuer, int times_considered, Type type, std::stringstream& stream); bool depends(const Transition* other) const override; + bool reversible_race(const Transition* other) const override; uintptr_t get_mutex() const { return this->mutex_; } aid_t get_owner() const { return this->owner_; } @@ -43,6 +45,8 @@ public: std::string to_string(bool verbose) const override; SemaphoreTransition(aid_t issuer, int times_considered, Type type, std::stringstream& stream); bool depends(const Transition* other) const override; + bool reversible_race(const Transition* other) const override; + int get_capacity() const { return capacity_; } }; diff --git a/tools/cmake/DefinePackages.cmake b/tools/cmake/DefinePackages.cmake index 2935cf4932..c28b7aa134 100644 --- a/tools/cmake/DefinePackages.cmake +++ b/tools/cmake/DefinePackages.cmake @@ -540,8 +540,6 @@ set(MC_SRC_STATELESS src/mc/explo/odpor/Execution.cpp src/mc/explo/odpor/Execution.hpp - src/mc/explo/odpor/ReversibleRaceCalculator.cpp - src/mc/explo/odpor/ReversibleRaceCalculator.hpp src/mc/explo/odpor/WakeupTree.cpp src/mc/explo/odpor/WakeupTree.hpp src/mc/explo/odpor/WakeupTreeIterator.cpp