X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/cdfee3627a1498e068e9163c64b24650dee52f25..39c935d6d5ee86d153f6f7e6a10d723ae7c57f6f:/src/mc/mc_api.cpp diff --git a/src/mc/mc_api.cpp b/src/mc/mc_api.cpp index b5cb13d6cb..bcb4f6663d 100644 --- a/src/mc/mc_api.cpp +++ b/src/mc/mc_api.cpp @@ -1,20 +1,53 @@ #include "mc_api.hpp" +#include "src/kernel/activity/MailboxImpl.hpp" +#include "src/kernel/activity/MutexImpl.hpp" #include "src/mc/Session.hpp" #include "src/mc/mc_comm_pattern.hpp" #include "src/mc/mc_private.hpp" -#include "src/mc/mc_record.hpp" #include "src/mc/mc_smx.hpp" #include "src/mc/remote/RemoteSimulation.hpp" - +#include "src/mc/mc_pattern.hpp" +#include "src/mc/checker/SimcallInspector.hpp" #include #include +// #include + +#if HAVE_SMPI +#include "src/smpi/include/smpi_request.hpp" +#endif XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_api, mc, "Logging specific to MC Fasade APIs "); +using Simcall = simgrid::simix::Simcall; + namespace simgrid { namespace mc { +static inline const char* get_color(int id) +{ + static constexpr std::array colors{{"blue", "red", "green3", "goldenrod", "brown", "purple", + "magenta", "turquoise4", "gray25", "forestgreen", "hotpink", + "lightblue", "tan"}}; + return colors[id % colors.size()]; +} + +static char *pointer_to_string(void *pointer) +{ + if (XBT_LOG_ISENABLED(mc_api, xbt_log_priority_verbose)) + return bprintf("%p", pointer); + + return xbt_strdup("(verbose only)"); +} + +static char *buff_size_to_string(size_t buff_size) +{ + if (XBT_LOG_ISENABLED(mc_api, xbt_log_priority_verbose)) + return bprintf("%zu", buff_size); + + return xbt_strdup("(verbose only)"); +} + /* Search an enabled transition for the given process. * * This can be seen as an iterator returning the next transition of the process. @@ -33,14 +66,14 @@ static inline smx_simcall_t MC_state_choose_request_for_process(simgrid::mc::Sta simgrid::mc::ActorState* procstate = &state->actor_states_[actor->get_pid()]; state->transition_.pid_ = -1; state->transition_.argument_ = -1; - state->executed_req_.call_ = SIMCALL_NONE; + state->executed_req_.call_ = Simcall::NONE; if (not simgrid::mc::actor_is_enabled(actor)) return nullptr; // Not executable in the application smx_simcall_t req = nullptr; switch (actor->simcall_.call_) { - case SIMCALL_COMM_WAITANY: + case Simcall::COMM_WAITANY: state->transition_.argument_ = -1; while (procstate->times_considered < simcall_comm_waitany__get__count(&actor->simcall_)) { if (simgrid::mc::request_is_enabled_by_idx(&actor->simcall_, procstate->times_considered)) { @@ -57,7 +90,7 @@ static inline smx_simcall_t MC_state_choose_request_for_process(simgrid::mc::Sta req = &actor->simcall_; break; - case SIMCALL_COMM_TESTANY: { + case Simcall::COMM_TESTANY: { unsigned start_count = procstate->times_considered; state->transition_.argument_ = -1; while (procstate->times_considered < simcall_comm_testany__get__count(&actor->simcall_)) { @@ -78,7 +111,7 @@ static inline smx_simcall_t MC_state_choose_request_for_process(simgrid::mc::Sta break; } - case SIMCALL_COMM_WAIT: { + case Simcall::COMM_WAIT: { simgrid::mc::RemotePtr remote_act = remote(simcall_comm_wait__getraw__comm(&actor->simcall_)); simgrid::mc::Remote temp_act; @@ -96,7 +129,7 @@ static inline smx_simcall_t MC_state_choose_request_for_process(simgrid::mc::Sta break; } - case SIMCALL_MC_RANDOM: { + case Simcall::MC_RANDOM: { int min_value = simcall_mc_random__get__min(&actor->simcall_); state->transition_.argument_ = procstate->times_considered + min_value; procstate->times_considered++; @@ -123,8 +156,8 @@ static inline smx_simcall_t MC_state_choose_request_for_process(simgrid::mc::Sta /* The waitany and testany request are transformed into a wait or test request over the corresponding communication * action so it can be treated later by the dependence function. */ switch (req->call_) { - case SIMCALL_COMM_WAITANY: { - state->internal_req_.call_ = SIMCALL_COMM_WAIT; + case Simcall::COMM_WAITANY: { + state->internal_req_.call_ = Simcall::COMM_WAIT; simgrid::kernel::activity::CommImpl* remote_comm; remote_comm = mc_model_checker->get_remote_simulation().read( remote(simcall_comm_waitany__get__comms(req) + state->transition_.argument_)); @@ -134,8 +167,8 @@ static inline smx_simcall_t MC_state_choose_request_for_process(simgrid::mc::Sta break; } - case SIMCALL_COMM_TESTANY: - state->internal_req_.call_ = SIMCALL_COMM_TEST; + case Simcall::COMM_TESTANY: + state->internal_req_.call_ = Simcall::COMM_TEST; if (state->transition_.argument_ > 0) { simgrid::kernel::activity::CommImpl* remote_comm = mc_model_checker->get_remote_simulation().read( @@ -147,14 +180,14 @@ static inline smx_simcall_t MC_state_choose_request_for_process(simgrid::mc::Sta simcall_comm_test__set__result(&state->internal_req_, state->transition_.argument_); break; - case SIMCALL_COMM_WAIT: + case Simcall::COMM_WAIT: mc_model_checker->get_remote_simulation().read_bytes(&state->internal_comm_, sizeof(state->internal_comm_), remote(simcall_comm_wait__getraw__comm(req))); simcall_comm_wait__set__comm(&state->executed_req_, state->internal_comm_.get_buffer()); simcall_comm_wait__set__comm(&state->internal_req_, state->internal_comm_.get_buffer()); break; - case SIMCALL_COMM_TEST: + case Simcall::COMM_TEST: mc_model_checker->get_remote_simulation().read_bytes(&state->internal_comm_, sizeof(state->internal_comm_), remote(simcall_comm_test__getraw__comm(req))); simcall_comm_test__set__comm(&state->executed_req_, state->internal_comm_.get_buffer()); @@ -169,7 +202,7 @@ static inline smx_simcall_t MC_state_choose_request_for_process(simgrid::mc::Sta return req; } -void mc_api::initialize(char** argv) +void mc_api::initialize(char** argv) const { simgrid::mc::session = new simgrid::mc::Session([argv] { int i = 1; @@ -197,24 +230,137 @@ unsigned long mc_api::get_maxpid() const return MC_smx_get_maxpid(); } -void mc_api::copy_incomplete_comm_pattern(const simgrid::mc::State* state) const +int mc_api::get_actors_size() const +{ + return mc_model_checker->get_remote_simulation().actors().size(); +} + +bool mc_api::comm_addr_equal(const kernel::activity::CommImpl* comm_addr1, const kernel::activity::CommImpl* comm_addr2) const +{ + return remote(comm_addr1) == remote(comm_addr2); +} + +kernel::activity::CommImpl* mc_api::get_comm_isend_raw_addr(smx_simcall_t request) const +{ + auto comm_addr = simcall_comm_isend__getraw__result(request); + return static_cast(comm_addr); +} + +kernel::activity::CommImpl* mc_api::get_comm_wait_raw_addr(smx_simcall_t request) const +{ + return simcall_comm_wait__getraw__comm(request); +} + +kernel::activity::CommImpl* mc_api::get_comm_waitany_raw_addr(smx_simcall_t request, int value) const +{ + auto addr = mc_model_checker->get_remote_simulation().read(remote(simcall_comm_waitany__getraw__comms(request) + value)); + return static_cast(addr); +} + +std::string mc_api::get_pattern_comm_rdv(void* addr) const +{ + Remote temp_synchro; + mc_model_checker->get_remote_simulation().read(temp_synchro, remote((simgrid::kernel::activity::CommImpl*)addr)); + const kernel::activity::CommImpl* synchro = temp_synchro.get_buffer(); + + char* remote_name = mc_model_checker->get_remote_simulation().read(RemotePtr( + (uint64_t)(synchro->get_mailbox() ? &synchro->get_mailbox()->get_name() : &synchro->mbox_cpy->get_name()))); + auto rdv = mc_model_checker->get_remote_simulation().read_string(RemotePtr(remote_name)); + return rdv; +} + +unsigned long mc_api::get_pattern_comm_src_proc(void* addr) const +{ + Remote temp_synchro; + mc_model_checker->get_remote_simulation().read(temp_synchro, remote((simgrid::kernel::activity::CommImpl*)addr)); + const kernel::activity::CommImpl* synchro = temp_synchro.get_buffer(); + auto src_proc = mc_model_checker->get_remote_simulation().resolve_actor(mc::remote(synchro->src_actor_.get()))->get_pid(); + return src_proc; +} + +unsigned long mc_api::get_pattern_comm_dst_proc(void* addr) const +{ + Remote temp_synchro; + mc_model_checker->get_remote_simulation().read(temp_synchro, remote((simgrid::kernel::activity::CommImpl*)addr)); + const kernel::activity::CommImpl* synchro = temp_synchro.get_buffer(); + auto src_proc = mc_model_checker->get_remote_simulation().resolve_actor(mc::remote(synchro->dst_actor_.get()))->get_pid(); + return src_proc; +} + +std::vector mc_api::get_pattern_comm_data(void* addr) const +{ + Remote temp_synchro; + mc_model_checker->get_remote_simulation().read(temp_synchro, remote((simgrid::kernel::activity::CommImpl*)addr)); + const kernel::activity::CommImpl* synchro = temp_synchro.get_buffer(); + + std::vector buffer {}; + if (synchro->src_buff_ != nullptr) { + buffer.resize(synchro->src_buff_size_); + mc_model_checker->get_remote_simulation().read_bytes(buffer.data(), buffer.size(), + remote(synchro->src_buff_)); + } + return buffer; +} + +std::vector mc_api::get_pattern_comm_data(const kernel::activity::CommImpl* comm_addr) const +{ + simgrid::mc::Remote temp_comm; + mc_model_checker->get_remote_simulation().read(temp_comm, remote((kernel::activity::CommImpl*)comm_addr)); + const simgrid::kernel::activity::CommImpl* comm = temp_comm.get_buffer(); + + std::vector buffer {}; + if (comm->src_buff_ != nullptr) { + buffer.resize(comm->src_buff_size_); + mc_model_checker->get_remote_simulation().read_bytes(buffer.data(), buffer.size(), + remote(comm->src_buff_)); + } + return buffer; +} + +const char* mc_api::get_actor_host_name(smx_actor_t actor) const +{ + const char* host_name = MC_smx_actor_get_host_name(actor); + return host_name; +} + +#if HAVE_SMPI +bool mc_api::check_send_request_detached(smx_simcall_t const& simcall) const { - MC_state_copy_incomplete_communications_pattern((simgrid::mc::State*)state); + simgrid::smpi::Request mpi_request; + mc_model_checker->get_remote_simulation().read( + &mpi_request, remote(static_cast(simcall_comm_isend__get__data(simcall)))); + return mpi_request.detached(); +} +#endif + +smx_actor_t mc_api::get_src_actor(const kernel::activity::CommImpl* comm_addr) const +{ + simgrid::mc::Remote temp_comm; + mc_model_checker->get_remote_simulation().read(temp_comm, remote((kernel::activity::CommImpl*)comm_addr)); + const simgrid::kernel::activity::CommImpl* comm = temp_comm.get_buffer(); + + auto src_proc = mc_model_checker->get_remote_simulation().resolve_actor(simgrid::mc::remote(comm->src_actor_.get())); + return src_proc; } -void mc_api::copy_index_comm_pattern(const simgrid::mc::State* state) const +smx_actor_t mc_api::get_dst_actor(const kernel::activity::CommImpl* comm_addr) const { - MC_state_copy_index_communications_pattern((simgrid::mc::State*)state); + simgrid::mc::Remote temp_comm; + mc_model_checker->get_remote_simulation().read(temp_comm, remote((kernel::activity::CommImpl*)comm_addr)); + const simgrid::kernel::activity::CommImpl* comm = temp_comm.get_buffer(); + + auto dst_proc = mc_model_checker->get_remote_simulation().resolve_actor(simgrid::mc::remote(comm->dst_actor_.get())); + return dst_proc; } std::size_t mc_api::get_remote_heap_bytes() const { RemoteSimulation& process = mc_model_checker->get_remote_simulation(); - auto heap_bytes_used = mmalloc_get_bytes_used_remote(process.get_heap()->heaplimit, process.get_malloc_info()); + auto heap_bytes_used = mmalloc_get_bytes_used_remote(process.get_heap()->heaplimit, process.get_malloc_info()); return heap_bytes_used; } -void mc_api::s_initialize() const +void mc_api::session_initialize() const { session->initialize(); } @@ -254,7 +400,7 @@ void mc_api::mc_show_deadlock() const MC_show_deadlock(); } -smx_actor_t mc_api::mc_smx_simcall_get_issuer(s_smx_simcall const* req) const +smx_actor_t mc_api::simcall_get_issuer(s_smx_simcall const* req) const { return MC_smx_simcall_get_issuer(req); } @@ -270,6 +416,13 @@ Checker* mc_api::mc_get_checker() const return mc_model_checker->getChecker(); } +void mc_api::set_checker(Checker* const checker) const +{ + xbt_assert(mc_model_checker); + xbt_assert(mc_model_checker->getChecker() == nullptr); + mc_model_checker->setChecker(checker); +} + RemoteSimulation& mc_api::mc_get_remote_simulation() const { return mc_model_checker->get_remote_simulation(); @@ -295,7 +448,7 @@ std::string const& mc_api::mc_get_host_name(std::string const& hostname) const return mc_model_checker->get_host_name(hostname); } -void mc_api::mc_dump_record_path() const +void mc_api::dump_record_path() const { simgrid::mc::dumpRecordPath(); } @@ -321,19 +474,347 @@ bool mc_api::request_depend(smx_simcall_t req1, smx_simcall_t req2) const std::string mc_api::request_to_string(smx_simcall_t req, int value, RequestType request_type) const { - return simgrid::mc::request_to_string(req, value, request_type).c_str(); + xbt_assert(mc_model_checker != nullptr, "Must be called from MCer"); + + if (req->inspector_ != nullptr) + return req->inspector_->to_string(); + + bool use_remote_comm = true; + switch(request_type) { + case simgrid::mc::RequestType::simix: + use_remote_comm = true; + break; + case simgrid::mc::RequestType::executed: + case simgrid::mc::RequestType::internal: + use_remote_comm = false; + break; + default: + THROW_IMPOSSIBLE; + } + + const char* type = nullptr; + char *args = nullptr; + + smx_actor_t issuer = MC_smx_simcall_get_issuer(req); + + switch (req->call_) { + case Simcall::COMM_ISEND: { + type = "iSend"; + char* p = pointer_to_string(simcall_comm_isend__get__src_buff(req)); + char* bs = buff_size_to_string(simcall_comm_isend__get__src_buff_size(req)); + if (issuer->get_host()) + args = bprintf("src=(%ld)%s (%s), buff=%s, size=%s", issuer->get_pid(), MC_smx_actor_get_host_name(issuer), + MC_smx_actor_get_name(issuer), p, bs); + else + args = bprintf("src=(%ld)%s, buff=%s, size=%s", issuer->get_pid(), MC_smx_actor_get_name(issuer), p, bs); + xbt_free(bs); + xbt_free(p); + break; + } + + case Simcall::COMM_IRECV: { + size_t* remote_size = simcall_comm_irecv__get__dst_buff_size(req); + size_t size = 0; + if (remote_size) + mc_model_checker->get_remote_simulation().read_bytes(&size, sizeof(size), remote(remote_size)); + + type = "iRecv"; + char* p = pointer_to_string(simcall_comm_irecv__get__dst_buff(req)); + char* bs = buff_size_to_string(size); + if (issuer->get_host()) + args = bprintf("dst=(%ld)%s (%s), buff=%s, size=%s", issuer->get_pid(), MC_smx_actor_get_host_name(issuer), + MC_smx_actor_get_name(issuer), p, bs); + else + args = bprintf("dst=(%ld)%s, buff=%s, size=%s", issuer->get_pid(), MC_smx_actor_get_name(issuer), p, bs); + xbt_free(bs); + xbt_free(p); + break; + } + + case Simcall::COMM_WAIT: { + simgrid::kernel::activity::CommImpl* remote_act = simcall_comm_wait__getraw__comm(req); + char* p; + if (value == -1) { + type = "WaitTimeout"; + p = pointer_to_string(remote_act); + args = bprintf("comm=%s", p); + } else { + type = "Wait"; + p = pointer_to_string(remote_act); + + simgrid::mc::Remote temp_synchro; + const simgrid::kernel::activity::CommImpl* act; + if (use_remote_comm) { + mc_model_checker->get_remote_simulation().read(temp_synchro, remote(remote_act)); + act = temp_synchro.get_buffer(); + } else + act = remote_act; + + smx_actor_t src_proc = + mc_model_checker->get_remote_simulation().resolve_actor(simgrid::mc::remote(act->src_actor_.get())); + smx_actor_t dst_proc = + mc_model_checker->get_remote_simulation().resolve_actor(simgrid::mc::remote(act->dst_actor_.get())); + args = bprintf("comm=%s [(%ld)%s (%s)-> (%ld)%s (%s)]", p, src_proc ? src_proc->get_pid() : 0, + src_proc ? MC_smx_actor_get_host_name(src_proc) : "", + src_proc ? MC_smx_actor_get_name(src_proc) : "", dst_proc ? dst_proc->get_pid() : 0, + dst_proc ? MC_smx_actor_get_host_name(dst_proc) : "", + dst_proc ? MC_smx_actor_get_name(dst_proc) : ""); + } + xbt_free(p); + break; + } + + case Simcall::COMM_TEST: { + simgrid::kernel::activity::CommImpl* remote_act = simcall_comm_test__getraw__comm(req); + simgrid::mc::Remote temp_synchro; + const simgrid::kernel::activity::CommImpl* act; + if (use_remote_comm) { + mc_model_checker->get_remote_simulation().read(temp_synchro, remote(remote_act)); + act = temp_synchro.get_buffer(); + } else + act = remote_act; + + char* p; + if (act->src_actor_.get() == nullptr || act->dst_actor_.get() == nullptr) { + type = "Test FALSE"; + p = pointer_to_string(remote_act); + args = bprintf("comm=%s", p); + } else { + type = "Test TRUE"; + p = pointer_to_string(remote_act); + + smx_actor_t src_proc = + mc_model_checker->get_remote_simulation().resolve_actor(simgrid::mc::remote(act->src_actor_.get())); + smx_actor_t dst_proc = + mc_model_checker->get_remote_simulation().resolve_actor(simgrid::mc::remote(act->dst_actor_.get())); + args = bprintf("comm=%s [(%ld)%s (%s) -> (%ld)%s (%s)]", p, src_proc->get_pid(), + MC_smx_actor_get_name(src_proc), MC_smx_actor_get_host_name(src_proc), dst_proc->get_pid(), + MC_smx_actor_get_name(dst_proc), MC_smx_actor_get_host_name(dst_proc)); + } + xbt_free(p); + break; + } + + case Simcall::COMM_WAITANY: { + type = "WaitAny"; + size_t count = simcall_comm_waitany__get__count(req); + if (count > 0) { + simgrid::kernel::activity::CommImpl* remote_sync; + remote_sync = + mc_model_checker->get_remote_simulation().read(remote(simcall_comm_waitany__get__comms(req) + value)); + char* p = pointer_to_string(remote_sync); + args = bprintf("comm=%s (%d of %zu)", p, value + 1, count); + xbt_free(p); + } else + args = bprintf("comm at idx %d", value); + break; + } + + case Simcall::COMM_TESTANY: + if (value == -1) { + type = "TestAny FALSE"; + args = xbt_strdup("-"); + } else { + type = "TestAny"; + args = bprintf("(%d of %zu)", value + 1, simcall_comm_testany__get__count(req)); + } + break; + + case Simcall::MUTEX_TRYLOCK: + case Simcall::MUTEX_LOCK: { + if (req->call_ == Simcall::MUTEX_LOCK) + type = "Mutex LOCK"; + else + type = "Mutex TRYLOCK"; + + simgrid::mc::Remote mutex; + mc_model_checker->get_remote_simulation().read_bytes(mutex.get_buffer(), sizeof(mutex), + remote(req->call_ == Simcall::MUTEX_LOCK + ? simcall_mutex_lock__get__mutex(req) + : simcall_mutex_trylock__get__mutex(req))); + args = bprintf("locked = %d, owner = %d, sleeping = n/a", mutex.get_buffer()->is_locked(), + mutex.get_buffer()->get_owner() != nullptr + ? (int)mc_model_checker->get_remote_simulation() + .resolve_actor(simgrid::mc::remote(mutex.get_buffer()->get_owner())) + ->get_pid() + : -1); + break; + } + + case Simcall::MC_RANDOM: + type = "MC_RANDOM"; + args = bprintf("%d", value); + break; + + default: + type = SIMIX_simcall_name(req->call_); + args = bprintf("??"); + break; + } + + std::string str; + if (args != nullptr) + str = simgrid::xbt::string_printf("[(%ld)%s (%s)] %s(%s)", issuer->get_pid(), MC_smx_actor_get_host_name(issuer), + MC_smx_actor_get_name(issuer), type, args); + else + str = simgrid::xbt::string_printf("[(%ld)%s (%s)] %s ", issuer->get_pid(), MC_smx_actor_get_host_name(issuer), + MC_smx_actor_get_name(issuer), type); + xbt_free(args); + return str; } std::string mc_api::request_get_dot_output(smx_simcall_t req, int value) const { - return simgrid::mc::request_get_dot_output(req, value); + const smx_actor_t issuer = MC_smx_simcall_get_issuer(req); + const char* color = get_color(issuer->get_pid() - 1); + + if (req->inspector_ != nullptr) + return simgrid::xbt::string_printf("label = \"%s\", color = %s, fontcolor = %s", + req->inspector_->dot_label().c_str(), color, color); + + std::string label; + + switch (req->call_) { + case Simcall::COMM_ISEND: + if (issuer->get_host()) + label = xbt::string_printf("[(%ld)%s] iSend", issuer->get_pid(), MC_smx_actor_get_host_name(issuer)); + else + label = bprintf("[(%ld)] iSend", issuer->get_pid()); + break; + + case Simcall::COMM_IRECV: + if (issuer->get_host()) + label = xbt::string_printf("[(%ld)%s] iRecv", issuer->get_pid(), MC_smx_actor_get_host_name(issuer)); + else + label = xbt::string_printf("[(%ld)] iRecv", issuer->get_pid()); + break; + + case Simcall::COMM_WAIT: + if (value == -1) { + if (issuer->get_host()) + label = xbt::string_printf("[(%ld)%s] WaitTimeout", issuer->get_pid(), MC_smx_actor_get_host_name(issuer)); + else + label = xbt::string_printf("[(%ld)] WaitTimeout", issuer->get_pid()); + } else { + kernel::activity::ActivityImpl* remote_act = simcall_comm_wait__getraw__comm(req); + Remote temp_comm; + mc_model_checker->get_remote_simulation().read(temp_comm, + remote(static_cast(remote_act))); + const kernel::activity::CommImpl* comm = temp_comm.get_buffer(); + + const kernel::actor::ActorImpl* src_proc = + mc_model_checker->get_remote_simulation().resolve_actor(mc::remote(comm->src_actor_.get())); + const kernel::actor::ActorImpl* dst_proc = + mc_model_checker->get_remote_simulation().resolve_actor(mc::remote(comm->dst_actor_.get())); + if (issuer->get_host()) + label = + xbt::string_printf("[(%ld)%s] Wait [(%ld)->(%ld)]", issuer->get_pid(), MC_smx_actor_get_host_name(issuer), + src_proc ? src_proc->get_pid() : 0, dst_proc ? dst_proc->get_pid() : 0); + else + label = xbt::string_printf("[(%ld)] Wait [(%ld)->(%ld)]", issuer->get_pid(), + src_proc ? src_proc->get_pid() : 0, dst_proc ? dst_proc->get_pid() : 0); + } + break; + + case Simcall::COMM_TEST: { + kernel::activity::ActivityImpl* remote_act = simcall_comm_test__getraw__comm(req); + Remote temp_comm; + mc_model_checker->get_remote_simulation().read(temp_comm, + remote(static_cast(remote_act))); + const kernel::activity::CommImpl* comm = temp_comm.get_buffer(); + if (comm->src_actor_.get() == nullptr || comm->dst_actor_.get() == nullptr) { + if (issuer->get_host()) + label = xbt::string_printf("[(%ld)%s] Test FALSE", issuer->get_pid(), MC_smx_actor_get_host_name(issuer)); + else + label = bprintf("[(%ld)] Test FALSE", issuer->get_pid()); + } else { + if (issuer->get_host()) + label = xbt::string_printf("[(%ld)%s] Test TRUE", issuer->get_pid(), MC_smx_actor_get_host_name(issuer)); + else + label = xbt::string_printf("[(%ld)] Test TRUE", issuer->get_pid()); + } + break; + } + + case Simcall::COMM_WAITANY: { + size_t comms_size = simcall_comm_waitany__get__count(req); + if (issuer->get_host()) + label = xbt::string_printf("[(%ld)%s] WaitAny [%d of %zu]", issuer->get_pid(), + MC_smx_actor_get_host_name(issuer), value + 1, comms_size); + else + label = xbt::string_printf("[(%ld)] WaitAny [%d of %zu]", issuer->get_pid(), value + 1, comms_size); + break; + } + + case Simcall::COMM_TESTANY: + if (value == -1) { + if (issuer->get_host()) + label = xbt::string_printf("[(%ld)%s] TestAny FALSE", issuer->get_pid(), MC_smx_actor_get_host_name(issuer)); + else + label = xbt::string_printf("[(%ld)] TestAny FALSE", issuer->get_pid()); + } else { + if (issuer->get_host()) + label = + xbt::string_printf("[(%ld)%s] TestAny TRUE [%d of %lu]", issuer->get_pid(), + MC_smx_actor_get_host_name(issuer), value + 1, simcall_comm_testany__get__count(req)); + else + label = xbt::string_printf("[(%ld)] TestAny TRUE [%d of %lu]", issuer->get_pid(), value + 1, + simcall_comm_testany__get__count(req)); + } + break; + + case Simcall::MUTEX_TRYLOCK: + label = xbt::string_printf("[(%ld)] Mutex TRYLOCK", issuer->get_pid()); + break; + + case Simcall::MUTEX_LOCK: + label = xbt::string_printf("[(%ld)] Mutex LOCK", issuer->get_pid()); + break; + + case Simcall::MC_RANDOM: + if (issuer->get_host()) + label = xbt::string_printf("[(%ld)%s] MC_RANDOM (%d)", issuer->get_pid(), MC_smx_actor_get_host_name(issuer), + value); + else + label = xbt::string_printf("[(%ld)] MC_RANDOM (%d)", issuer->get_pid(), value); + break; + + default: + THROW_UNIMPLEMENTED; + } + + return xbt::string_printf("label = \"%s\", color = %s, fontcolor = %s", label.c_str(), color, color); } -const char* mc_api::simix_simcall_name(e_smx_simcall_t kind) const +const char* mc_api::simcall_get_name(simgrid::simix::Simcall kind) const { return SIMIX_simcall_name(kind); } +#if HAVE_SMPI +int mc_api::get_smpi_request_tag(smx_simcall_t const& simcall, simgrid::simix::Simcall type) const +{ + simgrid::smpi::Request mpi_request; + void* simcall_data = nullptr; + if (type == Simcall::COMM_ISEND) + simcall_data = simcall_comm_isend__get__data(simcall); + else if (type == Simcall::COMM_IRECV) + simcall_data = simcall_comm_irecv__get__data(simcall); + mc_model_checker->get_remote_simulation().read(&mpi_request, remote(static_cast(simcall_data))); + return mpi_request.tag(); +} +#endif + +void mc_api::restore_state(std::shared_ptr system_state) const +{ + system_state->restore(&mc_model_checker->get_remote_simulation()); +} + +void mc_api::log_state() const +{ + session->log_state(); +} + bool mc_api::snapshot_equal(const Snapshot* s1, const Snapshot* s2) const { return simgrid::mc::snapshot_equal(s1, s2); @@ -350,19 +831,72 @@ void mc_api::s_close() const session->close(); } -void mc_api::s_restore_initial_state() const +void mc_api::restore_initial_state() const { session->restore_initial_state(); } -void mc_api::execute(Transition const& transition) +void mc_api::execute(Transition const& transition) const { session->execute(transition); } -void mc_api::s_log_state() const +#if SIMGRID_HAVE_MC +void mc_api::automaton_load(const char *file) const +{ + MC_automaton_load(file); +} +#endif + +std::vector mc_api::automaton_propositional_symbol_evaluate() const { - session->log_state(); + unsigned int cursor = 0; + std::vector values; + xbt_automaton_propositional_symbol_t ps = nullptr; + xbt_dynar_foreach (mc::property_automaton->propositional_symbols, cursor, ps) + values.push_back(xbt_automaton_propositional_symbol_evaluate(ps)); + return values; +} + +std::vector mc_api::get_automaton_state() const +{ + std::vector automaton_stack; + unsigned int cursor = 0; + xbt_automaton_state_t automaton_state; + xbt_dynar_foreach (mc::property_automaton->states, cursor, automaton_state) + if (automaton_state->type == -1) + automaton_stack.push_back(automaton_state); + return automaton_stack; +} + +int mc_api::compare_automaton_exp_label(const xbt_automaton_exp_label* l) const +{ + unsigned int cursor = 0; + xbt_automaton_propositional_symbol_t p = nullptr; + xbt_dynar_foreach (simgrid::mc::property_automaton->propositional_symbols, cursor, p) { + if (std::strcmp(xbt_automaton_propositional_symbol_get_name(p), l->u.predicat) == 0) + return cursor; + } + return -1; +} + +void mc_api::set_property_automaton(xbt_automaton_state_t const& automaton_state) const +{ + mc::property_automaton->current_state = automaton_state; +} + +xbt_automaton_exp_label_t mc_api::get_automaton_transition_label(xbt_dynar_t const& dynar, int index) const +{ + const xbt_automaton_transition* transition = + xbt_dynar_get_as(dynar, index, xbt_automaton_transition_t); + return transition->label; +} + +xbt_automaton_state_t mc_api::get_automaton_transition_dst(xbt_dynar_t const& dynar, int index) const +{ + const xbt_automaton_transition* transition = + xbt_dynar_get_as(dynar, index, xbt_automaton_transition_t); + return transition->dst; } } // namespace mc