From 717875729557ca0e76702af5be742600842664a3 Mon Sep 17 00:00:00 2001
From: cristianrosa <cristianrosa@48e7efb5-ca39-0410-a469-dd3cf9ba447f>
Date: Thu, 20 Jan 2011 15:45:57 +0000
Subject: [PATCH] Let the model-checker decide if the wait transitions should
 timeout or not.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/simgrid/simgrid/trunk@9464 48e7efb5-ca39-0410-a469-dd3cf9ba447f
---
 src/mc/mc_request.c         | 28 ++++++++++++++--------------
 src/mc/mc_state.c           | 12 ++++++++++++
 src/simix/network_private.h |  2 +-
 src/simix/smx_network.c     |  4 ++--
 src/simix/smx_smurf.c       |  2 +-
 5 files changed, 30 insertions(+), 18 deletions(-)

diff --git a/src/mc/mc_request.c b/src/mc/mc_request.c
index ac8840e521..92827f9241 100644
--- a/src/mc/mc_request.c
+++ b/src/mc/mc_request.c
@@ -13,20 +13,17 @@ int MC_request_depend(smx_req_t r1, smx_req_t r2)
 
   /* FIXME: the following rule assumes that the result of the
    * isend/irecv call is not stored in a buffer used in the
-   * wait/test call. */
+   * wait/test call.
   if(   (r1->call == REQ_COMM_ISEND || r1->call == REQ_COMM_IRECV)
      && (r2->call == REQ_COMM_WAIT || r2->call == REQ_COMM_TEST))
-    return FALSE;
+    return FALSE;*/
 
   /* FIXME: the following rule assumes that the result of the
    * isend/irecv call is not stored in a buffer used in the
-   * wait/test call. */
+   * wait/test call.
   if(   (r2->call == REQ_COMM_ISEND || r2->call == REQ_COMM_IRECV)
      && (r1->call == REQ_COMM_WAIT || r1->call == REQ_COMM_TEST))
-    return FALSE;
-
-  if(r1->call == REQ_COMM_WAIT && r2->call == REQ_COMM_IRECV)
-    return FALSE;
+    return FALSE;*/
 
   if(r1->call == REQ_COMM_ISEND && r2->call == REQ_COMM_ISEND
       && r1->comm_isend.rdv != r2->comm_isend.rdv)
@@ -166,17 +163,19 @@ int MC_request_is_enabled(smx_req_t req)
     case REQ_COMM_WAIT:
       /* FIXME: check also that src and dst processes are not suspended */
 
-      /* If there is a timeout it will be always enabled because, if the
-       * communication is not ready, it can timeout.
-       * This avoids false positives on dead-locks */
-      if(req->comm_wait.timeout >= 0)
+      /* If it has a timeout it will be always be enabled, because even if the
+       * communication is not ready, it can timeout and won't block.
+       * On the other hand if it hasn't a timeout, check if the comm is ready.*/
+      if(req->comm_wait.timeout >= 0){
         return TRUE;
-
-      act = req->comm_wait.comm;
-      return (act->comm.src_proc && act->comm.dst_proc);
+      }else{
+        act = req->comm_wait.comm;
+        return (act->comm.src_proc && act->comm.dst_proc);
+      }
       break;
 
     case REQ_COMM_WAITANY:
+      /* Check if it has at least one communication ready */
       xbt_dynar_foreach(req->comm_waitany.comms, index, act) {
         if (act->comm.src_proc && act->comm.dst_proc){
           return TRUE;
@@ -186,6 +185,7 @@ int MC_request_is_enabled(smx_req_t req)
       break;
 
     default:
+      /* The rest of the request are always enabled */
       return TRUE;
   }
 }
diff --git a/src/mc/mc_state.c b/src/mc/mc_state.c
index 9a5db9f1ee..bb47a1c452 100644
--- a/src/mc/mc_state.c
+++ b/src/mc/mc_state.c
@@ -157,6 +157,18 @@ smx_req_t MC_state_get_request(mc_state_t state, int *value)
 
             break;
 
+          case REQ_COMM_WAIT:
+            if(process->request.comm_wait.comm->comm.src_proc
+               && process->request.comm_wait.comm->comm.dst_proc){
+              *value = 0;
+            }else{
+              *value = -1;
+            }
+            procstate->state = MC_DONE;
+            return &process->request;
+
+            break;
+
           default:
             procstate->state = MC_DONE;
             *value = 0;
diff --git a/src/simix/network_private.h b/src/simix/network_private.h
index 784c7424ed..8d65b75890 100644
--- a/src/simix/network_private.h
+++ b/src/simix/network_private.h
@@ -38,7 +38,7 @@ smx_action_t SIMIX_comm_irecv(smx_process_t dst_proc, smx_rdv_t rdv,
                               int (*)(void *, void *), void *data);
 void SIMIX_comm_destroy(smx_action_t action);
 void SIMIX_comm_destroy_internal_actions(smx_action_t action);
-void SIMIX_pre_comm_wait(smx_req_t req);
+void SIMIX_pre_comm_wait(smx_req_t req, int idx);
 void SIMIX_pre_comm_waitany(smx_req_t req, int idx);
 void SIMIX_post_comm(smx_action_t action);
 void SIMIX_pre_comm_test(smx_req_t req);
diff --git a/src/simix/smx_network.c b/src/simix/smx_network.c
index e396a2df0f..5a1d6036f3 100644
--- a/src/simix/smx_network.c
+++ b/src/simix/smx_network.c
@@ -315,7 +315,7 @@ smx_action_t SIMIX_comm_irecv(smx_process_t dst_proc, smx_rdv_t rdv,
   return action;
 }
 
-void SIMIX_pre_comm_wait(smx_req_t req)
+void SIMIX_pre_comm_wait(smx_req_t req, int idx)
 {
   smx_action_t action = req->comm_wait.comm;
   double timeout = req->comm_wait.timeout;
@@ -326,7 +326,7 @@ void SIMIX_pre_comm_wait(smx_req_t req)
   req->issuer->waiting_action = action;
 
   if (MC_IS_ENABLED){
-    if(action->comm.src_proc && action->comm.dst_proc){
+    if(idx == 0){
       action->state = SIMIX_DONE;
     }else{
       /* If we reached this point, the wait request must have a timeout */
diff --git a/src/simix/smx_smurf.c b/src/simix/smx_smurf.c
index f80b6ce2d1..efaa26e1b9 100644
--- a/src/simix/smx_smurf.c
+++ b/src/simix/smx_smurf.c
@@ -324,7 +324,7 @@ void SIMIX_request_pre(smx_req_t req, int value)
       break;
 
     case REQ_COMM_WAIT:
-      SIMIX_pre_comm_wait(req);
+      SIMIX_pre_comm_wait(req, value);
       break;
 
     case REQ_COMM_TEST:
-- 
2.20.1