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
#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 <algorithm>
std::unordered_set<Execution::EventHandle> Execution::get_reversible_races_of(EventHandle handle) const
{
std::unordered_set<EventHandle> 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);
}
}
+++ /dev/null
-/* 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 <functional>
-#include <unordered_map>
-#include <xbt/asserts.h>
-#include <xbt/ex.h>
-
-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<bool(const Execution&, const Transition*, const Transition*)>;
- using HandlerMap = std::unordered_map<Action, Handler>;
-
- 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<const SemaphoreTransition*>(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
+++ /dev/null
-/* 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 <memory>
-
-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
#define SIMGRID_MC_TRANSITION_HPP
#include "simgrid/forward.h" // aid_t
+#include "xbt/ex.h"
#include "xbt/utility.hpp" // XBT_DECLARE_ENUM_CLASS
#include <sstream>
* calls.
*/
class Transition {
- /* Textual representation of the transition, to display backtraces */
+ /* Global statistics */
static unsigned long executed_transitions_;
static unsigned long replayed_transitions_;
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) */
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)
{
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
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 */
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
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)
{
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
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
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_); }
};
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)
{
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_)
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_)
{
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_)
{
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
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 */
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_; }
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_; }
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_; }
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
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
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
return aid_ == other->aid_;
} // Independent with any other transition
+ bool reversible_race(const Transition* other) const override;
};
} // namespace simgrid::mc
* 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"
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
{
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<const SemaphoreTransition*>(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)
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
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 {
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_; }
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_; }
};
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
