X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/001737a15701027974d89260771284a45013d2cd..d2cc5a5e537a7b2915f781dd75ad8f4d02f6fcf7:/src/mc/mc_request.cpp diff --git a/src/mc/mc_request.cpp b/src/mc/mc_request.cpp index c1bd140ee9..900a115e2f 100644 --- a/src/mc/mc_request.cpp +++ b/src/mc/mc_request.cpp @@ -74,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; } @@ -114,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; } } @@ -180,6 +176,9 @@ std::string simgrid::mc::request_to_string(smx_simcall_t req, int value, simgrid { xbt_assert(mc_model_checker != nullptr, "Must be called from MCer"); + if (req->transition != nullptr) + return req->transition->to_string(); + bool use_remote_comm = true; switch(request_type) { case simgrid::mc::RequestType::simix: @@ -251,12 +250,12 @@ std::string simgrid::mc::request_to_string(smx_simcall_t req, int value, simgrid if (use_remote_comm) { mc_model_checker->process().read(temp_synchro, remote(static_cast(remote_act))); - act = temp_synchro.getBuffer(); + act = temp_synchro.get_buffer(); } else act = remote_act; - smx_actor_t src_proc = mc_model_checker->process().resolveActor(simgrid::mc::remote(act->src_actor_.get())); - smx_actor_t dst_proc = mc_model_checker->process().resolveActor(simgrid::mc::remote(act->dst_actor_.get())); + smx_actor_t src_proc = mc_model_checker->process().resolve_actor(simgrid::mc::remote(act->src_actor_.get())); + smx_actor_t dst_proc = mc_model_checker->process().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) : "", @@ -275,7 +274,7 @@ std::string simgrid::mc::request_to_string(smx_simcall_t req, int value, simgrid if (use_remote_comm) { mc_model_checker->process().read(temp_synchro, remote(static_cast(remote_act))); - act = temp_synchro.getBuffer(); + act = temp_synchro.get_buffer(); } else act = remote_act; @@ -288,8 +287,8 @@ std::string simgrid::mc::request_to_string(smx_simcall_t req, int value, simgrid type = "Test TRUE"; p = pointer_to_string(remote_act); - smx_actor_t src_proc = mc_model_checker->process().resolveActor(simgrid::mc::remote(act->src_actor_.get())); - smx_actor_t dst_proc = mc_model_checker->process().resolveActor(simgrid::mc::remote(act->dst_actor_.get())); + smx_actor_t src_proc = mc_model_checker->process().resolve_actor(simgrid::mc::remote(act->src_actor_.get())); + smx_actor_t dst_proc = mc_model_checker->process().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)); @@ -332,16 +331,14 @@ std::string simgrid::mc::request_to_string(smx_simcall_t req, int value, simgrid type = "Mutex TRYLOCK"; simgrid::mc::Remote mutex; - mc_model_checker->process().read_bytes(mutex.getBuffer(), sizeof(mutex), - remote( - req->call == SIMCALL_MUTEX_LOCK - ? simcall_mutex_lock__get__mutex(req) - : simcall_mutex_trylock__get__mutex(req) - )); + mc_model_checker->process().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.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.get_buffer()->is_locked(), + mutex.get_buffer()->owner_ != nullptr + ? (int)mc_model_checker->process().resolve_actor(simgrid::mc::remote(mutex.get_buffer()->owner_))->get_pid() : -1); break; } @@ -395,7 +392,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(remote_act)); - simgrid::kernel::activity::CommImpl* comm = temp_comm.getBuffer(); + simgrid::kernel::activity::CommImpl* comm = temp_comm.get_buffer(); return comm->src_actor_.get() && comm->dst_actor_.get(); } @@ -423,9 +420,15 @@ static inline const char* get_color(int id) std::string request_get_dot_output(smx_simcall_t req, int value) { + const smx_actor_t issuer = MC_smx_simcall_get_issuer(req); + const char* color = get_color(issuer->get_pid() - 1); + + if (req->transition != nullptr) + return simgrid::xbt::string_printf("label = \"%s\", color = %s, fontcolor = %s", + req->transition->dot_label().c_str(), color, color); + std::string label; - const smx_actor_t issuer = MC_smx_simcall_get_issuer(req); switch (req->call) { case SIMCALL_COMM_ISEND: @@ -454,10 +457,10 @@ std::string request_get_dot_output(smx_simcall_t req, int value) simgrid::mc::Remote temp_comm; mc_model_checker->process().read(temp_comm, remote(static_cast(remote_act))); - simgrid::kernel::activity::CommImpl* comm = temp_comm.getBuffer(); + simgrid::kernel::activity::CommImpl* comm = temp_comm.get_buffer(); - smx_actor_t src_proc = mc_model_checker->process().resolveActor(simgrid::mc::remote(comm->src_actor_.get())); - smx_actor_t dst_proc = mc_model_checker->process().resolveActor(simgrid::mc::remote(comm->dst_actor_.get())); + smx_actor_t src_proc = mc_model_checker->process().resolve_actor(simgrid::mc::remote(comm->src_actor_.get())); + smx_actor_t dst_proc = mc_model_checker->process().resolve_actor(simgrid::mc::remote(comm->dst_actor_.get())); if (issuer->get_host()) label = simgrid::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, @@ -472,7 +475,7 @@ std::string request_get_dot_output(smx_simcall_t req, int value) simgrid::kernel::activity::ActivityImpl* remote_act = simcall_comm_test__getraw__comm(req); simgrid::mc::Remote temp_comm; mc_model_checker->process().read(temp_comm, remote(static_cast(remote_act))); - simgrid::kernel::activity::CommImpl* comm = temp_comm.getBuffer(); + simgrid::kernel::activity::CommImpl* comm = temp_comm.get_buffer(); if (comm->src_actor_.get() == nullptr || comm->dst_actor_.get() == nullptr) { if (issuer->get_host()) label = @@ -537,7 +540,6 @@ std::string request_get_dot_output(smx_simcall_t req, int value) THROW_UNIMPLEMENTED; } - const char* color = get_color(issuer->get_pid() - 1); return simgrid::xbt::string_printf( "label = \"%s\", color = %s, fontcolor = %s", label.c_str(), color, color);