From 6ec8e9d992b54560a1873c1d19f397b5b5d6a219 Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Mon, 1 Apr 2013 18:31:24 +0200 Subject: [PATCH 1/1] model-checker : restore independence between iSend/iRecv and Wait requests --- src/mc/mc_request.c | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/mc/mc_request.c b/src/mc/mc_request.c index c25a0bc400..c57dc08b0c 100644 --- a/src/mc/mc_request.c +++ b/src/mc/mc_request.c @@ -24,7 +24,7 @@ int MC_request_depend(smx_simcall_t r1, smx_simcall_t r2) { if(r1->call == SIMCALL_COMM_IRECV && r2->call == SIMCALL_COMM_ISEND) return FALSE; - /*if( (r1->call == SIMCALL_COMM_ISEND || r1->call == SIMCALL_COMM_IRECV) + if( (r1->call == SIMCALL_COMM_ISEND || r1->call == SIMCALL_COMM_IRECV) && r2->call == SIMCALL_COMM_WAIT){ if(simcall_comm_wait__get__comm(r2)->comm.rdv == NULL) @@ -58,7 +58,7 @@ int MC_request_depend(smx_simcall_t r1, smx_simcall_t r2) { if(simcall_comm_wait__get__comm(r1)->comm.type == SIMIX_COMM_RECEIVE && r2->call == SIMCALL_COMM_IRECV) return FALSE; - }*/ + } /* FIXME: the following rule assumes that the result of the * isend/irecv call is not stored in a buffer used in the -- 2.20.1