Add remaining handlers to ReversibleRaceCalculator

This commit adds handlers for each type of transition
to ReversibleRaceCalculator which, as the name suggests,
determines whether a reversible race exists between two
events e1 and e2 based on the type of transition found
at e2. The full semantics have not been added for each
type of transition and will need to be added in the future

diff --git a/src/mc/explo/odpor/ReversibleRaceCalculator.cpp b/src/mc/explo/odpor/ReversibleRaceCalculator.cpp
index 42eadb0..68d9ead 100644 (file)
--- a/src/mc/explo/odpor/ReversibleRaceCalculator.cpp
+++ b/src/mc/explo/odpor/ReversibleRaceCalculator.cpp
@@ -21,9 +21,25 @@ bool ReversibleRaceCalculator::is_race_reversible(const Execution& E, Execution:
   using HandlerMap = std::unordered_map<Action, Handler>;
 
   const static HandlerMap handlers =
-      HandlerMap{{Action::COMM_ASYNC_RECV, &ReversibleRaceCalculator::is_race_reversible_CommRecv},
+      HandlerMap{{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_WAIT, &ReversibleRaceCalculator::is_race_reversible_CommWait}};
+                 {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 e2_action = E.get_transition_for_handle(e2);
   if (const auto handler = handlers.find(e2_action->type_); handler != handlers.end()) {
@@ -41,6 +57,31 @@ bool ReversibleRaceCalculator::is_race_reversible(const Execution& E, Execution:
   }
 }
 
+bool ReversibleRaceCalculator::is_race_reversible_ActorJoin(const Execution&, Execution::EventHandle e1,
+                                                            const Transition* e2)
+{
+  // 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&, Execution::EventHandle e1,
+                                                                   const Transition* e2)
+{
+  // BarrierAsyncLock is always enabled
+  return true;
+}
+
+bool ReversibleRaceCalculator::is_race_reversible_BarrierWait(const Execution& E, Execution::EventHandle e1,
+                                                              const Transition* e2)
+{
+  // 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;
+}
+
 bool ReversibleRaceCalculator::is_race_reversible_CommRecv(const Execution&, Execution::EventHandle e1,
                                                            const Transition* e2)
 {
@@ -58,8 +99,8 @@ bool ReversibleRaceCalculator::is_race_reversible_CommSend(const Execution&, Exe
 bool ReversibleRaceCalculator::is_race_reversible_CommWait(const Execution& E, Execution::EventHandle e1,
                                                            const Transition* e2)
 {
-  // If the other event communication event, then we
-  // are not reversible. Otherwise we are reversible.
+  // 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 and e1_action != Transition::Type::COMM_ASYNC_RECV;
 }
@@ -67,6 +108,93 @@ bool ReversibleRaceCalculator::is_race_reversible_CommWait(const Execution& E, E
 bool ReversibleRaceCalculator::is_race_reversible_CommTest(const Execution&, Execution::EventHandle e1,
                                                            const Transition* e2)
 {
+  // CommTest is always enabled
+  return true;
+}
+
+bool ReversibleRaceCalculator::is_race_reversible_MutexAsyncLock(const Execution&, Execution::EventHandle e1,
+                                                                 const Transition* e2)
+{
+  // MutexAsyncLock is always enabled
+  return true;
+}
+
+bool ReversibleRaceCalculator::is_race_reversible_MutexTest(const Execution&, Execution::EventHandle e1,
+                                                            const Transition* e2)
+{
+  // MutexTest is always enabled
+  return true;
+}
+
+bool ReversibleRaceCalculator::is_race_reversible_MutexTrylock(const Execution&, Execution::EventHandle e1,
+                                                               const Transition* e2)
+{
+  // MutexTrylock is always enabled
+  return true;
+}
+
+bool ReversibleRaceCalculator::is_race_reversible_MutexUnlock(const Execution&, Execution::EventHandle e1,
+                                                              const Transition* e2)
+{
+  // MutexUnlock is always enabled
+  return true;
+}
+
+bool ReversibleRaceCalculator::is_race_reversible_MutexWait(const Execution& E, Execution::EventHandle e1,
+                                                            const Transition* e2)
+{
+  // TODO: Get the semantics correct here
+  const auto e1_action = E.get_transition_for_handle(e1)->type_;
+  return e1_action != Transition::Type::MUTEX_ASYNC_LOCK and e1_action != Transition::Type::MUTEX_UNLOCK;
+}
+
+bool ReversibleRaceCalculator::is_race_reversible_SemAsyncLock(const Execution&, Execution::EventHandle e1,
+                                                               const Transition* e2)
+{
+  // SemAsyncLock is always enabled
+  return true;
+}
+
+bool ReversibleRaceCalculator::is_race_reversible_SemUnlock(const Execution&, Execution::EventHandle e1,
+                                                            const Transition* e2)
+{
+  // SemUnlock is always enabled
+  return true;
+}
+
+bool ReversibleRaceCalculator::is_race_reversible_SemWait(const Execution&, Execution::EventHandle e1,
+                                                          const Transition* e2)
+{
+  // TODO: Get the semantics correct here
+  return false;
+}
+
+bool ReversibleRaceCalculator::is_race_reversible_ObjectAccess(const Execution&, Execution::EventHandle e1,
+                                                               const Transition* e2)
+{
+  // Object access is always enabled
+  return true;
+}
+
+bool ReversibleRaceCalculator::is_race_reversible_Random(const Execution&, Execution::EventHandle e1,
+                                                         const Transition* e2)
+{
+  // Random is always enabled
+  return true;
+}
+
+bool ReversibleRaceCalculator::is_race_reversible_TestAny(const Execution&, Execution::EventHandle e1,
+                                                          const Transition* e2)
+{
+  // TestAny is always enabled
+  return true;
+}
+
+bool ReversibleRaceCalculator::is_race_reversible_WaitAny(const Execution&, Execution::EventHandle e1,
+                                                          const Transition* e2)
+{
+  // TODO: We need to check if any of the transitions
+  // waited on occurred before `e1`
   return false;
 }
 

diff --git a/src/mc/explo/odpor/ReversibleRaceCalculator.hpp b/src/mc/explo/odpor/ReversibleRaceCalculator.hpp
index c199724..5135bd2 100644 (file)
--- a/src/mc/explo/odpor/ReversibleRaceCalculator.hpp
+++ b/src/mc/explo/odpor/ReversibleRaceCalculator.hpp
@@ -30,10 +30,25 @@ namespace simgrid::mc::odpor {
  * is only sensible in the context of a race
  */
 struct 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);
 
 public:
   static bool is_race_reversible(const Execution&, Execution::EventHandle e1, Execution::EventHandle e2);