src/mc/explo/udpor/ExtensionSetCalculator.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/udpor/ExtensionSetCalculator.hpp"
   7 #include "src/mc/explo/udpor/Configuration.hpp"
   8 #include "src/mc/explo/udpor/History.hpp"
   9 #include "src/mc/explo/udpor/Unfolding.hpp"
  10
  11 #include <functional>
  12 #include <unordered_map>
  13 #include <xbt/asserts.h>
  14 #include <xbt/ex.h>
  15
  16 using namespace simgrid::mc;
  17
  18 namespace simgrid::mc::udpor {
  19
  20 EventSet ExtensionSetCalculator::partially_extend(const Configuration& C, Unfolding* U,
  21                                                   const std::shared_ptr<Transition> action)
  22 {
  23   using Action     = Transition::Type;
  24   using Handler    = std::function<EventSet(const Configuration&, Unfolding*, const std::shared_ptr<Transition>)>;
  25   using HandlerMap = std::unordered_map<Action, Handler>;
  26
  27   const static HandlerMap handlers =
  28       HandlerMap{{Action::COMM_ASYNC_RECV, &ExtensionSetCalculator::partially_extend_CommRecv},
  29                  {Action::COMM_ASYNC_SEND, &ExtensionSetCalculator::partially_extend_CommSend},
  30                  {Action::COMM_WAIT, &ExtensionSetCalculator::partially_extend_CommWait}};
  31
  32   if (const auto handler = handlers.find(action->type_); handler != handlers.end()) {
  33     return handler->second(C, U, std::move(action));
  34   } else {
  35     xbt_assert(false,
  36                "There is currently no specialized computation for the transition "
  37                "'%s' for computing extension sets in UDPOR, so the model checker cannot "
  38                "determine how to proceed. Please submit a bug report requesting "
  39                "that the transition be supported in SimGrid using UDPOR and consider "
  40                "using the other model-checking algorithms supported by SimGrid instead "
  41                "in the meantime",
  42                action->to_string().c_str());
  43     DIE_IMPOSSIBLE;
  44   }
  45 }
  46
  47 EventSet ExtensionSetCalculator::partially_extend_CommSend(const Configuration& C, Unfolding* U,
  48                                                            const std::shared_ptr<Transition> action)
  49 {
  50   EventSet exC;
  51
  52   const auto send_action        = std::static_pointer_cast<CommSendTransition>(std::move(action));
  53   const auto pre_event_a_C      = C.pre_event(send_action->aid_);
  54   const unsigned sender_mailbox = send_action->get_mailbox();
  55
  56   // 1. Create `e' := <a, config(preEvt(a, C))>` and add `e'` to `ex(C)`
  57   // NOTE: If `preEvt(a, C)` doesn't exist, we're effectively asking
  58   // about `config({})`
  59   if (pre_event_a_C.has_value()) {
  60     const auto e_prime = U->discover_event(EventSet({pre_event_a_C.value()}), send_action);
  61     exC.insert(e_prime);
  62   } else {
  63     const auto e_prime = U->discover_event(EventSet(), send_action);
  64     exC.insert(e_prime);
  65   }
  66
  67   // 2. foreach e ∈ C s.t. λ(e) ∈ {AsyncSend(m, _), TestAny(Com)} where
  68   // Com contains a matching c' = AsyncReceive(m, _) with a
  69   for (const auto e : C) {
  70     const bool transition_type_check = [&]() {
  71       if (const auto* async_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
  72           async_send != nullptr) {
  73         return async_send->get_mailbox() == sender_mailbox;
  74       }
  75       // TODO: Add `TestAny` dependency
  76       return false;
  77     }();
  78
  79     if (transition_type_check) {
  80       const EventSet K = EventSet({e, pre_event_a_C.value_or(e)}).get_largest_maximal_subset();
  81
  82       // TODO: Check D_K(a, lambda(e))
  83       if (true) {
  84         const auto e_prime = U->discover_event(std::move(K), send_action);
  85         exC.insert(e_prime);
  86       }
  87     }
  88   }
  89
  90   // TODO: Add `TestAny` dependency case
  91   return exC;
  92 }
  93
  94 EventSet ExtensionSetCalculator::partially_extend_CommRecv(const Configuration& C, Unfolding* U,
  95                                                            const std::shared_ptr<Transition> action)
  96 {
  97   EventSet exC;
  98
  99   // TODO: if this is the first action by the actor, no such previous event exists.
 100   // How do we react here? Do we say we're dependent with the root event?
 101   const auto recv_action      = std::static_pointer_cast<CommRecvTransition>(std::move(action));
 102   const unsigned recv_mailbox = recv_action->get_mailbox();
 103   const auto pre_event_a_C    = C.pre_event(recv_action->aid_);
 104
 105   // 1. Create `e' := <a, config(preEvt(a, C))>` and add `e'` to `ex(C)`
 106   if (pre_event_a_C.has_value()) {
 107     const auto e_prime = U->discover_event(EventSet({pre_event_a_C.value()}), recv_action);
 108     exC.insert(e_prime);
 109   } else {
 110     const auto e_prime = U->discover_event(EventSet(), recv_action);
 111     exC.insert(e_prime);
 112   }
 113
 114   // 2. foreach e ∈ C s.t. λ(e) ∈ {AsyncSend(m, _), TestAny(Com)} where
 115   // Com contains a matching c' = AsyncReceive(m, _) with a
 116   for (const auto e : C) {
 117     const bool transition_type_check = [&]() {
 118       if (const auto* async_recv = dynamic_cast<const CommRecvTransition*>(e->get_transition());
 119           async_recv != nullptr && async_recv->get_mailbox() == recv_mailbox) {
 120         return true;
 121       }
 122       // TODO: Add `TestAny` dependency
 123       return false;
 124     }();
 125
 126     if (transition_type_check) {
 127       const EventSet K = EventSet({e, pre_event_a_C.value_or(e)}).get_largest_maximal_subset();
 128
 129       // TODO: Check D_K(a, lambda(e))
 130       if (true) {
 131         const auto e_prime = U->discover_event(std::move(K), recv_action);
 132         exC.insert(e_prime);
 133       }
 134     }
 135   }
 136
 137   // TODO: Add `TestAny` dependency case
 138   return exC;
 139 }
 140
 141 EventSet ExtensionSetCalculator::partially_extend_CommWait(const Configuration& C, Unfolding* U,
 142                                                            std::shared_ptr<Transition> action)
 143 {
 144   EventSet exC;
 145
 146   const auto wait_action   = std::static_pointer_cast<CommWaitTransition>(std::move(action));
 147   const auto wait_comm     = wait_action->get_comm();
 148   const auto pre_event_a_C = C.pre_event(wait_action->aid_);
 149
 150   // Determine the _issuer_ of the communication of the `CommWait` event
 151   // in `C`. The issuer of the `CommWait` in `C` is the event in `C`
 152   // whose transition is the `CommRecv` or `CommSend` whose resulting
 153   // communication this `CommWait` waits on
 154   const auto issuer = std::find_if(C.begin(), C.end(), [&](const UnfoldingEvent* e) {
 155     if (const CommRecvTransition* e_issuer_receive = dynamic_cast<const CommRecvTransition*>(e->get_transition());
 156         e_issuer_receive != nullptr) {
 157       return e_issuer_receive->aid_ == wait_action->aid_ && wait_comm == e_issuer_receive->get_comm();
 158     }
 159
 160     if (const CommSendTransition* e_issuer_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
 161         e_issuer_send != nullptr) {
 162       return e_issuer_send->aid_ == wait_action->aid_ && wait_comm == e_issuer_send->get_comm();
 163     }
 164
 165     return false;
 166   });
 167   xbt_assert(issuer != C.end(),
 168              "Invariant violation! A (supposedly) enabled `CommWait` transition "
 169              "waiting on commiunication %lu should not be enabled: the receive/send "
 170              "transition which generated the communication is not an action taken "
 171              "to reach state(C) (the state of the configuration), which should "
 172              "be an impossibility if `%s` is enabled. Please report this as "
 173              "a bug in SimGrid's UDPOR implementation",
 174              wait_action->get_comm(), wait_action->to_string(false).c_str());
 175   const UnfoldingEvent* e_issuer = *issuer;
 176   const History e_issuer_history(e_issuer);
 177
 178   // 1. if `a` is enabled at state(config({preEvt(a,C)})), then
 179   // create `e' := <a, config({preEvt(a,C)})>` and add `e'` to `ex(C)`
 180   //
 181   // First, if `pre_event_a_C == std::nullopt`, then there is nothing to
 182   // do: `CommWait` will never be enabled in the empty configuration (at
 183   // least two actions must be executed before)
 184   if (pre_event_a_C.has_value(); const auto unwrapped_pre_event = pre_event_a_C.value()) {
 185     // A necessary condition is that the issuer be present in
 186     // config({preEvt(a, C)}); otherwise, the `CommWait` could not
 187     // be enabled since the communication on which it waits would not
 188     // have been created for it!
 189     if (const auto config_pre_event = History(unwrapped_pre_event); config_pre_event.contains(e_issuer)) {
 190       // If the issuer is a `CommRecv` (resp. `CommSend`), then we check that there
 191       // are at least as many `CommSend` (resp. `CommRecv`) transitions in `config_pre_event`
 192       // as needed to reach the receive/send number that is `issuer`.
 193       // ...
 194       // ...
 195       if (const CommRecvTransition* e_issuer_receive =
 196               dynamic_cast<const CommRecvTransition*>(e_issuer->get_transition());
 197           e_issuer_receive != nullptr) {
 198         const unsigned issuer_mailbox = e_issuer_receive->get_mailbox();
 199
 200         // Check from the config -> how many sends have there been
 201         const unsigned send_position =
 202             std::count_if(config_pre_event.begin(), config_pre_event.end(), [=](const auto e) {
 203               const CommSendTransition* e_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
 204               if (e_send != nullptr) {
 205                 return e_send->get_mailbox() == issuer_mailbox;
 206               }
 207               return false;
 208             });
 209
 210         // Check from e_issuer -> what place is the issuer in?
 211         const unsigned receive_position =
 212             std::count_if(e_issuer_history.begin(), e_issuer_history.end(), [=](const auto e) {
 213               const CommRecvTransition* e_receive = dynamic_cast<const CommRecvTransition*>(e->get_transition());
 214               if (e_receive != nullptr) {
 215                 return e_receive->get_mailbox() == issuer_mailbox;
 216               }
 217               return false;
 218             });
 219
 220         if (send_position >= receive_position) {
 221           exC.insert(U->discover_event(EventSet({unwrapped_pre_event}), wait_action));
 222         }
 223
 224       } else if (const CommSendTransition* e_issuer_send =
 225                      dynamic_cast<const CommSendTransition*>(e_issuer->get_transition());
 226                  e_issuer_send != nullptr) {
 227         const unsigned issuer_mailbox = e_issuer_send->get_mailbox();
 228
 229         // Check from e_issuer -> what place is the issuer in?
 230         const unsigned send_position =
 231             std::count_if(e_issuer_history.begin(), e_issuer_history.end(), [=](const auto e) {
 232               const CommSendTransition* e_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
 233               if (e_send != nullptr) {
 234                 return e_send->get_mailbox() == issuer_mailbox;
 235               }
 236               return false;
 237             });
 238
 239         // Check from the config -> how many sends have there been
 240         const unsigned receive_position =
 241             std::count_if(config_pre_event.begin(), config_pre_event.end(), [=](const auto e) {
 242               const CommRecvTransition* e_receive = dynamic_cast<const CommRecvTransition*>(e->get_transition());
 243               if (e_receive != nullptr) {
 244                 return e_receive->get_mailbox() == issuer_mailbox;
 245               }
 246               return false;
 247             });
 248
 249         if (send_position <= receive_position) {
 250           exC.insert(U->discover_event(EventSet({unwrapped_pre_event}), wait_action));
 251         }
 252
 253       } else {
 254         xbt_assert(false,
 255                    "The transition which created the communication on which `%s` waits "
 256                    "is neither an async send nor an async receive. The current UDPOR "
 257                    "implementation does not know how to check if `CommWait` is enabled in "
 258                    "this case. Was a new transition added?",
 259                    e_issuer->get_transition()->to_string().c_str());
 260       }
 261     }
 262   }
 263
 264   // 3. foreach event e in C do
 265   for (const auto e : C) {
 266     if (const CommSendTransition* e_issuer_send = dynamic_cast<const CommSendTransition*>(e_issuer->get_transition());
 267         e_issuer_send != nullptr) {
 268       // If the provider of the communication for `CommWait` is a
 269       // `CommSend(m)`, then we only care about `e` if `λ(e) == `CommRecv(m)`.
 270       // All other actions would be independent with the wait action (including
 271       // another `CommSend` to the same mailbox: `CommWait` is "waiting" for its
 272       // corresponding receive action)
 273       if (e->get_transition()->type_ != Transition::Type::COMM_ASYNC_RECV) {
 274         continue;
 275       }
 276
 277       const auto issuer_mailbox        = e_issuer_send->get_mailbox();
 278       const CommRecvTransition* e_recv = dynamic_cast<const CommRecvTransition*>(e->get_transition());
 279       if (e_recv->get_mailbox() != issuer_mailbox) {
 280         continue;
 281       }
 282
 283       // If the `issuer` is not in `config(K)`, this implies that
 284       // `WaitAny()` is always disabled in `config(K)`; hence, it
 285       // is independent of any transition in `config(K)` (according
 286       // to formal definition of independence)
 287       const EventSet K    = EventSet({e, pre_event_a_C.value_or(e)});
 288       const auto config_K = History(K);
 289       if (not config_K.contains(e_issuer)) {
 290         continue;
 291       }
 292
 293       // TODO: Compute the send and receive positions
 294
 295       // What send # is the issuer
 296       const unsigned send_position = std::count_if(e_issuer_history.begin(), e_issuer_history.end(), [=](const auto e) {
 297         const CommSendTransition* e_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
 298         if (e_send != nullptr) {
 299           return e_send->get_mailbox() == issuer_mailbox;
 300         }
 301         return false;
 302       });
 303
 304       // What receive # is the event `e`?
 305       const unsigned receive_position = std::count_if(config_K.begin(), config_K.end(), [=](const auto e) {
 306         const CommRecvTransition* e_receive = dynamic_cast<const CommRecvTransition*>(e->get_transition());
 307         if (e_receive != nullptr) {
 308           return e_receive->get_mailbox() == issuer_mailbox;
 309         }
 310         return false;
 311       });
 312
 313       if (send_position == receive_position) {
 314         exC.insert(U->discover_event(std::move(K), wait_action));
 315       }
 316
 317     } else if (const CommRecvTransition* e_issuer_recv =
 318                    dynamic_cast<const CommRecvTransition*>(e_issuer->get_transition());
 319                e_issuer_recv != nullptr) {
 320       // If the provider of the communication for `CommWait` is a
 321       // `CommRecv(m)`, then we only care about `e` if `λ(e) == `CommSend(m)`.
 322       // All other actions would be independent with the wait action (including
 323       // another `CommRecv` to the same mailbox: `CommWait` is "waiting" for its
 324       // corresponding send action)
 325       if (e->get_transition()->type_ != Transition::Type::COMM_ASYNC_SEND) {
 326         continue;
 327       }
 328
 329       const auto issuer_mailbox        = e_issuer_recv->get_mailbox();
 330       const CommSendTransition* e_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
 331       if (e_send->get_mailbox() != issuer_mailbox) {
 332         continue;
 333       }
 334
 335       // If the `issuer` is not in `config(K)`, this implies that
 336       // `WaitAny()` is always disabled in `config(K)`; hence, it
 337       // is independent of any transition in `config(K)` (according
 338       // to formal definition of independence)
 339       const EventSet K    = EventSet({e, pre_event_a_C.value_or(e)});
 340       const auto config_K = History(K);
 341       if (not config_K.contains(e_issuer)) {
 342         continue;
 343       }
 344
 345       // What receive # is the event `e`?
 346       const unsigned send_position = std::count_if(config_K.begin(), config_K.end(), [=](const auto e) {
 347         const CommSendTransition* e_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
 348         if (e_send != nullptr) {
 349           return e_send->get_mailbox() == issuer_mailbox;
 350         }
 351         return false;
 352       });
 353
 354       // What send # is the issuer
 355       const unsigned receive_position =
 356           std::count_if(e_issuer_history.begin(), e_issuer_history.end(), [=](const auto e) {
 357             const CommRecvTransition* e_receive = dynamic_cast<const CommRecvTransition*>(e->get_transition());
 358             if (e_receive != nullptr) {
 359               return e_receive->get_mailbox() == issuer_mailbox;
 360             }
 361             return false;
 362           });
 363
 364       if (send_position == receive_position) {
 365         exC.insert(U->discover_event(std::move(K), wait_action));
 366       }
 367     }
 368   }
 369
 370   return exC;
 371 }
 372
 373 EventSet ExtensionSetCalculator::partially_extend_CommTest(const Configuration& C, Unfolding* U,
 374                                                            std::shared_ptr<Transition> test_action)
 375 {
 376   return EventSet();
 377 }
 378
 379 } // namespace simgrid::mc::udpor