model-checker : fix (again ..) DPOR for iSend/iRecv and Wait communications

- add rdv_cpy in s_smx_action_t structure. comm.rdv is used for
  garbage collection and set to NULL when the communication matches
  with another communication already pushed and waiting in the
  mailbox.
- iSend/iRecv and Wait communications are independant if the
  communications are not in the same mailbox. Otherwise, the
  iSend/iRecv communication process issuer must be different of the
  src_proc or dst_proc of the Wait communication, or, src_buff and
  dst_buff of the communications must be different.

diff --git a/src/mc/mc_request.c b/src/mc/mc_request.c
index 3e03859..9ce5f61 100644 (file)
--- a/src/mc/mc_request.c
+++ b/src/mc/mc_request.c
@@ -24,39 +24,43 @@ 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)
-        &&  r2->call == SIMCALL_COMM_WAIT){
-
-    if(simcall_comm_wait__get__comm(r2)->comm.rdv == NULL)
-      return FALSE;
+  if((r1->call == SIMCALL_COMM_ISEND || r1->call == SIMCALL_COMM_IRECV)
+     &&  r2->call == SIMCALL_COMM_WAIT){
 
     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) && (simcall_comm_wait__get__timeout(r2) <= 0))
+    if(rdv != simcall_comm_wait__get__comm(r2)->comm.rdv_cpy && simcall_comm_wait__get__timeout(r2) <= 0)
+      return FALSE;
+
+    if((r1->issuer != simcall_comm_wait__get__comm(r2)->comm.src_proc) && (r1->issuer != simcall_comm_wait__get__comm(r2)->comm.dst_proc))
       return FALSE;
 
-    if((simcall_comm_wait__get__comm(r2)->comm.type == SIMIX_COMM_SEND) && (r1->call == SIMCALL_COMM_ISEND) && (simcall_comm_wait__get__timeout(r2) <= 0))
+    if((r1->call == SIMCALL_COMM_ISEND) && (simcall_comm_wait__get__comm(r2)->comm.type == SIMIX_COMM_SEND) 
+       && (simcall_comm_wait__get__comm(r2)->comm.src_buff != simcall_comm_isend__get__src_buff(r1)))
       return FALSE;
 
-    if((simcall_comm_wait__get__comm(r2)->comm.type == SIMIX_COMM_RECEIVE) && (r1->call == SIMCALL_COMM_IRECV) && (simcall_comm_wait__get__timeout(r2) <= 0))
+    if((r1->call == SIMCALL_COMM_IRECV) && (simcall_comm_wait__get__comm(r2)->comm.type == SIMIX_COMM_RECEIVE) 
+       && (simcall_comm_wait__get__comm(r2)->comm.dst_buff != simcall_comm_irecv__get__dst_buff(r1)))
       return FALSE;
   }
 
-  if(   (r2->call == SIMCALL_COMM_ISEND || r2->call == SIMCALL_COMM_IRECV)
+  if((r2->call == SIMCALL_COMM_ISEND || r2->call == SIMCALL_COMM_IRECV)
         &&  r1->call == SIMCALL_COMM_WAIT){
 
-    if(simcall_comm_wait__get__comm(r1)->comm.rdv != NULL)
-      return FALSE;
-
     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) && (simcall_comm_wait__get__timeout(r1) <= 0))
+    if(rdv != simcall_comm_wait__get__comm(r1)->comm.rdv_cpy && 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) && (simcall_comm_wait__get__timeout(r1) <= 0))
+    if((r2->issuer != simcall_comm_wait__get__comm(r1)->comm.src_proc) && (r2->issuer != simcall_comm_wait__get__comm(r1)->comm.dst_proc))
+        return FALSE;  
+
+    if((r2->call == SIMCALL_COMM_ISEND) && (simcall_comm_wait__get__comm(r1)->comm.type == SIMIX_COMM_SEND) 
+       && (simcall_comm_wait__get__comm(r1)->comm.src_buff != simcall_comm_isend__get__src_buff(r2)))
       return FALSE;
 
-    if((simcall_comm_wait__get__comm(r1)->comm.type == SIMIX_COMM_RECEIVE) && (r2->call == SIMCALL_COMM_IRECV) && (simcall_comm_wait__get__timeout(r1) <= 0))
+    if((r2->call == SIMCALL_COMM_IRECV) && (simcall_comm_wait__get__comm(r1)->comm.type == SIMIX_COMM_RECEIVE) 
+       && (simcall_comm_wait__get__comm(r1)->comm.dst_buff != simcall_comm_irecv__get__dst_buff(r2)))
       return FALSE;
   }
 

diff --git a/src/simix/smx_network.c b/src/simix/smx_network.c
index 3cdc13b..2c0e3a1 100644 (file)
--- a/src/simix/smx_network.c
+++ b/src/simix/smx_network.c
@@ -199,6 +199,7 @@ smx_action_t SIMIX_fifo_get_comm(xbt_fifo_t fifo, e_smx_comm_type_t type,
       xbt_fifo_remove_item(fifo, item);
       xbt_fifo_free_item(item);
       action->comm.refcount++;
+      action->comm.rdv_cpy = action->comm.rdv;
       action->comm.rdv = NULL;
       return action;
     }

diff --git a/src/simix/smx_private.h b/src/simix/smx_private.h
index c966f22..1130ff9 100644 (file)
--- a/src/simix/smx_private.h
+++ b/src/simix/smx_private.h
@@ -132,6 +132,12 @@ typedef struct s_smx_action {
     struct {
       e_smx_comm_type_t type;         /* Type of the communication (SIMIX_COMM_SEND or SIMIX_COMM_RECEIVE) */
       smx_rdv_t rdv;                  /* Rendez-vous where the comm is queued */
+
+#ifdef HAVE_MC
+      smx_rdv_t rdv_cpy;              /* Copy of the rendez-vous where the comm is queued, MC needs it for DPOR 
+                                         (comm.rdv set to NULL when the communication is removed from the mailbox 
+                                         (used as garbage collector)) */
+#endif
       int refcount;                   /* Number of processes involved in the cond */
       int detached;                   /* If detached or not */