Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Rework MC transition interception/creation. Now it is more modular.
[simgrid.git] / 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 /************************** Interception Functions ****************************/
84 /* These functions intercept all the actions relevant to the model-checking
85  * process, the only difference between them is the type of transition they
86  * create. The interception works by yielding the process performer of the
87  * action, and depending on the execution mode it behaves diferently.
88  * There are two running modes, a replay (back-track process) in which no 
89  * transition needs to be created, or a new state expansion, which in 
90  * consecuence a transition needs to be created and added to the set of
91  * transitions associated to the current state.
92  */
93
94 /**
95  * \brief Intercept an iSend action
96  * \param rdv The rendez-vous of the iSend
97  */
98 void MC_trans_intercept_isend(smx_rdv_t rdv)
99 {
100   mc_transition_t trans=NULL;
101   mc_state_t current_state = NULL;
102   if(!mc_replay_mode){
103     MC_SET_RAW_MEM;
104     trans = MC_trans_isend_new(rdv);
105     current_state = (mc_state_t) 
106       xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
107     xbt_setset_set_insert(current_state->created_transitions, trans);
108     xbt_setset_set_insert(current_state->transitions, trans);
109     MC_UNSET_RAW_MEM;
110   }
111   SIMIX_process_yield();  
112 }
113
114 /**
115  * \brief Intercept an iRecv action
116  * \param rdv The rendez-vous of the iRecv
117  */
118 void MC_trans_intercept_irecv(smx_rdv_t rdv)
119 {
120   mc_transition_t trans=NULL;
121   mc_state_t current_state = NULL;
122   if(!mc_replay_mode){
123     MC_SET_RAW_MEM;
124     trans = MC_trans_irecv_new(rdv);
125     current_state = (mc_state_t) 
126       xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
127     xbt_setset_set_insert(current_state->created_transitions, trans);
128     xbt_setset_set_insert(current_state->transitions, trans);
129     MC_UNSET_RAW_MEM;
130   }
131   SIMIX_process_yield();
132 }
133
134 /**
135  * \brief Intercept a Wait action
136  * \param comm The communication associated to the wait
137  */
138 void MC_trans_intercept_wait(smx_comm_t comm)
139 {
140   mc_transition_t trans=NULL;
141   mc_state_t current_state = NULL;
142   if(!mc_replay_mode){
143     MC_SET_RAW_MEM;
144     trans = MC_trans_wait_new(comm);
145     current_state = (mc_state_t) 
146       xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
147     xbt_setset_set_insert(current_state->created_transitions, trans);
148     xbt_setset_set_insert(current_state->transitions, trans);
149     MC_UNSET_RAW_MEM;
150   }
151   SIMIX_process_yield();
152 }
153
154 /**
155  * \brief Intercept a Test action
156  * \param comm The communication associated to the Test
157  */
158 void MC_trans_intercept_test(smx_comm_t comm)
159 {
160   mc_transition_t trans=NULL;
161   mc_state_t current_state = NULL;
162   if(!mc_replay_mode){
163     MC_SET_RAW_MEM;
164     trans = MC_trans_test_new(comm);
165     current_state = (mc_state_t) 
166       xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
167     xbt_setset_set_insert(current_state->created_transitions, trans);
168     xbt_setset_set_insert(current_state->transitions, trans);
169     MC_UNSET_RAW_MEM;
170   }
171   SIMIX_process_yield();
172 }
173
174 /**
175  * \brief Intercept a WaitAny action
176  * \param comms The communications associated to the WaitAny
177  */
178 void MC_trans_intercept_waitany(xbt_dynar_t comms)
179 {
180   mc_transition_t trans=NULL;
181   mc_state_t current_state = NULL;
182   if(!mc_replay_mode){
183     MC_SET_RAW_MEM;
184     trans = MC_trans_waitany_new(comms);
185     current_state = (mc_state_t) 
186       xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
187     xbt_setset_set_insert(current_state->created_transitions, trans);
188     xbt_setset_set_insert(current_state->transitions, trans);
189     MC_UNSET_RAW_MEM;
190   }
191   SIMIX_process_yield();
192 }
193
194 /**
195  * \brief Intercept a Random action
196  * \param min The minimum value that can be returned by the Random action
197  * \param max The maximum value that can be returned by the Random action
198  */
199 void MC_trans_intercept_random(int min, int max)
200 {
201   mc_transition_t trans=NULL;
202   mc_state_t current_state = NULL;
203   if(!mc_replay_mode){
204     MC_SET_RAW_MEM;
205     trans = MC_trans_random_new(min, max);
206     current_state = (mc_state_t) 
207       xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
208     xbt_setset_set_insert(current_state->created_transitions, trans);
209     xbt_setset_set_insert(current_state->transitions, trans);
210     MC_UNSET_RAW_MEM;
211   }
212   SIMIX_process_yield();
213 }
214
215 /**
216  * \brief Deletes a transition
217  * \param trans The transition to be deleted
218  */
219 void MC_transition_delete(mc_transition_t trans)
220 {
221   xbt_free(trans->name);
222   xbt_free(trans);
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   mc_transition_t trans = NULL;
229   xbt_setset_cursor_t cursor = NULL;
230   /* Add all the transitions to the enabled set and then remove the disabled ones */
231   xbt_setset_add(enabled, transitions); 
232   xbt_setset_foreach(transitions, cursor, trans){
233     if(trans->type == mc_wait
234        && (trans->wait.comm->src_proc == NULL || trans->wait.comm->dst_proc == NULL)){
235       xbt_setset_set_remove(enabled, trans);
236     }
237   }
238 }
239
240 /**
241  * \brief Determine if two transitions are dependent
242  * \param t1 a transition
243  * \param t2 a transition
244  * \return TRUE if \a t1 and \a t2 are dependent. FALSE otherwise.
245  */
246 int MC_transition_depend(mc_transition_t t1, mc_transition_t t2)
247 {
248   if(t1->process == t2->process) 
249     return FALSE;
250
251   if(t1->type != t2->type)
252     return FALSE;
253   
254   if(t1->type == mc_isend && t2->type == mc_isend && t1->isend.rdv != t2->isend.rdv)
255     return FALSE;
256
257   if(t1->type == mc_irecv && t2->type == mc_irecv && t1->irecv.rdv != t2->irecv.rdv)
258     return FALSE;
259
260   if(t1->type == mc_wait && t2->type == mc_wait && t1->wait.comm == t2->wait.comm)
261     return FALSE;
262   
263   if(t1->type == mc_wait && t2->type == mc_wait 
264      && t1->wait.comm->src_buff != NULL
265      && t1->wait.comm->dst_buff != NULL
266      && t2->wait.comm->src_buff != NULL
267      && t2->wait.comm->dst_buff != NULL
268      && t1->wait.comm->dst_buff != t2->wait.comm->src_buff
269      && t1->wait.comm->dst_buff != t2->wait.comm->dst_buff
270      && t2->wait.comm->dst_buff != t1->wait.comm->src_buff)
271     return FALSE;
272   
273   return TRUE;
274 }