From: Martin Quinson Date: Tue, 18 Jul 2017 00:31:09 +0000 (+0200) Subject: MC: checker kindly ask the app whether an actor is enabled instead of reading tons... X-Git-Tag: v3_17~369 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/831d719023e7a0af690f54db87a5e6ba4802ede3 MC: checker kindly ask the app whether an actor is enabled instead of reading tons of remote memory --- diff --git a/src/mc/mc_base.cpp b/src/mc/mc_base.cpp index f84aad4cb6..90fedffd0a 100644 --- a/src/mc/mc_base.cpp +++ b/src/mc/mc_base.cpp @@ -69,8 +69,15 @@ void wait_for_requests() // Called from both MCer and MCed: bool actor_is_enabled(smx_actor_t actor) { +#if SIMGRID_HAVE_MC + // If in the MCer, ask the client app since it has all the data + if (mc_model_checker != nullptr) { + return mc_model_checker->process().actor_is_enabled(actor->pid); + } +#endif + + // Now, we are in the client app, no need for remote memory reading. smx_simcall_t req = &actor->simcall; - // TODO, add support for the subtypes? switch (req->call) { case SIMCALL_NONE: @@ -81,16 +88,6 @@ bool actor_is_enabled(smx_actor_t actor) simgrid::kernel::activity::CommImpl* act = static_cast(simcall_comm_wait__getraw__comm(req)); -#if SIMGRID_HAVE_MC - // Fetch from MCed memory: - // HACK, type puning - if (mc_model_checker != nullptr) { - simgrid::mc::Remote temp_comm; - mc_model_checker->process().read(temp_comm, remote(act)); - act = static_cast(temp_comm.getBuffer()); - } -#endif - if (act->src_timeout || act->dst_timeout) { /* If it has a timeout it will be always be enabled (regardless of who declared the timeout), * because even if the communication is not ready, it can timeout and won't block. */ @@ -108,38 +105,10 @@ bool actor_is_enabled(smx_actor_t actor) simgrid::kernel::activity::CommImpl* act = static_cast(simcall_comm_wait__getraw__comm(req)); -#if SIMGRID_HAVE_MC - s_xbt_dynar_t comms_buffer; - size_t buffer_size = 0; - if (mc_model_checker != nullptr) { - // Read dynar: - mc_model_checker->process().read(&comms_buffer, remote(simcall_comm_waitany__get__comms(req))); - assert(comms_buffer.elmsize == sizeof(act)); - buffer_size = comms_buffer.elmsize * comms_buffer.used; - comms = &comms_buffer; - } else - comms = simcall_comm_waitany__get__comms(req); - - // Read all the dynar buffer: - char buffer[buffer_size]; - if (mc_model_checker != nullptr) - mc_model_checker->process().read_bytes(buffer, sizeof(buffer), remote(comms->data)); -#else comms = simcall_comm_waitany__get__comms(req); -#endif for (unsigned int index = 0; index < comms->used; ++index) { -#if SIMGRID_HAVE_MC - // Fetch act from MCed memory: - // HACK, type puning - simgrid::mc::Remote temp_comm; - if (mc_model_checker != nullptr) { - memcpy(&act, buffer + comms->elmsize * index, sizeof(act)); - mc_model_checker->process().read(temp_comm, remote(act)); - act = static_cast(temp_comm.getBuffer()); - } else -#endif - act = xbt_dynar_get_as(comms, index, simgrid::kernel::activity::CommImpl*); + act = xbt_dynar_get_as(comms, index, simgrid::kernel::activity::CommImpl*); if (act->src_proc && act->dst_proc) return true; } @@ -148,24 +117,9 @@ bool actor_is_enabled(smx_actor_t actor) case SIMCALL_MUTEX_LOCK: { smx_mutex_t mutex = simcall_mutex_lock__get__mutex(req); -#if SIMGRID_HAVE_MC - simgrid::mc::Remote temp_mutex; - if (mc_model_checker != nullptr) { - mc_model_checker->process().read(temp_mutex.getBuffer(), remote(mutex)); - mutex = temp_mutex.getBuffer(); - } -#endif if (mutex->owner == nullptr) return true; -#if SIMGRID_HAVE_MC - else if (mc_model_checker != nullptr) { - simgrid::mc::RemoteClient& modelchecked = mc_model_checker->process(); - // TODO, *(mutex->owner) :/ - return modelchecked.resolveActor(simgrid::mc::remote(mutex->owner))->pid == - modelchecked.resolveActor(simgrid::mc::remote(req->issuer))->pid; - } -#endif else return mutex->owner->pid == req->issuer->pid; } @@ -197,7 +151,10 @@ bool actor_is_enabled(smx_actor_t actor) */ bool request_is_visible(smx_simcall_t req) { +#if SIMGRID_HAVE_MC xbt_assert(mc_model_checker == nullptr, "This should be called from the client side"); +#endif + return req->call == SIMCALL_COMM_ISEND || req->call == SIMCALL_COMM_IRECV || req->call == SIMCALL_COMM_WAIT diff --git a/src/mc/remote/Client.cpp b/src/mc/remote/Client.cpp index e82f14209f..9bfc523a19 100644 --- a/src/mc/remote/Client.cpp +++ b/src/mc/remote/Client.cpp @@ -118,6 +118,12 @@ void Client::handleRestore(s_mc_message_restore_t* message) smpi_really_switch_data_segment(message->index); #endif } +void Client::handleActorEnabled(s_mc_message_actor_enabled_t* msg) +{ + bool res = simgrid::mc::actor_is_enabled(SIMIX_process_from_PID(msg->aid)); + s_mc_message_int answer{MC_MESSAGE_ACTOR_ENABLED_REPLY, res}; + channel_.send(answer); +} void Client::handleMessages() { @@ -158,6 +164,13 @@ void Client::handleMessages() handleRestore((s_mc_message_restore_t*)message_buffer); break; + case MC_MESSAGE_ACTOR_ENABLED: + xbt_assert(received_size == sizeof(s_mc_message_actor_enabled_t), + "Unexpected size for ACTOR_ENABLED (%zu != %zu)", received_size, + sizeof(s_mc_message_actor_enabled_t)); + handleActorEnabled((s_mc_message_actor_enabled_t*)message_buffer); + break; + default: xbt_die("Received unexpected message %s (%i)", MC_message_type_name(message->type), message->type); break; diff --git a/src/mc/remote/Client.hpp b/src/mc/remote/Client.hpp index b9059a3229..7770b65324 100644 --- a/src/mc/remote/Client.hpp +++ b/src/mc/remote/Client.hpp @@ -42,6 +42,7 @@ private: void handleContinue(mc_message_t* msg); void handleSimcall(s_mc_message_simcall_handle_t* message); void handleRestore(s_mc_message_restore_t* msg); + void handleActorEnabled(s_mc_message_actor_enabled_t* msg); public: Channel const& getChannel() const { return channel_; } diff --git a/src/mc/remote/RemoteClient.cpp b/src/mc/remote/RemoteClient.cpp index 6046e09772..f96e1e5ab9 100644 --- a/src/mc/remote/RemoteClient.cpp +++ b/src/mc/remote/RemoteClient.cpp @@ -673,5 +673,15 @@ void RemoteClient::dumpStack() unw_destroy_addr_space(as); return; } + +bool RemoteClient::actor_is_enabled(aid_t pid) +{ + s_mc_message_actor_enabled msg{MC_MESSAGE_ACTOR_ENABLED, pid}; + process()->getChannel().send(msg); + char buff[MC_MESSAGE_LENGTH]; + ssize_t received = process()->getChannel().receive(buff, MC_MESSAGE_LENGTH, true); + xbt_assert(received == sizeof(s_mc_message_int), "Unexpected size in answer to ACTOR_ENABLED"); + return ((mc_message_int_t*)buff)->value; +} } } diff --git a/src/mc/remote/RemoteClient.hpp b/src/mc/remote/RemoteClient.hpp index 34c31b698f..2fc858674e 100644 --- a/src/mc/remote/RemoteClient.hpp +++ b/src/mc/remote/RemoteClient.hpp @@ -302,6 +302,9 @@ public: // Libunwind-data /** The corresponding context */ void* unw_underlying_context; + + /* Check whether the given actor is enabled */ + bool actor_is_enabled(aid_t pid); }; /** Open a FD to a remote process memory (`/dev/$pid/mem`) diff --git a/src/mc/remote/mc_protocol.cpp b/src/mc/remote/mc_protocol.cpp index 5baf1d568b..74bec4e710 100644 --- a/src/mc/remote/mc_protocol.cpp +++ b/src/mc/remote/mc_protocol.cpp @@ -46,6 +46,12 @@ const char* MC_message_type_name(e_mc_message_type type) return "SIMCALL_HANDLE"; case MC_MESSAGE_ASSERTION_FAILED: return "ASSERTION_FAILED"; + + case MC_MESSAGE_ACTOR_ENABLED: + return "ACTOR_ENABLED"; + case MC_MESSAGE_ACTOR_ENABLED_REPLY: + return "ACTOR_ENABLED_REPLY"; + default: return "?"; } diff --git a/src/mc/remote/mc_protocol.h b/src/mc/remote/mc_protocol.h index 4ca6653ad7..bac7981555 100644 --- a/src/mc/remote/mc_protocol.h +++ b/src/mc/remote/mc_protocol.h @@ -11,6 +11,7 @@ #include #include "mc/datatypes.h" +#include "simgrid/forward.h" SG_BEGIN_DECL() @@ -41,6 +42,8 @@ typedef enum { MC_MESSAGE_ASSERTION_FAILED, // MCer request to finish the restoration: MC_MESSAGE_RESTORE, + MC_MESSAGE_ACTOR_ENABLED, + MC_MESSAGE_ACTOR_ENABLED_REPLY } e_mc_message_type; #define MC_MESSAGE_LENGTH 512 @@ -112,6 +115,12 @@ struct s_mc_message_restore { }; typedef struct s_mc_message_restore s_mc_message_restore_t; +struct s_mc_message_actor_enabled { + e_mc_message_type type; + aid_t aid; // actor ID +}; +typedef struct s_mc_message_actor_enabled s_mc_message_actor_enabled_t; + XBT_PRIVATE const char* MC_message_type_name(e_mc_message_type type); SG_END_DECL()