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&, Execution::EventHandle, 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* e2_action = E.get_transition_for_handle(e2);
  57   if (const auto handler = handlers.find(e2_action->type_); handler != handlers.end()) {
  58     return handler->second(E, e1, e2_action);
  59   } else {
  60     xbt_die("There is currently no specialized computation for the transition "
  61             "'%s' for computing reversible races in ODPOR, so the model checker cannot "
  62             "determine how to proceed. Please submit a bug report requesting "
  63             "that the transition be supported in SimGrid using ODPPR and consider "
  64             "using the other model-checking algorithms supported by SimGrid instead "
  65             "in the meantime",
  66             e2_action->to_string().c_str());
  67   }
  68 }
  69
  70 bool ReversibleRaceCalculator::is_race_reversible_ActorJoin(const Execution&, Execution::EventHandle /*e1*/,
  71                                                             const Transition* /*e2*/)
  72 {
  73   // ActorJoin races with another event iff its target `T` is the same as
  74   // the actor executing the other transition. Clearly, then, we could not join
  75   // on that actor `T` and then run a transition by `T`, so no race is reversible
  76   return false;
  77 }
  78
  79 bool ReversibleRaceCalculator::is_race_reversible_BarrierAsyncLock(const Execution&, Execution::EventHandle /*e1*/,
  80                                                                    const Transition* /*e2*/)
  81 {
  82   // BarrierAsyncLock is always enabled
  83   return true;
  84 }
  85
  86 bool ReversibleRaceCalculator::is_race_reversible_BarrierWait(const Execution& E, Execution::EventHandle e1,
  87                                                               const Transition* /*e2*/)
  88 {
  89   // If the other event is a barrier lock event, then we
  90   // are not reversible; otherwise we are reversible.
  91   const auto e1_action = E.get_transition_for_handle(e1)->type_;
  92   return e1_action != Transition::Type::BARRIER_ASYNC_LOCK;
  93 }
  94
  95 bool ReversibleRaceCalculator::is_race_reversible_CommRecv(const Execution&, Execution::EventHandle /*e1*/,
  96                                                            const Transition* /*e2*/)
  97 {
  98   // CommRecv is always enabled
  99   return true;
 100 }
 101
 102 bool ReversibleRaceCalculator::is_race_reversible_CommSend(const Execution&, Execution::EventHandle /*e1*/,
 103                                                            const Transition* /*e2*/)
 104 {
 105   // CommSend is always enabled
 106   return true;
 107 }
 108
 109 bool ReversibleRaceCalculator::is_race_reversible_CommWait(const Execution& E, Execution::EventHandle e1,
 110                                                            const Transition* /*e2*/)
 111 {
 112   // If the other event is a communication event, then we
 113   // are not reversible; otherwise we are reversible.
 114   const auto e1_action = E.get_transition_for_handle(e1)->type_;
 115   return e1_action != Transition::Type::COMM_ASYNC_SEND && e1_action != Transition::Type::COMM_ASYNC_RECV;
 116 }
 117
 118 bool ReversibleRaceCalculator::is_race_reversible_CommTest(const Execution&, Execution::EventHandle /*e1*/,
 119                                                            const Transition* /*e2*/)
 120 {
 121   // CommTest is always enabled
 122   return true;
 123 }
 124
 125 bool ReversibleRaceCalculator::is_race_reversible_MutexAsyncLock(const Execution&, Execution::EventHandle /*e1*/,
 126                                                                  const Transition* /*e2*/)
 127 {
 128   // MutexAsyncLock is always enabled
 129   return true;
 130 }
 131
 132 bool ReversibleRaceCalculator::is_race_reversible_MutexTest(const Execution&, Execution::EventHandle /*e1*/,
 133                                                             const Transition* /*e2*/)
 134 {
 135   // MutexTest is always enabled
 136   return true;
 137 }
 138
 139 bool ReversibleRaceCalculator::is_race_reversible_MutexTrylock(const Execution&, Execution::EventHandle /*e1*/,
 140                                                                const Transition* /*e2*/)
 141 {
 142   // MutexTrylock is always enabled
 143   return true;
 144 }
 145
 146 bool ReversibleRaceCalculator::is_race_reversible_MutexUnlock(const Execution&, Execution::EventHandle /*e1*/,
 147                                                               const Transition* /*e2*/)
 148 {
 149   // MutexUnlock is always enabled
 150   return true;
 151 }
 152
 153 bool ReversibleRaceCalculator::is_race_reversible_MutexWait(const Execution& E, Execution::EventHandle e1,
 154                                                             const Transition* /*e2*/)
 155 {
 156   // TODO: for now we over approximate the reversibility
 157
 158   return true;
 159 }
 160
 161 bool ReversibleRaceCalculator::is_race_reversible_SemAsyncLock(const Execution&, Execution::EventHandle /*e1*/,
 162                                                                const Transition* /*e2*/)
 163 {
 164   // SemAsyncLock is always enabled
 165   return true;
 166 }
 167
 168 bool ReversibleRaceCalculator::is_race_reversible_SemUnlock(const Execution&, Execution::EventHandle /*e1*/,
 169                                                             const Transition* /*e2*/)
 170 {
 171   // SemUnlock is always enabled
 172   return true;
 173 }
 174
 175 bool ReversibleRaceCalculator::is_race_reversible_SemWait(const Execution& E, Execution::EventHandle e1,
 176                                                           const Transition* /*e2*/)
 177 {
 178
 179   const auto e1_transition = E.get_transition_for_handle(e1);
 180   if (e1_transition->type_ == Transition::Type::SEM_UNLOCK &&
 181       static_cast<const SemaphoreTransition*>(e1_transition)->get_capacity() <= 1) {
 182     return false;
 183   }
 184   xbt_assert(false, "SEM_WAIT that is dependent with a SEM_UNLOCK should not be reversible. FixMe");
 185   return true;
 186 }
 187
 188 bool ReversibleRaceCalculator::is_race_reversible_ObjectAccess(const Execution&, Execution::EventHandle /*e1*/,
 189                                                                const Transition* /*e2*/)
 190 {
 191   // Object access is always enabled
 192   return true;
 193 }
 194
 195 bool ReversibleRaceCalculator::is_race_reversible_Random(const Execution&, Execution::EventHandle /*e1*/,
 196                                                          const Transition* /*e2*/)
 197 {
 198   // Random is always enabled
 199   return true;
 200 }
 201
 202 bool ReversibleRaceCalculator::is_race_reversible_TestAny(const Execution&, Execution::EventHandle /*e1*/,
 203                                                           const Transition* /*e2*/)
 204 {
 205   // TestAny is always enabled
 206   return true;
 207 }
 208
 209 bool ReversibleRaceCalculator::is_race_reversible_WaitAny(const Execution&, Execution::EventHandle /*e1*/,
 210                                                           const Transition* /*e2*/)
 211 {
 212   // TODO: We need to check if any of the transitions
 213   // waited on occurred before `e1`
 214   return true; // Let's overapproximate to not miss branches
 215 }
 216
 217 } // namespace simgrid::mc::odpor