include src/mc/explo/udpor/EventSet.cpp
include src/mc/explo/udpor/EventSet.hpp
include src/mc/explo/udpor/EventSet_test.cpp
+include src/mc/explo/udpor/ExtensionSet_test.cpp
include src/mc/explo/udpor/ExtensionSetCalculator.cpp
include src/mc/explo/udpor/ExtensionSetCalculator.hpp
include src/mc/explo/udpor/History.cpp
const std::vector<std::shared_ptr<Transition>>& get_enabled_transitions() const
{
- return this->pending_transitions_;
+ static const auto no_enabled_transitions = std::vector<std::shared_ptr<Transition>>();
+ return this->is_enabled() ? this->pending_transitions_ : no_enabled_transitions;
};
};
// possibility is that we've finished running everything, and
// we wouldn't be in deadlock then)
if (enC.empty()) {
- XBT_VERB("Maximal configuration detected. Checking for deadlock...");
+ XBT_VERB("**************************");
+ XBT_VERB("*** TRACE INVESTIGATED ***");
+ XBT_VERB("**************************");
+ XBT_VERB("Execution sequence:");
+ for (auto const& s : get_textual_trace())
+ XBT_VERB(" %s", s.c_str());
get_remote_app().check_deadlock();
}
// that we are searching again from `state(C)`. While the
// stack of states is properly adjusted to represent
// `state(C)` all together, the RemoteApp is currently sitting
- // at some *future* state with resepct to `state(C)` since the
- // recursive calls have moved it there.
+ // at some *future* state with respect to `state(C)` since the
+ // recursive calls had moved it there.
restore_program_state_with_current_stack();
// Explore(C, D + {e}, J \ C)
EventSet exC = prev_exC;
exC.remove(e_cur);
+ // IMPORTANT NOTE: In order to have deterministic results, we need to process
+ // the actors in a deterministic manner so that events are discovered by
+ // UDPOR in a deterministic order. The processing done here always processes
+ // actors in a consistent order since `std::map` is by-default ordered using
+ // `std::less<Key>` (see the return type of `State::get_actors_list()`)
for (const auto& [aid, actor_state] : stateC.get_actors_list()) {
- for (const auto& transition : actor_state.get_enabled_transitions()) {
- XBT_DEBUG("\t Considering partial extension for %s", transition->to_string().c_str());
- EventSet extension = ExtensionSetCalculator::partially_extend(C, &unfolding, transition);
- exC.form_union(extension);
+ const auto& enabled_transitions = actor_state.get_enabled_transitions();
+ if (enabled_transitions.empty()) {
+ XBT_DEBUG("\t Actor `%ld` is disabled: no partial extensions need to be considered", aid);
+ } else {
+ XBT_DEBUG("\t Actor `%ld` is enabled", aid);
+ for (const auto& transition : enabled_transitions) {
+ XBT_DEBUG("\t Considering partial extension for %s", transition->to_string().c_str());
+ EventSet extension = ExtensionSetCalculator::partially_extend(C, &unfolding, transition);
+ exC.form_union(extension);
+ }
}
}
return exC;
"empty before attempting to select an event from it?");
}
+ // UDPOR's exploration is non-deterministic (as is DPOR's)
+ // in the sense that at any given point there may
+ // be multiple paths that can be followed. The correctness and optimality
+ // of the algorithm remains unaffected by the route taken by UDPOR when
+ // given multiple choices; but to ensure that SimGrid itself has deterministic
+ // behavior on all platforms, we always pick events with lower id's
+ // to ensure we explore the unfolding deterministically.
if (A.empty()) {
- return const_cast<UnfoldingEvent*>(*(enC.begin()));
- }
-
- for (const auto& event : A) {
- if (enC.contains(event)) {
- return const_cast<UnfoldingEvent*>(event);
- }
+ const auto min_event = std::min_element(enC.begin(), enC.end(),
+ [](const auto e1, const auto e2) { return e1->get_id() < e2->get_id(); });
+ return const_cast<UnfoldingEvent*>(*min_event);
+ } else {
+ const auto intersection = A.make_intersection(enC);
+ const auto min_event = std::min_element(intersection.begin(), intersection.end(),
+ [](const auto e1, const auto e2) { return e1->get_id() < e2->get_id(); });
+ return const_cast<UnfoldingEvent*>(*min_event);
}
- return nullptr;
}
void UdporChecker::clean_up_explore(const UnfoldingEvent* e, const Configuration& C, const EventSet& D)
return make_union(config.get_events());
}
+EventSet EventSet::make_intersection(const EventSet& other) const
+{
+ std::unordered_set<const UnfoldingEvent*> result;
+
+ for (const UnfoldingEvent* e : other.events_) {
+ if (contains(e)) {
+ result.insert(e);
+ }
+ }
+
+ return EventSet(std::move(result));
+}
+
EventSet EventSet::get_local_config() const
{
return History(*this).get_all_events();
return this->events_.find(e) != this->events_.end();
}
+bool EventSet::contains_equivalent_to(const UnfoldingEvent* e) const
+{
+ return std::find_if(begin(), end(), [=](const UnfoldingEvent* e_in_set) { return *e == *e_in_set; }) != end();
+}
+
bool EventSet::is_subset_of(const EventSet& other) const
{
// If there is some element not contained in `other`, then
EventSet& operator=(EventSet&&) = default;
EventSet(EventSet&&) = default;
explicit EventSet(Configuration&& config);
- explicit EventSet(std::vector<const UnfoldingEvent*>&& raw_events) : events_(raw_events.begin(), raw_events.end())
- {
- xbt_assert(std::none_of(events_.begin(), events_.end(), [](const auto* e) { return e == nullptr; }), "Oh no");
- }
- explicit EventSet(std::unordered_set<const UnfoldingEvent*>&& raw_events) : events_(raw_events)
- {
- xbt_assert(std::none_of(events_.begin(), events_.end(), [](const auto* e) { return e == nullptr; }), "Oh no");
- }
- explicit EventSet(std::initializer_list<const UnfoldingEvent*> event_list) : events_(std::move(event_list))
- {
- xbt_assert(std::none_of(events_.begin(), events_.end(), [](const auto* e) { return e == nullptr; }), "Oh no");
- }
+ explicit EventSet(std::vector<const UnfoldingEvent*>&& raw_events) : events_(raw_events.begin(), raw_events.end()) {}
+ explicit EventSet(std::unordered_set<const UnfoldingEvent*>&& raw_events) : events_(raw_events) {}
+ explicit EventSet(std::initializer_list<const UnfoldingEvent*> event_list) : events_(std::move(event_list)) {}
auto begin() const { return this->events_.begin(); }
auto end() const { return this->events_.end(); }
EventSet make_union(const UnfoldingEvent*) const;
EventSet make_union(const EventSet&) const;
EventSet make_union(const Configuration&) const;
+ EventSet make_intersection(const EventSet&) const;
EventSet get_local_config() const;
size_t size() const;
bool empty() const;
+
bool contains(const UnfoldingEvent*) const;
bool contains(const History&) const;
+ bool contains_equivalent_to(const UnfoldingEvent*) const;
bool intersects(const EventSet&) const;
bool intersects(const History&) const;
bool is_subset_of(const EventSet&) const;
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());
}
}
}
// 2. foreach e ∈ C s.t. λ(e) ∈ {AsyncSend(m, _), TestAny(Com)} where
- // Com contains a matching c' = AsyncReceive(m, _) with a
- for (const auto* e : C) {
+ // 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<const CommSendTransition*>(e->get_transition());
async_send != nullptr) {
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);
}
}
{
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<CommRecvTransition>(std::move(action));
const unsigned recv_mailbox = recv_action->get_mailbox();
const auto pre_event_a_C = C.pre_event(recv_action->aid_);
// 2. foreach e ∈ C s.t. λ(e) ∈ {AsyncSend(m, _), TestAny(Com)} where
// Com contains a matching c' = AsyncReceive(m, _) with a
- for (const auto* e : C) {
+ for (const auto e : C) {
const bool transition_type_check = [&]() {
if (const auto* async_recv = dynamic_cast<const CommRecvTransition*>(e->get_transition());
async_recv != nullptr && async_recv->get_mailbox() == recv_mailbox) {
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);
exC.insert(e_prime);
});
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 %lu 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 "
}
} 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<const CommSendTransition*>(e_issuer->get_transition());
- e_issuer_send != nullptr) {
+ if (const CommSendTransition* e_issuer_send = dynamic_cast<const CommSendTransition*>(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
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<const CommSendTransition*>(e->get_transition());
if (send_position == receive_position) {
exC.insert(U->discover_event(std::move(K), wait_action));
}
-
- } else if (const CommRecvTransition* e_issuer_recv =
- dynamic_cast<const CommRecvTransition*>(e_issuer->get_transition());
- e_issuer_recv != nullptr) {
+ }
+ } else if (const CommRecvTransition* e_issuer_recv =
+ dynamic_cast<const CommRecvTransition*>(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
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<Transition> test_action)
+ std::shared_ptr<Transition> action)
{
- return EventSet();
+ EventSet exC;
+
+ const auto test_action = std::static_pointer_cast<CommTestTransition>(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<const CommRecvTransition*>(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<const CommSendTransition*>(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"
+ "%lu 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<const CommSendTransition*>(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<const CommRecvTransition*>(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<const CommSendTransition*>(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<const CommRecvTransition*>(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<const CommRecvTransition*>(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<const CommSendTransition*>(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<const CommSendTransition*>(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<const CommRecvTransition*>(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<Transition> action)
+{
+ EventSet exC;
+ const auto mutex_lock = std::static_pointer_cast<MutexTransition>(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<const MutexTransition*>(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<Transition> action)
+{
+ EventSet exC;
+ const auto mutex_unlock = std::static_pointer_cast<MutexTransition>(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<const MutexTransition*>(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<Transition> action)
+{
+ EventSet exC;
+ const auto mutex_wait = std::static_pointer_cast<MutexTransition>(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<const MutexTransition*>(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<Transition> action)
+{
+ EventSet exC;
+ const auto mutex_test = std::static_pointer_cast<MutexTransition>(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<const MutexTransition*>(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<Transition> action)
+{
+ EventSet exC;
+
+ const auto join_action = std::static_pointer_cast<ActorJoinTransition>(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
static EventSet partially_extend_CommWait(const Configuration&, Unfolding*, std::shared_ptr<Transition>);
static EventSet partially_extend_CommTest(const Configuration&, Unfolding*, std::shared_ptr<Transition>);
+ static EventSet partially_extend_MutexAsyncLock(const Configuration&, Unfolding*, std::shared_ptr<Transition>);
+ static EventSet partially_extend_MutexWait(const Configuration&, Unfolding*, std::shared_ptr<Transition>);
+ static EventSet partially_extend_MutexTest(const Configuration&, Unfolding*, std::shared_ptr<Transition>);
+ static EventSet partially_extend_MutexUnlock(const Configuration&, Unfolding*, std::shared_ptr<Transition>);
+
+ static EventSet partially_extend_ActorJoin(const Configuration&, Unfolding*, std::shared_ptr<Transition>);
+
public:
static EventSet partially_extend(const Configuration&, Unfolding*, const std::shared_ptr<Transition>);
};
--- /dev/null
+/* Copyright (c) 2017-2023. The SimGrid Team. All rights reserved. */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#include "src/3rd-party/catch.hpp"
+#include "src/mc/explo/udpor/Configuration.hpp"
+#include "src/mc/explo/udpor/ExtensionSetCalculator.hpp"
+#include "src/mc/explo/udpor/History.hpp"
+#include "src/mc/explo/udpor/Unfolding.hpp"
+
+using namespace simgrid::mc;
+using namespace simgrid::mc::udpor;
+
+TEST_CASE("simgrid::mc::udpor: Testing Computation with AsyncSend/AsyncReceive Only")
+{
+ // This test checks that the unfolding constructed for the very
+ // simple program described below is extended correctly. Each
+ // step of UDPOR is observed to ensure that computations are carried
+ // out correctly. The program described is simply:
+ //
+ // 1 2
+ // AsyncSend(m) AsyncRecv(m)
+ //
+ // The unfolding of the simple program is as follows:
+ //
+ // ⊥
+ // / /
+ // (a) 1: AsyncSend(m) (b) 2: AsyncRecv(m)
+
+ const int times_considered = 0;
+ const int tag = 0;
+ const unsigned mbox = 0;
+ const uintptr_t comm = 0;
+
+ Unfolding U;
+
+ SECTION("Computing ex({⊥}) with 1: AsyncSend")
+ {
+ // Consider the extension with `1: AsyncSend(m)`
+ Configuration C;
+ aid_t issuer = 1;
+ const uintptr_t sbuff = 0;
+ const size_t size = 100;
+
+ const auto async_send =
+ std::make_shared<CommSendTransition>(issuer, times_considered, comm, mbox, sbuff, size, tag);
+ const auto incremental_exC = ExtensionSetCalculator::partially_extend(C, &U, async_send);
+
+ // Check that the events have been added to `U`
+ REQUIRE(U.size() == 1);
+
+ // Make assertions about the contents of ex(C)
+ UnfoldingEvent e(EventSet(), async_send);
+ REQUIRE(incremental_exC.contains_equivalent_to(&e));
+ }
+
+ SECTION("Computing ex({⊥}) with 2: AsyncRecv")
+ {
+ // Consider the extension with `2: AsyncRecv(m)`
+ Configuration C;
+ aid_t issuer = 2;
+ const uintptr_t rbuff = 0;
+
+ const auto async_recv = std::make_shared<CommRecvTransition>(issuer, times_considered, comm, mbox, rbuff, tag);
+ const auto incremental_exC = ExtensionSetCalculator::partially_extend(C, &U, async_recv);
+
+ // Check that the events have been added to `U`
+ REQUIRE(U.size() == 1);
+
+ // Make assertions about the contents of ex(C)
+ UnfoldingEvent e(EventSet(), async_recv);
+ REQUIRE(incremental_exC.contains_equivalent_to(&e));
+ }
+
+ SECTION("Computing ex({⊥}) fully")
+ {
+ // Consider the extension with `1: AsyncSend(m)`
+ Configuration C;
+ const uintptr_t rbuff = 0;
+ const uintptr_t sbuff = 0;
+ const size_t size = 100;
+
+ const auto async_send = std::make_shared<CommSendTransition>(1, times_considered, comm, mbox, sbuff, size, tag);
+ const auto incremental_exC_send = ExtensionSetCalculator::partially_extend(C, &U, async_send);
+
+ // Check that the events have been added to `U`
+ REQUIRE(U.size() == 1);
+
+ // Make assertions about the contents of ex(C)
+ UnfoldingEvent e_send(EventSet(), async_send);
+ REQUIRE(incremental_exC_send.contains_equivalent_to(&e_send));
+
+ // Consider the extension with `2: AsyncRecv(m)`
+ const auto async_recv = std::make_shared<CommRecvTransition>(2, times_considered, comm, mbox, rbuff, tag);
+ const auto incremental_exC_recv = ExtensionSetCalculator::partially_extend(C, &U, async_recv);
+
+ // Check that the events have been added to `U`
+ REQUIRE(U.size() == 2);
+
+ // Make assertions about the contents of ex(C)
+ UnfoldingEvent e_recv(EventSet(), async_recv);
+ REQUIRE(incremental_exC_recv.contains_equivalent_to(&e_recv));
+ }
+
+ SECTION("Computing the full sequence of extensions")
+ {
+ Configuration C;
+ const uintptr_t rbuff = 0;
+ const uintptr_t sbuff = 0;
+ const size_t size = 100;
+
+ // Consider the extension with `1: AsyncSend(m)`
+ const auto async_send = std::make_shared<CommSendTransition>(1, times_considered, comm, mbox, sbuff, size, tag);
+ const auto incremental_exC_send = ExtensionSetCalculator::partially_extend(C, &U, async_send);
+
+ // Check that event `a` has been added to `U`
+ REQUIRE(U.size() == 1);
+ UnfoldingEvent e_send(EventSet(), async_send);
+ REQUIRE(incremental_exC_send.contains_equivalent_to(&e_send));
+
+ // Consider the extension with `2: AsyncRecv(m)`
+ const auto async_recv = std::make_shared<CommRecvTransition>(2, times_considered, comm, mbox, rbuff, tag);
+ const auto incremental_exC_recv = ExtensionSetCalculator::partially_extend(C, &U, async_recv);
+
+ // Check that event `b` has been added to `U`
+ REQUIRE(U.size() == 2);
+ UnfoldingEvent e_recv(EventSet(), async_recv);
+ REQUIRE(incremental_exC_recv.contains_equivalent_to(&e_recv));
+
+ // At this point, UDPOR will pick one of the two events equivalent to
+ // `e_recv` and e`_send`
+
+ // Suppose it picks the event labeled `a` in the graph above first
+ // (ultimately, UDPOR will choose to search both directions since
+ // {⊥, b} will be an alternative to {⊥, a})
+
+ const auto* e_a = *incremental_exC_send.begin();
+ const auto* e_b = *incremental_exC_recv.begin();
+
+ SECTION("Pick `a` first (ex({⊥, a}))")
+ {
+ // After picking `a`, we need only consider the extensions
+ // possible with `2: AsyncRecv(m)` since actor 1 no longer
+ // has any actions to run
+ Configuration C_with_send{e_a};
+ const auto incremental_exC_with_send = ExtensionSetCalculator::partially_extend(C_with_send, &U, async_recv);
+
+ // Check that event `b` has not been duplicated
+ REQUIRE(U.size() == 2);
+
+ // Indeed, in this case we assert that the SAME identity has been
+ // supplied by the unfolding (it should note that `ex({⊥, a})`
+ // and `ex({⊥})` have an overlapping event `b`)
+ REQUIRE(incremental_exC_with_send.contains(e_b));
+ }
+
+ SECTION("Pick `b` first (ex({⊥, b}))")
+ {
+ // After picking `b`, we need only consider the extensions
+ // possible with `1: AsyncSend(m)` since actor 2 no longer
+ // has any actions to run
+ Configuration C_with_recv{e_b};
+ const auto incremental_exC_with_recv = ExtensionSetCalculator::partially_extend(C_with_recv, &U, async_send);
+
+ // Check that event `a` has not been duplicated
+ REQUIRE(U.size() == 2);
+
+ // Indeed, in this case we assert that the SAME identity has been
+ // supplied by the unfolding (it should note that `ex({⊥, b})`
+ // and `ex({⊥})` have an overlapping event `a`)
+ REQUIRE(incremental_exC_with_recv.contains(e_a));
+ }
+ }
+}
+
+TEST_CASE("simgrid::mc::udpor: Testing Waits, Receives, and Sends")
+{
+ // We're going to follow UDPOR down one path of computation
+ // in a relatively simple program (although the unfolding quickly
+ // becomes quite complex)
+ //
+ // 1 2
+ // AsyncSend(m) AsyncRecv(m)
+ // Wait(m) Wait(m)
+ //
+ // The unfolding of the simple program is as follows:
+ // ⊥
+ // / /
+ // (a) 1: AsyncSend(m) (b) 2: AsyncRecv(m)
+ // | \ / |
+ // | \ / |
+ // | / \ |
+ // | / \ |
+ // (c) 1: Wait(m) (d) 2: Wait(m)
+ const int times_considered = 0;
+ const int tag = 0;
+ const unsigned mbox = 0;
+ const uintptr_t comm = 0x800;
+ const uintptr_t rbuff = 0x200;
+ const uintptr_t sbuff = 0x400;
+ const size_t size = 100;
+ const bool timeout = false;
+
+ Unfolding U;
+ const auto comm_send = std::make_shared<CommSendTransition>(1, times_considered, comm, mbox, sbuff, size, tag);
+ const auto comm_recv = std::make_shared<CommRecvTransition>(2, times_considered, comm, mbox, rbuff, tag);
+ const auto comm_wait_1 =
+ std::make_shared<CommWaitTransition>(1, times_considered, timeout, comm, 1, 2, mbox, sbuff, rbuff, size);
+ const auto comm_wait_2 =
+ std::make_shared<CommWaitTransition>(2, times_considered, timeout, comm, 1, 2, mbox, sbuff, rbuff, size);
+
+ // 1. UDPOR will attempt to expand first ex({⊥})
+
+ // --- ex({⊥}) ---
+ const auto incremental_exC_send = ExtensionSetCalculator::partially_extend(Configuration(), &U, comm_send);
+ { // Assert that event `a` has been added
+ UnfoldingEvent e_send(EventSet(), comm_send);
+ REQUIRE(incremental_exC_send.size() == 1);
+ REQUIRE(incremental_exC_send.contains_equivalent_to(&e_send));
+ REQUIRE(U.size() == 1);
+ }
+
+ const auto incremental_exC_recv = ExtensionSetCalculator::partially_extend(Configuration(), &U, comm_recv);
+ { // Assert that event `b` has been added
+ UnfoldingEvent e_recv(EventSet(), comm_recv);
+ REQUIRE(incremental_exC_recv.size() == 1);
+ REQUIRE(incremental_exC_recv.contains_equivalent_to(&e_recv));
+ REQUIRE(U.size() == 2);
+ }
+ // --- ex({⊥}) ---
+
+ // 2. UDPOR will then attempt to expand ex({⊥, a}) or ex({⊥, b}). Both have
+ // parallel effects and should simply return events already added to ex(C)
+ //
+ // NOTE: Note that only once actor is enabled in both cases, meaning that
+ // we need only consider one incremental expansion for each
+
+ const auto* e_a = *incremental_exC_send.begin();
+ const auto* e_b = *incremental_exC_recv.begin();
+
+ // --- ex({⊥, a}) ---
+ const auto incremental_exC_recv2 = ExtensionSetCalculator::partially_extend(Configuration({e_a}), &U, comm_recv);
+ { // Assert that no event has been added and that
+ // e_b is contained in the extension set
+ UnfoldingEvent e_send(EventSet(), comm_send);
+ REQUIRE(incremental_exC_recv2.size() == 1);
+ REQUIRE(incremental_exC_recv2.contains(e_b));
+
+ // Here, `e_a` shouldn't be added again
+ REQUIRE(U.size() == 2);
+ }
+ // --- ex({⊥, a}) ---
+
+ // --- ex({⊥, b}) ---
+ const auto incremental_exC_send2 = ExtensionSetCalculator::partially_extend(Configuration({e_b}), &U, comm_send);
+ { // Assert that no event has been added and that
+ // e_a is contained in the extension set
+ REQUIRE(incremental_exC_send2.size() == 1);
+ REQUIRE(incremental_exC_send2.contains(e_a));
+
+ // Here, `e_b` shouldn't be added again
+ REQUIRE(U.size() == 2);
+ }
+ // --- ex({⊥, b}) ---
+
+ // 3. Expanding from ex({⊥, a, b}) brings in both `CommWait` events since they
+ // become enabled as soon as the communication has been paired
+
+ // --- ex({⊥, a, b}) ---
+ const auto incremental_exC_wait_actor_1 =
+ ExtensionSetCalculator::partially_extend(Configuration({e_a, e_b}), &U, comm_wait_1);
+ { // Assert that events `c` has been added
+ UnfoldingEvent e_wait_1(EventSet({e_a, e_b}), comm_wait_1);
+ REQUIRE(incremental_exC_wait_actor_1.size() == 1);
+ REQUIRE(incremental_exC_wait_actor_1.contains_equivalent_to(&e_wait_1));
+ REQUIRE(U.size() == 3);
+ }
+
+ const auto incremental_exC_wait_actor_2 =
+ ExtensionSetCalculator::partially_extend(Configuration({e_a, e_b}), &U, comm_wait_2);
+ { // Assert that events `d` has been added
+ UnfoldingEvent e_wait_2(EventSet({e_a, e_b}), comm_wait_2);
+ REQUIRE(incremental_exC_wait_actor_2.size() == 1);
+ REQUIRE(incremental_exC_wait_actor_2.contains_equivalent_to(&e_wait_2));
+ REQUIRE(U.size() == 4);
+ }
+ // --- ex({⊥, a, b}) ---
+
+ // 4. Expanding from either wait action should simply yield the other event
+ // with a wait action associated with it.
+ // This is analogous to the scenario before with send and receive
+ // ex({⊥, a, b, c}) or ex({⊥, a, b, d})
+
+ const auto* e_c = *incremental_exC_wait_actor_1.begin();
+ const auto* e_d = *incremental_exC_wait_actor_2.begin();
+
+ // --- ex({⊥, a, b, d}) ---
+ const auto incremental_exC_wait_actor_1_2 =
+ ExtensionSetCalculator::partially_extend(Configuration({e_a, e_b, e_d}), &U, comm_wait_1);
+ { // Assert that no event has been added and that
+ // `e_c` is contained in the extension set
+ REQUIRE(incremental_exC_wait_actor_1_2.size() == 1);
+ REQUIRE(incremental_exC_wait_actor_1_2.contains(e_c));
+ REQUIRE(U.size() == 4);
+ }
+ // --- ex({⊥, a, b, d}) ---
+
+ // --- ex({⊥, a, b, c}) ---
+ const auto incremental_exC_wait_actor_2_2 =
+ ExtensionSetCalculator::partially_extend(Configuration({e_a, e_b, e_c}), &U, comm_wait_2);
+ { // Assert that no event has been added and that
+ // `e_d` is contained in the extension set
+ REQUIRE(incremental_exC_wait_actor_2_2.size() == 1);
+ REQUIRE(incremental_exC_wait_actor_2_2.contains(e_d));
+ REQUIRE(U.size() == 4);
+ }
+ // --- ex({⊥, a, b, c}) ---
+}
\ No newline at end of file
UnfoldingEvent::UnfoldingEvent(EventSet immediate_causes, std::shared_ptr<Transition> transition)
: associated_transition(std::move(transition)), immediate_causes(std::move(immediate_causes))
{
+ static uint64_t event_id = 0;
+ this->id = ++event_id;
}
bool UnfoldingEvent::operator==(const UnfoldingEvent& other) const
dependencies_string += "[";
for (const auto* e : immediate_causes) {
+ dependencies_string += " ";
dependencies_string += e->to_string();
+ dependencies_string += " and ";
}
dependencies_string += "]";
- return xbt::string_printf("(%p) Actor %ld: %s (%zu dependencies: %s)", this, associated_transition->aid_,
+ return xbt::string_printf("Event %lu, Actor %ld: %s (%zu dependencies: %s)", this->id, associated_transition->aid_,
associated_transition->to_string().c_str(), immediate_causes.size(),
dependencies_string.c_str());
}
bool is_dependent_with(const Transition*) const;
bool is_dependent_with(const UnfoldingEvent* other) const;
+ unsigned get_id() const { return this->id; }
+ aid_t get_actor() const { return get_transition()->aid_; }
const EventSet& get_immediate_causes() const { return this->immediate_causes; }
Transition* get_transition() const { return this->associated_transition.get(); }
- aid_t get_actor() const { return get_transition()->aid_; }
void set_transition(std::shared_ptr<Transition> t) { this->associated_transition = std::move(t); }
* so on.
*/
EventSet immediate_causes;
+
+ /**
+ * @brief An identifier which is used to sort events
+ * deterministically
+ */
+ uint64_t id = 0;
};
} // namespace simgrid::mc::udpor
namespace simgrid::mc {
+CommWaitTransition::CommWaitTransition(aid_t issuer, int times_considered, bool timeout_, uintptr_t comm_,
+ aid_t sender_, aid_t receiver_, unsigned mbox_, uintptr_t sbuff_,
+ uintptr_t rbuff_, size_t size_)
+ : Transition(Type::COMM_WAIT, issuer, times_considered)
+ , timeout_(timeout_)
+ , comm_(comm_)
+ , sender_(sender_)
+ , receiver_(receiver_)
+ , mbox_(mbox_)
+ , sbuff_(sbuff_)
+ , rbuff_(rbuff_)
+ , size_(size_)
+{
+}
CommWaitTransition::CommWaitTransition(aid_t issuer, int times_considered, std::stringstream& stream)
: Transition(Type::COMM_WAIT, issuer, times_considered)
{
return false; // Comm transitions are INDEP with non-comm transitions
}
+CommTestTransition::CommTestTransition(aid_t issuer, int times_considered, uintptr_t comm_, aid_t sender_,
+ aid_t receiver_, unsigned mbox_, uintptr_t sbuff_, uintptr_t rbuff_,
+ size_t size_)
+ : Transition(Type::COMM_TEST, issuer, times_considered)
+ , comm_(comm_)
+ , sender_(sender_)
+ , receiver_(receiver_)
+ , mbox_(mbox_)
+ , sbuff_(sbuff_)
+ , rbuff_(rbuff_)
+ , size_(size_)
+{
+}
CommTestTransition::CommTestTransition(aid_t issuer, int times_considered, std::stringstream& stream)
: Transition(Type::COMM_TEST, issuer, times_considered)
{
return false; // Comm transitions are INDEP with non-comm transitions
}
+CommRecvTransition::CommRecvTransition(aid_t issuer, int times_considered, uintptr_t comm_, unsigned mbox_,
+ uintptr_t rbuff_, int tag_)
+ : Transition(Type::COMM_ASYNC_RECV, issuer, times_considered)
+ , comm_(comm_)
+ , mbox_(mbox_)
+ , rbuff_(rbuff_)
+ , tag_(tag_)
+{
+}
CommRecvTransition::CommRecvTransition(aid_t issuer, int times_considered, std::stringstream& stream)
: Transition(Type::COMM_ASYNC_RECV, issuer, times_considered)
{
if ((aid_ != test->sender_) && (aid_ != test->receiver_) && (test->rbuff_ != rbuff_))
return false;
+ // If the test is checking a paired comm already, we're independent!
+ // If we happen to make up that pair, then we're dependent...
+ if (test->comm_ != comm_)
+ return false;
+
return true; // DEP with other send transitions
}
if ((aid_ != wait->sender_) && (aid_ != wait->receiver_) && (wait->rbuff_ != rbuff_))
return false;
+ // If the wait is waiting on a paired comm already, we're independent!
+ // If we happen to make up that pair, then we're dependent...
+ if ((aid_ != wait->aid_) && wait->comm_ != comm_)
+ return false;
+
return true; // DEP with other wait transitions
}
return false; // Comm transitions are INDEP with non-comm transitions
}
+CommSendTransition::CommSendTransition(aid_t issuer, int times_considered, uintptr_t comm_, unsigned mbox_,
+ uintptr_t sbuff_, size_t size_, int tag_)
+ : Transition(Type::COMM_ASYNC_SEND, issuer, times_considered)
+ , comm_(comm_)
+ , mbox_(mbox_)
+ , sbuff_(sbuff_)
+ , size_(size_)
+ , tag_(tag_)
+{
+}
CommSendTransition::CommSendTransition(aid_t issuer, int times_considered, std::stringstream& stream)
: Transition(Type::COMM_ASYNC_SEND, issuer, times_considered)
{
if ((aid_ != test->sender_) && (aid_ != test->receiver_) && (test->sbuff_ != sbuff_))
return false;
+ // If the test is checking a paired comm already, we're independent!
+ // If we happen to make up that pair, then we're dependent...
+ if (test->comm_ != comm_)
+ return false;
+
return true; // DEP with other test transitions
}
if ((aid_ != wait->sender_) && (aid_ != wait->receiver_) && (wait->sbuff_ != sbuff_))
return false;
+ // If the wait is waiting on a paired comm already, we're independent!
+ // If we happen to make up that pair, then we're dependent...
+ if ((aid_ != wait->aid_) && wait->comm_ != comm_)
+ return false;
+
return true; // DEP with other wait transitions
}
friend CommTestTransition;
public:
+ CommWaitTransition(aid_t issuer, int times_considered, bool timeout_, uintptr_t comm_, aid_t sender_, aid_t receiver_,
+ unsigned mbox_, uintptr_t sbuff_, uintptr_t rbuff_, size_t size_);
CommWaitTransition(aid_t issuer, int times_considered, std::stringstream& stream);
std::string to_string(bool verbose) const override;
bool depends(const Transition* other) const override;
friend CommRecvTransition;
public:
+ CommTestTransition(aid_t issuer, int times_considered, uintptr_t comm_, aid_t sender_, aid_t receiver_,
+ unsigned mbox_, uintptr_t sbuff_, uintptr_t rbuff_, size_t size_);
CommTestTransition(aid_t issuer, int times_considered, std::stringstream& stream);
std::string to_string(bool verbose) const override;
bool depends(const Transition* other) const override;
int tag_;
public:
+ CommRecvTransition(aid_t issuer, int times_considered, uintptr_t comm_, unsigned mbox_, uintptr_t rbuff_, int tag_);
CommRecvTransition(aid_t issuer, int times_considered, std::stringstream& stream);
std::string to_string(bool verbose) const override;
bool depends(const Transition* other) const override;
int tag_;
public:
+ CommSendTransition(aid_t issuer, int times_considered, uintptr_t comm_, unsigned mbox_, uintptr_t sbuff_,
+ size_t size_, int tag_);
CommSendTransition(aid_t issuer, int times_considered, std::stringstream& stream);
std::string to_string(bool verbose) const override;
bool depends(const Transition* other) const override;
std::string to_string(bool verbose) const override;
MutexTransition(aid_t issuer, int times_considered, Type type, std::stringstream& stream);
bool depends(const Transition* other) const override;
+
+ uintptr_t get_mutex() const { return this->mutex_; }
+ aid_t get_owner() const { return this->owner_; }
};
class SemaphoreTransition : public Transition {
src/mc/sosp/PageStore_test.cpp
src/mc/explo/udpor/Unfolding_test.cpp
src/mc/explo/udpor/UnfoldingEvent_test.cpp
-
src/mc/explo/udpor/EventSet_test.cpp
+ src/mc/explo/udpor/ExtensionSet_test.cpp
src/mc/explo/udpor/History_test.cpp
src/mc/explo/udpor/Configuration_test.cpp)
