X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/e3f2b0103f46b876785e374a2781ff7d48f8ec59..b4aa5009927bf7616908aeb10381027302b1ca3d:/src/mc/mc_api.cpp diff --git a/src/mc/mc_api.cpp b/src/mc/mc_api.cpp index 8e305f460a..4b27ad2f31 100644 --- a/src/mc/mc_api.cpp +++ b/src/mc/mc_api.cpp @@ -1,6 +1,7 @@ #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" @@ -8,9 +9,10 @@ #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" @@ -23,6 +25,30 @@ 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. @@ -205,22 +231,33 @@ 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 { - MC_state_copy_incomplete_communications_pattern((simgrid::mc::State*)state); + return mc_model_checker->get_remote_simulation().actors().size(); } -void mc_api::copy_index_comm_pattern(const simgrid::mc::State* state) const +bool mc_api::comm_addr_equal(const kernel::activity::CommImpl* comm_addr1, const kernel::activity::CommImpl* comm_addr2) const { - MC_state_copy_index_communications_pattern((simgrid::mc::State*)state); + return remote(comm_addr1) == remote(comm_addr2); } -kernel::activity::CommImpl* mc_api::get_pattern_comm_addr(smx_simcall_t request) const +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; @@ -266,12 +303,28 @@ std::vector mc_api::get_pattern_comm_data(void* addr) const 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 { simgrid::smpi::Request mpi_request; @@ -279,21 +332,22 @@ bool mc_api::check_send_request_detached(smx_simcall_t const& simcall) const &mpi_request, remote(static_cast(simcall_comm_isend__get__data(simcall)))); return mpi_request.detached(); } +#endif -smx_actor_t mc_api::get_src_actor(mc::RemotePtr const& comm_addr) const +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, comm_addr); + 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; } -smx_actor_t mc_api::get_dst_actor(mc::RemotePtr const& comm_addr) const +smx_actor_t mc_api::get_dst_actor(const kernel::activity::CommImpl* comm_addr) const { simgrid::mc::Remote temp_comm; - mc_model_checker->get_remote_simulation().read(temp_comm, comm_addr); + 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())); @@ -307,7 +361,7 @@ std::size_t mc_api::get_remote_heap_bytes() const return heap_bytes_used; } -void mc_api::s_initialize() const +void mc_api::session_initialize() const { session->initialize(); } @@ -347,7 +401,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); } @@ -388,7 +442,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(); } @@ -414,15 +468,319 @@ 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(simgrid::simix::Simcall kind) const +const char* mc_api::simcall_get_name(simgrid::simix::Simcall kind) const { return SIMIX_simcall_name(kind); } @@ -441,6 +799,16 @@ int mc_api::get_smpi_request_tag(smx_simcall_t const& simcall, simgrid::simix::S } #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); @@ -457,19 +825,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_lable(const xbt_automaton_exp_label* l, std::vector const& values) 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