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
select the decision logic either of the OpenMPI or the MPICH libraries. (By
default SMPI uses naive version of collective operations.)
-Each collective operation can be manually selected with a
-``smpi/collective_name:algo_name``. Available algorithms are listed in
-:ref:`SMPI_use_colls`.
-
-.. TODO:: All available collective algorithms will be made available
- via the ``smpirun --help-coll`` command.
+Each collective operation can be manually selected with a ``smpi/collective_name:algo_name``. For example, if you want to use
+the Bruck algorithm for the Alltoall algorithm, you should use ``--cfg=smpi/alltoall:bruck`` on the command-line of smpirun. The
+reference of all available algorithms are listed in :ref:`SMPI_use_colls`.
.. _cfg=smpi/barrier-collectives:
<link_ctn id="link1" />
</route>
-If host `A` sends ``100kB`` (a hundred kilobytes) to host `B`, one can expect that this communication would take `0.81`
-seconds to complete according to a simple latency-plus-size-divided-by-bandwidth model (0.01 + 8e5/1e6 = 0.81) since the
-latency is small enough to ensure that the physical bandwidth is used (see the discussion on CM02 above). However, the
-LV08 model is more complex to account for three phenomena that directly impact the simulation time:
+If host `A` sends ``100kB`` (a hundred kilobytes, that is, 8e5 bits) to host `B`, one can expect that this communication would
+take `0.81` seconds to complete according to a simple latency-plus-size-divided-by-bandwidth model (0.01 + 8e5/1e6 = 0.81 -- the
+size was converted from bytes to bits) since the latency is small enough to ensure that the physical bandwidth is used (see the
+discussion on CM02 above). However, the LV08 model is more complex to account for three phenomena that directly impact the
+simulation time:
- The size of a message at the application level (i.e., 100kB in this example) is not the size that is actually
transferred over the network. To mimic the fact that TCP and IP headers are added to each packet of the original
payload, the TCP model of SimGrid empirically considers that `only 97% of the nominal bandwidth` are available. In
- other words, the size of your message is increased by a few percents, whatever this size be.
+ other words, the size of your message is increased by a few percents, whichever this size.
- In the real world, the TCP protocol is not able to fully exploit the bandwidth of a link from the emission of the
first packet. To reflect this `slow start` phenomenon, the latency declared in the platform file is multiplied by
# This example never ends, disable it for now
set(_mc-bugged2-liveness_disable 1)
- ADD_TESH(s4u-mc-bugged1-liveness-visited-ucontext --setenv bindir=${CMAKE_CURRENT_BINARY_DIR}/mc-bugged1-liveness
- --setenv platfdir=${CMAKE_HOME_DIRECTORY}/examples/platforms
- --cd ${CMAKE_CURRENT_SOURCE_DIR}/mc-bugged1-liveness
- ${CMAKE_HOME_DIRECTORY}/examples/cpp/mc-bugged1-liveness/s4u-mc-bugged1-liveness-visited.tesh)
+ if ("${CMAKE_SYSTEM}" MATCHES "Linux")
+ # timeout under FreeBSD (test never stops)
+ ADD_TESH(s4u-mc-bugged1-liveness-visited-ucontext --setenv bindir=${CMAKE_CURRENT_BINARY_DIR}/mc-bugged1-liveness
+ --setenv platfdir=${CMAKE_HOME_DIRECTORY}/examples/platforms
+ --cd ${CMAKE_CURRENT_SOURCE_DIR}/mc-bugged1-liveness
+ ${CMAKE_HOME_DIRECTORY}/examples/cpp/mc-bugged1-liveness/s4u-mc-bugged1-liveness-visited.tesh)
+ endif()
IF(HAVE_C_STACK_CLEANER)
add_dependencies(tests-mc s4u-mc-bugged1-liveness-stack-cleaner)
# This test checks if the stack cleaner is making a difference:
#define SIMIX_H_NO_DEPRECATED_WARNING // avoid deprecation warning on include (remove with XBT_ATTRIB_DEPRECATED_v335)
#include <simgrid/simix.h>
+#include <cmath>
+
void simcall_comm_send(simgrid::kernel::actor::ActorImpl* sender, simgrid::kernel::activity::MailboxImpl* mbox,
double task_size, double rate, void* src_buff, size_t src_buff_size,
bool (*match_fun)(void*, void*, simgrid::kernel::activity::CommImpl*),
#include "src/kernel/activity/SleepImpl.hpp"
#include "src/kernel/activity/Synchro.hpp"
#include "src/kernel/actor/ActorImpl.hpp"
-#include "src/kernel/resource/SplitDuplexLinkImpl.hpp"
#include <boost/intrusive/list.hpp>
#include <map>
* under the terms of the license (GNU LGPL) which comes with this package. */
#include "src/kernel/resource/CpuImpl.hpp"
-#include "src/kernel/EngineImpl.hpp"
#include "src/kernel/resource/models/cpu_ti.hpp"
#include "src/kernel/resource/profile/Profile.hpp"
#include "src/simgrid/math_utils.h"
{
if (is_on()) {
Resource::turn_off();
-
- const kernel::lmm::Element* elem = nullptr;
- double now = EngineImpl::get_clock();
- while (const auto* var = get_constraint()->get_variable(&elem)) {
- Action* action = var->get_id();
- if (action->get_state() == Action::State::INITED || action->get_state() == Action::State::STARTED) {
- action->set_finish_time(now);
- action->set_state(Action::State::FAILED);
- }
- }
+ cancel_actions();
}
}
Resource::turn_off();
s4u::Disk::on_onoff(piface_);
piface_.on_this_onoff(piface_);
-
- const kernel::lmm::Element* elem = nullptr;
- double now = EngineImpl::get_clock();
- while (const auto* var = get_constraint()->get_variable(&elem)) {
- Action* action = var->get_id();
- if (action->get_state() == Action::State::INITED || action->get_state() == Action::State::STARTED) {
- action->set_finish_time(now);
- action->set_state(Action::State::FAILED);
- }
- }
+ cancel_actions();
}
}
#define SIMGRID_KERNEL_RESOURCE_RESOURCE_HPP
#include "simgrid/forward.h"
+#include "src/kernel/EngineImpl.hpp"
#include "src/kernel/actor/Simcall.hpp"
#include "src/kernel/lmm/maxmin.hpp" // Constraint
#include "src/kernel/resource/profile/Event.hpp"
Model* model_ = nullptr;
lmm::Constraint* constraint_ = nullptr;
+protected:
+ void cancel_actions()
+ {
+ const kernel::lmm::Element* elem = nullptr;
+ double now = EngineImpl::get_clock();
+ while (const auto* var = get_constraint()->get_variable(&elem)) {
+ Action* action = var->get_id();
+ if (action->get_state() == Action::State::INITED || action->get_state() == Action::State::STARTED ||
+ action->get_state() == Action::State::IGNORED) {
+ action->set_finish_time(now);
+ action->set_state(Action::State::FAILED);
+ }
+ }
+ }
+
public:
using Resource::Resource;
/** @brief setup the profile file with states events (ON or OFF). The profile must contain boolean values. */
#include <simgrid/s4u/Engine.hpp>
-#include "src/kernel/EngineImpl.hpp"
#include "src/kernel/resource/StandardLinkImpl.hpp"
#include <numeric>
Resource::turn_off();
s4u::Link::on_onoff(piface_);
piface_.on_this_onoff(piface_);
-
- const kernel::lmm::Element* elem = nullptr;
- double now = EngineImpl::get_clock();
- while (const auto* var = get_constraint()->get_variable(&elem)) {
- Action* action = var->get_id();
- if (action->get_state() == Action::State::INITED || action->get_state() == Action::State::STARTED) {
- action->set_finish_time(now);
- action->set_state(Action::State::FAILED);
- }
- }
+ cancel_actions();
}
}
get_iface()->turn_on();
}
} else {
- const lmm::Element* elem = nullptr;
- double date = EngineImpl::get_clock();
-
get_iface()->turn_off();
-
- while (const auto* var = get_constraint()->get_variable(&elem)) {
- Action* action = var->get_id();
-
- if (action->get_state() == Action::State::INITED || action->get_state() == Action::State::STARTED ||
- action->get_state() == Action::State::IGNORED) {
- action->set_finish_time(date);
- action->set_state(Action::State::FAILED);
- }
- }
+ cancel_actions();
}
unref_state_event();
}
} else {
get_iface()->turn_off();
- double date = EngineImpl::get_clock();
/* put all action running on cpu to failed */
+ double now = EngineImpl::get_clock();
for (CpuTiAction& action : action_set_) {
if (action.get_state() == Action::State::INITED || action.get_state() == Action::State::STARTED ||
action.get_state() == Action::State::IGNORED) {
- action.set_finish_time(date);
+ action.set_finish_time(now);
action.set_state(Action::State::FAILED);
get_model()->get_action_heap().remove(&action);
}
#include "src/kernel/EngineImpl.hpp"
#include "src/kernel/resource/DiskImpl.hpp"
#include "src/kernel/resource/HostImpl.hpp"
+#include "src/kernel/resource/StandardLinkImpl.hpp"
#include "src/kernel/resource/profile/Profile.hpp"
#include "src/kernel/xml/platf.hpp"
#include "src/kernel/xml/platf_private.hpp"
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
MAP_PRIVATE | MAP_ANONYMOUS | MAP_POPULATE, -1, 0);
xbt_assert(new_memory != MAP_FAILED, "Could not mremap snapshot pages.");
// Check if expanding worked
- if (new_memory != (char*)this->memory_ + old_bytesize) {
+ if (new_memory == (char*)this->memory_ + old_bytesize) {
+ new_memory = this->memory_;
+ } else {
// New memory segment could not be put at the end of this->memory_,
// so cancel this one and try to relocate everything and copy data
munmap(new_memory, new_bytesize - old_bytesize);
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)
