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