src/mc/explo/odpor/ReversibleRaceCalculator.cpp

   1 /* Copyright (c) 2008-2023. The SimGrid Team. All rights reserved.          */
   2
   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. */
   5
   6 #include "src/mc/explo/odpor/ReversibleRaceCalculator.hpp"
   7 #include "src/mc/explo/odpor/Execution.hpp"
   8
   9 #include <functional>
  10 #include <unordered_map>
  11 #include <xbt/asserts.h>
  12 #include <xbt/ex.h>
  13
  14 namespace simgrid::mc::odpor {
  15
  16 bool ReversibleRaceCalculator::is_race_reversible(const Execution& E, Execution::EventHandle e1,
  17                                                   Execution::EventHandle e2)
  18 {
  19   using Action     = Transition::Type;
  20   using Handler    = std::function<bool(const Execution&, Execution::EventHandle, const Transition*)>;
  21   using HandlerMap = std::unordered_map<Action, Handler>;
  22
  23   const static HandlerMap handlers =
  24       HandlerMap{{Action::ACTOR_JOIN, &ReversibleRaceCalculator::is_race_reversible_ActorJoin},
  25                  {Action::BARRIER_ASYNC_LOCK, &ReversibleRaceCalculator::is_race_reversible_BarrierAsyncLock},
  26                  {Action::BARRIER_WAIT, &ReversibleRaceCalculator::is_race_reversible_BarrierWait},
  27                  {Action::COMM_ASYNC_SEND, &ReversibleRaceCalculator::is_race_reversible_CommSend},
  28                  {Action::COMM_ASYNC_RECV, &ReversibleRaceCalculator::is_race_reversible_CommRecv},
  29                  {Action::COMM_TEST, &ReversibleRaceCalculator::is_race_reversible_CommTest},
  30                  {Action::COMM_WAIT, &ReversibleRaceCalculator::is_race_reversible_CommWait},
  31                  {Action::MUTEX_ASYNC_LOCK, &ReversibleRaceCalculator::is_race_reversible_MutexAsyncLock},
  32                  {Action::MUTEX_TEST, &ReversibleRaceCalculator::is_race_reversible_MutexTest},
  33                  {Action::MUTEX_TRYLOCK, &ReversibleRaceCalculator::is_race_reversible_MutexTrylock},
  34                  {Action::MUTEX_UNLOCK, &ReversibleRaceCalculator::is_race_reversible_MutexUnlock},
  35                  {Action::MUTEX_WAIT, &ReversibleRaceCalculator::is_race_reversible_MutexWait},
  36                  {Action::OBJECT_ACCESS, &ReversibleRaceCalculator::is_race_reversible_ObjectAccess},
  37                  {Action::RANDOM, &ReversibleRaceCalculator::is_race_reversible_Random},
  38                  {Action::SEM_ASYNC_LOCK, &ReversibleRaceCalculator::is_race_reversible_SemAsyncLock},
  39                  {Action::SEM_UNLOCK, &ReversibleRaceCalculator::is_race_reversible_SemUnlock},
  40                  {Action::SEM_WAIT, &ReversibleRaceCalculator::is_race_reversible_SemWait},
  41                  {Action::TESTANY, &ReversibleRaceCalculator::is_race_reversible_TestAny},
  42                  {Action::WAITANY, &ReversibleRaceCalculator::is_race_reversible_WaitAny}};
  43
  44   const auto e2_action = E.get_transition_for_handle(e2);
  45   if (const auto handler = handlers.find(e2_action->type_); handler != handlers.end()) {
  46     return handler->second(E, e1, e2_action);
  47   } else {
  48     xbt_die("There is currently no specialized computation for the transition "
  49             "'%s' for computing reversible races in ODPOR, so the model checker cannot "
  50             "determine how to proceed. Please submit a bug report requesting "
  51             "that the transition be supported in SimGrid using ODPPR and consider "
  52             "using the other model-checking algorithms supported by SimGrid instead "
  53             "in the meantime",
  54             e2_action->to_string().c_str());
  55   }
  56 }
  57
  58 bool ReversibleRaceCalculator::is_race_reversible_ActorJoin(const Execution&, Execution::EventHandle e1,
  59                                                             const Transition* e2)
  60 {
  61   // ActorJoin races with another event iff its target `T` is the same as
  62   // the actor executing the other transition. Clearly, then, we could not join
  63   // on that actor `T` and then run a transition by `T`, so no race is reversible
  64   return false;
  65 }
  66
  67 bool ReversibleRaceCalculator::is_race_reversible_BarrierAsyncLock(const Execution&, Execution::EventHandle e1,
  68                                                                    const Transition* e2)
  69 {
  70   // BarrierAsyncLock is always enabled
  71   return true;
  72 }
  73
  74 bool ReversibleRaceCalculator::is_race_reversible_BarrierWait(const Execution& E, Execution::EventHandle e1,
  75                                                               const Transition* e2)
  76 {
  77   // If the other event is a barrier lock event, then we
  78   // are not reversible; otherwise we are reversible.
  79   const auto e1_action = E.get_transition_for_handle(e1)->type_;
  80   return e1_action != Transition::Type::BARRIER_ASYNC_LOCK;
  81 }
  82
  83 bool ReversibleRaceCalculator::is_race_reversible_CommRecv(const Execution&, Execution::EventHandle e1,
  84                                                            const Transition* e2)
  85 {
  86   // CommRecv is always enabled
  87   return true;
  88 }
  89
  90 bool ReversibleRaceCalculator::is_race_reversible_CommSend(const Execution&, Execution::EventHandle e1,
  91                                                            const Transition* e2)
  92 {
  93   // CommSend is always enabled
  94   return true;
  95 }
  96
  97 bool ReversibleRaceCalculator::is_race_reversible_CommWait(const Execution& E, Execution::EventHandle e1,
  98                                                            const Transition* e2)
  99 {
 100   // If the other event is a communication event, then we
 101   // are not reversible; otherwise we are reversible.
 102   const auto e1_action = E.get_transition_for_handle(e1)->type_;
 103   return e1_action != Transition::Type::COMM_ASYNC_SEND and e1_action != Transition::Type::COMM_ASYNC_RECV;
 104 }
 105
 106 bool ReversibleRaceCalculator::is_race_reversible_CommTest(const Execution&, Execution::EventHandle e1,
 107                                                            const Transition* e2)
 108 {
 109   // CommTest is always enabled
 110   return true;
 111 }
 112
 113 bool ReversibleRaceCalculator::is_race_reversible_MutexAsyncLock(const Execution&, Execution::EventHandle e1,
 114                                                                  const Transition* e2)
 115 {
 116   // MutexAsyncLock is always enabled
 117   return true;
 118 }
 119
 120 bool ReversibleRaceCalculator::is_race_reversible_MutexTest(const Execution&, Execution::EventHandle e1,
 121                                                             const Transition* e2)
 122 {
 123   // MutexTest is always enabled
 124   return true;
 125 }
 126
 127 bool ReversibleRaceCalculator::is_race_reversible_MutexTrylock(const Execution&, Execution::EventHandle e1,
 128                                                                const Transition* e2)
 129 {
 130   // MutexTrylock is always enabled
 131   return true;
 132 }
 133
 134 bool ReversibleRaceCalculator::is_race_reversible_MutexUnlock(const Execution&, Execution::EventHandle e1,
 135                                                               const Transition* e2)
 136 {
 137   // MutexUnlock is always enabled
 138   return true;
 139 }
 140
 141 bool ReversibleRaceCalculator::is_race_reversible_MutexWait(const Execution& E, Execution::EventHandle e1,
 142                                                             const Transition* e2)
 143 {
 144   // TODO: Get the semantics correct here
 145   const auto e1_action = E.get_transition_for_handle(e1)->type_;
 146   return e1_action != Transition::Type::MUTEX_ASYNC_LOCK and e1_action != Transition::Type::MUTEX_UNLOCK;
 147 }
 148
 149 bool ReversibleRaceCalculator::is_race_reversible_SemAsyncLock(const Execution&, Execution::EventHandle e1,
 150                                                                const Transition* e2)
 151 {
 152   // SemAsyncLock is always enabled
 153   return true;
 154 }
 155
 156 bool ReversibleRaceCalculator::is_race_reversible_SemUnlock(const Execution&, Execution::EventHandle e1,
 157                                                             const Transition* e2)
 158 {
 159   // SemUnlock is always enabled
 160   return true;
 161 }
 162
 163 bool ReversibleRaceCalculator::is_race_reversible_SemWait(const Execution&, Execution::EventHandle e1,
 164                                                           const Transition* e2)
 165 {
 166   // TODO: Get the semantics correct here
 167   return false;
 168 }
 169
 170 bool ReversibleRaceCalculator::is_race_reversible_ObjectAccess(const Execution&, Execution::EventHandle e1,
 171                                                                const Transition* e2)
 172 {
 173   // Object access is always enabled
 174   return true;
 175 }
 176
 177 bool ReversibleRaceCalculator::is_race_reversible_Random(const Execution&, Execution::EventHandle e1,
 178                                                          const Transition* e2)
 179 {
 180   // Random is always enabled
 181   return true;
 182 }
 183
 184 bool ReversibleRaceCalculator::is_race_reversible_TestAny(const Execution&, Execution::EventHandle e1,
 185                                                           const Transition* e2)
 186 {
 187   // TestAny is always enabled
 188   return true;
 189 }
 190
 191 bool ReversibleRaceCalculator::is_race_reversible_WaitAny(const Execution&, Execution::EventHandle e1,
 192                                                           const Transition* e2)
 193 {
 194   // TODO: We need to check if any of the transitions
 195   // waited on occurred before `e1`
 196   return false;
 197 }
 198
 199 } // namespace simgrid::mc::odpor