}
static inline
-smx_mailbox_t MC_get_rdv(smx_simcall_t r)
+smx_mailbox_t MC_get_mbox(smx_simcall_t r)
{
switch(r->call) {
case SIMCALL_COMM_ISEND:
- return simcall_comm_isend__get__rdv(r);
+ return simcall_comm_isend__get__mbox(r);
case SIMCALL_COMM_IRECV:
- return simcall_comm_irecv__get__rdv(r);
+ return simcall_comm_irecv__get__mbox(r);
default:
return nullptr;
}
if ((r1->call == SIMCALL_COMM_ISEND || r1->call == SIMCALL_COMM_IRECV)
&& r2->call == SIMCALL_COMM_WAIT) {
- smx_mailbox_t rdv = MC_get_rdv(r1);
+ smx_mailbox_t mbox = MC_get_mbox(r1);
- if (rdv != synchro2->comm.rdv_cpy
+ if (mbox != synchro2->comm.mbox_cpy
&& 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( (r1->call == SIMCALL_COMM_ISEND || r1->call == SIMCALL_COMM_IRECV)
+#if 0
+ if((r1->call == SIMCALL_COMM_ISEND || r1->call == SIMCALL_COMM_IRECV)
&& r2->call == SIMCALL_COMM_TEST)
- return FALSE; */
+ return FALSE;
+#endif
if (r1->call == SIMCALL_COMM_WAIT
&& (r2->call == SIMCALL_COMM_WAIT || r2->call == SIMCALL_COMM_TEST)
switch(r1->call) {
case SIMCALL_COMM_ISEND:
- return simcall_comm_isend__get__rdv(r1) == simcall_comm_isend__get__rdv(r2);
+ return simcall_comm_isend__get__mbox(r1) == simcall_comm_isend__get__mbox(r2);
case SIMCALL_COMM_IRECV:
- return simcall_comm_irecv__get__rdv(r1) == simcall_comm_irecv__get__rdv(r2);
+ return simcall_comm_irecv__get__mbox(r1) == simcall_comm_irecv__get__mbox(r2);
case SIMCALL_COMM_WAIT:
if (synchro1->comm.src_buff == synchro2->comm.src_buff
&& synchro1->comm.dst_buff == synchro2->comm.dst_buff)
std::string simgrid::mc::request_to_string(smx_simcall_t req, int value, simgrid::mc::RequestType request_type)
{
+ xbt_assert(mc_mode == MC_MODE_SERVER);
+
bool use_remote_comm = true;
switch(request_type) {
case simgrid::mc::RequestType::simix:
} else
act = remote_act;
- smx_process_t src_proc = MC_smx_resolve_process(act->comm.src_proc);
- smx_process_t dst_proc = MC_smx_resolve_process(act->comm.dst_proc);
+ smx_process_t src_proc = mc_model_checker->process().resolveProcess(
+ simgrid::mc::remote(act->comm.src_proc));
+ smx_process_t dst_proc = mc_model_checker->process().resolveProcess(
+ simgrid::mc::remote(act->comm.dst_proc));
args = bprintf("comm=%s [(%lu)%s (%s)-> (%lu)%s (%s)]", p,
src_proc ? src_proc->pid : 0,
src_proc ? MC_smx_process_get_host_name(src_proc) : "",
type = "Test TRUE";
p = pointer_to_string(remote_act);
- smx_process_t src_proc = MC_smx_resolve_process(act->comm.src_proc);
- smx_process_t dst_proc = MC_smx_resolve_process(act->comm.dst_proc);
+ smx_process_t src_proc = mc_model_checker->process().resolveProcess(
+ simgrid::mc::remote(act->comm.src_proc));
+ smx_process_t dst_proc = mc_model_checker->process().resolveProcess(
+ simgrid::mc::remote(act->comm.dst_proc));
args = bprintf("comm=%s [(%lu)%s (%s) -> (%lu)%s (%s)]", p,
src_proc->pid,
MC_smx_process_get_name(src_proc),
args = bprintf("locked = %d, owner = %d, sleeping = %d",
mutex.locked,
- mutex.owner != nullptr ? (int) MC_smx_resolve_process(mutex.owner)->pid : -1,
+ mutex.owner != nullptr ? (int) mc_model_checker->process().resolveProcess(
+ simgrid::mc::remote(mutex.owner))->pid : -1,
mutex_sleeping.count);
break;
}
mc_model_checker->process().read_bytes(&synchro,
sizeof(synchro), remote(remote_act));
- smx_process_t src_proc = MC_smx_resolve_process(synchro.comm.src_proc);
- smx_process_t dst_proc = MC_smx_resolve_process(synchro.comm.dst_proc);
+ smx_process_t src_proc = mc_model_checker->process().resolveProcess(
+ simgrid::mc::remote(synchro.comm.src_proc));
+ smx_process_t dst_proc = mc_model_checker->process().resolveProcess(
+ simgrid::mc::remote(synchro.comm.dst_proc));
if (issuer->host)
label = simgrid::xbt::string_printf("[(%lu)%s] Wait [(%lu)->(%lu)]",
issuer->pid,