X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/2cf13759ba1696d88f5ff86afee5324f30ccdbfc..4bcfd40036f842e976d329cd0cee7349b8e0f4d6:/src/mc/mc_request.cpp diff --git a/src/mc/mc_request.cpp b/src/mc/mc_request.cpp index 27a7ec8158..735a629441 100644 --- a/src/mc/mc_request.cpp +++ b/src/mc/mc_request.cpp @@ -9,7 +9,6 @@ #include "src/kernel/activity/MutexImpl.hpp" #include "src/mc/ModelChecker.hpp" #include "src/mc/mc_smx.hpp" -#include "src/mc/mc_xbt.hpp" using simgrid::mc::remote; @@ -75,11 +74,11 @@ bool request_depend_asymmetric(smx_simcall_t r1, smx_simcall_t r2) simcall_comm_wait__get__timeout(r2) <= 0) return false; - if ((r1->call == SIMCALL_COMM_ISEND) && (synchro2->type == kernel::activity::CommImpl::Type::SEND) && + 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) && + 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; } @@ -115,43 +114,39 @@ bool request_depend_asymmetric(smx_simcall_t r1, smx_simcall_t r2) } // Those are internal_req -bool request_depend(smx_simcall_t r1, smx_simcall_t r2) +bool request_depend(smx_simcall_t req1, smx_simcall_t req2) { - if (r1->issuer == r2->issuer) + 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 ((r1->call == SIMCALL_COMM_WAIT && simcall_comm_wait__get__timeout(r1) > 0) - || (r2->call == SIMCALL_COMM_WAIT - && simcall_comm_wait__get__timeout(r2) > 0)) + 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 (r1->call != r2->call) - return request_depend_asymmetric(r1, r2) - && request_depend_asymmetric(r2, r1); + 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: - simgrid::kernel::activity::CommImpl* synchro1 = MC_get_comm(r1); - simgrid::kernel::activity::CommImpl* synchro2 = MC_get_comm(r2); - - switch(r1->call) { - case SIMCALL_COMM_ISEND: - return simcall_comm_isend__get__mbox(r1) - == simcall_comm_isend__get__mbox(r2); - case SIMCALL_COMM_IRECV: - return simcall_comm_irecv__get__mbox(r1) - == simcall_comm_irecv__get__mbox(r2); - 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; + simgrid::kernel::activity::CommImpl* synchro1 = MC_get_comm(req1); + simgrid::kernel::activity::CommImpl* synchro2 = MC_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; } } @@ -301,17 +296,12 @@ std::string simgrid::mc::request_to_string(smx_simcall_t req, int value, simgrid case SIMCALL_COMM_WAITANY: { type = "WaitAny"; - s_xbt_dynar_t comms; - mc_model_checker->process().read_bytes( - &comms, sizeof(comms), remote(simcall_comm_waitany__get__comms(req))); - if (not xbt_dynar_is_empty(&comms)) { - smx_activity_t remote_sync; - read_element(mc_model_checker->process(), - &remote_sync, remote(simcall_comm_waitany__get__comms(req)), value, - sizeof(remote_sync)); - char* p = pointer_to_string(remote_sync.get()); - args = bprintf("comm=%s (%d of %lu)", - p, value + 1, xbt_dynar_length(&comms)); + size_t count = simcall_comm_waitany__get__count(req); + if (count > 0) { + simgrid::kernel::activity::CommImpl* remote_sync; + remote_sync = mc_model_checker->process().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); @@ -345,9 +335,9 @@ std::string simgrid::mc::request_to_string(smx_simcall_t req, int value, simgrid : simcall_mutex_trylock__get__mutex(req) )); args = bprintf( - "locked = %d, owner = %d, sleeping = n/a", mutex.getBuffer()->locked, - mutex.getBuffer()->owner != nullptr - ? (int)mc_model_checker->process().resolveActor(simgrid::mc::remote(mutex.getBuffer()->owner))->get_pid() + "locked = %d, owner = %d, sleeping = n/a", mutex.getBuffer()->is_locked(), + mutex.getBuffer()->owner_ != nullptr + ? (int)mc_model_checker->process().resolveActor(simgrid::mc::remote(mutex.getBuffer()->owner_))->get_pid() : -1); break; } @@ -379,7 +369,7 @@ namespace mc { bool request_is_enabled_by_idx(smx_simcall_t req, unsigned int idx) { - simgrid::kernel::activity::ActivityImpl* remote_act = nullptr; + simgrid::kernel::activity::CommImpl* remote_act = nullptr; switch (req->call) { case SIMCALL_COMM_WAIT: @@ -388,12 +378,11 @@ bool request_is_enabled_by_idx(smx_simcall_t req, unsigned int idx) break; case SIMCALL_COMM_WAITANY: - read_element(mc_model_checker->process(), &remote_act, remote(simcall_comm_waitany__getraw__comms(req)), idx, - sizeof(remote_act)); + remote_act = mc_model_checker->process().read(remote(simcall_comm_testany__get__comms(req) + idx)); break; case SIMCALL_COMM_TESTANY: - remote_act = mc_model_checker->process().read(remote(simcall_comm_testany__getraw__comms(req) + idx)); + remote_act = mc_model_checker->process().read(remote(simcall_comm_testany__get__comms(req) + idx)); break; default: @@ -401,7 +390,7 @@ bool request_is_enabled_by_idx(smx_simcall_t req, unsigned int idx) } simgrid::mc::Remote temp_comm; - mc_model_checker->process().read(temp_comm, remote(static_cast(remote_act))); + mc_model_checker->process().read(temp_comm, remote(remote_act)); simgrid::kernel::activity::CommImpl* comm = temp_comm.getBuffer(); return comm->src_actor_.get() && comm->dst_actor_.get(); } @@ -497,13 +486,12 @@ std::string request_get_dot_output(smx_simcall_t req, int value) } case SIMCALL_COMM_WAITANY: { - unsigned long comms_size = read_length( - mc_model_checker->process(), remote(simcall_comm_waitany__get__comms(req))); + size_t comms_size = simcall_comm_waitany__get__count(req); if (issuer->get_host()) - label = simgrid::xbt::string_printf("[(%ld)%s] WaitAny [%d of %lu]", issuer->get_pid(), + label = simgrid::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 = simgrid::xbt::string_printf("[(%ld)] WaitAny [%d of %lu]", issuer->get_pid(), value + 1, comms_size); + label = simgrid::xbt::string_printf("[(%ld)] WaitAny [%d of %zu]", issuer->get_pid(), value + 1, comms_size); break; }