X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/7792ce44dc2744211836680af4775a35a823b242..e01a8f10de51f1d10f5ee7529c201d132e630904:/src/mc/mc_api.cpp diff --git a/src/mc/mc_api.cpp b/src/mc/mc_api.cpp index cbf5bbc173..33cc69249d 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/checker/SimcallInspector.hpp" #include "src/mc/mc_comm_pattern.hpp" +#include "src/mc/mc_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 #include +// #include #if HAVE_SMPI #include "src/smpi/include/smpi_request.hpp" @@ -23,6 +24,117 @@ 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)"); +} + +inline +smx_mailbox_t get_mbox(smx_simcall_t const r) +{ + switch (r->call_) { + case Simcall::COMM_ISEND: + return simcall_comm_isend__get__mbox(r); + case Simcall::COMM_IRECV: + return simcall_comm_irecv__get__mbox(r); + default: + return nullptr; + } +} + +inline simgrid::kernel::activity::CommImpl* get_comm(smx_simcall_t const r) +{ + switch (r->call_) { + case Simcall::COMM_WAIT: + return simcall_comm_wait__getraw__comm(r); + case Simcall::COMM_TEST: + return simcall_comm_test__getraw__comm(r); + default: + return nullptr; + } +} + +// Does half the job +inline bool request_depend_asymmetric(smx_simcall_t r1, smx_simcall_t r2) +{ + if (r1->call_ == Simcall::COMM_ISEND && r2->call_ == Simcall::COMM_IRECV) + return false; + + if (r1->call_ == Simcall::COMM_IRECV && r2->call_ == Simcall::COMM_ISEND) + return false; + + // Those are internal requests, we do not need indirection because those objects are copies: + const kernel::activity::CommImpl* synchro1 = get_comm(r1); + const kernel::activity::CommImpl* synchro2 = get_comm(r2); + + if ((r1->call_ == Simcall::COMM_ISEND || r1->call_ == Simcall::COMM_IRECV) && r2->call_ == Simcall::COMM_WAIT) { + const kernel::activity::MailboxImpl* mbox = get_mbox(r1); + + if (mbox != synchro2->mbox_cpy + && simcall_comm_wait__get__timeout(r2) <= 0) + return false; + + if ((r1->issuer_ != synchro2->src_actor_.get()) && (r1->issuer_ != synchro2->dst_actor_.get()) && + simcall_comm_wait__get__timeout(r2) <= 0) + return false; + + if ((r1->call_ == Simcall::COMM_ISEND) && (synchro2->type_ == kernel::activity::CommImpl::Type::SEND) && + (synchro2->src_buff_ != simcall_comm_isend__get__src_buff(r1)) && simcall_comm_wait__get__timeout(r2) <= 0) + return false; + + if ((r1->call_ == Simcall::COMM_IRECV) && (synchro2->type_ == kernel::activity::CommImpl::Type::RECEIVE) && + (synchro2->dst_buff_ != simcall_comm_irecv__get__dst_buff(r1)) && simcall_comm_wait__get__timeout(r2) <= 0) + return false; + } + + /* FIXME: the following rule assumes that the result of the isend/irecv call is not stored in a buffer used in the + * test call. */ +#if 0 + if((r1->call == Simcall::COMM_ISEND || r1->call == Simcall::COMM_IRECV) + && r2->call == Simcall::COMM_TEST) + return false; +#endif + + if (r1->call_ == Simcall::COMM_WAIT && (r2->call_ == Simcall::COMM_WAIT || r2->call_ == Simcall::COMM_TEST) && + (synchro1->src_actor_.get() == nullptr || synchro1->dst_actor_.get() == nullptr)) + return false; + + if (r1->call_ == Simcall::COMM_TEST && + (simcall_comm_test__get__comm(r1) == nullptr || synchro1->src_buff_ == nullptr || synchro1->dst_buff_ == nullptr)) + return false; + + if (r1->call_ == Simcall::COMM_TEST && r2->call_ == Simcall::COMM_WAIT && + synchro1->src_buff_ == synchro2->src_buff_ && synchro1->dst_buff_ == synchro2->dst_buff_) + return false; + + if (r1->call_ == Simcall::COMM_WAIT && r2->call_ == Simcall::COMM_TEST && synchro1->src_buff_ != nullptr && + synchro1->dst_buff_ != nullptr && synchro2->src_buff_ != nullptr && synchro2->dst_buff_ != nullptr && + synchro1->dst_buff_ != synchro2->src_buff_ && synchro1->dst_buff_ != synchro2->dst_buff_ && + synchro2->dst_buff_ != synchro1->src_buff_) + return false; + + return true; +} + /* Search an enabled transition for the given process. * * This can be seen as an iterator returning the next transition of the process. @@ -41,7 +153,7 @@ 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 @@ -177,7 +289,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; @@ -210,7 +322,8 @@ 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 +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); } @@ -228,7 +341,8 @@ kernel::activity::CommImpl* mc_api::get_comm_wait_raw_addr(smx_simcall_t 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)); + auto addr = + mc_model_checker->get_remote_simulation().read(remote(simcall_comm_waitany__getraw__comms(request) + value)); return static_cast(addr); } @@ -240,7 +354,7 @@ std::string mc_api::get_pattern_comm_rdv(void* addr) const 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)); + auto rdv = mc_model_checker->get_remote_simulation().read_string(RemotePtr(remote_name)); return rdv; } @@ -249,7 +363,8 @@ 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(); + auto src_proc = + mc_model_checker->get_remote_simulation().resolve_actor(mc::remote(synchro->src_actor_.get()))->get_pid(); return src_proc; } @@ -258,7 +373,8 @@ 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(); + auto src_proc = + mc_model_checker->get_remote_simulation().resolve_actor(mc::remote(synchro->dst_actor_.get()))->get_pid(); return src_proc; } @@ -268,11 +384,10 @@ std::vector mc_api::get_pattern_comm_data(void* addr) const 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 {}; + 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_)); + mc_model_checker->get_remote_simulation().read_bytes(buffer.data(), buffer.size(), remote(synchro->src_buff_)); } return buffer; } @@ -282,12 +397,11 @@ std::vector mc_api::get_pattern_comm_data(const kernel::activity::CommImpl 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 {}; + + 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_)); + mc_model_checker->get_remote_simulation().read_bytes(buffer.data(), buffer.size(), remote(comm->src_buff_)); } return buffer; } @@ -340,11 +454,6 @@ void mc_api::session_initialize() const session->initialize(); } -ModelChecker* mc_api::get_model_checker() const -{ - return mc_model_checker; -} - void mc_api::mc_inc_visited_states() const { mc_model_checker->visited_states++; @@ -380,6 +489,21 @@ smx_actor_t mc_api::simcall_get_issuer(s_smx_simcall const* req) const return MC_smx_simcall_get_issuer(req); } +long mc_api::simcall_get_actor_id(s_smx_simcall const* req) const +{ + return MC_smx_simcall_get_issuer(req)->get_pid(); +} + +smx_mailbox_t mc_api::simcall_get_mbox(smx_simcall_t const req) const +{ + return get_mbox(req); +} + +simgrid::kernel::activity::CommImpl* mc_api::simcall_get_comm(smx_simcall_t const req) const +{ + return get_comm(req); +} + bool mc_api::mc_is_null() const { auto is_null = (mc_model_checker == nullptr) ? true : false; @@ -391,6 +515,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(); @@ -435,19 +566,353 @@ smx_simcall_t mc_api::mc_state_choose_request(simgrid::mc::State* state) const return nullptr; } -bool mc_api::request_depend(smx_simcall_t req1, smx_simcall_t req2) const +bool mc_api::simcall_check_dependency(smx_simcall_t const req1, smx_simcall_t const req2) const { - return simgrid::mc::request_depend(req1, req2); + if (req1->issuer_ == req2->issuer_) + return false; + + /* Wait with timeout transitions are not considered by the independence theorem, thus we consider them as dependent with all other transitions */ + if ((req1->call_ == Simcall::COMM_WAIT && simcall_comm_wait__get__timeout(req1) > 0) || + (req2->call_ == Simcall::COMM_WAIT && simcall_comm_wait__get__timeout(req2) > 0)) + return true; + + if (req1->call_ != req2->call_) + return request_depend_asymmetric(req1, req2) && request_depend_asymmetric(req2, req1); + + // Those are internal requests, we do not need indirection because those objects are copies: + const kernel::activity::CommImpl* synchro1 = get_comm(req1); + const kernel::activity::CommImpl* synchro2 = get_comm(req2); + + switch (req1->call_) { + case Simcall::COMM_ISEND: + return simcall_comm_isend__get__mbox(req1) == simcall_comm_isend__get__mbox(req2); + case Simcall::COMM_IRECV: + return simcall_comm_irecv__get__mbox(req1) == simcall_comm_irecv__get__mbox(req2); + case Simcall::COMM_WAIT: + if (synchro1->src_buff_ == synchro2->src_buff_ && synchro1->dst_buff_ == synchro2->dst_buff_) + return false; + if (synchro1->src_buff_ != nullptr && synchro1->dst_buff_ != nullptr && synchro2->src_buff_ != nullptr && + synchro2->dst_buff_ != nullptr && synchro1->dst_buff_ != synchro2->src_buff_ && + synchro1->dst_buff_ != synchro2->dst_buff_ && synchro2->dst_buff_ != synchro1->src_buff_) + return false; + return true; + default: + return true; + } } 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 @@ -474,6 +939,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); @@ -501,15 +971,59 @@ void mc_api::execute(Transition const& transition) const } #if SIMGRID_HAVE_MC -void mc_api::automaton_load(const char *file) const -{ - MC_automaton_load(file); +void mc_api::automaton_load(const char* file) const +{ + MC_automaton_load(file); } #endif -void mc_api::log_state() const +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