From 934f086b51d328c46cb8fb20db2ad3efd4668ac9 Mon Sep 17 00:00:00 2001 From: Martin Quinson Date: Fri, 18 Feb 2022 17:10:54 +0100 Subject: [PATCH] Have the application execute its transition before returning SIMCALL_EXECUTE_ANSWER This makes the RPC protocol somewhat more complex, but it's mandatory to get the updated observer. This is useful in particular to Isend/Irecv observers that have a set_comm() field that cannot be set before executing the simcall. CommDet need that field anyway, so let's change the protocol that way. --- src/mc/ModelChecker.cpp | 8 ++++---- src/mc/remote/AppSide.cpp | 10 +++++----- 2 files changed, 9 insertions(+), 9 deletions(-) diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp index 0f0d02c3c0..9dbc7412bf 100644 --- a/src/mc/ModelChecker.cpp +++ b/src/mc/ModelChecker.cpp @@ -318,6 +318,10 @@ Transition* ModelChecker::handle_simcall(aid_t aid, int times_considered, bool n m.times_considered_ = times_considered; checker_side_.get_channel().send(m); + this->remote_process_->clear_cache(); + if (this->remote_process_->running()) + checker_side_.dispatch(); // The app may send messages while processing the transition + s_mc_message_simcall_execute_answer_t answer; ssize_t s = checker_side_.get_channel().receive(answer); xbt_assert(s != -1, "Could not receive message"); @@ -327,10 +331,6 @@ Transition* ModelChecker::handle_simcall(aid_t aid, int times_considered, bool n to_c_str(answer.type), (int)answer.type, (int)s, (int)MessageType::SIMCALL_EXECUTE_ANSWER, (int)sizeof(answer)); - this->remote_process_->clear_cache(); - if (this->remote_process_->running()) - checker_side_.dispatch(); // The app may send messages while processing the transition - if (new_transition) { std::stringstream stream(answer.buffer.data()); return deserialize_transition(aid, times_considered, stream); diff --git a/src/mc/remote/AppSide.cpp b/src/mc/remote/AppSide.cpp index ed860fc103..e56a85476d 100644 --- a/src/mc/remote/AppSide.cpp +++ b/src/mc/remote/AppSide.cpp @@ -99,6 +99,11 @@ 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_); + // 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)); @@ -118,11 +123,6 @@ void AppSide::handle_simcall_execute(const s_mc_message_simcall_execute_t* messa XBT_DEBUG("send SIMCALL_EXECUTE_ANSWER(%s) ~> '%s'", actor->get_cname(), str.c_str()); 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"); } void AppSide::handle_actor_enabled(const s_mc_message_actor_enabled_t* msg) const -- 2.20.1