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
 186     // A necessary condition is that the issuer be present in
 187     // config({preEvt(a, C)}); otherwise, the `CommWait` could not
 188     // be enabled since the communication on which it waits would not
 189     // have been created for it!
 190     if (const auto config_pre_event = History(unwrapped_pre_event); config_pre_event.contains(e_issuer)) {
 191       // If the issuer is a `CommRecv` (resp. `CommSend`), then we check that there
 192       // are at least as many `CommSend` (resp. `CommRecv`) transitions in `config_pre_event`
 193       // as needed to reach the receive/send number that is `issuer`.
 194       // ...
 195       // ...
 196       if (const CommRecvTransition* e_issuer_receive =
 197               dynamic_cast<const CommRecvTransition*>(e_issuer->get_transition());
 198           e_issuer_receive != nullptr) {
 199
 200         const unsigned issuer_mailbox = e_issuer_receive->get_mailbox();
 201
 202         // Check from the config -> how many sends have there been
 203         const unsigned send_position =
 204             std::count_if(config_pre_event.begin(), config_pre_event.end(), [=](const auto e) {
 205               const CommSendTransition* e_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
 206               if (e_send != nullptr) {
 207                 return e_send->get_mailbox() == issuer_mailbox;
 208               }
 209               return false;
 210             });
 211
 212         // Check from e_issuer -> what place is the issuer in?
 213         const unsigned receive_position =
 214             std::count_if(e_issuer_history.begin(), e_issuer_history.end(), [=](const auto e) {
 215               const CommRecvTransition* e_receive = dynamic_cast<const CommRecvTransition*>(e->get_transition());
 216               if (e_receive != nullptr) {
 217                 return e_receive->get_mailbox() == issuer_mailbox;
 218               }
 219               return false;
 220             });
 221
 222         if (send_position >= receive_position) {
 223           exC.insert(U->discover_event(EventSet({unwrapped_pre_event}), wait_action));
 224         }
 225
 226       } else if (const CommSendTransition* e_issuer_send =
 227                      dynamic_cast<const CommSendTransition*>(e_issuer->get_transition());
 228                  e_issuer_send != nullptr) {
 229
 230         const unsigned issuer_mailbox = e_issuer_send->get_mailbox();
 231
 232         // Check from e_issuer -> what place is the issuer in?
 233         const unsigned send_position =
 234             std::count_if(e_issuer_history.begin(), e_issuer_history.end(), [=](const auto e) {
 235               const CommSendTransition* e_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
 236               if (e_send != nullptr) {
 237                 return e_send->get_mailbox() == issuer_mailbox;
 238               }
 239               return false;
 240             });
 241
 242         // Check from the config -> how many sends have there been
 243         const unsigned receive_position =
 244             std::count_if(config_pre_event.begin(), config_pre_event.end(), [=](const auto e) {
 245               const CommRecvTransition* e_receive = dynamic_cast<const CommRecvTransition*>(e->get_transition());
 246               if (e_receive != nullptr) {
 247                 return e_receive->get_mailbox() == issuer_mailbox;
 248               }
 249               return false;
 250             });
 251
 252         if (send_position <= receive_position) {
 253           exC.insert(U->discover_event(EventSet({unwrapped_pre_event}), wait_action));
 254         }
 255
 256       } else {
 257         xbt_assert(false,
 258                    "The transition which created the communication on which `%s` waits "
 259                    "is neither an async send nor an async receive. The current UDPOR "
 260                    "implementation does not know how to check if `CommWait` is enabled in "
 261                    "this case. Was a new transition added?",
 262                    e_issuer->get_transition()->to_string().c_str());
 263       }
 264     }
 265   }
 266
 267   // 3. foreach event e in C do
 268   for (const auto e : C) {
 269     if (const CommSendTransition* e_issuer_send = dynamic_cast<const CommSendTransition*>(e_issuer->get_transition());
 270         e_issuer_send != nullptr) {
 271
 272       // If the provider of the communication for `CommWait` is a
 273       // `CommSend(m)`, then we only care about `e` if `λ(e) == `CommRecv(m)`.
 274       // All other actions would be independent with the wait action (including
 275       // another `CommSend` to the same mailbox: `CommWait` is "waiting" for its
 276       // corresponding receive action)
 277       if (e->get_transition()->type_ != Transition::Type::COMM_ASYNC_RECV) {
 278         continue;
 279       }
 280
 281       const auto issuer_mailbox        = e_issuer_send->get_mailbox();
 282       const CommRecvTransition* e_recv = dynamic_cast<const CommRecvTransition*>(e->get_transition());
 283       if (e_recv->get_mailbox() != issuer_mailbox) {
 284         continue;
 285       }
 286
 287       // If the `issuer` is not in `config(K)`, this implies that
 288       // `WaitAny()` is always disabled in `config(K)`; hence, it
 289       // is independent of any transition in `config(K)` (according
 290       // to formal definition of independence)
 291       const EventSet K    = EventSet({e, pre_event_a_C.value_or(e)});
 292       const auto config_K = History(K);
 293       if (not config_K.contains(e_issuer)) {
 294         continue;
 295       }
 296
 297       // TODO: Compute the send and receive positions
 298
 299       // What send # is the issuer
 300       const unsigned send_position = std::count_if(e_issuer_history.begin(), e_issuer_history.end(), [=](const auto e) {
 301         const CommSendTransition* e_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
 302         if (e_send != nullptr) {
 303           return e_send->get_mailbox() == issuer_mailbox;
 304         }
 305         return false;
 306       });
 307
 308       // What receive # is the event `e`?
 309       const unsigned receive_position = std::count_if(config_K.begin(), config_K.end(), [=](const auto e) {
 310         const CommRecvTransition* e_receive = dynamic_cast<const CommRecvTransition*>(e->get_transition());
 311         if (e_receive != nullptr) {
 312           return e_receive->get_mailbox() == issuer_mailbox;
 313         }
 314         return false;
 315       });
 316
 317       if (send_position == receive_position) {
 318         exC.insert(U->discover_event(std::move(K), wait_action));
 319       }
 320
 321     } else if (const CommRecvTransition* e_issuer_recv =
 322                    dynamic_cast<const CommRecvTransition*>(e_issuer->get_transition());
 323                e_issuer_recv != nullptr) {
 324
 325       // If the provider of the communication for `CommWait` is a
 326       // `CommRecv(m)`, then we only care about `e` if `λ(e) == `CommSend(m)`.
 327       // All other actions would be independent with the wait action (including
 328       // another `CommRecv` to the same mailbox: `CommWait` is "waiting" for its
 329       // corresponding send action)
 330       if (e->get_transition()->type_ != Transition::Type::COMM_ASYNC_SEND) {
 331         continue;
 332       }
 333
 334       const auto issuer_mailbox        = e_issuer_recv->get_mailbox();
 335       const CommSendTransition* e_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
 336       if (e_send->get_mailbox() != issuer_mailbox) {
 337         continue;
 338       }
 339
 340       // If the `issuer` is not in `config(K)`, this implies that
 341       // `WaitAny()` is always disabled in `config(K)`; hence, it
 342       // is independent of any transition in `config(K)` (according
 343       // to formal definition of independence)
 344       const EventSet K    = EventSet({e, pre_event_a_C.value_or(e)});
 345       const auto config_K = History(K);
 346       if (not config_K.contains(e_issuer)) {
 347         continue;
 348       }
 349
 350       // What receive # is the event `e`?
 351       const unsigned send_position = std::count_if(config_K.begin(), config_K.end(), [=](const auto e) {
 352         const CommSendTransition* e_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
 353         if (e_send != nullptr) {
 354           return e_send->get_mailbox() == issuer_mailbox;
 355         }
 356         return false;
 357       });
 358
 359       // What send # is the issuer
 360       const unsigned receive_position =
 361           std::count_if(e_issuer_history.begin(), e_issuer_history.end(), [=](const auto e) {
 362             const CommRecvTransition* e_receive = dynamic_cast<const CommRecvTransition*>(e->get_transition());
 363             if (e_receive != nullptr) {
 364               return e_receive->get_mailbox() == issuer_mailbox;
 365             }
 366             return false;
 367           });
 368
 369       if (send_position == receive_position) {
 370         exC.insert(U->discover_event(std::move(K), wait_action));
 371       }
 372     }
 373   }
 374
 375   return exC;
 376 }
 377
 378 EventSet ExtensionSetCalculator::partially_extend_CommTest(const Configuration& C, Unfolding* U,
 379                                                            std::shared_ptr<Transition> test_action)
 380 {
 381   return EventSet();
 382 }
 383
 384 } // namespace simgrid::mc::udpor