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

diff --git a/src/mc/mc_request.c b/src/mc/mc_request.c
index ac8840e..92827f9 100644 (file)
--- 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 9a5db9f..bb47a1c 100644 (file)
--- 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 784c742..8d65b75 100644 (file)
--- 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 e396a2d..5a1d603 100644 (file)
--- 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 f80b6ce..efaa26e 100644 (file)
--- 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: