Translate the executed TestAny and WaitAny requests into Test and Wait ones.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/simgrid/simgrid/trunk@9457 48e7efb5-ca39-0410-a469-dd3cf9ba447f

diff --git a/src/mc/mc_dpor.c b/src/mc/mc_dpor.c
index bed97ec..920ee40 100644 (file)
--- a/src/mc/mc_dpor.c
+++ b/src/mc/mc_dpor.c
@@ -52,7 +52,7 @@ void MC_dpor_init()
 void MC_dpor(void)
 {
   char *req_str;
-  unsigned int value;
+  int value;
   smx_req_t req = NULL;
   mc_state_t state = NULL, prev_state = NULL, next_state = NULL;
   smx_process_t process = NULL;
@@ -98,7 +98,6 @@ void MC_dpor(void)
       next_state = MC_state_new();
       xbt_fifo_unshift(mc_stack, next_state);
 
-
       /* Get an enabled process and insert it in the interleave set of the next state */
       xbt_swag_foreach(process, simix_global->process_list){
         if(SIMIX_process_is_enabled(process)){
@@ -138,15 +137,15 @@ void MC_dpor(void)
          executed before it. If it does then add it to the interleave set of the
          state that executed that previous request. */
       while ((state = xbt_fifo_shift(mc_stack)) != NULL) {
-        req = MC_state_get_executed_request(state, &value);
+        req = MC_state_get_internal_request(state);
         xbt_fifo_foreach(mc_stack, item, prev_state, mc_state_t) {
-          if(MC_request_depend(req, MC_state_get_executed_request(prev_state, &value))){
+          if(MC_request_depend(req, MC_state_get_internal_request(prev_state))){
             if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
               DEBUG0("Dependent Transitions:");
               req_str = MC_request_to_string(MC_state_get_executed_request(prev_state, &value));
               DEBUG2("%s (state=%p)", req_str, prev_state);
               xbt_free(req_str);
-              req_str = MC_request_to_string(req);
+              req_str = MC_request_to_string(MC_state_get_executed_request(state, &value));
               DEBUG2("%s (state=%p)", req_str, state);
               xbt_free(req_str);              
             }

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index 4e24e3c..7c77d37 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -113,7 +113,7 @@ int MC_deadlock_check()
 */
 void MC_replay(xbt_fifo_t stack)
 {
-  unsigned int value;
+  int value;
   char *req_str;
   smx_req_t req = NULL, saved_req = NULL;
   xbt_fifo_item_t item;
@@ -177,7 +177,7 @@ void MC_dump_stack(xbt_fifo_t stack)
 
 void MC_show_stack(xbt_fifo_t stack)
 {
-  unsigned int value;
+  int value;
   mc_state_t state;
   xbt_fifo_item_t item;
   smx_req_t req;

diff --git a/src/mc/mc_request.c b/src/mc/mc_request.c
index fcc1d9c..97617a8 100644 (file)
--- a/src/mc/mc_request.c
+++ b/src/mc/mc_request.c
@@ -27,6 +27,26 @@ int MC_request_depend(smx_req_t r1, smx_req_t r2)
       && r2->comm_wait.comm->comm.dst_buff != r1->comm_wait.comm->comm.src_buff)
     return FALSE;
 
+  if(r1->call == REQ_COMM_TEST &&
+      (r1->comm_test.comm == NULL
+       || r1->comm_test.comm->comm.src_buff == NULL
+       || r1->comm_test.comm->comm.dst_buff == NULL))
+    return FALSE;
+
+  if(r2->call == REQ_COMM_TEST &&
+      (r2->comm_test.comm == NULL
+       || r2->comm_test.comm->comm.src_buff == NULL
+       || r2->comm_test.comm->comm.dst_buff == NULL))
+    return FALSE;
+
+  if (r1->call == REQ_COMM_TEST && r2->call == REQ_COMM_WAIT
+      && r1->comm_test.comm == r2->comm_wait.comm)
+    return FALSE;
+
+  if (r1->call == REQ_COMM_WAIT && r2->call == REQ_COMM_TEST
+      && r1->comm_wait.comm == r2->comm_test.comm)
+    return FALSE;
+
   return TRUE;
 }
 

diff --git a/src/mc/mc_state.c b/src/mc/mc_state.c
index e289fd1..6163c7c 100644 (file)
--- a/src/mc/mc_state.c
+++ b/src/mc/mc_state.c
@@ -49,19 +49,54 @@ int MC_state_process_is_done(mc_state_t state, smx_process_t process){
   return state->proc_status[process->pid].state == MC_DONE ? TRUE : FALSE;
 }
 
-void MC_state_set_executed_request(mc_state_t state, smx_req_t req, unsigned int value)
+void MC_state_set_executed_request(mc_state_t state, smx_req_t req, int value)
 {
-  state->executed_value = value;
-  state->executed = *req;
+  /* The waitany and testany request are transformed into a wait or test request over the
+   * corresponding communication action so it can be treated later by the dependence
+   * function. */
+  switch(req->call){
+    case REQ_COMM_WAITANY:
+      state->internal_req.call = REQ_COMM_WAIT;
+      state->internal_req.issuer = req->issuer;
+      state->internal_req.comm_wait.comm =
+        xbt_dynar_get_as(req->comm_waitany.comms, value, smx_action_t);
+      state->internal_req.comm_wait.timeout = 0;
+      break;
+
+    case REQ_COMM_TESTANY:
+      state->internal_req.call = REQ_COMM_TEST;
+      state->internal_req.issuer = req->issuer;
+
+      if(value > 0)
+        state->internal_req.comm_test.comm =
+          xbt_dynar_get_as(req->comm_testany.comms, value, smx_action_t);
+      else
+        state->internal_req.comm_test.comm = NULL;
+
+      state->internal_req.comm_test.result = value;
+      break;
+
+    default:
+      state->internal_req = *req;
+      break;
+  }
+
+  state->executed_req = *req;
+  state->req_num = value;
+}
+
+smx_req_t MC_state_get_executed_request(mc_state_t state, int *value)
+{
+  *value = state->req_num;
+  return &state->executed_req;
 }
 
-smx_req_t MC_state_get_executed_request(mc_state_t state, unsigned int *value)
+smx_req_t MC_state_get_internal_request(mc_state_t state)
 {
-  *value = state->executed_value;
-  return &state->executed;
+  return &state->internal_req;
 }
 
-smx_req_t MC_state_get_request(mc_state_t state, unsigned int *value)
+smx_req_t MC_state_get_request(mc_state_t state, int *value)
 {
   smx_process_t process = NULL;
   mc_procstate_t procstate = NULL;
@@ -86,7 +121,7 @@ smx_req_t MC_state_get_request(mc_state_t state, unsigned int *value)
           case REQ_COMM_TESTANY:
             if(MC_request_testany_fail(&process->request)){
               procstate->state = MC_DONE;
-              *value = (unsigned int)-1;
+              *value = -1;
               return &process->request;
             }
 

diff --git a/src/mc/private.h b/src/mc/private.h
index 7c13977..6dbfe04 100644 (file)
--- a/src/mc/private.h
+++ b/src/mc/private.h
@@ -79,8 +79,10 @@ typedef struct mc_procstate{
 typedef struct mc_state {
   unsigned long max_pid;            /* Maximum pid at state's creation time */
   mc_procstate_t proc_status;       /* State's exploration status by process */
-  s_smx_req_t executed;             /* The executed request of the state */
-  unsigned int executed_value;      /* The value associated to the request */
+  s_smx_req_t internal_req;         /* Internal translation of request */
+  s_smx_req_t executed_req;         /* The executed request of the state */
+  int req_num;                      /* The request number (in the case of a
+                                       multi-request like waitany ) */
 } s_mc_state_t, *mc_state_t;
 
 extern xbt_fifo_t mc_stack;
@@ -90,9 +92,10 @@ void MC_state_delete(mc_state_t state);
 void MC_state_interleave_process(mc_state_t state, smx_process_t process);
 unsigned int MC_state_interleave_size(mc_state_t state);
 int MC_state_process_is_done(mc_state_t state, smx_process_t process);
-void MC_state_set_executed_request(mc_state_t state, smx_req_t req, unsigned int value);
-smx_req_t MC_state_get_executed_request(mc_state_t state, unsigned int *value);
-smx_req_t MC_state_get_request(mc_state_t state, unsigned int *value);
+void MC_state_set_executed_request(mc_state_t state, smx_req_t req, int value);
+smx_req_t MC_state_get_executed_request(mc_state_t state, int *value);
+smx_req_t MC_state_get_internal_request(mc_state_t state);
+smx_req_t MC_state_get_request(mc_state_t state, int *value);
 
 /****************************** Statistics ************************************/
 typedef struct mc_stats {

diff --git a/src/simix/network_private.h b/src/simix/network_private.h
index 292e656..784c742 100644 (file)
--- a/src/simix/network_private.h
+++ b/src/simix/network_private.h
@@ -39,10 +39,10 @@ smx_action_t SIMIX_comm_irecv(smx_process_t dst_proc, smx_rdv_t rdv,
 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_waitany(smx_req_t req, unsigned 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);
-void SIMIX_pre_comm_testany(smx_req_t req, unsigned int idx);
+void SIMIX_pre_comm_testany(smx_req_t req, int idx);
 void SIMIX_comm_cancel(smx_action_t action);
 double SIMIX_comm_get_remains(smx_action_t action);
 e_smx_state_t SIMIX_comm_get_state(smx_action_t action);

diff --git a/src/simix/smurf_private.h b/src/simix/smurf_private.h
index f9659fc..7667dc7 100644 (file)
--- a/src/simix/smurf_private.h
+++ b/src/simix/smurf_private.h
@@ -474,7 +474,7 @@ void SIMIX_request_destroy(void);
 void SIMIX_request_push(void);
 smx_req_t SIMIX_request_pop(void);
 void SIMIX_request_answer(smx_req_t);
-void SIMIX_request_pre(smx_req_t, unsigned int);
+void SIMIX_request_pre(smx_req_t, int);
 void SIMIX_request_post(smx_action_t);
 int SIMIX_request_is_visible(smx_req_t req);
 int SIMIX_request_is_enabled(smx_req_t req);

diff --git a/src/simix/smx_network.c b/src/simix/smx_network.c
index 8280532..e396a2d 100644 (file)
--- a/src/simix/smx_network.c
+++ b/src/simix/smx_network.c
@@ -372,7 +372,7 @@ void SIMIX_pre_comm_test(smx_req_t req)
   }
 }
 
-void SIMIX_pre_comm_testany(smx_req_t req, unsigned int idx)
+void SIMIX_pre_comm_testany(smx_req_t req, int idx)
 {
   unsigned int cursor;
   smx_action_t action;
@@ -380,7 +380,7 @@ void SIMIX_pre_comm_testany(smx_req_t req, unsigned int idx)
   req->comm_testany.result = -1;
 
   if (MC_IS_ENABLED){
-    if((int)idx == -1){
+    if(idx == -1){
       SIMIX_request_answer(req);
     }else{
       action = xbt_dynar_get_as(actions, idx, smx_action_t);
@@ -402,7 +402,7 @@ void SIMIX_pre_comm_testany(smx_req_t req, unsigned int idx)
   SIMIX_request_answer(req);
 }
 
-void SIMIX_pre_comm_waitany(smx_req_t req, unsigned int idx)
+void SIMIX_pre_comm_waitany(smx_req_t req, int idx)
 {
   smx_action_t action;
   unsigned int cursor = 0;

diff --git a/src/simix/smx_smurf.c b/src/simix/smx_smurf.c
index a80a17f..c873e2c 100644 (file)
--- a/src/simix/smx_smurf.c
+++ b/src/simix/smx_smurf.c
@@ -136,7 +136,7 @@ int SIMIX_request_is_enabled_by_idx(smx_req_t req, unsigned int idx)
   }
 }
 
-void SIMIX_request_pre(smx_req_t req, unsigned int value)
+void SIMIX_request_pre(smx_req_t req, int value)
 {
   switch (req->call) {
   case REQ_NO_REQ: