src/mc/mc_request.c

   1 #include "private.h"
   2
   3 int MC_request_depend(smx_req_t r1, smx_req_t r2)
   4 {
   5   if(_surf_do_model_check == 2)
   6     return TRUE;
   7
   8   if (r1->issuer == r2->issuer)
   9     return FALSE;
  10
  11   if(r1->call == REQ_COMM_ISEND && r2->call == REQ_COMM_IRECV)
  12     return FALSE;
  13
  14   if(r1->call == REQ_COMM_IRECV && r2->call == REQ_COMM_ISEND)
  15     return FALSE;
  16
  17   if(   (r1->call == REQ_COMM_ISEND || r1->call == REQ_COMM_IRECV)
  18        &&  r2->call == REQ_COMM_WAIT){
  19
  20     if(r2->comm_wait.comm->comm.rdv == NULL)
  21       return FALSE;
  22
  23     smx_rdv_t rdv = r1->call == REQ_COMM_ISEND ? r1->comm_isend.rdv : r1->comm_irecv.rdv;
  24
  25     if(r2->comm_wait.comm->comm.rdv != rdv)
  26       return FALSE;
  27
  28     if(r2->comm_wait.comm->type == SIMIX_COMM_SEND && r1->call == REQ_COMM_ISEND)
  29       return FALSE;
  30
  31     if(r2->comm_wait.comm->type == SIMIX_COMM_RECEIVE && r1->call == REQ_COMM_IRECV)
  32       return FALSE;
  33   }
  34
  35   if(   (r2->call == REQ_COMM_ISEND || r2->call == REQ_COMM_IRECV)
  36        &&  r1->call == REQ_COMM_WAIT){
  37
  38     if(r1->comm_wait.comm->comm.rdv != NULL)
  39       return FALSE;
  40
  41     smx_rdv_t rdv = r2->call == REQ_COMM_ISEND ? r2->comm_isend.rdv : r2->comm_irecv.rdv;
  42
  43     if(r1->comm_wait.comm->comm.rdv != rdv)
  44       return FALSE;
  45
  46     if(r1->comm_wait.comm->type == SIMIX_COMM_SEND && r2->call == REQ_COMM_ISEND)
  47       return FALSE;
  48
  49     if(r1->comm_wait.comm->type == SIMIX_COMM_RECEIVE && r2->call == REQ_COMM_IRECV)
  50       return FALSE;
  51   }
  52
  53   /* FIXME: the following rule assumes that the result of the
  54    * isend/irecv call is not stored in a buffer used in the
  55    * test call. */
  56   if(   (r1->call == REQ_COMM_ISEND || r1->call == REQ_COMM_IRECV)
  57      &&  r2->call == REQ_COMM_TEST)
  58     return FALSE;
  59
  60   /* FIXME: the following rule assumes that the result of the
  61    * isend/irecv call is not stored in a buffer used in the
  62    * test call.*/
  63   if(   (r2->call == REQ_COMM_ISEND || r2->call == REQ_COMM_IRECV)
  64      && r1->call == REQ_COMM_TEST)
  65     return FALSE;
  66
  67   if(r1->call == REQ_COMM_ISEND && r2->call == REQ_COMM_ISEND
  68       && r1->comm_isend.rdv != r2->comm_isend.rdv)
  69     return FALSE;
  70
  71   if(r1->call == REQ_COMM_IRECV && r2->call == REQ_COMM_IRECV
  72       && r1->comm_irecv.rdv != r2->comm_irecv.rdv)
  73     return FALSE;
  74
  75   if(r1->call == REQ_COMM_WAIT && (r2->call == REQ_COMM_WAIT || r2->call == REQ_COMM_TEST)
  76      && (r1->comm_wait.comm->comm.src_proc == NULL
  77          || r1->comm_wait.comm->comm.dst_proc == NULL))
  78     return FALSE;
  79
  80   if(r2->call == REQ_COMM_WAIT && (r1->call == REQ_COMM_WAIT || r1->call == REQ_COMM_TEST)
  81      && (r2->comm_wait.comm->comm.src_proc == NULL
  82          || r2->comm_wait.comm->comm.dst_proc == NULL))
  83     return FALSE;
  84
  85   if(r1->call == REQ_COMM_WAIT && r2->call == REQ_COMM_WAIT
  86       && r1->comm_wait.comm->comm.src_buff == r2->comm_wait.comm->comm.src_buff
  87       && r1->comm_wait.comm->comm.dst_buff == r2->comm_wait.comm->comm.dst_buff)
  88     return FALSE;
  89
  90   if (r1->call == REQ_COMM_WAIT && r2->call == REQ_COMM_WAIT
  91       && r1->comm_wait.comm->comm.src_buff != NULL
  92       && r1->comm_wait.comm->comm.dst_buff != NULL
  93       && r2->comm_wait.comm->comm.src_buff != NULL
  94       && r2->comm_wait.comm->comm.dst_buff != NULL
  95       && r1->comm_wait.comm->comm.dst_buff != r2->comm_wait.comm->comm.src_buff
  96       && r1->comm_wait.comm->comm.dst_buff != r2->comm_wait.comm->comm.dst_buff
  97       && r2->comm_wait.comm->comm.dst_buff != r1->comm_wait.comm->comm.src_buff)
  98     return FALSE;
  99
 100   if(r1->call == REQ_COMM_TEST &&
 101       (r1->comm_test.comm == NULL
 102        || r1->comm_test.comm->comm.src_buff == NULL
 103        || r1->comm_test.comm->comm.dst_buff == NULL))
 104     return FALSE;
 105
 106   if(r2->call == REQ_COMM_TEST &&
 107       (r2->comm_test.comm == NULL
 108        || r2->comm_test.comm->comm.src_buff == NULL
 109        || r2->comm_test.comm->comm.dst_buff == NULL))
 110     return FALSE;
 111
 112   if(r1->call == REQ_COMM_TEST && r2->call == REQ_COMM_WAIT
 113       && r1->comm_test.comm->comm.src_buff == r2->comm_wait.comm->comm.src_buff
 114       && r1->comm_test.comm->comm.dst_buff == r2->comm_wait.comm->comm.dst_buff)
 115     return FALSE;
 116
 117   if(r1->call == REQ_COMM_WAIT && r2->call == REQ_COMM_TEST
 118       && r1->comm_wait.comm->comm.src_buff == r2->comm_test.comm->comm.src_buff
 119       && r1->comm_wait.comm->comm.dst_buff == r2->comm_test.comm->comm.dst_buff)
 120     return FALSE;
 121
 122   if (r1->call == REQ_COMM_WAIT && r2->call == REQ_COMM_TEST
 123         && r1->comm_wait.comm->comm.src_buff != NULL
 124         && r1->comm_wait.comm->comm.dst_buff != NULL
 125         && r2->comm_test.comm->comm.src_buff != NULL
 126         && r2->comm_test.comm->comm.dst_buff != NULL
 127         && r1->comm_wait.comm->comm.dst_buff != r2->comm_test.comm->comm.src_buff
 128         && r1->comm_wait.comm->comm.dst_buff != r2->comm_test.comm->comm.dst_buff
 129         && r2->comm_test.comm->comm.dst_buff != r1->comm_wait.comm->comm.src_buff)
 130     return FALSE;
 131
 132   if (r1->call == REQ_COMM_TEST && r2->call == REQ_COMM_WAIT
 133           && r1->comm_test.comm->comm.src_buff != NULL
 134           && r1->comm_test.comm->comm.dst_buff != NULL
 135           && r2->comm_wait.comm->comm.src_buff != NULL
 136           && r2->comm_wait.comm->comm.dst_buff != NULL
 137           && r1->comm_test.comm->comm.dst_buff != r2->comm_wait.comm->comm.src_buff
 138           && r1->comm_test.comm->comm.dst_buff != r2->comm_wait.comm->comm.dst_buff
 139           && r2->comm_wait.comm->comm.dst_buff != r1->comm_test.comm->comm.src_buff)
 140       return FALSE;
 141
 142   return TRUE;
 143 }
 144
 145 char *MC_request_to_string(smx_req_t req, int value)
 146 {
 147   char *type = NULL, *args = NULL, *str = NULL;
 148   smx_action_t act = NULL;
 149   size_t size = 0;
 150
 151   switch(req->call){
 152     case REQ_COMM_ISEND:
 153       type = bprintf("iSend");
 154       args = bprintf("src=%s, buff=%p, size=%zu", req->issuer->name,
 155                      req->comm_isend.src_buff, req->comm_isend.src_buff_size);
 156       break;
 157     case REQ_COMM_IRECV:
 158       size = req->comm_irecv.dst_buff_size ? *req->comm_irecv.dst_buff_size : 0;
 159       type = bprintf("iRecv");
 160       args = bprintf("dst=%s, buff=%p, size=%zu", req->issuer->name,
 161                      req->comm_irecv.dst_buff, size);
 162       break;
 163     case REQ_COMM_WAIT:
 164       act = req->comm_wait.comm;
 165       if(value == -1){
 166         type = bprintf("WaitTimeout");
 167         args = bprintf("comm=%p", act);
 168       }else{
 169         type = bprintf("Wait");
 170         args  = bprintf("comm=%p [(%lu)%s -> (%lu)%s]", act,
 171                         act->comm.src_proc ? act->comm.src_proc->pid : 0,
 172                         act->comm.src_proc ? act->comm.src_proc->name : "",
 173                         act->comm.dst_proc ? act->comm.dst_proc->pid : 0,
 174                         act->comm.dst_proc ? act->comm.dst_proc->name : "");
 175       }
 176       break;
 177     case REQ_COMM_TEST:
 178       act = req->comm_test.comm;
 179       if(act->comm.src_proc == NULL || act->comm.src_proc == NULL){
 180         type = bprintf("Test FALSE");
 181         args = bprintf("comm=%p", act);
 182       }else{
 183         type = bprintf("Test TRUE");
 184         args  = bprintf("comm=%p [(%lu)%s -> (%lu)%s]", act,
 185                           act->comm.src_proc ? act->comm.src_proc->pid : 0,
 186                           act->comm.src_proc ? act->comm.src_proc->name : "",
 187                           act->comm.dst_proc ? act->comm.dst_proc->pid : 0,
 188                           act->comm.dst_proc ? act->comm.dst_proc->name : "");
 189       }
 190       break;
 191
 192     case REQ_COMM_WAITANY:
 193       type = bprintf("WaitAny");
 194       args = bprintf("comm=%p (%d of %lu)", xbt_dynar_get_as(req->comm_waitany.comms, value, smx_action_t),
 195                      value+1, xbt_dynar_length(req->comm_waitany.comms));
 196       break;
 197
 198     case REQ_COMM_TESTANY:
 199       if(value == -1){
 200         type = bprintf("TestAny FALSE");
 201         args = bprintf("-");
 202       }else{
 203         type = bprintf("TestAny");
 204         args = bprintf("(%d of %lu)", value+1, xbt_dynar_length(req->comm_testany.comms));
 205       }
 206       break;
 207
 208     default:
 209       THROW_UNIMPLEMENTED;
 210   }
 211
 212   str = bprintf("[(%lu)%s] %s (%s)", req->issuer->pid ,req->issuer->name, type, args);
 213   xbt_free(type);
 214   xbt_free(args);
 215   return str;
 216 }
 217
 218 unsigned int MC_request_testany_fail(smx_req_t req)
 219 {
 220   unsigned int cursor;
 221   smx_action_t action;
 222
 223   xbt_dynar_foreach(req->comm_testany.comms, cursor, action){
 224     if(action->comm.src_proc && action->comm.dst_proc)
 225       return FALSE;
 226   }
 227
 228   return TRUE;
 229 }
 230
 231 int MC_request_is_visible(smx_req_t req)
 232 {
 233   return req->call == REQ_COMM_ISEND
 234      || req->call == REQ_COMM_IRECV
 235      || req->call == REQ_COMM_WAIT
 236      || req->call == REQ_COMM_WAITANY
 237      || req->call == REQ_COMM_TEST
 238      || req->call == REQ_COMM_TESTANY;
 239 }
 240
 241 int MC_request_is_enabled(smx_req_t req)
 242 {
 243   unsigned int index = 0;
 244   smx_action_t act;
 245
 246   switch (req->call) {
 247
 248     case REQ_COMM_WAIT:
 249       /* FIXME: check also that src and dst processes are not suspended */
 250
 251       /* If it has a timeout it will be always be enabled, because even if the
 252        * communication is not ready, it can timeout and won't block.
 253        * On the other hand if it hasn't a timeout, check if the comm is ready.*/
 254       if(req->comm_wait.timeout >= 0){
 255         return TRUE;
 256       }else{
 257         act = req->comm_wait.comm;
 258         return (act->comm.src_proc && act->comm.dst_proc);
 259       }
 260       break;
 261
 262     case REQ_COMM_WAITANY:
 263       /* Check if it has at least one communication ready */
 264       xbt_dynar_foreach(req->comm_waitany.comms, index, act) {
 265         if (act->comm.src_proc && act->comm.dst_proc){
 266           return TRUE;
 267         }
 268       }
 269       return FALSE;
 270       break;
 271
 272     default:
 273       /* The rest of the request are always enabled */
 274       return TRUE;
 275   }
 276 }
 277
 278 int MC_request_is_enabled_by_idx(smx_req_t req, unsigned int idx)
 279 {
 280   smx_action_t act;
 281
 282   switch (req->call) {
 283
 284     case REQ_COMM_WAIT:
 285       /* FIXME: check also that src and dst processes are not suspended */
 286       act = req->comm_wait.comm;
 287       return (act->comm.src_proc && act->comm.dst_proc);
 288       break;
 289
 290     case REQ_COMM_WAITANY:
 291       act = xbt_dynar_get_as(req->comm_waitany.comms, idx, smx_action_t);
 292       return (act->comm.src_proc && act->comm.dst_proc);
 293       break;
 294
 295     case REQ_COMM_TESTANY:
 296       act = xbt_dynar_get_as(req->comm_testany.comms, idx, smx_action_t);
 297       return (act->comm.src_proc && act->comm.dst_proc);
 298       break;
 299
 300     default:
 301       return TRUE;
 302   }
 303 }
 304
 305 int MC_process_is_enabled(smx_process_t process)
 306 {
 307   if (process->request.call != REQ_NO_REQ && MC_request_is_enabled(&process->request))
 308     return TRUE;
 309
 310   return FALSE;
 311 }