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_assert(false,
  49                "There is currently no specialized computation for the transition "
  50                "'%s' for computing reversible races in ODPOR, so the model checker cannot "
  51                "determine how to proceed. Please submit a bug report requesting "
  52                "that the transition be supported in SimGrid using ODPPR and consider "
  53                "using the other model-checking algorithms supported by SimGrid instead "
  54                "in the meantime",
  55                e2_action->to_string().c_str());
  56     DIE_IMPOSSIBLE;
  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 and 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 and 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&, Execution::EventHandle e1,
 166                                                           const Transition* e2)
 167 {
 168   // TODO: Get the semantics correct here
 169   return false;
 170 }
 171
 172 bool ReversibleRaceCalculator::is_race_reversible_ObjectAccess(const Execution&, Execution::EventHandle e1,
 173                                                                const Transition* e2)
 174 {
 175   // Object access is always enabled
 176   return true;
 177 }
 178
 179 bool ReversibleRaceCalculator::is_race_reversible_Random(const Execution&, Execution::EventHandle e1,
 180                                                          const Transition* e2)
 181 {
 182   // Random is always enabled
 183   return true;
 184 }
 185
 186 bool ReversibleRaceCalculator::is_race_reversible_TestAny(const Execution&, Execution::EventHandle e1,
 187                                                           const Transition* e2)
 188 {
 189   // TestAny is always enabled
 190   return true;
 191 }
 192
 193 bool ReversibleRaceCalculator::is_race_reversible_WaitAny(const Execution&, Execution::EventHandle e1,
 194                                                           const Transition* e2)
 195 {
 196   // TODO: We need to check if any of the transitions
 197   // waited on occurred before `e1`
 198   return false;
 199 }
 200
 201 } // namespace simgrid::mc::odpor