3 int MC_request_depend(smx_req_t r1, smx_req_t r2)
5 if(_surf_do_model_check == 2)
8 if (r1->issuer == r2->issuer)
11 if(r1->call == REQ_COMM_ISEND && r2->call == REQ_COMM_IRECV)
14 if(r1->call == REQ_COMM_IRECV && r2->call == REQ_COMM_ISEND)
17 if( (r1->call == REQ_COMM_ISEND || r1->call == REQ_COMM_IRECV)
18 && r2->call == REQ_COMM_WAIT){
20 if(r2->comm_wait.comm->comm.rdv == NULL)
23 smx_rdv_t rdv = r1->call == REQ_COMM_ISEND ? r1->comm_isend.rdv : r1->comm_irecv.rdv;
25 if(r2->comm_wait.comm->comm.rdv != rdv)
28 if(r2->comm_wait.comm->type == SIMIX_COMM_SEND && r1->call == REQ_COMM_ISEND)
31 if(r2->comm_wait.comm->type == SIMIX_COMM_RECEIVE && r1->call == REQ_COMM_IRECV)
35 if( (r2->call == REQ_COMM_ISEND || r2->call == REQ_COMM_IRECV)
36 && r1->call == REQ_COMM_WAIT){
38 if(r1->comm_wait.comm->comm.rdv != NULL)
41 smx_rdv_t rdv = r2->call == REQ_COMM_ISEND ? r2->comm_isend.rdv : r2->comm_irecv.rdv;
43 if(r1->comm_wait.comm->comm.rdv != rdv)
46 if(r1->comm_wait.comm->type == SIMIX_COMM_SEND && r2->call == REQ_COMM_ISEND)
49 if(r1->comm_wait.comm->type == SIMIX_COMM_RECEIVE && r2->call == REQ_COMM_IRECV)
53 /* FIXME: the following rule assumes that the result of the
54 * isend/irecv call is not stored in a buffer used in the
56 if( (r1->call == REQ_COMM_ISEND || r1->call == REQ_COMM_IRECV)
57 && r2->call == REQ_COMM_TEST)
60 /* FIXME: the following rule assumes that the result of the
61 * isend/irecv call is not stored in a buffer used in the
63 if( (r2->call == REQ_COMM_ISEND || r2->call == REQ_COMM_IRECV)
64 && r1->call == REQ_COMM_TEST)
67 if(r1->call == REQ_COMM_ISEND && r2->call == REQ_COMM_ISEND
68 && r1->comm_isend.rdv != r2->comm_isend.rdv)
71 if(r1->call == REQ_COMM_IRECV && r2->call == REQ_COMM_IRECV
72 && r1->comm_irecv.rdv != r2->comm_irecv.rdv)
75 if(r1->call == REQ_COMM_WAIT && (r2->call == REQ_COMM_WAIT || r2->call == REQ_COMM_TEST)
76 && (r1->comm_wait.comm->comm.src_proc == NULL
77 || r1->comm_wait.comm->comm.dst_proc == NULL))
80 if(r2->call == REQ_COMM_WAIT && (r1->call == REQ_COMM_WAIT || r1->call == REQ_COMM_TEST)
81 && (r2->comm_wait.comm->comm.src_proc == NULL
82 || r2->comm_wait.comm->comm.dst_proc == NULL))
85 if(r1->call == REQ_COMM_WAIT && r2->call == REQ_COMM_WAIT
86 && r1->comm_wait.comm->comm.src_buff == r2->comm_wait.comm->comm.src_buff
87 && r1->comm_wait.comm->comm.dst_buff == r2->comm_wait.comm->comm.dst_buff)
90 if (r1->call == REQ_COMM_WAIT && r2->call == REQ_COMM_WAIT
91 && r1->comm_wait.comm->comm.src_buff != NULL
92 && r1->comm_wait.comm->comm.dst_buff != NULL
93 && r2->comm_wait.comm->comm.src_buff != NULL
94 && r2->comm_wait.comm->comm.dst_buff != NULL
95 && r1->comm_wait.comm->comm.dst_buff != r2->comm_wait.comm->comm.src_buff
96 && r1->comm_wait.comm->comm.dst_buff != r2->comm_wait.comm->comm.dst_buff
97 && r2->comm_wait.comm->comm.dst_buff != r1->comm_wait.comm->comm.src_buff)
100 if(r1->call == REQ_COMM_TEST &&
101 (r1->comm_test.comm == NULL
102 || r1->comm_test.comm->comm.src_buff == NULL
103 || r1->comm_test.comm->comm.dst_buff == NULL))
106 if(r2->call == REQ_COMM_TEST &&
107 (r2->comm_test.comm == NULL
108 || r2->comm_test.comm->comm.src_buff == NULL
109 || r2->comm_test.comm->comm.dst_buff == NULL))
112 if(r1->call == REQ_COMM_TEST && r2->call == REQ_COMM_WAIT
113 && r1->comm_test.comm->comm.src_buff == r2->comm_wait.comm->comm.src_buff
114 && r1->comm_test.comm->comm.dst_buff == r2->comm_wait.comm->comm.dst_buff)
117 if(r1->call == REQ_COMM_WAIT && r2->call == REQ_COMM_TEST
118 && r1->comm_wait.comm->comm.src_buff == r2->comm_test.comm->comm.src_buff
119 && r1->comm_wait.comm->comm.dst_buff == r2->comm_test.comm->comm.dst_buff)
122 if (r1->call == REQ_COMM_WAIT && r2->call == REQ_COMM_TEST
123 && r1->comm_wait.comm->comm.src_buff != NULL
124 && r1->comm_wait.comm->comm.dst_buff != NULL
125 && r2->comm_test.comm->comm.src_buff != NULL
126 && r2->comm_test.comm->comm.dst_buff != NULL
127 && r1->comm_wait.comm->comm.dst_buff != r2->comm_test.comm->comm.src_buff
128 && r1->comm_wait.comm->comm.dst_buff != r2->comm_test.comm->comm.dst_buff
129 && r2->comm_test.comm->comm.dst_buff != r1->comm_wait.comm->comm.src_buff)
132 if (r1->call == REQ_COMM_TEST && r2->call == REQ_COMM_WAIT
133 && r1->comm_test.comm->comm.src_buff != NULL
134 && r1->comm_test.comm->comm.dst_buff != NULL
135 && r2->comm_wait.comm->comm.src_buff != NULL
136 && r2->comm_wait.comm->comm.dst_buff != NULL
137 && r1->comm_test.comm->comm.dst_buff != r2->comm_wait.comm->comm.src_buff
138 && r1->comm_test.comm->comm.dst_buff != r2->comm_wait.comm->comm.dst_buff
139 && r2->comm_wait.comm->comm.dst_buff != r1->comm_test.comm->comm.src_buff)
145 char *MC_request_to_string(smx_req_t req, int value)
147 char *type = NULL, *args = NULL, *str = NULL;
148 smx_action_t act = NULL;
153 type = bprintf("iSend");
154 args = bprintf("src=%s, buff=%p, size=%zu", req->issuer->name,
155 req->comm_isend.src_buff, req->comm_isend.src_buff_size);
158 size = req->comm_irecv.dst_buff_size ? *req->comm_irecv.dst_buff_size : 0;
159 type = bprintf("iRecv");
160 args = bprintf("dst=%s, buff=%p, size=%zu", req->issuer->name,
161 req->comm_irecv.dst_buff, size);
164 act = req->comm_wait.comm;
166 type = bprintf("WaitTimeout");
167 args = bprintf("comm=%p", act);
169 type = bprintf("Wait");
170 args = bprintf("comm=%p [(%lu)%s -> (%lu)%s]", act,
171 act->comm.src_proc ? act->comm.src_proc->pid : 0,
172 act->comm.src_proc ? act->comm.src_proc->name : "",
173 act->comm.dst_proc ? act->comm.dst_proc->pid : 0,
174 act->comm.dst_proc ? act->comm.dst_proc->name : "");
178 act = req->comm_test.comm;
179 if(act->comm.src_proc == NULL || act->comm.src_proc == NULL){
180 type = bprintf("Test FALSE");
181 args = bprintf("comm=%p", act);
183 type = bprintf("Test TRUE");
184 args = bprintf("comm=%p [(%lu)%s -> (%lu)%s]", act,
185 act->comm.src_proc ? act->comm.src_proc->pid : 0,
186 act->comm.src_proc ? act->comm.src_proc->name : "",
187 act->comm.dst_proc ? act->comm.dst_proc->pid : 0,
188 act->comm.dst_proc ? act->comm.dst_proc->name : "");
192 case REQ_COMM_WAITANY:
193 type = bprintf("WaitAny");
194 args = bprintf("comm=%p (%d of %lu)", xbt_dynar_get_as(req->comm_waitany.comms, value, smx_action_t),
195 value+1, xbt_dynar_length(req->comm_waitany.comms));
198 case REQ_COMM_TESTANY:
200 type = bprintf("TestAny FALSE");
203 type = bprintf("TestAny");
204 args = bprintf("(%d of %lu)", value+1, xbt_dynar_length(req->comm_testany.comms));
212 str = bprintf("[(%lu)%s] %s (%s)", req->issuer->pid ,req->issuer->name, type, args);
218 unsigned int MC_request_testany_fail(smx_req_t req)
223 xbt_dynar_foreach(req->comm_testany.comms, cursor, action){
224 if(action->comm.src_proc && action->comm.dst_proc)
231 int MC_request_is_visible(smx_req_t req)
233 return req->call == REQ_COMM_ISEND
234 || req->call == REQ_COMM_IRECV
235 || req->call == REQ_COMM_WAIT
236 || req->call == REQ_COMM_WAITANY
237 || req->call == REQ_COMM_TEST
238 || req->call == REQ_COMM_TESTANY;
241 int MC_request_is_enabled(smx_req_t req)
243 unsigned int index = 0;
249 /* FIXME: check also that src and dst processes are not suspended */
251 /* If it has a timeout it will be always be enabled, because even if the
252 * communication is not ready, it can timeout and won't block.
253 * On the other hand if it hasn't a timeout, check if the comm is ready.*/
254 if(req->comm_wait.timeout >= 0){
257 act = req->comm_wait.comm;
258 return (act->comm.src_proc && act->comm.dst_proc);
262 case REQ_COMM_WAITANY:
263 /* Check if it has at least one communication ready */
264 xbt_dynar_foreach(req->comm_waitany.comms, index, act) {
265 if (act->comm.src_proc && act->comm.dst_proc){
273 /* The rest of the request are always enabled */
278 int MC_request_is_enabled_by_idx(smx_req_t req, unsigned int idx)
285 /* FIXME: check also that src and dst processes are not suspended */
286 act = req->comm_wait.comm;
287 return (act->comm.src_proc && act->comm.dst_proc);
290 case REQ_COMM_WAITANY:
291 act = xbt_dynar_get_as(req->comm_waitany.comms, idx, smx_action_t);
292 return (act->comm.src_proc && act->comm.dst_proc);
295 case REQ_COMM_TESTANY:
296 act = xbt_dynar_get_as(req->comm_testany.comms, idx, smx_action_t);
297 return (act->comm.src_proc && act->comm.dst_proc);
305 int MC_process_is_enabled(smx_process_t process)
307 if (process->request.call != REQ_NO_REQ && MC_request_is_enabled(&process->request))