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   mc_transition_t trans=NULL;
 193   mc_state_t current_state = NULL;
 194   if(!mc_replay_mode){
 195     MC_SET_RAW_MEM;
 196     trans = MC_trans_waitany_new(comms);
 197     current_state = (mc_state_t)
 198       xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
 199     xbt_setset_set_insert(current_state->created_transitions, trans);
 200     xbt_setset_set_insert(current_state->transitions, trans);
 201     MC_UNSET_RAW_MEM;
 202   }
 203   SIMIX_process_yield();
 204 }
 205
 206 /**
 207  * \brief Intercept a Random action
 208  * \param min The minimum value that can be returned by the Random action
 209  * \param max The maximum value that can be returned by the Random action
 210  */
 211 void MC_trans_intercept_random(int min, int max)
 212 {
 213   int i;
 214   mc_transition_t trans=NULL;
 215   mc_state_t current_state = NULL;
 216   if(!mc_replay_mode){
 217     MC_SET_RAW_MEM;
 218     current_state = (mc_state_t)
 219         xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
 220     for(i=min; i <= max; i++){
 221       trans = MC_trans_random_new(i);
 222       xbt_setset_set_insert(current_state->created_transitions, trans);
 223       xbt_setset_set_insert(current_state->transitions, trans);
 224     }
 225     MC_UNSET_RAW_MEM;
 226   }
 227   SIMIX_process_yield();
 228 }
 229
 230 /* Compute the subset of enabled transitions of the transition set */
 231 void MC_trans_compute_enabled(xbt_setset_set_t enabled, xbt_setset_set_t transitions)
 232 {
 233   unsigned int index = 0;
 234   smx_comm_t comm = NULL;
 235   mc_transition_t trans = NULL;
 236   xbt_setset_cursor_t cursor = NULL;
 237   xbt_setset_foreach(transitions, cursor, trans){
 238     switch(trans->type){
 239       /* Wait transitions are enabled only if the communication has both a
 240          sender and receiver */
 241       case mc_wait:
 242         if(trans->wait.comm->src_proc && trans->wait.comm->dst_proc){
 243           xbt_setset_set_insert(enabled, trans);
 244           DEBUG1("Transition %p is enabled for next state", trans);
 245         }
 246         break;
 247
 248       /* WaitAny transitions are enabled if any of it's communications has both
 249          a sender and a receiver */
 250       case mc_waitany:
 251         xbt_dynar_foreach(trans->waitany.comms, index, comm){
 252           if(comm->src_proc && comm->dst_proc){
 253             xbt_setset_set_insert(enabled, trans);
 254             DEBUG1("Transition %p is enabled for next state", trans);
 255             break;
 256           }
 257         }
 258         break;
 259
 260       /* The rest of the transitions cannot be disabled */
 261       default:
 262         xbt_setset_set_insert(enabled, trans);
 263         DEBUG1("Transition %p is enabled for next state", trans);
 264         break;
 265     }
 266   }
 267 }
 268
 269 /**
 270  * \brief Determine if two transitions are dependent
 271  * \param t1 a transition
 272  * \param t2 a transition
 273  * \return TRUE if \a t1 and \a t2 are dependent. FALSE otherwise.
 274  */
 275 int MC_transition_depend(mc_transition_t t1, mc_transition_t t2)
 276 {
 277   if(t1->process == t2->process)
 278     return FALSE;
 279
 280   if(t1->type != t2->type)
 281     return FALSE;
 282
 283   if(t1->type == mc_random || t2->type == mc_random)
 284     return FALSE;
 285
 286   if(t1->type == mc_isend && t2->type == mc_isend && t1->isend.rdv != t2->isend.rdv)
 287     return FALSE;
 288
 289   if(t1->type == mc_irecv && t2->type == mc_irecv && t1->irecv.rdv != t2->irecv.rdv)
 290     return FALSE;
 291
 292   if(t1->type == mc_wait && t2->type == mc_wait && t1->wait.comm == t2->wait.comm)
 293     return FALSE;
 294
 295   if(t1->type == mc_wait && t2->type == mc_wait
 296      && t1->wait.comm->src_buff != NULL
 297      && t1->wait.comm->dst_buff != NULL
 298      && t2->wait.comm->src_buff != NULL
 299      && t2->wait.comm->dst_buff != NULL
 300      && t1->wait.comm->dst_buff != t2->wait.comm->src_buff
 301      && t1->wait.comm->dst_buff != t2->wait.comm->dst_buff
 302      && t2->wait.comm->dst_buff != t1->wait.comm->src_buff)
 303     return FALSE;
 304
 305   return TRUE;
 306 }