Logo AND Algorithmique Numérique Distribuée

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