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 min, int max)
  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.min = min;
  79   trans->random.max = max;
  80   trans->random.current_value = min;
  81   trans->name = bprintf("[%s][%s] Random (%p)", trans->process->smx_host->name,
  82                         trans->process->name, trans);
  83   return trans;
  84 }
  85
  86 /**
  87  * \brief Deletes a transition
  88  * \param trans The transition to be deleted
  89  */
  90 void MC_transition_delete(mc_transition_t trans)
  91 {
  92   xbt_free(trans->name);
  93   xbt_free(trans);
  94 }
  95
  96 /************************** Interception Functions ****************************/
  97 /* These functions intercept all the actions relevant to the model-checking
  98  * process, the only difference between them is the type of transition they
  99  * create. The interception works by yielding the process performer of the
 100  * action, and depending on the execution mode it behaves diferently.
 101  * There are two running modes, a replay (back-track process) in which no
 102  * transition needs to be created, or a new state expansion, which in
 103  * consecuence a transition needs to be created and added to the set of
 104  * transitions associated to the current state.
 105  */
 106
 107 /**
 108  * \brief Intercept an iSend action
 109  * \param rdv The rendez-vous of the iSend
 110  */
 111 void MC_trans_intercept_isend(smx_rdv_t rdv)
 112 {
 113   mc_transition_t trans=NULL;
 114   mc_state_t current_state = NULL;
 115   if(!mc_replay_mode){
 116     MC_SET_RAW_MEM;
 117     trans = MC_trans_isend_new(rdv);
 118     current_state = (mc_state_t)
 119       xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
 120     xbt_setset_set_insert(current_state->created_transitions, trans);
 121     xbt_setset_set_insert(current_state->transitions, trans);
 122     MC_UNSET_RAW_MEM;
 123   }
 124   SIMIX_process_yield();
 125 }
 126
 127 /**
 128  * \brief Intercept an iRecv action
 129  * \param rdv The rendez-vous of the iRecv
 130  */
 131 void MC_trans_intercept_irecv(smx_rdv_t rdv)
 132 {
 133   mc_transition_t trans=NULL;
 134   mc_state_t current_state = NULL;
 135   if(!mc_replay_mode){
 136     MC_SET_RAW_MEM;
 137     trans = MC_trans_irecv_new(rdv);
 138     current_state = (mc_state_t)
 139       xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
 140     xbt_setset_set_insert(current_state->created_transitions, trans);
 141     xbt_setset_set_insert(current_state->transitions, trans);
 142     MC_UNSET_RAW_MEM;
 143   }
 144   SIMIX_process_yield();
 145 }
 146
 147 /**
 148  * \brief Intercept a Wait action
 149  * \param comm The communication associated to the wait
 150  */
 151 void MC_trans_intercept_wait(smx_comm_t comm)
 152 {
 153   mc_transition_t trans=NULL;
 154   mc_state_t current_state = NULL;
 155   if(!mc_replay_mode){
 156     MC_SET_RAW_MEM;
 157     trans = MC_trans_wait_new(comm);
 158     current_state = (mc_state_t)
 159       xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
 160     xbt_setset_set_insert(current_state->created_transitions, trans);
 161     xbt_setset_set_insert(current_state->transitions, trans);
 162     MC_UNSET_RAW_MEM;
 163   }
 164   SIMIX_process_yield();
 165 }
 166
 167 /**
 168  * \brief Intercept a Test action
 169  * \param comm The communication associated to the Test
 170  */
 171 void MC_trans_intercept_test(smx_comm_t comm)
 172 {
 173   mc_transition_t trans=NULL;
 174   mc_state_t current_state = NULL;
 175   if(!mc_replay_mode){
 176     MC_SET_RAW_MEM;
 177     trans = MC_trans_test_new(comm);
 178     current_state = (mc_state_t)
 179       xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
 180     xbt_setset_set_insert(current_state->created_transitions, trans);
 181     xbt_setset_set_insert(current_state->transitions, trans);
 182     MC_UNSET_RAW_MEM;
 183   }
 184   SIMIX_process_yield();
 185 }
 186
 187 /**
 188  * \brief Intercept a WaitAny action
 189  * \param comms The communications associated to the WaitAny
 190  */
 191 void MC_trans_intercept_waitany(xbt_dynar_t comms)
 192 {
 193   mc_transition_t trans=NULL;
 194   mc_state_t current_state = NULL;
 195   if(!mc_replay_mode){
 196     MC_SET_RAW_MEM;
 197     trans = MC_trans_waitany_new(comms);
 198     current_state = (mc_state_t)
 199       xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
 200     xbt_setset_set_insert(current_state->created_transitions, trans);
 201     xbt_setset_set_insert(current_state->transitions, trans);
 202     MC_UNSET_RAW_MEM;
 203   }
 204   SIMIX_process_yield();
 205 }
 206
 207 /**
 208  * \brief Intercept a Random action
 209  * \param min The minimum value that can be returned by the Random action
 210  * \param max The maximum value that can be returned by the Random action
 211  */
 212 void MC_trans_intercept_random(int min, int max)
 213 {
 214   mc_transition_t trans=NULL;
 215   mc_state_t current_state = NULL;
 216   if(!mc_replay_mode){
 217     MC_SET_RAW_MEM;
 218     trans = MC_trans_random_new(min, max);
 219     current_state = (mc_state_t)
 220       xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
 221     xbt_setset_set_insert(current_state->created_transitions, trans);
 222     xbt_setset_set_insert(current_state->transitions, trans);
 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 != t2->type)
 279     return FALSE;
 280
 281   if(t1->type == mc_isend && t2->type == mc_isend && t1->isend.rdv != t2->isend.rdv)
 282     return FALSE;
 283
 284   if(t1->type == mc_irecv && t2->type == mc_irecv && t1->irecv.rdv != t2->irecv.rdv)
 285     return FALSE;
 286
 287   if(t1->type == mc_wait && t2->type == mc_wait && t1->wait.comm == t2->wait.comm)
 288     return FALSE;
 289
 290   if(t1->type == mc_wait && t2->type == mc_wait
 291      && t1->wait.comm->src_buff != NULL
 292      && t1->wait.comm->dst_buff != NULL
 293      && t2->wait.comm->src_buff != NULL
 294      && t2->wait.comm->dst_buff != NULL
 295      && t1->wait.comm->dst_buff != t2->wait.comm->src_buff
 296      && t1->wait.comm->dst_buff != t2->wait.comm->dst_buff
 297      && t2->wait.comm->dst_buff != t1->wait.comm->src_buff)
 298     return FALSE;
 299
 300   return TRUE;
 301 }