X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/45c3a73f3553c8d365f61eaa8445f038db9bdb8f..3cb644bc04ff9dd4da159790850b6bcfda970cf9:/src/mc/explo/udpor/ExtensionSetCalculator.cpp diff --git a/src/mc/explo/udpor/ExtensionSetCalculator.cpp b/src/mc/explo/udpor/ExtensionSetCalculator.cpp index 849337d233..deeec2367e 100644 --- a/src/mc/explo/udpor/ExtensionSetCalculator.cpp +++ b/src/mc/explo/udpor/ExtensionSetCalculator.cpp @@ -28,20 +28,23 @@ EventSet ExtensionSetCalculator::partially_extend(const Configuration& C, Unfold 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_TEST, &ExtensionSetCalculator::partially_extend_CommTest}}; + {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()); } } @@ -80,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); } } @@ -165,7 +166,7 @@ EventSet ExtensionSetCalculator::partially_extend_CommWait(const Configuration& }); xbt_assert(issuer != C.end(), "Invariant violation! A (supposedly) enabled `CommWait` transition " - "waiting on communication %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 " @@ -408,7 +409,7 @@ EventSet ExtensionSetCalculator::partially_extend_CommTest(const Configuration& }); xbt_assert(issuer != C.end(), "An enabled `CommTest` transition (%s) is testing a communication" - "%lu not created by a receive/send " + "%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.", @@ -528,6 +529,168 @@ EventSet ExtensionSetCalculator::partially_extend_CommTest(const Configuration& "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) +{ + 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; }