Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
MC: perform actual model-checking in tesh tests
[simgrid.git] / src / mc / mc_request.c
1 #include "private.h"
2
3 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_request, mc,
4                                 "Logging specific to MC (request)");
5
6 static char* pointer_to_string(void* pointer);
7
8 int MC_request_depend(smx_req_t r1, smx_req_t r2)
9 {
10   if(_surf_do_model_check == 2)
11     return TRUE;
12
13   if (r1->issuer == r2->issuer)
14     return FALSE;
15
16   if(r1->call == REQ_COMM_ISEND && r2->call == REQ_COMM_IRECV)
17     return FALSE;
18
19   if(r1->call == REQ_COMM_IRECV && r2->call == REQ_COMM_ISEND)
20     return FALSE;
21
22   if(   (r1->call == REQ_COMM_ISEND || r1->call == REQ_COMM_IRECV)
23        &&  r2->call == REQ_COMM_WAIT){
24
25     if(r2->comm_wait.comm->comm.rdv == NULL)
26       return FALSE;
27
28     smx_rdv_t rdv = r1->call == REQ_COMM_ISEND ? r1->comm_isend.rdv : r1->comm_irecv.rdv;
29
30     if(r2->comm_wait.comm->comm.rdv != rdv)
31       return FALSE;
32
33     if(r2->comm_wait.comm->comm.type == SIMIX_COMM_SEND && r1->call == REQ_COMM_ISEND)
34       return FALSE;
35
36     if(r2->comm_wait.comm->comm.type == SIMIX_COMM_RECEIVE && r1->call == REQ_COMM_IRECV)
37       return FALSE;
38   }
39
40   if(   (r2->call == REQ_COMM_ISEND || r2->call == REQ_COMM_IRECV)
41        &&  r1->call == REQ_COMM_WAIT){
42
43     if(r1->comm_wait.comm->comm.rdv != NULL)
44       return FALSE;
45
46     smx_rdv_t rdv = r2->call == REQ_COMM_ISEND ? r2->comm_isend.rdv : r2->comm_irecv.rdv;
47
48     if(r1->comm_wait.comm->comm.rdv != rdv)
49       return FALSE;
50
51     if(r1->comm_wait.comm->comm.type == SIMIX_COMM_SEND && r2->call == REQ_COMM_ISEND)
52       return FALSE;
53
54     if(r1->comm_wait.comm->comm.type == SIMIX_COMM_RECEIVE && r2->call == REQ_COMM_IRECV)
55       return FALSE;
56   }
57
58   /* FIXME: the following rule assumes that the result of the
59    * isend/irecv call is not stored in a buffer used in the
60    * test call. */
61   if(   (r1->call == REQ_COMM_ISEND || r1->call == REQ_COMM_IRECV)
62      &&  r2->call == REQ_COMM_TEST)
63     return FALSE;
64
65   /* FIXME: the following rule assumes that the result of the
66    * isend/irecv call is not stored in a buffer used in the
67    * test call.*/
68   if(   (r2->call == REQ_COMM_ISEND || r2->call == REQ_COMM_IRECV)
69      && r1->call == REQ_COMM_TEST)
70     return FALSE;
71
72   if(r1->call == REQ_COMM_ISEND && r2->call == REQ_COMM_ISEND
73       && r1->comm_isend.rdv != r2->comm_isend.rdv)
74     return FALSE;
75
76   if(r1->call == REQ_COMM_IRECV && r2->call == REQ_COMM_IRECV
77       && r1->comm_irecv.rdv != r2->comm_irecv.rdv)
78     return FALSE;
79
80   if(r1->call == REQ_COMM_WAIT && (r2->call == REQ_COMM_WAIT || r2->call == REQ_COMM_TEST)
81      && (r1->comm_wait.comm->comm.src_proc == NULL
82          || r1->comm_wait.comm->comm.dst_proc == NULL))
83     return FALSE;
84
85   if(r2->call == REQ_COMM_WAIT && (r1->call == REQ_COMM_WAIT || r1->call == REQ_COMM_TEST)
86      && (r2->comm_wait.comm->comm.src_proc == NULL
87          || r2->comm_wait.comm->comm.dst_proc == NULL))
88     return FALSE;
89
90   if(r1->call == REQ_COMM_WAIT && r2->call == REQ_COMM_WAIT
91       && r1->comm_wait.comm->comm.src_buff == r2->comm_wait.comm->comm.src_buff
92       && r1->comm_wait.comm->comm.dst_buff == r2->comm_wait.comm->comm.dst_buff)
93     return FALSE;
94
95   if (r1->call == REQ_COMM_WAIT && r2->call == REQ_COMM_WAIT
96       && r1->comm_wait.comm->comm.src_buff != NULL
97       && r1->comm_wait.comm->comm.dst_buff != NULL
98       && r2->comm_wait.comm->comm.src_buff != NULL
99       && r2->comm_wait.comm->comm.dst_buff != NULL
100       && r1->comm_wait.comm->comm.dst_buff != r2->comm_wait.comm->comm.src_buff
101       && r1->comm_wait.comm->comm.dst_buff != r2->comm_wait.comm->comm.dst_buff
102       && r2->comm_wait.comm->comm.dst_buff != r1->comm_wait.comm->comm.src_buff)
103     return FALSE;
104
105   if(r1->call == REQ_COMM_TEST &&
106       (r1->comm_test.comm == NULL
107        || r1->comm_test.comm->comm.src_buff == NULL
108        || r1->comm_test.comm->comm.dst_buff == NULL))
109     return FALSE;
110
111   if(r2->call == REQ_COMM_TEST &&
112       (r2->comm_test.comm == NULL
113        || r2->comm_test.comm->comm.src_buff == NULL
114        || r2->comm_test.comm->comm.dst_buff == NULL))
115     return FALSE;
116
117   if(r1->call == REQ_COMM_TEST && r2->call == REQ_COMM_WAIT
118       && r1->comm_test.comm->comm.src_buff == r2->comm_wait.comm->comm.src_buff
119       && r1->comm_test.comm->comm.dst_buff == r2->comm_wait.comm->comm.dst_buff)
120     return FALSE;
121
122   if(r1->call == REQ_COMM_WAIT && r2->call == REQ_COMM_TEST
123       && r1->comm_wait.comm->comm.src_buff == r2->comm_test.comm->comm.src_buff
124       && r1->comm_wait.comm->comm.dst_buff == r2->comm_test.comm->comm.dst_buff)
125     return FALSE;
126
127   if (r1->call == REQ_COMM_WAIT && r2->call == REQ_COMM_TEST
128         && r1->comm_wait.comm->comm.src_buff != NULL
129         && r1->comm_wait.comm->comm.dst_buff != NULL
130         && r2->comm_test.comm->comm.src_buff != NULL
131         && r2->comm_test.comm->comm.dst_buff != NULL
132         && r1->comm_wait.comm->comm.dst_buff != r2->comm_test.comm->comm.src_buff
133         && r1->comm_wait.comm->comm.dst_buff != r2->comm_test.comm->comm.dst_buff
134         && r2->comm_test.comm->comm.dst_buff != r1->comm_wait.comm->comm.src_buff)
135     return FALSE;
136
137   if (r1->call == REQ_COMM_TEST && r2->call == REQ_COMM_WAIT
138           && r1->comm_test.comm->comm.src_buff != NULL
139           && r1->comm_test.comm->comm.dst_buff != NULL
140           && r2->comm_wait.comm->comm.src_buff != NULL
141           && r2->comm_wait.comm->comm.dst_buff != NULL
142           && r1->comm_test.comm->comm.dst_buff != r2->comm_wait.comm->comm.src_buff
143           && r1->comm_test.comm->comm.dst_buff != r2->comm_wait.comm->comm.dst_buff
144           && r2->comm_wait.comm->comm.dst_buff != r1->comm_test.comm->comm.src_buff)
145       return FALSE;
146
147   return TRUE;
148 }
149
150 static char* pointer_to_string(void* pointer) {
151
152   if (XBT_LOG_ISENABLED(mc_request, xbt_log_priority_verbose))
153     return bprintf("%p", pointer);
154
155   return xbt_strdup("(verbose only)");
156 }
157
158 char *MC_request_to_string(smx_req_t req, int value)
159 {
160   char *type = NULL, *args = NULL, *str = NULL, *p = NULL;
161   smx_action_t act = NULL;
162   size_t size = 0;
163
164   switch(req->call){
165     case REQ_COMM_ISEND:
166       type = xbt_strdup("iSend");
167       p = pointer_to_string(req->comm_isend.src_buff);
168       args = bprintf("src=%s, buff=%s, size=%zu", req->issuer->name, 
169                      p, req->comm_isend.src_buff_size);
170       break;
171     case REQ_COMM_IRECV:
172       size = req->comm_irecv.dst_buff_size ? *req->comm_irecv.dst_buff_size : 0;
173       type = xbt_strdup("iRecv");
174       p = pointer_to_string(req->comm_irecv.dst_buff); 
175       args = bprintf("dst=%s, buff=%s, size=%zu", req->issuer->name, 
176                      p, size);
177       break;
178     case REQ_COMM_WAIT:
179       act = req->comm_wait.comm;
180       if(value == -1){
181         type = xbt_strdup("WaitTimeout");
182         p = pointer_to_string(act);
183         args = bprintf("comm=%p", p);
184       }else{
185         type = xbt_strdup("Wait");
186         p = pointer_to_string(act);
187         args  = bprintf("comm=%s [(%lu)%s -> (%lu)%s]", p,
188                         act->comm.src_proc ? act->comm.src_proc->pid : 0,
189                         act->comm.src_proc ? act->comm.src_proc->name : "",
190                         act->comm.dst_proc ? act->comm.dst_proc->pid : 0,
191                         act->comm.dst_proc ? act->comm.dst_proc->name : "");
192       }
193       break;
194     case REQ_COMM_TEST:
195       act = req->comm_test.comm;
196       if(act->comm.src_proc == NULL || act->comm.src_proc == NULL){
197         type = xbt_strdup("Test FALSE");
198         p = pointer_to_string(act);
199         args = bprintf("comm=%s", p);
200       }else{
201         type = xbt_strdup("Test TRUE");
202         p = pointer_to_string(act);
203         args  = bprintf("comm=%s [(%lu)%s -> (%lu)%s]", p,
204                         act->comm.src_proc ? act->comm.src_proc->pid : 0,
205                         act->comm.src_proc ? act->comm.src_proc->name : "",
206                         act->comm.dst_proc ? act->comm.dst_proc->pid : 0,
207                         act->comm.dst_proc ? act->comm.dst_proc->name : "");
208       }
209       break;
210
211     case REQ_COMM_WAITANY:
212       type = xbt_strdup("WaitAny");
213       p = pointer_to_string(xbt_dynar_get_as(req->comm_waitany.comms, value, smx_action_t));
214       args = bprintf("comm=%s (%d of %lu)", p,
215                      value+1, xbt_dynar_length(req->comm_waitany.comms));
216       break;
217
218     case REQ_COMM_TESTANY:
219       if(value == -1){
220         type = xbt_strdup("TestAny FALSE");
221         args = xbt_strdup("-");
222       }else{
223         type = xbt_strdup("TestAny");
224         args = bprintf("(%d of %lu)", value+1, xbt_dynar_length(req->comm_testany.comms));
225       }
226       break;
227
228     default:
229       THROW_UNIMPLEMENTED;
230   }
231
232   str = bprintf("[(%lu)%s] %s (%s)", req->issuer->pid ,req->issuer->name, type, args);
233   xbt_free(type);
234   xbt_free(args);
235   xbt_free(p);
236   return str;
237 }
238
239 unsigned int MC_request_testany_fail(smx_req_t req)
240 {
241   unsigned int cursor;
242   smx_action_t action;
243
244   xbt_dynar_foreach(req->comm_testany.comms, cursor, action){
245     if(action->comm.src_proc && action->comm.dst_proc)
246       return FALSE;
247   }
248
249   return TRUE;
250 }
251
252 int MC_request_is_visible(smx_req_t req)
253 {
254   return req->call == REQ_COMM_ISEND
255      || req->call == REQ_COMM_IRECV
256      || req->call == REQ_COMM_WAIT
257      || req->call == REQ_COMM_WAITANY
258      || req->call == REQ_COMM_TEST
259      || req->call == REQ_COMM_TESTANY;
260 }
261
262 int MC_request_is_enabled(smx_req_t req)
263 {
264   unsigned int index = 0;
265   smx_action_t act;
266
267   switch (req->call) {
268
269     case REQ_COMM_WAIT:
270       /* FIXME: check also that src and dst processes are not suspended */
271
272       /* If it has a timeout it will be always be enabled, because even if the
273        * communication is not ready, it can timeout and won't block.
274        * On the other hand if it hasn't a timeout, check if the comm is ready.*/
275       if(req->comm_wait.timeout >= 0){
276         return TRUE;
277       }else{
278         act = req->comm_wait.comm;
279         return (act->comm.src_proc && act->comm.dst_proc);
280       }
281       break;
282
283     case REQ_COMM_WAITANY:
284       /* Check if it has at least one communication ready */
285       xbt_dynar_foreach(req->comm_waitany.comms, index, act) {
286         if (act->comm.src_proc && act->comm.dst_proc){
287           return TRUE;
288         }
289       }
290       return FALSE;
291       break;
292
293     default:
294       /* The rest of the request are always enabled */
295       return TRUE;
296   }
297 }
298
299 int MC_request_is_enabled_by_idx(smx_req_t req, unsigned int idx)
300 {
301   smx_action_t act;
302
303   switch (req->call) {
304
305     case REQ_COMM_WAIT:
306       /* FIXME: check also that src and dst processes are not suspended */
307       act = req->comm_wait.comm;
308       return (act->comm.src_proc && act->comm.dst_proc);
309       break;
310
311     case REQ_COMM_WAITANY:
312       act = xbt_dynar_get_as(req->comm_waitany.comms, idx, smx_action_t);
313       return (act->comm.src_proc && act->comm.dst_proc);
314       break;
315
316     case REQ_COMM_TESTANY:
317       act = xbt_dynar_get_as(req->comm_testany.comms, idx, smx_action_t);
318       return (act->comm.src_proc && act->comm.dst_proc);
319       break;
320
321     default:
322       return TRUE;
323   }
324 }
325
326 int MC_process_is_enabled(smx_process_t process)
327 {
328   if (process->request.call != REQ_NO_REQ && MC_request_is_enabled(&process->request))
329     return TRUE;
330
331   return FALSE;
332 }