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