$ pip install simgrid
If you installed SimGrid to a non-standard directory (such as ``/opt/simgrid`` as advised earlier), you should tell python where
-to find the libraries as follows (notice the ``/lib`` added to the configured prefix).
+to find the libraries as follows (notice the elements suffixed to the configured prefix).
.. code-block:: console
- $ PYTHONPATH="/opt/simgrid/lib" python your_script.py
+ $ PYTHONPATH="/opt/simgrid/lib/python3/dist-packages" LD_LIBRARY_PATH="/opt/simgrid/lib" python your_script.py
-You can add the PYTHONPATH variable to your bash profile to not specify it each time by adding this line to your ``~/.profile``:
-``export PYTHONPATH=$PYTHONPATH:/opt/simgrid/lib/``
+You can add those variables to your bash profile to not specify it each time by adding these lines to your ``~/.profile``:
+
+.. code-block:: console
+
+ export PYTHONPATH="$PYTHONPATH:/opt/simgrid/lib/python3/dist-packages"
+ export LD_LIBRARY_PATH="$PYTHONPATH:/opt/simgrid/lib"
// Test attaching some user data to the file
file->set_data(new std::string("777"));
- const auto* file_data = file->get_data<std::string>();
+ auto file_data = file->get_unique_data<std::string>();
XBT_INFO("User data attached to the file: %s", file_data->c_str());
- delete file_data;
// Close the file
file->close();
> [0.000000] [mc_explo/INFO] 3: iSend(mbox=0)
> [0.000000] [mc_explo/INFO] 1: WaitComm(from 3 to 1, mbox=0, no timeout)
> [0.000000] [mc_explo/INFO] You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1;3;1;1;3;3;1'
-> [0.000000] [mc_dfs/INFO] DFS exploration ended. 148 unique states visited; 34 backtracks (240 transition replays, 422 states visited overall)
+> [0.000000] [mc_dfs/INFO] DFS exploration ended. 98 unique states visited; 21 backtracks (153 transition replays, 272 states visited overall)
! expect return 1
! timeout 20
> [0.000000] [mc_explo/INFO] 2: iSend(mbox=0)
> [0.000000] [mc_explo/INFO] 1: WaitComm(from 3 to 1, mbox=0, no timeout)
> [0.000000] [mc_explo/INFO] You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1;3;1;1;3;3;2;1'
-> [0.000000] [mc_dfs/INFO] DFS exploration ended. 157 unique states visited; 32 backtracks (184 transition replays, 373 states visited overall)
+> [0.000000] [mc_dfs/INFO] DFS exploration ended. 83 unique states visited; 12 backtracks (65 transition replays, 160 states visited overall)
! expect return 1
! timeout 20
> [0.000000] [mc_explo/INFO] 3: iSend(mbox=0)
> [0.000000] [mc_explo/INFO] 1: WaitComm(from 3 to 1, mbox=0, no timeout)
> [0.000000] [mc_explo/INFO] You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1;3;1;3;1;3;1'
-> [0.000000] [mc_dfs/INFO] DFS exploration ended. 49 unique states visited; 5 backtracks (23 transition replays, 77 states visited overall)
+> [0.000000] [mc_dfs/INFO] DFS exploration ended. 44 unique states visited; 3 backtracks (11 transition replays, 58 states visited overall)
XBT_PUBLIC void MC_automaton_new_propositional_symbol_pointer(const char* id, int* value);
XBT_PUBLIC void MC_ignore(void* addr, size_t size);
+XBT_PUBLIC void MC_unignore(void* addr, size_t size);
XBT_PUBLIC void MC_ignore_heap(void* address, size_t size);
XBT_PUBLIC void MC_unignore_heap(void* address, size_t size);
namespace simgrid::kernel::activity {
+unsigned CommImpl::next_id_ = 0;
+
+/* In stateful MC, we need to ignore some private memory that is not relevant to the application state */
+void CommImpl::setup_mc()
+{
+ MC_ignore(&CommImpl::next_id_, sizeof(CommImpl::next_id_));
+}
+
+CommImpl::CommImpl()
+{
+ MC_ignore((void*)&id_, sizeof(id_));
+}
+
std::function<void(CommImpl*, void*, size_t)> CommImpl::copy_data_callback_ = [](kernel::activity::CommImpl* comm,
void* buff, size_t buff_size) {
xbt_assert((buff_size == sizeof(void*)), "Cannot copy %zu bytes: must be sizeof(void*)", buff_size);
} else if (mbox_) {
mbox_->remove(this);
}
+
+ MC_unignore((void*)&id_, sizeof(id_));
}
/** @brief Starts the simulation of a communication synchro. */
s4u::Host* to_ = nullptr; /* Otherwise, computed at start() time from the actors */
CommImplType type_ = CommImplType::SEND; /* Type of the communication (SEND or RECEIVE) */
+ static unsigned next_id_; // Next ID to be given (for MC)
+ const unsigned id_ = ++next_id_; // ID of this comm (for MC) -- 0 as an ID denotes "invalid/unknown comm"
+
public:
- CommImpl() = default;
+ CommImpl();
static void set_copy_data_callback(const std::function<void(CommImpl*, void*, size_t)>& callback);
double get_rate() const { return rate_; }
MailboxImpl* get_mailbox() const { return mbox_; }
- long get_mailbox_id() const { return mbox_id_; }
+ unsigned get_mailbox_id() const { return mbox_id_; }
+ unsigned get_id() const { return id_; }
bool is_detached() const { return detached_; }
bool is_assigned() const { return (to_ != nullptr && from_ != nullptr); }
expectations of the other side, too. See */
std::function<void(CommImpl*, void*, size_t)> copy_data_fun;
+ /* In stateful MC, we need to ignore some private memory that is not relevant to the application state */
+ static void setup_mc();
+
/* Model actions */
timeout_action_type src_timeout_{nullptr, [](resource::Action* a) { a->unref(); }}; /* timeout set by the sender */
timeout_action_type dst_timeout_{nullptr, [](resource::Action* a) { a->unref(); }}; /* timeout set by the receiver */
{
if (const auto* comm = dynamic_cast<activity::CommImpl const*>(act)) {
stream << " " << (short)mc::Transition::Type::COMM_TEST;
- stream << ' ' << (uintptr_t)comm;
+ stream << ' ' << comm->get_id();
stream << ' ' << (comm->src_actor_ != nullptr ? comm->src_actor_->get_pid() : -1);
stream << ' ' << (comm->dst_actor_ != nullptr ? comm->dst_actor_->get_pid() : -1);
stream << ' ' << comm->get_mailbox_id();
if (const auto* comm = dynamic_cast<activity::CommImpl const*>(act)) {
const std::string src_buff_id = ptr_to_id<unsigned char>(comm->src_buff_);
const std::string dst_buff_id = ptr_to_id<unsigned char>(comm->dst_buff_);
- return "CommTest(comm_id:" + ptr_to_id<activity::CommImpl const>(comm) +
+ return "CommTest(comm_id:" + std::to_string(comm->get_id()) +
" src:" + std::to_string(comm->src_actor_ != nullptr ? comm->src_actor_->get_pid() : -1) +
" dst:" + std::to_string(comm->dst_actor_ != nullptr ? comm->dst_actor_->get_pid() : -1) +
" mbox:" + std::to_string(comm->get_mailbox_id()) + " srcbuf:" + src_buff_id + " dstbuf:" + dst_buff_id +
{
if (const auto* comm = dynamic_cast<activity::CommImpl const*>(act)) {
stream << (short)mc::Transition::Type::COMM_WAIT << ' ';
- stream << timeout << ' ' << (uintptr_t)comm;
+ stream << timeout << ' ' << comm->get_id();
stream << ' ' << (comm->src_actor_ != nullptr ? comm->src_actor_->get_pid() : -1);
stream << ' ' << (comm->dst_actor_ != nullptr ? comm->dst_actor_->get_pid() : -1);
if (const auto* comm = dynamic_cast<activity::CommImpl const*>(act)) {
const std::string src_buff_id = ptr_to_id<unsigned char>(comm->src_buff_);
const std::string dst_buff_id = ptr_to_id<unsigned char>(comm->dst_buff_);
- return "CommWait(comm_id:" + ptr_to_id<activity::CommImpl const>(comm) +
+ return "CommWait(comm_id:" + std::to_string(comm->get_id()) +
" src:" + std::to_string(comm->src_actor_ != nullptr ? comm->src_actor_->get_pid() : -1) +
" dst:" + std::to_string(comm->dst_actor_ != nullptr ? comm->dst_actor_->get_pid() : -1) +
" mbox:" + (comm->get_mailbox() == nullptr ? "-" : comm->get_mailbox()->get_name()) +
{
/* Note that the comm_ is 0 until after the execution of the simcall */
stream << (short)mc::Transition::Type::COMM_ASYNC_SEND << ' ';
- stream << (uintptr_t)comm_ << ' ' << mbox_->get_id() << ' ' << (uintptr_t)src_buff_ << ' ' << src_buff_size_ << ' '
- << tag_;
+ stream << (comm_ ? comm_->get_id() : 0) << ' ' << mbox_->get_id() << ' ' << (uintptr_t)src_buff_ << ' '
+ << src_buff_size_ << ' ' << tag_;
XBT_DEBUG("SendObserver comm:%p mbox:%u buff:%p size:%zu tag:%d", comm_, mbox_->get_id(), src_buff_, src_buff_size_,
tag_);
}
std::string CommIsendSimcall::to_string() const
{
- return "CommAsyncSend(comm_id: " + std::to_string((uintptr_t)comm_) + " mbox:" + std::to_string(mbox_->get_id()) +
+ return "CommAsyncSend(comm_id: " + std::to_string(comm_->get_id()) + " mbox:" + std::to_string(mbox_->get_id()) +
" srcbuf:" + ptr_to_id<unsigned char>(src_buff_) + " bufsize:" + std::to_string(src_buff_size_) +
" tag: " + std::to_string(tag_) + ")";
}
{
/* Note that the comm_ is 0 until after the execution of the simcall */
stream << (short)mc::Transition::Type::COMM_ASYNC_RECV << ' ';
- stream << (uintptr_t)comm_ << ' ' << mbox_->get_id() << ' ' << (uintptr_t)dst_buff_ << ' ' << tag_;
+ stream << (comm_ ? comm_->get_id() : 0) << ' ' << mbox_->get_id() << ' ' << (uintptr_t)dst_buff_ << ' ' << tag_;
XBT_DEBUG("RecvObserver comm:%p mbox:%u buff:%p tag:%d", comm_, mbox_->get_id(), dst_buff_, tag_);
}
std::string CommIrecvSimcall::to_string() const
{
- return "CommAsyncRecv(comm_id: " + ptr_to_id<activity::CommImpl const>(comm_) +
- " mbox:" + std::to_string(mbox_->get_id()) + " dstbuf:" + ptr_to_id<unsigned char>(dst_buff_) +
- " tag: " + std::to_string(tag_) + ")";
+ return "CommAsyncRecv(comm_id: " + std::to_string(comm_->get_id()) + " mbox:" + std::to_string(mbox_->get_id()) +
+ " dstbuf:" + ptr_to_id<unsigned char>(dst_buff_) + " tag: " + std::to_string(tag_) + ")";
}
} // namespace simgrid::kernel::actor
#include "src/mc/explo/odpor/WakeupTreeIterator.hpp"
#include "src/mc/explo/odpor/WakeupTree.hpp"
+#include "xbt/asserts.h"
namespace simgrid::mc::odpor {
// there are no cycles. This means that at least
// one node in the tree won't have any children,
// so the loop will eventually terminate
- auto* cur_top_node = *post_order_iteration.top();
+ WakeupTreeNode* cur_top_node = *post_order_iteration.top();
while (not cur_top_node->is_leaf()) {
// INVARIANT: Since we push children in
// reverse order (right-most to left-most),
// we ensure that we'll always process left-most
// children first
auto& children = cur_top_node->children_;
-
for (auto iter = children.rbegin(); iter != children.rend(); ++iter) {
- // iter.base() points one element past where we seek; hence,
- // we move it over one position
+ // iter.base() points one element past where we seek; that is,
+ // we want the value one position forward
post_order_iteration.push(std::prev(iter.base()));
}
+ has_added_children.push(cur_top_node);
cur_top_node = *post_order_iteration.top();
}
}
return;
}
- auto prev_top_handle = post_order_iteration.top();
post_order_iteration.pop();
// If there are now no longer any nodes left,
return;
}
- // Otherwise, look at the next top node. If
- // `prev_top` is that node's right-most child,
- // then we don't attempt to re-add `next_top`'s
- // children again for we would have already seen them.
- // To actually determine "right-most", we check if
- // moving over to the right one spot brings us to the
- // end of the candidate parent's list
- const auto* next_top_node = *post_order_iteration.top();
- if ((++prev_top_handle) != next_top_node->get_ordered_children().end()) {
+ xbt_assert(not has_added_children.empty(), "Invariant violated: There are more "
+ "nodes in the iteration that we must search "
+ "yet nobody has claimed to have added these nodes. "
+ "This implies that the algorithm is not iterating over "
+ "the wakeup tree is not following the post-fix order "
+ "correctly");
+
+ // Otherwise, look at what is the new, current top node.
+ // We're traversing the tree in
+ //
+ // If we've already added our children, we want
+ // to be sure not to add them again; but we ALSO
+ // want to be sure that we now start checking against
+ // the the node that's next in line as "finished"
+ //
+ // INVARIANT: Since we're searching in post-fix order,
+ // it always suffices to compare the current node
+ // with the top of the stack of nodes which have added their
+ // children
+ if (*post_order_iteration.top() == has_added_children.top()) {
+ has_added_children.pop();
+ } else {
push_until_left_most_found();
}
}
*/
std::stack<node_handle> post_order_iteration;
+ /**
+ * @brief The nodes in the current ordering that have already
+ * added their own children
+ *
+ * We need to be able to determine whether to add the children
+ * of a given node. Eventually, we want to search that node itself,
+ * but we have to first search its children. Later, when we
+ * reach each node in this stack again, we'll remember not to add
+ * its children and will search the node in the stack instead.
+ */
+ std::stack<WakeupTreeNode*> has_added_children;
+
/**
* @brief Search the wakeup tree until a leaf node appears at the front
* of the iteration, pushing all children towards the top of the stack
});
xbt_assert(issuer != C.end(),
"Invariant violation! A (supposedly) enabled `CommWait` transition "
- "waiting on communication %lu should not be enabled: the receive/send "
+ "waiting on communication %u should not be enabled: the receive/send "
"transition which generated the communication is not an action taken "
"to reach state(C) (the state of the configuration), which should "
"be an impossibility if `%s` is enabled. Please report this as "
});
xbt_assert(issuer != C.end(),
"An enabled `CommTest` transition (%s) is testing a communication"
- "%lu not created by a receive/send "
+ "%u not created by a receive/send "
"transition. SimGrid cannot currently handle test actions "
"under which a test is performed on a communication that was "
"not directly created by a receive/send operation of the same actor.",
#endif
}
+void MC_unignore(void* addr, size_t size)
+{
+#if SIMGRID_HAVE_STATEFUL_MC
+ xbt_assert(get_model_checking_mode() != ModelCheckingMode::CHECKER_SIDE,
+ "This should be called from the client side");
+ if (MC_is_active())
+ AppSide::get()->unignore_memory(addr, size);
+#endif
+}
+
void MC_ignore_heap(void *address, size_t size)
{
#if SIMGRID_HAVE_STATEFUL_MC
simgrid::mc::processes_time.resize(simgrid::kernel::actor::ActorImpl::get_maxpid());
MC_ignore_heap(simgrid::mc::processes_time.data(),
simgrid::mc::processes_time.size() * sizeof(simgrid::mc::processes_time[0]));
+ kernel::activity::CommImpl::setup_mc();
sthread_disable();
coverage_checkpoint();
message.size = size;
xbt_assert(channel_.send(message) == 0, "Could not send IGNORE_MEMORY message to model-checker: %s", strerror(errno));
#else
- xbt_die("Cannot really call ignore_heap() in non-SIMGRID_MC mode.");
+ xbt_die("Cannot really call ignore_memory() in non-SIMGRID_MC mode.");
+#endif
+}
+
+void AppSide::unignore_memory(void* addr, std::size_t size) const
+{
+ if (not MC_is_active() || not need_memory_info_)
+ return;
+
+#if SIMGRID_HAVE_STATEFUL_MC
+ s_mc_message_ignore_memory_t message = {};
+ message.type = MessageType::UNIGNORE_MEMORY;
+ message.addr = (std::uintptr_t)addr;
+ message.size = size;
+ xbt_assert(channel_.send(message) == 0, "Could not send UNIGNORE_MEMORY message to model-checker: %s",
+ strerror(errno));
+#else
+ xbt_die("Cannot really call unignore_memory() in non-SIMGRID_MC mode.");
#endif
}
XBT_ATTRIB_NORETURN void main_loop();
void report_assertion_failure();
void ignore_memory(void* addr, std::size_t size) const;
+ void unignore_memory(void* addr, std::size_t size) const;
void ignore_heap(void* addr, std::size_t size) const;
void unignore_heap(void* addr, std::size_t size) const;
void declare_symbol(const char* name, int* value) const;
break;
}
+ case MessageType::UNIGNORE_MEMORY: {
+ consumed = sizeof(s_mc_message_ignore_memory_t);
+#if SIMGRID_HAVE_STATEFUL_MC
+ if (remote_memory_ != nullptr) {
+ s_mc_message_ignore_memory_t message;
+ xbt_assert(size >= static_cast<ssize_t>(sizeof(message)), "Broken message");
+ memcpy(&message, buffer, sizeof(message));
+ get_remote_memory()->unignore_region(message.addr, message.size);
+ } else
+#endif
+ XBT_INFO("Ignoring an UNIGNORE_MEMORY message because we don't need to introspect memory.");
+ break;
+ }
+
case MessageType::STACK_REGION: {
consumed = sizeof(s_mc_message_stack_region_t);
#if SIMGRID_HAVE_STATEFUL_MC
namespace simgrid::mc {
XBT_DECLARE_ENUM_CLASS(MessageType, NONE, NEED_MEMINFO, NEED_MEMINFO_REPLY, FORK, FORK_REPLY, WAIT_CHILD,
- WAIT_CHILD_REPLY, CONTINUE, IGNORE_HEAP, UNIGNORE_HEAP, IGNORE_MEMORY, STACK_REGION,
- REGISTER_SYMBOL, DEADLOCK_CHECK, DEADLOCK_CHECK_REPLY, WAITING, SIMCALL_EXECUTE,
+ WAIT_CHILD_REPLY, CONTINUE, IGNORE_HEAP, UNIGNORE_HEAP, IGNORE_MEMORY, UNIGNORE_MEMORY,
+ STACK_REGION, REGISTER_SYMBOL, DEADLOCK_CHECK, DEADLOCK_CHECK_REPLY, WAITING, SIMCALL_EXECUTE,
SIMCALL_EXECUTE_REPLY, ASSERTION_FAILED, ACTORS_STATUS, ACTORS_STATUS_REPLY_COUNT,
ACTORS_STATUS_REPLY_SIMCALL, ACTORS_STATUS_REPLY_TRANSITION, ACTORS_MAXPID, ACTORS_MAXPID_REPLY,
FINALIZE, FINALIZE_REPLY);
ignored_regions_.insert(pos, region);
}
+void RemoteProcessMemory::unignore_region(std::uint64_t addr, std::size_t size)
+{
+ IgnoredRegion region;
+ region.addr = addr;
+ region.size = size;
+
+ auto pos = std::lower_bound(ignored_regions_.begin(), ignored_regions_.end(), region,
+ [](auto const& reg1, auto const& reg2) {
+ return reg1.addr < reg2.addr || (reg1.addr == reg2.addr && reg1.size < reg2.size);
+ });
+ if (pos != ignored_regions_.end())
+ ignored_regions_.erase(pos);
+}
+
void RemoteProcessMemory::ignore_heap(IgnoredHeapRegion const& region)
{
// Binary search the position of insertion:
std::vector<IgnoredRegion> const& ignored_regions() const { return ignored_regions_; }
void ignore_region(std::uint64_t address, std::size_t size);
+ void unignore_region(std::uint64_t address, std::size_t size);
bool in_maestro_stack(RemotePtr<void> p) const
{
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_)
+CommWaitTransition::CommWaitTransition(aid_t issuer, int times_considered, bool timeout_, unsigned 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_)
+ , mbox_(mbox_)
, sender_(sender_)
, receiver_(receiver_)
- , mbox_(mbox_)
, sbuff_(sbuff_)
, rbuff_(rbuff_)
, size_(size_)
: Transition(Type::COMM_WAIT, issuer, times_considered)
{
xbt_assert(stream >> timeout_ >> comm_ >> sender_ >> receiver_ >> mbox_ >> sbuff_ >> rbuff_ >> size_);
- XBT_DEBUG("CommWaitTransition %s comm:%" PRIxPTR ", sender:%ld receiver:%ld mbox:%u sbuff:%" PRIxPTR
- " rbuff:%" PRIxPTR " size:%zu",
+ XBT_DEBUG("CommWaitTransition %s comm:%u, sender:%ld receiver:%ld mbox:%u sbuff:%" PRIxPTR " rbuff:%" PRIxPTR
+ " size:%zu",
(timeout_ ? "timeout" : "no-timeout"), comm_, sender_, receiver_, mbox_, sbuff_, rbuff_, size_);
}
std::string CommWaitTransition::to_string(bool verbose) const
return false; // Comm transitions are INDEP with non-comm transitions
}
-CommTestTransition::CommTestTransition(aid_t issuer, int times_considered, uintptr_t comm_, aid_t sender_,
+CommTestTransition::CommTestTransition(aid_t issuer, int times_considered, unsigned 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_)
+ , mbox_(mbox_)
, sender_(sender_)
, receiver_(receiver_)
- , mbox_(mbox_)
, sbuff_(sbuff_)
, rbuff_(rbuff_)
, size_(size_)
: Transition(Type::COMM_TEST, issuer, times_considered)
{
xbt_assert(stream >> comm_ >> sender_ >> receiver_ >> mbox_ >> sbuff_ >> rbuff_ >> size_);
- XBT_DEBUG("CommTestTransition comm:%" PRIxPTR ", sender:%ld receiver:%ld mbox:%u sbuff:%" PRIxPTR " rbuff:%" PRIxPTR
+ XBT_DEBUG("CommTestTransition comm:%u, sender:%ld receiver:%ld mbox:%u sbuff:%" PRIxPTR " rbuff:%" PRIxPTR
" size:%zu",
comm_, sender_, receiver_, mbox_, sbuff_, rbuff_, size_);
}
return false; // Comm transitions are INDEP with non-comm transitions
}
-CommRecvTransition::CommRecvTransition(aid_t issuer, int times_considered, uintptr_t comm_, unsigned mbox_,
+CommRecvTransition::CommRecvTransition(aid_t issuer, int times_considered, unsigned comm_, unsigned mbox_,
uintptr_t rbuff_, int tag_)
: Transition(Type::COMM_ASYNC_RECV, issuer, times_considered)
, comm_(comm_)
if (mbox_ != test->mbox_)
return false;
- if ((aid_ != test->sender_) && (aid_ != test->receiver_) && (test->rbuff_ != rbuff_))
+ if ((aid_ != test->sender_) && (aid_ != test->receiver_))
return false;
// If the test is checking a paired comm already, we're independent!
if (mbox_ != wait->mbox_)
return false;
- if ((aid_ != wait->sender_) && (aid_ != wait->receiver_) && (wait->rbuff_ != rbuff_))
+ if ((aid_ != wait->sender_) && (aid_ != wait->receiver_))
return false;
// If the wait is waiting on a paired comm already, we're independent!
return false; // Comm transitions are INDEP with non-comm transitions
}
-CommSendTransition::CommSendTransition(aid_t issuer, int times_considered, uintptr_t comm_, unsigned mbox_,
+CommSendTransition::CommSendTransition(aid_t issuer, int times_considered, unsigned comm_, unsigned mbox_,
uintptr_t sbuff_, size_t size_, int tag_)
: Transition(Type::COMM_ASYNC_SEND, issuer, times_considered)
, comm_(comm_)
: Transition(Type::COMM_ASYNC_SEND, issuer, times_considered)
{
xbt_assert(stream >> comm_ >> mbox_ >> sbuff_ >> size_ >> tag_);
- XBT_DEBUG("SendTransition comm:%" PRIxPTR " mbox:%u sbuff:%" PRIxPTR " size:%zu", comm_, mbox_, sbuff_, size_);
+ XBT_DEBUG("SendTransition comm:%u mbox:%u sbuff:%" PRIxPTR " size:%zu", comm_, mbox_, sbuff_, size_);
}
std::string CommSendTransition::to_string(bool verbose = false) const
{
if (mbox_ != test->mbox_)
return false;
- if ((aid_ != test->sender_) && (aid_ != test->receiver_) && (test->sbuff_ != sbuff_))
+ if ((aid_ != test->sender_) && (aid_ != test->receiver_))
return false;
// If the test is checking a paired comm already, we're independent!
if (mbox_ != wait->mbox_)
return false;
- if ((aid_ != wait->sender_) && (aid_ != wait->receiver_) && (wait->sbuff_ != sbuff_))
+ if ((aid_ != wait->sender_) && (aid_ != wait->receiver_))
return false;
// If the wait is waiting on a paired comm already, we're independent!
class CommWaitTransition : public Transition {
bool timeout_;
- uintptr_t comm_;
+ unsigned comm_;
+ unsigned mbox_;
aid_t sender_;
aid_t receiver_;
- unsigned mbox_;
uintptr_t sbuff_;
uintptr_t rbuff_;
size_t size_;
friend CommTestTransition;
public:
- CommWaitTransition(aid_t issuer, int times_considered, bool timeout_, uintptr_t comm_, aid_t sender_, aid_t receiver_,
+ CommWaitTransition(aid_t issuer, int times_considered, bool timeout_, unsigned 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;
bool get_timeout() const { return timeout_; }
- /** Address of the corresponding Communication object in the application */
- uintptr_t get_comm() const { return comm_; }
+ /** ID of the corresponding Communication object in the application, or 0 if unknown */
+ unsigned get_comm() const { return comm_; }
/** Sender ID */
aid_t get_sender() const { return sender_; }
/** Receiver ID */
size_t get_size() const { return size_; }
};
class CommTestTransition : public Transition {
- uintptr_t comm_;
+ unsigned comm_;
+ unsigned mbox_;
aid_t sender_;
aid_t receiver_;
- unsigned mbox_;
uintptr_t sbuff_;
uintptr_t rbuff_;
size_t size_;
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, unsigned 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;
- /** Address of the corresponding Communication object in the application */
- uintptr_t get_comm() const { return comm_; }
+ /** ID of the corresponding Communication object in the application, or 0 if unknown */
+ unsigned get_comm() const { return comm_; }
/** Sender ID */
aid_t get_sender() const { return sender_; }
/** Receiver ID */
};
class CommRecvTransition : public Transition {
- uintptr_t comm_; /* Addr of the CommImpl */
+ unsigned comm_; /* ID of the CommImpl or 0 if not known */
unsigned mbox_;
uintptr_t rbuff_;
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, unsigned 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;
- /** Address of the corresponding Communication object in the application */
- uintptr_t get_comm() const { return comm_; }
+ /** ID of the corresponding Communication object in the application (or 0 if unknown)*/
+ unsigned get_comm() const { return comm_; }
/** Mailbox ID */
unsigned get_mailbox() const { return mbox_; }
/** Receiver buffer */
};
class CommSendTransition : public Transition {
- uintptr_t comm_; /* Addr of the CommImpl */
+ unsigned comm_;
unsigned mbox_;
uintptr_t sbuff_;
size_t size_;
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, unsigned 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;
- /** Address of the corresponding Communication object in the application */
- uintptr_t get_comm() const { return comm_; }
+ /** ID of the corresponding Communication object in the application, or 0 if unknown */
+ unsigned get_comm() const { return comm_; }
/** Mailbox ID */
unsigned get_mailbox() const { return mbox_; }
/** Sender buffer */
{
XBT_INFO("*** GET/SET DATA for disk: %s ***", disk->get_cname());
- const std::string* data = disk->get_data<std::string>();
+ auto data = disk->get_unique_data<std::string>();
XBT_INFO("Get data: '%s'", data ? data->c_str() : "No User Data");
disk->set_data(new std::string("Some data"));
- data = disk->get_data<std::string>();
+ data = disk->get_unique_data<std::string>();
XBT_INFO(" Set and get data: '%s'", data->c_str());
- delete data;
}
static void dump_platform_disks()
> If this is too much, consider sharing allocations for computation buffers.
> This can be done automatically by setting --cfg=smpi/auto-shared-malloc-thresh to the minimum size wanted size (this can alter execution if data content is necessary)
>
-> [0.000000] [mc_dfs/INFO] DFS exploration ended. 228 unique states visited; 54 backtracks (866 transition replays, 1148 states visited overall)
+> [0.000000] [mc_dfs/INFO] DFS exploration ended. 211 unique states visited; 50 backtracks (837 transition replays, 1098 states visited overall)
