X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/15d31e14a311cc080f5f60d5d57ab6218fb510c0..da64c6383731d10c6174f81b4b6a20ff0ea186ae:/src/mc/explo/udpor/ExtensionSetCalculator.cpp diff --git a/src/mc/explo/udpor/ExtensionSetCalculator.cpp b/src/mc/explo/udpor/ExtensionSetCalculator.cpp index 491ec2d9e5..deeec2367e 100644 --- a/src/mc/explo/udpor/ExtensionSetCalculator.cpp +++ b/src/mc/explo/udpor/ExtensionSetCalculator.cpp @@ -27,20 +27,24 @@ EventSet ExtensionSetCalculator::partially_extend(const Configuration& C, Unfold const static HandlerMap handlers = HandlerMap{{Action::COMM_ASYNC_RECV, &ExtensionSetCalculator::partially_extend_CommRecv}, {Action::COMM_ASYNC_SEND, &ExtensionSetCalculator::partially_extend_CommSend}, - {Action::COMM_WAIT, &ExtensionSetCalculator::partially_extend_CommWait}}; + {Action::COMM_WAIT, &ExtensionSetCalculator::partially_extend_CommWait}, + {Action::COMM_TEST, &ExtensionSetCalculator::partially_extend_CommTest}, + {Action::MUTEX_ASYNC_LOCK, &ExtensionSetCalculator::partially_extend_MutexAsyncLock}, + {Action::MUTEX_UNLOCK, &ExtensionSetCalculator::partially_extend_MutexUnlock}, + {Action::MUTEX_WAIT, &ExtensionSetCalculator::partially_extend_MutexWait}, + {Action::MUTEX_TEST, &ExtensionSetCalculator::partially_extend_MutexTest}, + {Action::ACTOR_JOIN, &ExtensionSetCalculator::partially_extend_ActorJoin}}; if (const auto handler = handlers.find(action->type_); handler != handlers.end()) { return handler->second(C, U, std::move(action)); } else { - xbt_assert(false, - "There is currently no specialized computation for the transition " - "'%s' for computing extension sets in UDPOR, so the model checker cannot " - "determine how to proceed. Please submit a bug report requesting " - "that the transition be supported in SimGrid using UDPOR and consider " - "using the other model-checking algorithms supported by SimGrid instead " - "in the meantime", - action->to_string().c_str()); - DIE_IMPOSSIBLE; + xbt_die("There is currently no specialized computation for the transition " + "'%s' for computing extension sets in UDPOR, so the model checker cannot " + "determine how to proceed. Please submit a bug report requesting " + "that the transition be supported in SimGrid using UDPOR and consider " + "using the other model-checking algorithms supported by SimGrid instead " + "in the meantime", + action->to_string().c_str()); } } @@ -57,15 +61,15 @@ EventSet ExtensionSetCalculator::partially_extend_CommSend(const Configuration& // NOTE: If `preEvt(a, C)` doesn't exist, we're effectively asking // about `config({})` if (pre_event_a_C.has_value()) { - const auto e_prime = U->discover_event(EventSet({pre_event_a_C.value()}), send_action); + const auto* e_prime = U->discover_event(EventSet({pre_event_a_C.value()}), send_action); exC.insert(e_prime); } else { - const auto e_prime = U->discover_event(EventSet(), send_action); + const auto* e_prime = U->discover_event(EventSet(), send_action); exC.insert(e_prime); } // 2. foreach e ∈ C s.t. λ(e) ∈ {AsyncSend(m, _), TestAny(Com)} where - // Com contains a matching c' = AsyncReceive(m, _) with a + // Com contains a matching c' = AsyncReceive(m, _) with `action` for (const auto e : C) { const bool transition_type_check = [&]() { if (const auto* async_send = dynamic_cast(e->get_transition()); @@ -79,11 +83,9 @@ EventSet ExtensionSetCalculator::partially_extend_CommSend(const Configuration& if (transition_type_check) { const EventSet K = EventSet({e, pre_event_a_C.value_or(e)}).get_largest_maximal_subset(); - // TODO: Check D_K(a, lambda(e)) - if (true) { - const auto e_prime = U->discover_event(std::move(K), send_action); - exC.insert(e_prime); - } + // TODO: Check D_K(a, lambda(e)) (only matters in the case of CommTest) + const auto e_prime = U->discover_event(std::move(K), send_action); + exC.insert(e_prime); } } @@ -96,18 +98,16 @@ EventSet ExtensionSetCalculator::partially_extend_CommRecv(const Configuration& { EventSet exC; - // TODO: if this is the first action by the actor, no such previous event exists. - // How do we react here? Do we say we're dependent with the root event? const auto recv_action = std::static_pointer_cast(std::move(action)); const unsigned recv_mailbox = recv_action->get_mailbox(); const auto pre_event_a_C = C.pre_event(recv_action->aid_); // 1. Create `e' := ` and add `e'` to `ex(C)` if (pre_event_a_C.has_value()) { - const auto e_prime = U->discover_event(EventSet({pre_event_a_C.value()}), recv_action); + const auto* e_prime = U->discover_event(EventSet({pre_event_a_C.value()}), recv_action); exC.insert(e_prime); } else { - const auto e_prime = U->discover_event(EventSet(), recv_action); + const auto* e_prime = U->discover_event(EventSet(), recv_action); exC.insert(e_prime); } @@ -126,9 +126,9 @@ EventSet ExtensionSetCalculator::partially_extend_CommRecv(const Configuration& if (transition_type_check) { const EventSet K = EventSet({e, pre_event_a_C.value_or(e)}).get_largest_maximal_subset(); - // TODO: Check D_K(a, lambda(e)) + // TODO: Check D_K(a, lambda(e)) (ony matters in the case of TestAny) if (true) { - const auto e_prime = U->discover_event(std::move(K), recv_action); + const auto* e_prime = U->discover_event(std::move(K), recv_action); exC.insert(e_prime); } } @@ -166,7 +166,7 @@ EventSet ExtensionSetCalculator::partially_extend_CommWait(const Configuration& }); xbt_assert(issuer != C.end(), "Invariant violation! A (supposedly) enabled `CommWait` transition " - "waiting on commiunication %lu should not be enabled: the receive/send " + "waiting on communication %u should not be enabled: the receive/send " "transition which generated the communication is not an action taken " "to reach state(C) (the state of the configuration), which should " "be an impossibility if `%s` is enabled. Please report this as " @@ -181,7 +181,7 @@ EventSet ExtensionSetCalculator::partially_extend_CommWait(const Configuration& // First, if `pre_event_a_C == std::nullopt`, then there is nothing to // do: `CommWait` will never be enabled in the empty configuration (at // least two actions must be executed before) - if (pre_event_a_C.has_value(); const auto unwrapped_pre_event = pre_event_a_C.value()) { + if (pre_event_a_C.has_value(); const auto* unwrapped_pre_event = pre_event_a_C.value()) { // A necessary condition is that the issuer be present in // config({preEvt(a, C)}); otherwise, the `CommWait` could not // be enabled since the communication on which it waits would not @@ -251,20 +251,19 @@ EventSet ExtensionSetCalculator::partially_extend_CommWait(const Configuration& } } else { - xbt_assert(false, - "The transition which created the communication on which `%s` waits " - "is neither an async send nor an async receive. The current UDPOR " - "implementation does not know how to check if `CommWait` is enabled in " - "this case. Was a new transition added?", - e_issuer->get_transition()->to_string().c_str()); + xbt_die("The transition which created the communication on which `%s` waits " + "is neither an async send nor an async receive. The current UDPOR " + "implementation does not know how to check if `CommWait` is enabled in " + "this case. Was a new transition added?", + e_issuer->get_transition()->to_string().c_str()); } } } // 3. foreach event e in C do - for (const auto e : C) { - if (const CommSendTransition* e_issuer_send = dynamic_cast(e_issuer->get_transition()); - e_issuer_send != nullptr) { + if (const CommSendTransition* e_issuer_send = dynamic_cast(e_issuer->get_transition()); + e_issuer_send != nullptr) { + for (const auto e : C) { // If the provider of the communication for `CommWait` is a // `CommSend(m)`, then we only care about `e` if `λ(e) == `CommRecv(m)`. // All other actions would be independent with the wait action (including @@ -290,8 +289,6 @@ EventSet ExtensionSetCalculator::partially_extend_CommWait(const Configuration& continue; } - // TODO: Compute the send and receive positions - // What send # is the issuer const unsigned send_position = std::count_if(e_issuer_history.begin(), e_issuer_history.end(), [=](const auto e) { const CommSendTransition* e_send = dynamic_cast(e->get_transition()); @@ -313,10 +310,11 @@ EventSet ExtensionSetCalculator::partially_extend_CommWait(const Configuration& if (send_position == receive_position) { exC.insert(U->discover_event(std::move(K), wait_action)); } - - } else if (const CommRecvTransition* e_issuer_recv = - dynamic_cast(e_issuer->get_transition()); - e_issuer_recv != nullptr) { + } + } else if (const CommRecvTransition* e_issuer_recv = + dynamic_cast(e_issuer->get_transition()); + e_issuer_recv != nullptr) { + for (const auto e : C) { // If the provider of the communication for `CommWait` is a // `CommRecv(m)`, then we only care about `e` if `λ(e) == `CommSend(m)`. // All other actions would be independent with the wait action (including @@ -365,15 +363,336 @@ EventSet ExtensionSetCalculator::partially_extend_CommWait(const Configuration& exC.insert(U->discover_event(std::move(K), wait_action)); } } + } else { + xbt_die("The transition which created the communication on which `%s` waits " + "is neither an async send nor an async receive. The current UDPOR " + "implementation does not know how to check if `CommWait` is enabled in " + "this case. Was a new transition added?", + e_issuer->get_transition()->to_string().c_str()); } return exC; } EventSet ExtensionSetCalculator::partially_extend_CommTest(const Configuration& C, Unfolding* U, - std::shared_ptr test_action) + std::shared_ptr action) +{ + EventSet exC; + + const auto test_action = std::static_pointer_cast(std::move(action)); + const auto test_comm = test_action->get_comm(); + const auto test_aid = test_action->aid_; + const auto pre_event_a_C = C.pre_event(test_action->aid_); + + // Add the previous event as a dependency (if it's there) + if (pre_event_a_C.has_value()) { + const auto e_prime = U->discover_event(EventSet({pre_event_a_C.value()}), test_action); + exC.insert(e_prime); + } + + // Determine the _issuer_ of the communication of the `CommTest` event + // in `C`. The issuer of the `CommTest` in `C` is the event in `C` + // whose transition is the `CommRecv` or `CommSend` whose resulting + // communication this `CommTest` tests on + const auto issuer = std::find_if(C.begin(), C.end(), [=](const UnfoldingEvent* e) { + if (const CommRecvTransition* e_issuer_receive = dynamic_cast(e->get_transition()); + e_issuer_receive != nullptr) { + return e_issuer_receive->aid_ == test_aid && test_comm == e_issuer_receive->get_comm(); + } + + if (const CommSendTransition* e_issuer_send = dynamic_cast(e->get_transition()); + e_issuer_send != nullptr) { + return e_issuer_send->aid_ == test_aid && test_comm == e_issuer_send->get_comm(); + } + + return false; + }); + xbt_assert(issuer != C.end(), + "An enabled `CommTest` transition (%s) is testing a communication" + "%u not created by a receive/send " + "transition. SimGrid cannot currently handle test actions " + "under which a test is performed on a communication that was " + "not directly created by a receive/send operation of the same actor.", + test_action->to_string(false).c_str(), test_action->get_comm()); + const UnfoldingEvent* e_issuer = *issuer; + const History e_issuer_history(e_issuer); + + // 3. foreach event e in C do + if (const CommSendTransition* e_issuer_send = dynamic_cast(e_issuer->get_transition()); + e_issuer_send != nullptr) { + for (const auto e : C) { + // If the provider of the communication for `CommTest` is a + // `CommSend(m)`, then we only care about `e` if `λ(e) == `CommRecv(m)`. + // All other actions would be independent with the test action (including + // another `CommSend` to the same mailbox: `CommTest` is testing the + // corresponding receive action) + if (e->get_transition()->type_ != Transition::Type::COMM_ASYNC_RECV) { + continue; + } + + const auto issuer_mailbox = e_issuer_send->get_mailbox(); + + if (const CommRecvTransition* e_recv = dynamic_cast(e->get_transition()); + e_recv->get_mailbox() != issuer_mailbox) { + continue; + } + + // If the `issuer` is not in `config(K)`, this implies that + // `CommTest()` is always disabled in `config(K)`; hence, it + // is independent of any transition in `config(K)` (according + // to formal definition of independence) + const EventSet K = EventSet({e, pre_event_a_C.value_or(e)}); + const auto config_K = History(K); + if (not config_K.contains(e_issuer)) { + continue; + } + + // What send # is the issuer + const unsigned send_position = std::count_if(e_issuer_history.begin(), e_issuer_history.end(), [=](const auto e) { + const CommSendTransition* e_send = dynamic_cast(e->get_transition()); + if (e_send != nullptr) { + return e_send->get_mailbox() == issuer_mailbox; + } + return false; + }); + + // What receive # is the event `e`? + const unsigned receive_position = std::count_if(config_K.begin(), config_K.end(), [=](const auto e) { + const CommRecvTransition* e_receive = dynamic_cast(e->get_transition()); + if (e_receive != nullptr) { + return e_receive->get_mailbox() == issuer_mailbox; + } + return false; + }); + + if (send_position == receive_position) { + exC.insert(U->discover_event(std::move(K), test_action)); + } + } + } else if (const CommRecvTransition* e_issuer_recv = + dynamic_cast(e_issuer->get_transition()); + e_issuer_recv != nullptr) { + + for (const auto e : C) { + // If the provider of the communication for `CommTest` is a + // `CommRecv(m)`, then we only care about `e` if `λ(e) == `CommSend(m)`. + // All other actions would be independent with the wait action (including + // another `CommRecv` to the same mailbox: `CommWait` is "waiting" for its + // corresponding send action) + if (e->get_transition()->type_ != Transition::Type::COMM_ASYNC_SEND) { + continue; + } + + const auto issuer_mailbox = e_issuer_recv->get_mailbox(); + const CommSendTransition* e_send = dynamic_cast(e->get_transition()); + if (e_send->get_mailbox() != issuer_mailbox) { + continue; + } + + // If the `issuer` is not in `config(K)`, this implies that + // `WaitAny()` is always disabled in `config(K)`; hence, it + // is independent of any transition in `config(K)` (according + // to formal definition of independence) + const EventSet K = EventSet({e, pre_event_a_C.value_or(e)}); + const auto config_K = History(K); + if (not config_K.contains(e_issuer)) { + continue; + } + + // What receive # is the event `e`? + const unsigned send_position = std::count_if(config_K.begin(), config_K.end(), [=](const auto e) { + const CommSendTransition* e_send = dynamic_cast(e->get_transition()); + if (e_send != nullptr) { + return e_send->get_mailbox() == issuer_mailbox; + } + return false; + }); + + // What send # is the issuer + const unsigned receive_position = + std::count_if(e_issuer_history.begin(), e_issuer_history.end(), [=](const auto e) { + const CommRecvTransition* e_receive = dynamic_cast(e->get_transition()); + if (e_receive != nullptr) { + return e_receive->get_mailbox() == issuer_mailbox; + } + return false; + }); + + if (send_position == receive_position) { + exC.insert(U->discover_event(std::move(K), test_action)); + } + } + } else { + xbt_die("The transition which created the communication on which `%s` waits " + "is neither an async send nor an async receive. The current UDPOR " + "implementation does not know how to check if `CommWait` is enabled in " + "this case. Was a new transition added?", + e_issuer->get_transition()->to_string().c_str()); + } + return exC; +} + +EventSet ExtensionSetCalculator::partially_extend_MutexAsyncLock(const Configuration& C, Unfolding* U, + std::shared_ptr action) { - return EventSet(); + EventSet exC; + const auto mutex_lock = std::static_pointer_cast(std::move(action)); + const auto pre_event_a_C = C.pre_event(mutex_lock->aid_); + + // for each event e in C + // 1. If lambda(e) := pre(a) -> add it. Note that if + // pre_event_a_C.has_value() == false, this implies `C` is + // empty or which we treat as implicitly containing the bottom event + if (pre_event_a_C.has_value()) { + const auto e_prime = U->discover_event(EventSet({pre_event_a_C.value()}), mutex_lock); + exC.insert(e_prime); + } else { + const auto e_prime = U->discover_event(EventSet(), mutex_lock); + exC.insert(e_prime); + } + + // for each event e in C + for (const auto e : C) { + // Check for other locks on the same mutex + if (const MutexTransition* e_mutex = dynamic_cast(e->get_transition()); + e_mutex != nullptr) { + + if (e_mutex->type_ == Transition::Type::MUTEX_ASYNC_LOCK && mutex_lock->get_mutex() == e_mutex->get_mutex()) { + const EventSet K = EventSet({e, pre_event_a_C.value_or(e)}); + exC.insert(U->discover_event(std::move(K), mutex_lock)); + } + } + } + return exC; +} + +EventSet ExtensionSetCalculator::partially_extend_MutexUnlock(const Configuration& C, Unfolding* U, + std::shared_ptr action) +{ + EventSet exC; + const auto mutex_unlock = std::static_pointer_cast(std::move(action)); + const auto pre_event_a_C = C.pre_event(mutex_unlock->aid_); + + // for each event e in C + // 1. If lambda(e) := pre(a) -> add it. Note that if + // pre_event_a_C.has_value() == false, this implies `C` is + // empty or which we treat as implicitly containing the bottom event + if (pre_event_a_C.has_value()) { + const auto e_prime = U->discover_event(EventSet({pre_event_a_C.value()}), mutex_unlock); + exC.insert(e_prime); + } else { + const auto e_prime = U->discover_event(EventSet(), mutex_unlock); + exC.insert(e_prime); + } + + // for each event e in C + for (const auto e : C) { + // Check for MutexTest + if (const MutexTransition* e_mutex = dynamic_cast(e->get_transition()); + e_mutex != nullptr) { + + if (e_mutex->type_ == Transition::Type::MUTEX_TEST || e_mutex->type_ == Transition::Type::MUTEX_WAIT) { + // TODO: Check if dependent or not + // This entails getting information about + // the relative position of the mutex in the queue, which + // again means we need more context... + const EventSet K = EventSet({e, pre_event_a_C.value_or(e)}); + exC.insert(U->discover_event(std::move(K), mutex_unlock)); + } + } + } + return exC; +} + +EventSet ExtensionSetCalculator::partially_extend_MutexWait(const Configuration& C, Unfolding* U, + std::shared_ptr action) +{ + EventSet exC; + const auto mutex_wait = std::static_pointer_cast(std::move(action)); + const auto pre_event_a_C = C.pre_event(mutex_wait->aid_); + + // for each event e in C + // 1. If lambda(e) := pre(a) -> add it. In the case of MutexWait, we also check that the + // actor which is executing the MutexWait is the owner of the mutex + if (pre_event_a_C.has_value() && mutex_wait->get_owner() == mutex_wait->aid_) { + const auto e_prime = U->discover_event(EventSet({pre_event_a_C.value()}), mutex_wait); + exC.insert(e_prime); + } else { + const auto e_prime = U->discover_event(EventSet(), mutex_wait); + exC.insert(e_prime); + } + + // for each event e in C + for (const auto e : C) { + // Check for any unlocks + if (const MutexTransition* e_mutex = dynamic_cast(e->get_transition()); + e_mutex != nullptr && e_mutex->type_ == Transition::Type::MUTEX_UNLOCK) { + // TODO: Check if dependent or not + // This entails getting information about + // the relative position of the mutex in the queue, which + // again means we need more context... + const EventSet K = EventSet({e, pre_event_a_C.value_or(e)}); + exC.insert(U->discover_event(std::move(K), mutex_wait)); + } + } + return exC; +} + +EventSet ExtensionSetCalculator::partially_extend_MutexTest(const Configuration& C, Unfolding* U, + std::shared_ptr action) +{ + EventSet exC; + const auto mutex_test = std::static_pointer_cast(std::move(action)); + const auto pre_event_a_C = C.pre_event(mutex_test->aid_); + + // for each event e in C + // 1. If lambda(e) := pre(a) -> add it. Note that if + // pre_evevnt_a_C.has_value() == false, this implies `C` is + // empty or which we treat as implicitly containing the bottom event + if (pre_event_a_C.has_value()) { + const auto e_prime = U->discover_event(EventSet({pre_event_a_C.value()}), mutex_test); + exC.insert(e_prime); + } else { + const auto e_prime = U->discover_event(EventSet(), mutex_test); + exC.insert(e_prime); + } + + // for each event e in C + for (const auto e : C) { + // Check for any unlocks + if (const MutexTransition* e_mutex = dynamic_cast(e->get_transition()); + e_mutex != nullptr && e_mutex->type_ == Transition::Type::MUTEX_UNLOCK) { + // TODO: Check if dependent or not + // This entails getting information about + // the relative position of the mutex in the queue, which + // again means we need more context... + const EventSet K = EventSet({e, pre_event_a_C.value_or(e)}); + exC.insert(U->discover_event(std::move(K), mutex_test)); + } + } + return exC; +} + +EventSet ExtensionSetCalculator::partially_extend_ActorJoin(const Configuration& C, Unfolding* U, + std::shared_ptr action) +{ + EventSet exC; + + const auto join_action = std::static_pointer_cast(std::move(action)); + const auto pre_event_a_C = C.pre_event(join_action->aid_); + + // Handling ActorJoin is very simple: it is independent with all + // other transitions. Thus the only event it could possibly depend + // on is pre(a, C) or the root + if (pre_event_a_C.has_value()) { + const auto e_prime = U->discover_event(EventSet({pre_event_a_C.value()}), join_action); + exC.insert(e_prime); + } else { + const auto e_prime = U->discover_event(EventSet(), join_action); + exC.insert(e_prime); + } + + return exC; } } // namespace simgrid::mc::udpor