1 /* Copyright (c) 2008-2015. The SimGrid Team.
2 * All rights reserved. */
4 /* This program is free software; you can redistribute it and/or modify it
5 * under the terms of the license (GNU LGPL) which comes with this package. */
11 #include <xbt/sysdep.h>
12 #include <xbt/dynar.h>
14 #include "src/mc/mc_request.h"
15 #include "src/mc/mc_safety.h"
16 #include "src/mc/mc_private.h"
17 #include "src/mc/mc_smx.h"
18 #include "src/mc/mc_xbt.hpp"
20 using simgrid::mc::remote;
24 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_request, mc,
25 "Logging specific to MC (request)");
29 static char *pointer_to_string(void *pointer);
30 static char *buff_size_to_string(size_t size);
33 smx_synchro_t MC_get_comm(smx_simcall_t r)
36 case SIMCALL_COMM_WAIT:
37 return simcall_comm_wait__get__comm(r);
38 case SIMCALL_COMM_TEST:
39 return simcall_comm_test__get__comm(r);
46 smx_mailbox_t MC_get_rdv(smx_simcall_t r)
49 case SIMCALL_COMM_ISEND:
50 return simcall_comm_isend__get__rdv(r);
51 case SIMCALL_COMM_IRECV:
52 return simcall_comm_irecv__get__rdv(r);
63 bool request_depend_asymmetric(smx_simcall_t r1, smx_simcall_t r2)
65 if (r1->call == SIMCALL_COMM_ISEND && r2->call == SIMCALL_COMM_IRECV)
68 if (r1->call == SIMCALL_COMM_IRECV && r2->call == SIMCALL_COMM_ISEND)
71 // Those are internal requests, we do not need indirection
72 // because those objects are copies:
73 smx_synchro_t synchro1 = MC_get_comm(r1);
74 smx_synchro_t synchro2 = MC_get_comm(r2);
76 if ((r1->call == SIMCALL_COMM_ISEND || r1->call == SIMCALL_COMM_IRECV)
77 && r2->call == SIMCALL_COMM_WAIT) {
79 smx_mailbox_t rdv = MC_get_rdv(r1);
81 if (rdv != synchro2->comm.rdv_cpy
82 && simcall_comm_wait__get__timeout(r2) <= 0)
85 if ((r1->issuer != synchro2->comm.src_proc)
86 && (r1->issuer != synchro2->comm.dst_proc)
87 && simcall_comm_wait__get__timeout(r2) <= 0)
90 if ((r1->call == SIMCALL_COMM_ISEND)
91 && (synchro2->comm.type == SIMIX_COMM_SEND)
92 && (synchro2->comm.src_buff !=
93 simcall_comm_isend__get__src_buff(r1))
94 && simcall_comm_wait__get__timeout(r2) <= 0)
97 if ((r1->call == SIMCALL_COMM_IRECV)
98 && (synchro2->comm.type == SIMIX_COMM_RECEIVE)
99 && (synchro2->comm.dst_buff != simcall_comm_irecv__get__dst_buff(r1))
100 && simcall_comm_wait__get__timeout(r2) <= 0)
104 /* FIXME: the following rule assumes that the result of the
105 * isend/irecv call is not stored in a buffer used in the
107 /*if( (r1->call == SIMCALL_COMM_ISEND || r1->call == SIMCALL_COMM_IRECV)
108 && r2->call == SIMCALL_COMM_TEST)
111 if (r1->call == SIMCALL_COMM_WAIT
112 && (r2->call == SIMCALL_COMM_WAIT || r2->call == SIMCALL_COMM_TEST)
113 && (synchro1->comm.src_proc == nullptr || synchro1->comm.dst_proc == NULL))
116 if (r1->call == SIMCALL_COMM_TEST &&
117 (simcall_comm_test__get__comm(r1) == nullptr
118 || synchro1->comm.src_buff == nullptr
119 || synchro1->comm.dst_buff == nullptr))
122 if (r1->call == SIMCALL_COMM_TEST && r2->call == SIMCALL_COMM_WAIT
123 && synchro1->comm.src_buff == synchro2->comm.src_buff
124 && synchro1->comm.dst_buff == synchro2->comm.dst_buff)
127 if (r1->call == SIMCALL_COMM_WAIT && r2->call == SIMCALL_COMM_TEST
128 && synchro1->comm.src_buff != nullptr
129 && synchro1->comm.dst_buff != nullptr
130 && synchro2->comm.src_buff != nullptr
131 && synchro2->comm.dst_buff != nullptr
132 && synchro1->comm.dst_buff != synchro2->comm.src_buff
133 && synchro1->comm.dst_buff != synchro2->comm.dst_buff
134 && synchro2->comm.dst_buff != synchro1->comm.src_buff)
140 // Those are MC_state_get_internal_request(state)
141 bool request_depend(smx_simcall_t r1, smx_simcall_t r2)
143 if (simgrid::mc::reduction_mode == simgrid::mc::ReductionMode::none)
146 if (r1->issuer == r2->issuer)
149 /* Wait with timeout transitions are not considered by the independance theorem, thus we consider them as dependant with all other transitions */
150 if ((r1->call == SIMCALL_COMM_WAIT && simcall_comm_wait__get__timeout(r1) > 0)
151 || (r2->call == SIMCALL_COMM_WAIT
152 && simcall_comm_wait__get__timeout(r2) > 0))
155 if (r1->call != r2->call)
156 return request_depend_asymmetric(r1, r2)
157 && request_depend_asymmetric(r2, r1);
159 // Those are internal requests, we do not need indirection
160 // because those objects are copies:
161 smx_synchro_t synchro1 = MC_get_comm(r1);
162 smx_synchro_t synchro2 = MC_get_comm(r2);
165 case SIMCALL_COMM_ISEND:
166 return simcall_comm_isend__get__rdv(r1) == simcall_comm_isend__get__rdv(r2);
167 case SIMCALL_COMM_IRECV:
168 return simcall_comm_irecv__get__rdv(r1) == simcall_comm_irecv__get__rdv(r2);
169 case SIMCALL_COMM_WAIT:
170 if (synchro1->comm.src_buff == synchro2->comm.src_buff
171 && synchro1->comm.dst_buff == synchro2->comm.dst_buff)
173 else if (synchro1->comm.src_buff != nullptr
174 && synchro1->comm.dst_buff != nullptr
175 && synchro2->comm.src_buff != nullptr
176 && synchro2->comm.dst_buff != nullptr
177 && synchro1->comm.dst_buff != synchro2->comm.src_buff
178 && synchro1->comm.dst_buff != synchro2->comm.dst_buff
179 && synchro2->comm.dst_buff != synchro1->comm.src_buff)
191 static char *pointer_to_string(void *pointer)
194 if (XBT_LOG_ISENABLED(mc_request, xbt_log_priority_verbose))
195 return bprintf("%p", pointer);
197 return xbt_strdup("(verbose only)");
200 static char *buff_size_to_string(size_t buff_size)
203 if (XBT_LOG_ISENABLED(mc_request, xbt_log_priority_verbose))
204 return bprintf("%zu", buff_size);
206 return xbt_strdup("(verbose only)");
210 char *simgrid::mc::request_to_string(smx_simcall_t req, int value, simgrid::mc::RequestType request_type)
212 bool use_remote_comm = true;
213 switch(request_type) {
214 case simgrid::mc::RequestType::simix:
215 use_remote_comm = true;
217 case simgrid::mc::RequestType::executed:
218 case simgrid::mc::RequestType::internal:
219 use_remote_comm = false;
223 const char* type = nullptr;
224 char *args = nullptr;
226 smx_process_t issuer = MC_smx_simcall_get_issuer(req);
230 case SIMCALL_COMM_ISEND: {
232 char* p = pointer_to_string(simcall_comm_isend__get__src_buff(req));
233 char* bs = buff_size_to_string(simcall_comm_isend__get__src_buff_size(req));
236 bprintf("src=(%lu)%s (%s), buff=%s, size=%s", issuer->pid,
237 MC_smx_process_get_host_name(issuer),
238 MC_smx_process_get_name(issuer),
242 bprintf("src=(%lu)%s, buff=%s, size=%s", issuer->pid,
243 MC_smx_process_get_name(issuer), p, bs);
249 case SIMCALL_COMM_IRECV: {
250 size_t* remote_size = simcall_comm_irecv__get__dst_buff_size(req);
252 // size_t size = size_pointer ? *size_pointer : 0;
255 mc_model_checker->process().read_bytes(&size, sizeof(size),
256 remote(remote_size));
259 char* p = pointer_to_string(simcall_comm_irecv__get__dst_buff(req));
260 char* bs = buff_size_to_string(size);
263 bprintf("dst=(%lu)%s (%s), buff=%s, size=%s", issuer->pid,
264 MC_smx_process_get_host_name(issuer),
265 MC_smx_process_get_name(issuer),
269 bprintf("dst=(%lu)%s, buff=%s, size=%s", issuer->pid,
270 MC_smx_process_get_name(issuer),
277 case SIMCALL_COMM_WAIT: {
278 smx_synchro_t remote_act = simcall_comm_wait__get__comm(req);
281 type = "WaitTimeout";
282 p = pointer_to_string(remote_act);
283 args = bprintf("comm=%s", p);
286 p = pointer_to_string(remote_act);
288 s_smx_synchro_t synchro;
290 if (use_remote_comm) {
291 mc_model_checker->process().read_bytes(&synchro,
292 sizeof(synchro), remote(remote_act));
297 smx_process_t src_proc = MC_smx_resolve_process(act->comm.src_proc);
298 smx_process_t dst_proc = MC_smx_resolve_process(act->comm.dst_proc);
299 args = bprintf("comm=%s [(%lu)%s (%s)-> (%lu)%s (%s)]", p,
300 src_proc ? src_proc->pid : 0,
301 src_proc ? MC_smx_process_get_host_name(src_proc) : "",
302 src_proc ? MC_smx_process_get_name(src_proc) : "",
303 dst_proc ? dst_proc->pid : 0,
304 dst_proc ? MC_smx_process_get_host_name(dst_proc) : "",
305 dst_proc ? MC_smx_process_get_name(dst_proc) : "");
311 case SIMCALL_COMM_TEST: {
312 smx_synchro_t remote_act = simcall_comm_test__get__comm(req);
313 s_smx_synchro_t synchro;
315 if (use_remote_comm) {
316 mc_model_checker->process().read_bytes(&synchro,
317 sizeof(synchro), remote(remote_act));
323 if (act->comm.src_proc == nullptr || act->comm.dst_proc == NULL) {
325 p = pointer_to_string(remote_act);
326 args = bprintf("comm=%s", p);
329 p = pointer_to_string(remote_act);
331 smx_process_t src_proc = MC_smx_resolve_process(act->comm.src_proc);
332 smx_process_t dst_proc = MC_smx_resolve_process(act->comm.dst_proc);
333 args = bprintf("comm=%s [(%lu)%s (%s) -> (%lu)%s (%s)]", p,
335 MC_smx_process_get_name(src_proc),
336 MC_smx_process_get_host_name(src_proc),
338 MC_smx_process_get_name(dst_proc),
339 MC_smx_process_get_host_name(dst_proc));
345 case SIMCALL_COMM_WAITANY: {
348 mc_model_checker->process().read_bytes(
349 &comms, sizeof(comms), remote(simcall_comm_waitany__get__comms(req)));
350 if (!xbt_dynar_is_empty(&comms)) {
351 smx_synchro_t remote_sync;
352 read_element(mc_model_checker->process(),
353 &remote_sync, remote(simcall_comm_waitany__get__comms(req)), value,
354 sizeof(remote_sync));
355 char* p = pointer_to_string(remote_sync);
356 args = bprintf("comm=%s (%d of %lu)",
357 p, value + 1, xbt_dynar_length(&comms));
360 args = bprintf("comm at idx %d", value);
364 case SIMCALL_COMM_TESTANY:
366 type = "TestAny FALSE";
367 args = xbt_strdup("-");
371 bprintf("(%d of %zu)", value + 1,
372 read_length(mc_model_checker->process(),
373 simcall_comm_testany__get__comms(req)));
377 case SIMCALL_MUTEX_TRYLOCK:
378 case SIMCALL_MUTEX_LOCK: {
379 if (req->call == SIMCALL_MUTEX_LOCK)
382 type = "Mutex TRYLOCK";
385 mc_model_checker->process().read_bytes(&mutex, sizeof(mutex),
387 req->call == SIMCALL_MUTEX_LOCK
388 ? simcall_mutex_lock__get__mutex(req)
389 : simcall_mutex_trylock__get__mutex(req)
391 s_xbt_swag_t mutex_sleeping;
392 mc_model_checker->process().read_bytes(&mutex_sleeping, sizeof(mutex_sleeping),
393 remote(mutex.sleeping));
395 args = bprintf("locked = %d, owner = %d, sleeping = %d",
397 mutex.owner != nullptr ? (int) MC_smx_resolve_process(mutex.owner)->pid : -1,
398 mutex_sleeping.count);
402 case SIMCALL_MC_RANDOM:
404 args = bprintf("%d", value);
414 bprintf("[(%lu)%s (%s)] %s(%s)", issuer->pid,
415 MC_smx_process_get_host_name(issuer),
416 MC_smx_process_get_name(issuer),
420 bprintf("[(%lu)%s (%s)] %s ", issuer->pid,
421 MC_smx_process_get_host_name(issuer),
422 MC_smx_process_get_name(issuer),
431 bool request_is_enabled_by_idx(smx_simcall_t req, unsigned int idx)
433 smx_synchro_t remote_act = nullptr;
436 case SIMCALL_COMM_WAIT:
437 /* FIXME: check also that src and dst processes are not suspended */
438 remote_act = simcall_comm_wait__get__comm(req);
441 case SIMCALL_COMM_WAITANY: {
443 mc_model_checker->process(), &remote_act,
444 remote(simcall_comm_waitany__get__comms(req)),
445 idx, sizeof(remote_act));
449 case SIMCALL_COMM_TESTANY: {
451 mc_model_checker->process(), &remote_act,
452 remote(simcall_comm_testany__get__comms(req)),
453 idx, sizeof(remote_act));
461 s_smx_synchro_t synchro;
462 mc_model_checker->process().read_bytes(
463 &synchro, sizeof(synchro), remote(remote_act));
464 return synchro.comm.src_proc && synchro.comm.dst_proc;
467 bool process_is_enabled(smx_process_t process)
469 return simgrid::mc::request_is_enabled(&process->simcall);
472 char *request_get_dot_output(smx_simcall_t req, int value)
474 char *label = nullptr;
476 const smx_process_t issuer = MC_smx_simcall_get_issuer(req);
479 case SIMCALL_COMM_ISEND:
482 bprintf("[(%lu)%s] iSend", issuer->pid,
483 MC_smx_process_get_host_name(issuer));
485 label = bprintf("[(%lu)] iSend", issuer->pid);
488 case SIMCALL_COMM_IRECV:
491 bprintf("[(%lu)%s] iRecv", issuer->pid,
492 MC_smx_process_get_host_name(issuer));
494 label = bprintf("[(%lu)] iRecv", issuer->pid);
497 case SIMCALL_COMM_WAIT: {
501 bprintf("[(%lu)%s] WaitTimeout", issuer->pid,
502 MC_smx_process_get_host_name(issuer));
504 label = bprintf("[(%lu)] WaitTimeout", issuer->pid);
506 smx_synchro_t remote_act = simcall_comm_wait__get__comm(req);
507 s_smx_synchro_t synchro;
508 mc_model_checker->process().read_bytes(&synchro,
509 sizeof(synchro), remote(remote_act));
511 smx_process_t src_proc = MC_smx_resolve_process(synchro.comm.src_proc);
512 smx_process_t dst_proc = MC_smx_resolve_process(synchro.comm.dst_proc);
515 bprintf("[(%lu)%s] Wait [(%lu)->(%lu)]", issuer->pid,
516 MC_smx_process_get_host_name(issuer),
517 src_proc ? src_proc->pid : 0,
518 dst_proc ? dst_proc->pid : 0);
521 bprintf("[(%lu)] Wait [(%lu)->(%lu)]", issuer->pid,
522 src_proc ? src_proc->pid : 0,
523 dst_proc ? dst_proc->pid : 0);
528 case SIMCALL_COMM_TEST: {
529 smx_synchro_t remote_act = simcall_comm_test__get__comm(req);
530 s_smx_synchro_t synchro;
531 mc_model_checker->process().read_bytes(&synchro,
532 sizeof(synchro), remote(remote_act));
533 if (synchro.comm.src_proc == nullptr || synchro.comm.dst_proc == NULL) {
536 bprintf("[(%lu)%s] Test FALSE", issuer->pid,
537 MC_smx_process_get_host_name(issuer));
539 label = bprintf("[(%lu)] Test FALSE", issuer->pid);
543 bprintf("[(%lu)%s] Test TRUE", issuer->pid,
544 MC_smx_process_get_host_name(issuer));
546 label = bprintf("[(%lu)] Test TRUE", issuer->pid);
551 case SIMCALL_COMM_WAITANY: {
552 unsigned long comms_size = read_length(
553 mc_model_checker->process(), remote(simcall_comm_waitany__get__comms(req)));
556 bprintf("[(%lu)%s] WaitAny [%d of %lu]", issuer->pid,
557 MC_smx_process_get_host_name(issuer), value + 1,
561 bprintf("[(%lu)] WaitAny [%d of %lu]", issuer->pid, value + 1,
566 case SIMCALL_COMM_TESTANY:
570 bprintf("[(%lu)%s] TestAny FALSE", issuer->pid,
571 MC_smx_process_get_host_name(issuer));
573 label = bprintf("[(%lu)] TestAny FALSE", issuer->pid);
577 bprintf("[(%lu)%s] TestAny TRUE [%d of %lu]", issuer->pid,
578 MC_smx_process_get_host_name(issuer), value + 1,
579 xbt_dynar_length(simcall_comm_testany__get__comms(req)));
582 bprintf("[(%lu)] TestAny TRUE [%d of %lu]", issuer->pid,
584 xbt_dynar_length(simcall_comm_testany__get__comms(req)));
588 case SIMCALL_MUTEX_TRYLOCK:
589 label = bprintf("[(%lu)] Mutex TRYLOCK", issuer->pid);
592 case SIMCALL_MUTEX_LOCK:
593 label = bprintf("[(%lu)] Mutex LOCK", issuer->pid);
596 case SIMCALL_MC_RANDOM:
599 bprintf("[(%lu)%s] MC_RANDOM (%d)", issuer->pid,
600 MC_smx_process_get_host_name(issuer), value);
602 label = bprintf("[(%lu)] MC_RANDOM (%d)", issuer->pid, value);
610 bprintf("label = \"%s\", color = %s, fontcolor = %s", label,
611 colors[issuer->pid - 1], colors[issuer->pid - 1]);