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