src/mc/mc_transition.c

   1 #include "private.h"
   2
   3 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_trans, mc,
   4                                 "Logging specific to MC transitions");
   5
   6 /* Creates a new iSend transition */
   7 mc_transition_t MC_trans_isend_new(smx_rdv_t rdv)
   8 {
   9   mc_transition_t trans = xbt_new0(s_mc_transition_t, 1);
  10
  11   trans->type = mc_isend;
  12   trans->process = SIMIX_process_self();
  13   trans->isend.rdv = rdv;
  14   trans->name = bprintf("[%s][%s] iSend (%p)", trans->process->smx_host->name,
  15                         trans->process->name, trans);
  16   return trans;
  17 }
  18
  19 /* Creates a new iRecv transition */
  20 mc_transition_t MC_trans_irecv_new(smx_rdv_t rdv)
  21 {
  22   mc_transition_t trans = xbt_new0(s_mc_transition_t, 1);
  23
  24   trans->type = mc_irecv;
  25   trans->process = SIMIX_process_self();
  26   trans->irecv.rdv = rdv;
  27   trans->name = bprintf("[%s][%s] iRecv (%p)", trans->process->smx_host->name,
  28                         trans->process->name, trans);
  29   return trans;
  30 }
  31
  32 /* Creates a new Wait transition */
  33 mc_transition_t MC_trans_wait_new(smx_comm_t comm)
  34 {
  35   mc_transition_t trans = xbt_new0(s_mc_transition_t, 1);
  36
  37   trans->type = mc_wait;
  38   trans->process = SIMIX_process_self();
  39   trans->wait.comm = comm;
  40   trans->name = bprintf("[%s][%s] Wait (%p)", trans->process->smx_host->name,
  41                         trans->process->name, trans);
  42   return trans;
  43 }
  44
  45 /* Creates a new test transition */
  46 mc_transition_t MC_trans_test_new(smx_comm_t comm)
  47 {
  48   mc_transition_t trans = xbt_new0(s_mc_transition_t, 1);
  49
  50   trans->type = mc_test;
  51   trans->process = SIMIX_process_self();
  52   trans->test.comm = comm;
  53   trans->name = bprintf("[%s][%s] Test (%p)", trans->process->smx_host->name,
  54                         trans->process->name, trans);
  55   return trans;
  56 }
  57
  58 /* Creates a new WaitAny transition */
  59 mc_transition_t MC_trans_waitany_new(xbt_dynar_t comms)
  60 {
  61   mc_transition_t trans = xbt_new0(s_mc_transition_t, 1);
  62
  63   trans->type = mc_waitany;
  64   trans->process = SIMIX_process_self();
  65   trans->waitany.comms = comms;
  66   trans->name = bprintf("[%s][%s] WaitAny (%p)", trans->process->smx_host->name,
  67                         trans->process->name, trans);
  68   return trans;
  69 }
  70
  71 /* Creates a new Random transition */
  72 mc_transition_t MC_trans_random_new(int value)
  73 {
  74   mc_transition_t trans = xbt_new0(s_mc_transition_t, 1);
  75
  76   trans->type = mc_random;
  77   trans->process = SIMIX_process_self();
  78   trans->random.value = value;
  79   trans->name = bprintf("[%s][%s] Random %d (%p)", trans->process->smx_host->name,
  80                         trans->process->name, value, trans);
  81
  82   return trans;
  83 }
  84
  85 /**
  86  * \brief Deletes a transition
  87  * \param trans The transition to be deleted
  88  */
  89 void MC_transition_delete(mc_transition_t trans)
  90 {
  91   xbt_free(trans->name);
  92   xbt_free(trans);
  93 }
  94
  95 /************************** Interception Functions ****************************/
  96 /* These functions intercept all the actions relevant to the model-checking
  97  * process, the only difference between them is the type of transition they
  98  * create. The interception works by yielding the process performer of the
  99  * action, and depending on the execution mode it behaves diferently.
 100  * There are two running modes, a replay (back-track process) in which no
 101  * transition needs to be created, or a new state expansion, which in
 102  * consecuence a transition needs to be created and added to the set of
 103  * transitions associated to the current state.
 104  */
 105
 106 /**
 107  * \brief Intercept an iSend action
 108  * \param rdv The rendez-vous of the iSend
 109  */
 110 void MC_trans_intercept_isend(smx_rdv_t rdv)
 111 {
 112   mc_transition_t trans=NULL;
 113   mc_state_t current_state = NULL;
 114   if(!mc_replay_mode){
 115     MC_SET_RAW_MEM;
 116     trans = MC_trans_isend_new(rdv);
 117     current_state = (mc_state_t)
 118       xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
 119     xbt_setset_set_insert(current_state->created_transitions, trans);
 120     xbt_setset_set_insert(current_state->transitions, trans);
 121     MC_UNSET_RAW_MEM;
 122   }
 123   SIMIX_process_yield();
 124 }
 125
 126 /**
 127  * \brief Intercept an iRecv action
 128  * \param rdv The rendez-vous of the iRecv
 129  */
 130 void MC_trans_intercept_irecv(smx_rdv_t rdv)
 131 {
 132   mc_transition_t trans=NULL;
 133   mc_state_t current_state = NULL;
 134   if(!mc_replay_mode){
 135     MC_SET_RAW_MEM;
 136     trans = MC_trans_irecv_new(rdv);
 137     current_state = (mc_state_t)
 138       xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
 139     xbt_setset_set_insert(current_state->created_transitions, trans);
 140     xbt_setset_set_insert(current_state->transitions, trans);
 141     MC_UNSET_RAW_MEM;
 142   }
 143   SIMIX_process_yield();
 144 }
 145
 146 /**
 147  * \brief Intercept a Wait action
 148  * \param comm The communication associated to the wait
 149  */
 150 void MC_trans_intercept_wait(smx_comm_t comm)
 151 {
 152   mc_transition_t trans=NULL;
 153   mc_state_t current_state = NULL;
 154   if(!mc_replay_mode){
 155     MC_SET_RAW_MEM;
 156     trans = MC_trans_wait_new(comm);
 157     current_state = (mc_state_t)
 158       xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
 159     xbt_setset_set_insert(current_state->created_transitions, trans);
 160     xbt_setset_set_insert(current_state->transitions, trans);
 161     MC_UNSET_RAW_MEM;
 162   }
 163   SIMIX_process_yield();
 164 }
 165
 166 /**
 167  * \brief Intercept a Test action
 168  * \param comm The communication associated to the Test
 169  */
 170 void MC_trans_intercept_test(smx_comm_t comm)
 171 {
 172   mc_transition_t trans=NULL;
 173   mc_state_t current_state = NULL;
 174   if(!mc_replay_mode){
 175     MC_SET_RAW_MEM;
 176     trans = MC_trans_test_new(comm);
 177     current_state = (mc_state_t)
 178       xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
 179     xbt_setset_set_insert(current_state->created_transitions, trans);
 180     xbt_setset_set_insert(current_state->transitions, trans);
 181     MC_UNSET_RAW_MEM;
 182   }
 183   SIMIX_process_yield();
 184 }
 185
 186 /**
 187  * \brief Intercept a WaitAny action
 188  * \param comms The communications associated to the WaitAny
 189  */
 190 void MC_trans_intercept_waitany(xbt_dynar_t comms)
 191 {
 192   unsigned int cursor;
 193   mc_transition_t trans = NULL;
 194   mc_state_t current_state = NULL;
 195   smx_comm_t comm = NULL;
 196
 197   if(!mc_replay_mode){
 198     MC_SET_RAW_MEM;
 199     current_state = (mc_state_t)
 200       xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
 201     xbt_dynar_foreach(comms, cursor, comm){
 202       trans = MC_trans_wait_new(comm);
 203       xbt_setset_set_insert(current_state->created_transitions, trans);
 204       xbt_setset_set_insert(current_state->transitions, trans);
 205     }
 206     MC_UNSET_RAW_MEM;
 207   }
 208   SIMIX_process_yield();
 209 }
 210
 211 /**
 212  * \brief Intercept a Random action
 213  * \param min The minimum value that can be returned by the Random action
 214  * \param max The maximum value that can be returned by the Random action
 215  */
 216 void MC_trans_intercept_random(int min, int max)
 217 {
 218   int i;
 219   mc_transition_t trans=NULL;
 220   mc_state_t current_state = NULL;
 221   if(!mc_replay_mode){
 222     MC_SET_RAW_MEM;
 223     current_state = (mc_state_t)
 224       xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
 225     for(i=min; i <= max; i++){
 226       trans = MC_trans_random_new(i);
 227       xbt_setset_set_insert(current_state->created_transitions, trans);
 228       xbt_setset_set_insert(current_state->transitions, trans);
 229     }
 230     MC_UNSET_RAW_MEM;
 231   }
 232   SIMIX_process_yield();
 233 }
 234
 235 /* Compute the subset of enabled transitions of the transition set */
 236 void MC_trans_compute_enabled(xbt_setset_set_t enabled, xbt_setset_set_t transitions)
 237 {
 238   unsigned int index = 0;
 239   smx_comm_t comm = NULL;
 240   mc_transition_t trans = NULL;
 241   xbt_setset_cursor_t cursor = NULL;
 242   xbt_setset_foreach(transitions, cursor, trans){
 243     switch(trans->type){
 244       /* Wait transitions are enabled only if the communication has both a
 245          sender and receiver */
 246       case mc_wait:
 247         if(trans->wait.comm->src_proc && trans->wait.comm->dst_proc){
 248           xbt_setset_set_insert(enabled, trans);
 249           DEBUG1("Transition %p is enabled for next state", trans);
 250         }
 251         break;
 252
 253       /* WaitAny transitions are enabled if any of it's communications has both
 254          a sender and a receiver */
 255       case mc_waitany:
 256         xbt_dynar_foreach(trans->waitany.comms, index, comm){
 257           if(comm->src_proc && comm->dst_proc){
 258             xbt_setset_set_insert(enabled, trans);
 259             DEBUG1("Transition %p is enabled for next state", trans);
 260             break;
 261           }
 262         }
 263         break;
 264
 265       /* The rest of the transitions cannot be disabled */
 266       default:
 267         xbt_setset_set_insert(enabled, trans);
 268         DEBUG1("Transition %p is enabled for next state", trans);
 269         break;
 270     }
 271   }
 272 }
 273
 274 /**
 275  * \brief Determine if two transitions are dependent
 276  * \param t1 a transition
 277  * \param t2 a transition
 278  * \return TRUE if \a t1 and \a t2 are dependent. FALSE otherwise.
 279  */
 280 int MC_transition_depend(mc_transition_t t1, mc_transition_t t2)
 281 {
 282   if(t1->process == t2->process)
 283     return FALSE;
 284
 285   if(t1->type == mc_isend && t2->type == mc_irecv)
 286     return FALSE;
 287
 288   if(t1->type == mc_irecv && t2->type == mc_isend)
 289     return FALSE;
 290
 291   if(t1->type == mc_random || t2->type == mc_random)
 292     return FALSE;
 293
 294   if(t1->type == mc_isend && t2->type == mc_isend && t1->isend.rdv != t2->isend.rdv)
 295     return FALSE;
 296
 297   if(t1->type == mc_irecv && t2->type == mc_irecv && t1->irecv.rdv != t2->irecv.rdv)
 298     return FALSE;
 299
 300   if(t1->type == mc_wait && t2->type == mc_wait && t1->wait.comm == t2->wait.comm)
 301     return FALSE;
 302
 303   if(t1->type == mc_wait && t2->type == mc_wait
 304      && t1->wait.comm->src_buff != NULL
 305      && t1->wait.comm->dst_buff != NULL
 306      && t2->wait.comm->src_buff != NULL
 307      && t2->wait.comm->dst_buff != NULL
 308      && t1->wait.comm->dst_buff != t2->wait.comm->src_buff
 309      && t1->wait.comm->dst_buff != t2->wait.comm->dst_buff
 310      && t2->wait.comm->dst_buff != t1->wait.comm->src_buff)
 311     return FALSE;
 312
 313   return TRUE;
 314 }