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());
"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();
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;
}
// 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) {
// 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) {
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());
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
