From e42c0a20b488f6fa0f3bb084bb4429bf9572bea6 Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Wed, 3 Apr 2013 11:34:47 +0200 Subject: [PATCH 1/1] model-checker : iSend/iRecv independent with Wait but not with WaitTimeout --- src/mc/mc_request.c | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/mc/mc_request.c b/src/mc/mc_request.c index c57dc08b0c..f92580b157 100644 --- a/src/mc/mc_request.c +++ b/src/mc/mc_request.c @@ -32,13 +32,13 @@ int MC_request_depend(smx_simcall_t r1, smx_simcall_t r2) { smx_rdv_t rdv = r1->call == SIMCALL_COMM_ISEND ? simcall_comm_isend__get__rdv(r1) : simcall_comm_irecv__get__rdv(r1); - if(simcall_comm_wait__get__comm(r2)->comm.rdv != rdv) + if((simcall_comm_wait__get__comm(r2)->comm.rdv != rdv) && (simcall_comm_wait__get__timeout(r2) <= 0)) return FALSE; - if(simcall_comm_wait__get__comm(r2)->comm.type == SIMIX_COMM_SEND && r1->call == SIMCALL_COMM_ISEND) + if((simcall_comm_wait__get__comm(r2)->comm.type == SIMIX_COMM_SEND) && (r1->call == SIMCALL_COMM_ISEND) && (simcall_comm_wait__get__timeout(r2) <= 0)) return FALSE; - if(simcall_comm_wait__get__comm(r2)->comm.type == SIMIX_COMM_RECEIVE && r1->call == SIMCALL_COMM_IRECV) + if((simcall_comm_wait__get__comm(r2)->comm.type == SIMIX_COMM_RECEIVE) && (r1->call == SIMCALL_COMM_IRECV) && (simcall_comm_wait__get__timeout(r2) <= 0)) return FALSE; } @@ -50,13 +50,13 @@ int MC_request_depend(smx_simcall_t r1, smx_simcall_t r2) { smx_rdv_t rdv = r2->call == SIMCALL_COMM_ISEND ? simcall_comm_isend__get__rdv(r2) : simcall_comm_irecv__get__rdv(r2); - if(simcall_comm_wait__get__comm(r1)->comm.rdv != rdv) + if((simcall_comm_wait__get__comm(r1)->comm.rdv != rdv) && (simcall_comm_wait__get__timeout(r1) <= 0)) return FALSE; - if(simcall_comm_wait__get__comm(r1)->comm.type == SIMIX_COMM_SEND && r2->call == SIMCALL_COMM_ISEND) + if((simcall_comm_wait__get__comm(r1)->comm.type == SIMIX_COMM_SEND) && (r2->call == SIMCALL_COMM_ISEND) && (simcall_comm_wait__get__timeout(r1) <= 0)) return FALSE; - if(simcall_comm_wait__get__comm(r1)->comm.type == SIMIX_COMM_RECEIVE && r2->call == SIMCALL_COMM_IRECV) + if((simcall_comm_wait__get__comm(r1)->comm.type == SIMIX_COMM_RECEIVE) && (r2->call == SIMCALL_COMM_IRECV) && (simcall_comm_wait__get__timeout(r1) <= 0)) return FALSE; } -- 2.20.1