return answer;
}
+void ModelChecker::finalize_app()
+{
+ int res = checker_side_.get_channel().send(MessageType::FINALIZE);
+ xbt_assert(res == 0, "Could not ask the app to finalize MPI on need");
+ s_mc_message_int_t message;
+ ssize_t s = checker_side_.get_channel().receive(message);
+ xbt_assert(s != -1, "Could not receive answer to FINALIZE");
+}
+
bool ModelChecker::checkDeadlock()
{
int res = checker_side_.get_channel().send(MessageType::DEADLOCK_CHECK);
XBT_ATTRIB_NORETURN void exit(int status);
bool checkDeadlock();
+ void finalize_app();
Checker* getChecker() const { return checker_; }
void setChecker(Checker* checker) { checker_ = checker; }
if (req == nullptr) {
XBT_DEBUG("There are no more processes to interleave. (depth %zu)", stack_.size() + 1);
+// mc_model_checker->finalize_app();
this->backtrack();
continue;
}
handle_actor_enabled((s_mc_message_actor_enabled_t*)message_buffer.data());
break;
+ case MessageType::FINALIZE: {
+#if HAVE_SMPI
+ XBT_INFO("Finalize. Smpi_enabled: %d", (int)smpi_enabled());
+ simix_global->display_all_actor_status();
+ if (smpi_enabled())
+ SMPI_finalize();
+#endif
+ s_mc_message_int_t answer{MessageType::DEADLOCK_CHECK_REPLY, 0};
+ xbt_assert(channel_.send(answer) == 0, "Could answer to FINALIZE");
+ break;
+ }
+
default:
xbt_die("Received unexpected message %s (%i)", to_c_str(message->type), static_cast<int>(message->type));
break;
XBT_DECLARE_ENUM_CLASS(MessageType, NONE, INITIAL_ADDRESSES, CONTINUE, IGNORE_HEAP, UNIGNORE_HEAP, IGNORE_MEMORY,
STACK_REGION, REGISTER_SYMBOL, DEADLOCK_CHECK, DEADLOCK_CHECK_REPLY, WAITING, SIMCALL_HANDLE,
SIMCALL_IS_VISIBLE, SIMCALL_IS_VISIBLE_ANSWER, SIMCALL_TO_STRING, SIMCALL_TO_STRING_ANSWER,
- SIMCALL_DOT_LABEL, ASSERTION_FAILED, ACTOR_ENABLED, ACTOR_ENABLED_REPLY);
+ SIMCALL_DOT_LABEL, ASSERTION_FAILED, ACTOR_ENABLED, ACTOR_ENABLED_REPLY, FINALIZE);
} // namespace mc
} // namespace simgrid
(xbt_log_no_loc ? (size_t)0xDEADBEEF : (size_t)actor->waiting_synchro_.get()),
actor->waiting_synchro_->get_cname(), (int)actor->waiting_synchro_->state_);
} else {
- XBT_INFO("Actor %ld (%s@%s)", actor->get_pid(), actor->get_cname(), actor->get_host()->get_cname());
+ XBT_INFO("Actor %ld (%s@%s) simcall %s", actor->get_pid(), actor->get_cname(), actor->get_host()->get_cname(), SIMIX_simcall_name(actor->simcall_.call_));
+
}
}
}