X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/56ef99a0f0332f8ee7a287df00ed74059a864b00..39c935d6d5ee86d153f6f7e6a10d723ae7c57f6f:/src/mc/mc_api.cpp diff --git a/src/mc/mc_api.cpp b/src/mc/mc_api.cpp index 34dd01c58c..bcb4f6663d 100644 --- a/src/mc/mc_api.cpp +++ b/src/mc/mc_api.cpp @@ -1,16 +1,17 @@ #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" @@ -23,6 +24,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. @@ -177,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; @@ -298,6 +323,7 @@ const char* mc_api::get_actor_host_name(smx_actor_t actor) const return host_name; } +#if HAVE_SMPI bool mc_api::check_send_request_detached(smx_simcall_t const& simcall) const { simgrid::smpi::Request mpi_request; @@ -305,6 +331,7 @@ 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(const kernel::activity::CommImpl* comm_addr) const { @@ -333,7 +360,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(); } @@ -389,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(); @@ -440,12 +474,316 @@ 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::simcall_get_name(simgrid::simix::Simcall kind) const @@ -472,6 +810,11 @@ void mc_api::restore_state(std::shared_ptr system_state) 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); @@ -493,14 +836,67 @@ 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::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