src/mc/mc_transition.c

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