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