X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/e00dc5d578e936984b3f4be8e9b56956acd5387d..e01a8f10de51f1d10f5ee7529c201d132e630904:/src/mc/mc_api.cpp diff --git a/src/mc/mc_api.cpp b/src/mc/mc_api.cpp index 61f8dd0f00..33cc69249d 100644 --- a/src/mc/mc_api.cpp +++ b/src/mc/mc_api.cpp @@ -3,12 +3,12 @@ #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_smx.hpp" #include "src/mc/remote/RemoteSimulation.hpp" -#include "src/mc/mc_pattern.hpp" -#include "src/mc/checker/SimcallInspector.hpp" #include #include // #include @@ -32,7 +32,7 @@ static inline const char* get_color(int id) return colors[id % colors.size()]; } -static char *pointer_to_string(void *pointer) +static char* pointer_to_string(void* pointer) { if (XBT_LOG_ISENABLED(mc_api, xbt_log_priority_verbose)) return bprintf("%p", pointer); @@ -40,7 +40,7 @@ static char *pointer_to_string(void *pointer) return xbt_strdup("(verbose only)"); } -static char *buff_size_to_string(size_t buff_size) +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); @@ -48,6 +48,93 @@ static char *buff_size_to_string(size_t 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. @@ -66,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 @@ -202,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; @@ -235,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); } @@ -253,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); } @@ -265,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; } @@ -274,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; } @@ -283,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; } @@ -293,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; } @@ -307,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; } @@ -365,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++; @@ -405,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; @@ -467,9 +566,39 @@ 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 @@ -480,20 +609,20 @@ std::string mc_api::request_to_string(smx_simcall_t req, int value, RequestType 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; + 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; + char* args = nullptr; smx_actor_t issuer = MC_smx_simcall_get_issuer(req); @@ -554,7 +683,7 @@ std::string mc_api::request_to_string(smx_simcall_t req, int value, RequestType 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, + 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) : "", @@ -587,7 +716,7 @@ std::string mc_api::request_to_string(smx_simcall_t req, int value, RequestType 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(), + 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)); } @@ -602,8 +731,8 @@ std::string mc_api::request_to_string(smx_simcall_t req, int value, RequestType 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); + 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); @@ -660,7 +789,7 @@ std::string mc_api::request_to_string(smx_simcall_t req, int value, RequestType 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; + return str; } std::string mc_api::request_get_dot_output(smx_simcall_t req, int value) const @@ -783,7 +912,7 @@ std::string mc_api::request_get_dot_output(smx_simcall_t req, int value) const THROW_UNIMPLEMENTED; } - return xbt::string_printf("label = \"%s\", color = %s, fontcolor = %s", label.c_str(), color, color); + 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 @@ -842,16 +971,16 @@ 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 -std::vector mc_api::automaton_propositional_symbol_evaluate() const +std::vector mc_api::automaton_propositional_symbol_evaluate() const { unsigned int cursor = 0; - std::vector values; + 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)); @@ -871,7 +1000,7 @@ std::vector mc_api::get_automaton_state() const int mc_api::compare_automaton_exp_label(const xbt_automaton_exp_label* l) const { - unsigned int cursor = 0; + 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) @@ -887,15 +1016,13 @@ void mc_api::set_property_automaton(xbt_automaton_state_t const& 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); + 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); + const xbt_automaton_transition* transition = xbt_dynar_get_as(dynar, index, xbt_automaton_transition_t); return transition->dst; }