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