1 /* Copyright (c) 2007-2023. The SimGrid Team. All rights reserved. */
3 /* This program is free software; you can redistribute it and/or modify it
4 * under the terms of the license (GNU LGPL) which comes with this package. */
6 #ifndef SIMGRID_MC_ODPOR_REVERSIBLE_RACE_CALCULATOR_HPP
7 #define SIMGRID_MC_ODPOR_REVERSIBLE_RACE_CALCULATOR_HPP
9 #include "src/mc/explo/odpor/Execution.hpp"
10 #include "src/mc/explo/odpor/odpor_forward.hpp"
11 #include "src/mc/transition/Transition.hpp"
12 #include "src/mc/transition/TransitionActor.hpp"
13 #include "src/mc/transition/TransitionAny.hpp"
14 #include "src/mc/transition/TransitionComm.hpp"
15 #include "src/mc/transition/TransitionObjectAccess.hpp"
16 #include "src/mc/transition/TransitionRandom.hpp"
17 #include "src/mc/transition/TransitionSynchro.hpp"
21 namespace simgrid::mc::odpor {
24 * @brief Computes whether a race between two events
25 * in a given execution is a reversible race.
27 * @note: All of the methods assume that there is
28 * indeed a race between the two events in the
29 * execution; indeed, the question the method answers
30 * is only sensible in the context of a race
32 class ReversibleRaceCalculator final {
33 static bool is_race_reversible_ActorJoin(const Execution&, const Transition* t1, const Transition* t2);
34 static bool is_race_reversible_BarrierAsyncLock(const Execution&, const Transition* t1, const Transition* t2);
35 static bool is_race_reversible_BarrierWait(const Execution&, const Transition* t1, const Transition* t2);
36 static bool is_race_reversible_CommRecv(const Execution&, const Transition* t1, const Transition* t2);
37 static bool is_race_reversible_CommSend(const Execution&, const Transition* t1, const Transition* t2);
38 static bool is_race_reversible_CommWait(const Execution&, const Transition* t1, const Transition* t2);
39 static bool is_race_reversible_CommTest(const Execution&, const Transition* t1, const Transition* t2);
40 static bool is_race_reversible_MutexAsyncLock(const Execution&, const Transition* t1, const Transition* t2);
41 static bool is_race_reversible_MutexTest(const Execution&, const Transition* t1, const Transition* t2);
42 static bool is_race_reversible_MutexTrylock(const Execution&, const Transition* t1, const Transition* t2);
43 static bool is_race_reversible_MutexUnlock(const Execution&, const Transition* t1, const Transition* t2);
44 static bool is_race_reversible_MutexWait(const Execution&, const Transition* t1, const Transition* t2);
45 static bool is_race_reversible_SemAsyncLock(const Execution&, const Transition* t1, const Transition* t2);
46 static bool is_race_reversible_SemUnlock(const Execution&, const Transition* t1, const Transition* t2);
47 static bool is_race_reversible_SemWait(const Execution&, const Transition* t1, const Transition* t2);
48 static bool is_race_reversible_ObjectAccess(const Execution&, const Transition* t1, const Transition* t2);
49 static bool is_race_reversible_Random(const Execution&, const Transition* t1, const Transition* t2);
50 static bool is_race_reversible_TestAny(const Execution&, const Transition* t1, const Transition* t2);
51 static bool is_race_reversible_WaitAny(const Execution&, const Transition* t1, const Transition* t2);
54 static bool is_race_reversible(const Execution&, Execution::EventHandle e1, Execution::EventHandle e2);
57 } // namespace simgrid::mc::odpor