X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/ec6c3b084bc456d7d1cd6e2b83e189c4cc308b6e..aa64bb0b015da853b7f904a9384cfa14cf42326f:/src/mc/remote/AppSide.cpp diff --git a/src/mc/remote/AppSide.cpp b/src/mc/remote/AppSide.cpp index 102fdcb8fd..bf79dfcf2b 100644 --- a/src/mc/remote/AppSide.cpp +++ b/src/mc/remote/AppSide.cpp @@ -4,6 +4,7 @@ * under the terms of the license (GNU LGPL) which comes with this package. */ #include "src/mc/remote/AppSide.hpp" +#include "simgrid/s4u/Host.hpp" #include "src/internal_config.h" #include "src/kernel/EngineImpl.hpp" #include "src/kernel/actor/ActorImpl.hpp" @@ -74,8 +75,7 @@ AppSide* AppSide::initialize() strerror(errno)); s_mc_message_initial_addresses_t message{MessageType::INITIAL_ADDRESSES, mmalloc_preinit(), - kernel::actor::get_maxpid_addr(), kernel::get_actors_addr(), - kernel::get_dead_actors_addr()}; + kernel::actor::get_maxpid_addr(), kernel::get_actors_addr()}; xbt_assert(instance_->channel_.send(message) == 0, "Could not send the initial message with addresses."); instance_->handle_messages(); @@ -97,21 +97,31 @@ void AppSide::handle_simcall_execute(const s_mc_message_simcall_execute_t* messa { kernel::actor::ActorImpl* actor = kernel::actor::ActorImpl::by_pid(message->aid_); xbt_assert(actor != nullptr, "Invalid pid %ld", message->aid_); - simgrid::kernel::actor::SimcallObserver* observer = nullptr; - if (actor->simcall_.observer_ != nullptr) { - observer = actor->simcall_.observer_->clone(); - actor->observer_stack_.push_back(observer); - } - // Finish the RPC from the server: we need to return a pointer to the observer, saved in a stable storage - s_mc_message_simcall_execute_answer_t answer{MessageType::SIMCALL_EXECUTE_ANSWER, observer}; - XBT_DEBUG("send SIMCALL_EXECUTE_ANSWER(%p)", observer); - xbt_assert(channel_.send(answer) == 0, "Could not send response"); // The client may send some messages to the server while processing the transition actor->simcall_handle(message->times_considered_); - // Say the server that the transition is over and that it should proceed xbt_assert(channel_.send(MessageType::WAITING) == 0, "Could not send MESSAGE_WAITING to model-checker"); + + // Finish the RPC from the server: return a serialized observer, to build a Transition on Checker side + s_mc_message_simcall_execute_answer_t answer; + memset(&answer, 0, sizeof(answer)); + answer.type = MessageType::SIMCALL_EXECUTE_ANSWER; + std::stringstream stream; + if (actor->simcall_.observer_ != nullptr) { + actor->simcall_.observer_->serialize(stream); + } else { + stream << (short)mc::Transition::Type::UNKNOWN; + } + std::string str = stream.str(); + xbt_assert(str.size() + 1 <= answer.buffer.size(), + "The serialized simcall is too large for the buffer. Please fix the code."); + strncpy(answer.buffer.data(), str.c_str(), answer.buffer.size() - 1); + answer.buffer.back() = '\0'; + + XBT_DEBUG("send SIMCALL_EXECUTE_ANSWER(%s) ~> '%s'", actor->get_cname(), str.c_str()); + xbt_assert(channel_.send(answer) == 0, "Could not send response"); + } void AppSide::handle_actor_enabled(const s_mc_message_actor_enabled_t* msg) const @@ -152,70 +162,6 @@ void AppSide::handle_messages() const handle_simcall_execute((s_mc_message_simcall_execute_t*)message_buffer.data()); break; - case MessageType::SIMCALL_IS_VISIBLE: { - assert_msg_size("SIMCALL_IS_VISIBLE", s_mc_message_simcall_is_visible_t); - auto msg_simcall = (s_mc_message_simcall_is_visible_t*)message_buffer.data(); - const kernel::actor::ActorImpl* actor = kernel::actor::ActorImpl::by_pid(msg_simcall->aid); - xbt_assert(actor != nullptr, "Invalid pid %ld", msg_simcall->aid); - xbt_assert(actor->simcall_.observer_, "The transition of %s has no observer", actor->get_cname()); - bool value = actor->simcall_.observer_->is_visible(); - - // Send result: - s_mc_message_simcall_is_visible_answer_t answer{MessageType::SIMCALL_IS_VISIBLE_ANSWER, value}; - xbt_assert(channel_.send(answer) == 0, "Could not send response"); - break; - } - - case MessageType::SIMCALL_TO_STRING: { - assert_msg_size("SIMCALL_TO_STRING", s_mc_message_simcall_to_string_t); - auto msg_simcall = (s_mc_message_simcall_to_string_t*)message_buffer.data(); - const kernel::actor::ActorImpl* actor = kernel::actor::ActorImpl::by_pid(msg_simcall->aid); - xbt_assert(actor != nullptr, "Invalid pid %ld", msg_simcall->aid); - xbt_assert(actor->simcall_.observer_, "The transition of %s has no observer", actor->get_cname()); - std::string value = actor->simcall_.observer_->to_string(msg_simcall->time_considered); - - // Send result: - s_mc_message_simcall_to_string_answer_t answer{MessageType::SIMCALL_TO_STRING_ANSWER, {0}}; - value.copy(answer.value, (sizeof answer.value) - 1); // last byte was set to '\0' by initialization above - xbt_assert(channel_.send(answer) == 0, "Could not send response"); - break; - } - - case MessageType::SIMCALLS_DEPENDENT: { - assert_msg_size("SIMCALLS_DEPENDENT", s_mc_message_simcalls_dependent_t); - auto msg_simcalls = (s_mc_message_simcalls_dependent_t*)message_buffer.data(); - auto* obs1 = msg_simcalls->obs1; - auto* obs2 = msg_simcalls->obs2; - bool res = true; - - if (obs1 != nullptr && obs2 != nullptr) - res = obs1->depends(obs2); - - XBT_DEBUG("return SIMCALLS_DEPENDENT(%s, %s) = %s", obs1->to_string(0).c_str(), obs2->to_string(0).c_str(), - (res ? "true" : "false")); - - // Send result: - s_mc_message_simcalls_dependent_answer_t answer{MessageType::SIMCALLS_DEPENDENT_ANSWER, 0}; - answer.value = res; - xbt_assert(channel_.send(answer) == 0, "Could not send response"); - break; - } - - case MessageType::SIMCALL_DOT_LABEL: { - assert_msg_size("SIMCALL_DOT_LABEL", s_mc_message_simcall_to_string_t); - auto msg_simcall = (s_mc_message_simcall_to_string_t*)message_buffer.data(); - const kernel::actor::ActorImpl* actor = kernel::actor::ActorImpl::by_pid(msg_simcall->aid); - xbt_assert(actor != nullptr, "Invalid pid %ld", msg_simcall->aid); - xbt_assert(actor->simcall_.observer_, "The transition of %s has no observer", actor->get_cname()); - std::string value = actor->simcall_.observer_->dot_label(msg_simcall->time_considered); - - // Send result: - s_mc_message_simcall_to_string_answer_t answer{MessageType::SIMCALL_TO_STRING_ANSWER, {0}}; - value.copy(answer.value, (sizeof answer.value) - 1); // last byte was set to '\0' by initialization above - xbt_assert(channel_.send(answer) == 0, "Could not send response"); - break; - } - case MessageType::ACTOR_ENABLED: assert_msg_size("ACTOR_ENABLED", s_mc_message_actor_enabled_t); handle_actor_enabled((s_mc_message_actor_enabled_t*)message_buffer.data());