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 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_odpor_reversible_race, mc_dfs, "ODPOR exploration algorithm of the model-checker");
  15
  16 namespace simgrid::mc::odpor {
  17
  18 /**
  19    The reversible race detector should only be used if we already have the assumption
  20    e1 <* e2 (see Source set: a foundation for ODPOR). In particular this means that :
  21    - e1 -->_E e2
  22    - proc(e1) != proc(e2)
  23    - there is no event e3 s.t. e1 --> e3 --> e2
  24 */
  25
  26 bool ReversibleRaceCalculator::is_race_reversible(const Execution& E, Execution::EventHandle e1,
  27                                                   Execution::EventHandle e2)
  28 {
  29   using Action     = Transition::Type;
  30   using Handler    = std::function<bool(const Execution&, Execution::EventHandle, const Transition*)>;
  31   using HandlerMap = std::unordered_map<Action, Handler>;
  32
  33   const static HandlerMap handlers = {
  34       {Action::ACTOR_JOIN, &ReversibleRaceCalculator::is_race_reversible_ActorJoin},
  35       {Action::BARRIER_ASYNC_LOCK, &ReversibleRaceCalculator::is_race_reversible_BarrierAsyncLock},
  36       {Action::BARRIER_WAIT, &ReversibleRaceCalculator::is_race_reversible_BarrierWait},
  37       {Action::COMM_ASYNC_SEND, &ReversibleRaceCalculator::is_race_reversible_CommSend},
  38       {Action::COMM_ASYNC_RECV, &ReversibleRaceCalculator::is_race_reversible_CommRecv},
  39       {Action::COMM_TEST, &ReversibleRaceCalculator::is_race_reversible_CommTest},
  40       {Action::COMM_WAIT, &ReversibleRaceCalculator::is_race_reversible_CommWait},
  41       {Action::MUTEX_ASYNC_LOCK, &ReversibleRaceCalculator::is_race_reversible_MutexAsyncLock},
  42       {Action::MUTEX_TEST, &ReversibleRaceCalculator::is_race_reversible_MutexTest},
  43       {Action::MUTEX_TRYLOCK, &ReversibleRaceCalculator::is_race_reversible_MutexTrylock},
  44       {Action::MUTEX_UNLOCK, &ReversibleRaceCalculator::is_race_reversible_MutexUnlock},
  45       {Action::MUTEX_WAIT, &ReversibleRaceCalculator::is_race_reversible_MutexWait},
  46       {Action::OBJECT_ACCESS, &ReversibleRaceCalculator::is_race_reversible_ObjectAccess},
  47       {Action::RANDOM, &ReversibleRaceCalculator::is_race_reversible_Random},
  48       {Action::SEM_ASYNC_LOCK, &ReversibleRaceCalculator::is_race_reversible_SemAsyncLock},
  49       {Action::SEM_UNLOCK, &ReversibleRaceCalculator::is_race_reversible_SemUnlock},
  50       {Action::SEM_WAIT, &ReversibleRaceCalculator::is_race_reversible_SemWait},
  51       {Action::TESTANY, &ReversibleRaceCalculator::is_race_reversible_TestAny},
  52       {Action::WAITANY, &ReversibleRaceCalculator::is_race_reversible_WaitAny}};
  53
  54   const auto* e2_action = E.get_transition_for_handle(e2);
  55   if (const auto handler = handlers.find(e2_action->type_); handler != handlers.end()) {
  56     return handler->second(E, e1, e2_action);
  57   } else {
  58     xbt_die("There is currently no specialized computation for the transition "
  59             "'%s' for computing reversible races in ODPOR, so the model checker cannot "
  60             "determine how to proceed. Please submit a bug report requesting "
  61             "that the transition be supported in SimGrid using ODPPR and consider "
  62             "using the other model-checking algorithms supported by SimGrid instead "
  63             "in the meantime",
  64             e2_action->to_string().c_str());
  65   }
  66 }
  67
  68 bool ReversibleRaceCalculator::is_race_reversible_ActorJoin(const Execution&, Execution::EventHandle /*e1*/,
  69                                                             const Transition* /*e2*/)
  70 {
  71   // ActorJoin races with another event iff its target `T` is the same as
  72   // the actor executing the other transition. Clearly, then, we could not join
  73   // on that actor `T` and then run a transition by `T`, so no race is reversible
  74   return false;
  75 }
  76
  77 bool ReversibleRaceCalculator::is_race_reversible_BarrierAsyncLock(const Execution&, Execution::EventHandle /*e1*/,
  78                                                                    const Transition* /*e2*/)
  79 {
  80   // BarrierAsyncLock is always enabled
  81   return true;
  82 }
  83
  84 bool ReversibleRaceCalculator::is_race_reversible_BarrierWait(const Execution& E, Execution::EventHandle e1,
  85                                                               const Transition* /*e2*/)
  86 {
  87   // If the other event is a barrier lock event, then we
  88   // are not reversible; otherwise we are reversible.
  89   const auto e1_action = E.get_transition_for_handle(e1)->type_;
  90   return e1_action != Transition::Type::BARRIER_ASYNC_LOCK;
  91 }
  92
  93 bool ReversibleRaceCalculator::is_race_reversible_CommRecv(const Execution&, Execution::EventHandle /*e1*/,
  94                                                            const Transition* /*e2*/)
  95 {
  96   // CommRecv is always enabled
  97   return true;
  98 }
  99
 100 bool ReversibleRaceCalculator::is_race_reversible_CommSend(const Execution&, Execution::EventHandle /*e1*/,
 101                                                            const Transition* /*e2*/)
 102 {
 103   // CommSend is always enabled
 104   return true;
 105 }
 106
 107 bool ReversibleRaceCalculator::is_race_reversible_CommWait(const Execution& E, Execution::EventHandle e1,
 108                                                            const Transition* /*e2*/)
 109 {
 110   // If the other event is a communication event, then we
 111   // are not reversible; otherwise we are reversible.
 112   const auto e1_action = E.get_transition_for_handle(e1)->type_;
 113   return e1_action != Transition::Type::COMM_ASYNC_SEND && e1_action != Transition::Type::COMM_ASYNC_RECV;
 114 }
 115
 116 bool ReversibleRaceCalculator::is_race_reversible_CommTest(const Execution&, Execution::EventHandle /*e1*/,
 117                                                            const Transition* /*e2*/)
 118 {
 119   // CommTest is always enabled
 120   return true;
 121 }
 122
 123 bool ReversibleRaceCalculator::is_race_reversible_MutexAsyncLock(const Execution&, Execution::EventHandle /*e1*/,
 124                                                                  const Transition* /*e2*/)
 125 {
 126   // MutexAsyncLock is always enabled
 127   return true;
 128 }
 129
 130 bool ReversibleRaceCalculator::is_race_reversible_MutexTest(const Execution&, Execution::EventHandle /*e1*/,
 131                                                             const Transition* /*e2*/)
 132 {
 133   // MutexTest is always enabled
 134   return true;
 135 }
 136
 137 bool ReversibleRaceCalculator::is_race_reversible_MutexTrylock(const Execution&, Execution::EventHandle /*e1*/,
 138                                                                const Transition* /*e2*/)
 139 {
 140   // MutexTrylock is always enabled
 141   return true;
 142 }
 143
 144 bool ReversibleRaceCalculator::is_race_reversible_MutexUnlock(const Execution&, Execution::EventHandle /*e1*/,
 145                                                               const Transition* /*e2*/)
 146 {
 147   // MutexUnlock is always enabled
 148   return true;
 149 }
 150
 151 bool ReversibleRaceCalculator::is_race_reversible_MutexWait(const Execution& E, Execution::EventHandle e1,
 152                                                             const Transition* /*e2*/)
 153 {
 154   // The only possibilities for e1 to satisfy the pre-condition are :
 155     // - MUTEX_ASYNC_LOCK
 156
 157
 158   const auto e1_action = E.get_transition_for_handle(e1)->type_;
 159   xbt_assert(e1_action == Transition::Type::MUTEX_UNLOCK);
 160   return e1_action != Transition::Type::MUTEX_ASYNC_LOCK && e1_action != Transition::Type::MUTEX_UNLOCK;
 161 }
 162
 163 bool ReversibleRaceCalculator::is_race_reversible_SemAsyncLock(const Execution&, Execution::EventHandle /*e1*/,
 164                                                                const Transition* /*e2*/)
 165 {
 166   // SemAsyncLock is always enabled
 167   return true;
 168 }
 169
 170 bool ReversibleRaceCalculator::is_race_reversible_SemUnlock(const Execution&, Execution::EventHandle /*e1*/,
 171                                                             const Transition* /*e2*/)
 172 {
 173   // SemUnlock is always enabled
 174   return true;
 175 }
 176
 177 bool ReversibleRaceCalculator::is_race_reversible_SemWait(const Execution&, Execution::EventHandle /*e1*/,
 178                                                           const Transition* /*e2*/)
 179 {
 180   // TODO: Get the semantics correct here
 181     // Certainement qu'il suffit de considérer les SemUnlock. ⋀ a priori,
 182     // il doit même suffir de considérer le cas où leur capacity après execution est <=1
 183     // ces cas disent qu'avant éxecution la capacity était de 0. Donc aucune chance de pouvoir
 184     // wait avant le unlock.
 185   return false;
 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 false;
 215 }
 216
 217 } // namespace simgrid::mc::odpor