const simgrid::kernel::activity::CommImpl* act = temp_act.get_buffer();
if (act->src_actor_.get() && act->dst_actor_.get())
state->transition_.argument_ = 0; // OK
- else if (act->src_actor_.get() == nullptr && act->type_ == simgrid::kernel::activity::CommImpl::Type::READY &&
+ else if (act->src_actor_.get() == nullptr && act->state_ == simgrid::kernel::activity::State::READY &&
act->detached())
state->transition_.argument_ = 0; // OK
else
}
// Does half the job
-bool Api::request_depend_asymmetric(smx_simcall_t r1, smx_simcall_t r2) const
+bool Api::request_depend_asymmetric(smx_simcall_t r1, smx_simcall_t r2) const
{
if (r1->call_ == Simcall::COMM_ISEND && r2->call_ == Simcall::COMM_IRECV)
return false;
const kernel::activity::CommImpl* synchro2 = get_comm(r2);
if ((r1->call_ == Simcall::COMM_ISEND || r1->call_ == Simcall::COMM_IRECV) && r2->call_ == Simcall::COMM_WAIT) {
- const kernel::activity::MailboxImpl* mbox = get_mbox_remote_addr(r1);
+ auto mbox = get_mbox_remote_addr(r1);
+ RemotePtr<kernel::activity::MailboxImpl> synchro2_mbox_cpy = remote(synchro2->mbox_cpy);
- if (mbox != synchro2->mbox_cpy
- && simcall_comm_wait__get__timeout(r2) <= 0)
+ if (mbox != synchro2_mbox_cpy && simcall_comm_wait__get__timeout(r2) <= 0)
return false;
if ((r1->issuer_ != synchro2->src_actor_.get()) && (r1->issuer_ != synchro2->dst_actor_.get()) &&
RemotePtr<kernel::activity::CommImpl> Api::get_comm_waitany_raw_addr(smx_simcall_t request, int value) const
{
- auto addr = simgrid::simix::unmarshal_raw<simgrid::kernel::activity::CommImpl**>(request->args_[0]) + value;
+ auto addr = simgrid::simix::unmarshal_raw<simgrid::kernel::activity::CommImpl**>(request->args_[0]) + value;
auto comm_addr = mc_model_checker->get_remote_simulation().read(remote(addr));
return RemotePtr<kernel::activity::CommImpl>(static_cast<kernel::activity::CommImpl*>(comm_addr));
}
return simcall_get_issuer(req)->get_pid();
}
-smx_mailbox_t Api::get_mbox_remote_addr(smx_simcall_t const req) const
+RemotePtr<kernel::activity::MailboxImpl> Api::get_mbox_remote_addr(smx_simcall_t const req) const
{
+ RemotePtr<kernel::activity::MailboxImpl> mbox_addr;
switch (req->call_) {
case Simcall::COMM_ISEND:
- return simix::unmarshal<smx_mailbox_t>(req->args_[1]); // simcall_comm_isend__get__mbox
- case Simcall::COMM_IRECV:
- return simix::unmarshal<smx_mailbox_t>(req->args_[1]); // simcall_comm_irecv__get__mbox
+ case Simcall::COMM_IRECV: {
+ auto mbox_addr_ptr = simix::unmarshal<smx_mailbox_t>(req->args_[1]);
+ mbox_addr = remote(mbox_addr_ptr);
+ break;
+ }
default:
- return nullptr;
+ mbox_addr = RemotePtr<kernel::activity::MailboxImpl>();
+ break;
+ }
+ return mbox_addr;
+}
+
+RemotePtr<kernel::activity::ActivityImpl> Api::get_comm_remote_addr(smx_simcall_t const req) const
+{
+ RemotePtr<kernel::activity::ActivityImpl> comm_addr;
+ switch (req->call_) {
+ case Simcall::COMM_ISEND:
+ case Simcall::COMM_IRECV: {
+ auto comm_addr_ptr = simgrid::simix::unmarshal_raw<simgrid::kernel::activity::ActivityImpl*>(req->result_);
+ comm_addr = remote(comm_addr_ptr);
+ break;
+ }
+ default:
+ comm_addr = RemotePtr<kernel::activity::ActivityImpl>();
+ break;
}
+ return comm_addr;
}
bool Api::mc_is_null() const
return nullptr;
}
+std::list<udpor_transition_t> Api::get_enabled_transitions(simgrid::mc::State* state)
+{
+ std::list<udpor_transition_t> tr_list{};
+
+ for (auto& actor : mc_model_checker->get_remote_simulation().actors()) {
+ auto actor_pid = actor.copy.get_buffer()->get_pid();
+ auto actor_impl = actor.copy.get_buffer();
+
+ // Only consider the actors that were marked as interleaving by the checker algorithm
+ if (not state->actor_states_[actor_pid].is_todo())
+ continue;
+ // Not executable in the application
+ if (not simgrid::mc::actor_is_enabled(actor_impl))
+ continue;
+
+ udpor_transition_t udpor_transition = std::unique_ptr<s_udpor_transition>(new s_udpor_transition());
+ Simcall simcall_call = actor_impl->simcall_.call_;
+ smx_simcall_t simcall = &actor_impl->simcall_;
+ udpor_transition->call_ = simcall_call;
+ switch (simcall_call) {
+ case Simcall::COMM_ISEND:
+ case Simcall::COMM_IRECV: {
+ udpor_transition->mbox_remote_addr = get_mbox_remote_addr(simcall);
+ udpor_transition->comm_remote_addr = get_comm_remote_addr(simcall);
+ break;
+ }
+
+ default:
+ break;
+ }
+ tr_list.emplace_back(std::move(udpor_transition));
+ }
+
+ return tr_list;
+}
+
bool Api::simcall_check_dependency(smx_simcall_t const req1, smx_simcall_t const req2) const
{
if (req1->issuer_ == req2->issuer_)
return false;
- /* Wait with timeout transitions are not considered by the independence theorem, thus we consider them as dependent with all other transitions */
+ /* Wait with timeout transitions are not considered by the independence theorem, thus we consider them as dependent
+ * with all other transitions */
if ((req1->call_ == Simcall::COMM_WAIT && simcall_comm_wait__get__timeout(req1) > 0) ||
(req2->call_ == Simcall::COMM_WAIT && simcall_comm_wait__get__timeout(req2) > 0))
return true;
const char* Api::simcall_get_name(simgrid::simix::Simcall kind) const
{
- return SIMIX_simcall_name(kind);
+ return simcall_names[static_cast<int>(kind)];
}
#if HAVE_SMPI