Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
[mc] Move things in the MC namespace
[simgrid.git] / src / mc / mc_request.cpp
1 /* Copyright (c) 2008-2015. The SimGrid Team.
2  * All rights reserved.                                                     */
3
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. */
6
7 #include <cassert>
8
9 #include <xbt/log.h>
10 #include <xbt/str.h>
11 #include <xbt/sysdep.h>
12 #include <xbt/dynar.h>
13
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"
19
20 using simgrid::mc::remote;
21
22 extern "C" {
23
24 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_request, mc,
25                                 "Logging specific to MC (request)");
26
27 }
28
29 static char *pointer_to_string(void *pointer);
30 static char *buff_size_to_string(size_t size);
31
32 static inline
33 smx_synchro_t MC_get_comm(smx_simcall_t r)
34 {
35   switch (r->call ) {
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);
40   default:
41     return nullptr;
42   }
43 }
44
45 static inline
46 smx_mailbox_t MC_get_rdv(smx_simcall_t r)
47 {
48   switch(r->call) {
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);
53   default:
54     return nullptr;
55   }
56 }
57
58 namespace simgrid {
59 namespace mc {
60
61 // Does half the job
62 static inline
63 bool request_depend_asymmetric(smx_simcall_t r1, smx_simcall_t r2)
64 {
65   if (r1->call == SIMCALL_COMM_ISEND && r2->call == SIMCALL_COMM_IRECV)
66     return false;
67
68   if (r1->call == SIMCALL_COMM_IRECV && r2->call == SIMCALL_COMM_ISEND)
69     return false;
70
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);
75
76   if ((r1->call == SIMCALL_COMM_ISEND || r1->call == SIMCALL_COMM_IRECV)
77       && r2->call == SIMCALL_COMM_WAIT) {
78
79     smx_mailbox_t rdv = MC_get_rdv(r1);
80
81     if (rdv != synchro2->comm.rdv_cpy
82         && simcall_comm_wait__get__timeout(r2) <= 0)
83       return false;
84
85     if ((r1->issuer != synchro2->comm.src_proc)
86         && (r1->issuer != synchro2->comm.dst_proc)
87         && simcall_comm_wait__get__timeout(r2) <= 0)
88       return false;
89
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)
95       return false;
96
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)
101       return false;
102   }
103
104   /* FIXME: the following rule assumes that the result of the
105    * isend/irecv call is not stored in a buffer used in the
106    * test call. */
107   /*if(   (r1->call == SIMCALL_COMM_ISEND || r1->call == SIMCALL_COMM_IRECV)
108      &&  r2->call == SIMCALL_COMM_TEST)
109      return FALSE; */
110
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))
114     return false;
115
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))
120     return false;
121
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)
125     return false;
126
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)
135     return false;
136
137   return true;
138 }
139
140 // Those are MC_state_get_internal_request(state)
141 bool request_depend(smx_simcall_t r1, smx_simcall_t r2)
142 {
143   if (mc_reduce_kind == e_mc_reduce_none)
144     return true;
145
146   if (r1->issuer == r2->issuer)
147     return false;
148
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))
153     return TRUE;
154
155   if (r1->call != r2->call)
156     return request_depend_asymmetric(r1, r2)
157       && request_depend_asymmetric(r2, r1);
158
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);
163
164   switch(r1->call) {
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)
172       return false;
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)
180       return false;
181     else
182       return true;
183   default:
184     return true;
185   }
186 }
187
188 }
189 }
190
191 static char *pointer_to_string(void *pointer)
192 {
193
194   if (XBT_LOG_ISENABLED(mc_request, xbt_log_priority_verbose))
195     return bprintf("%p", pointer);
196
197   return xbt_strdup("(verbose only)");
198 }
199
200 static char *buff_size_to_string(size_t buff_size)
201 {
202
203   if (XBT_LOG_ISENABLED(mc_request, xbt_log_priority_verbose))
204     return bprintf("%zu", buff_size);
205
206   return xbt_strdup("(verbose only)");
207 }
208
209
210 char *simgrid::mc::request_to_string(smx_simcall_t req, int value, simgrid::mc::RequestType request_type)
211 {
212   bool use_remote_comm = true;
213   switch(request_type) {
214   case simgrid::mc::RequestType::simix:
215     use_remote_comm = true;
216     break;
217   case simgrid::mc::RequestType::executed:
218   case simgrid::mc::RequestType::internal:
219     use_remote_comm = false;
220     break;
221   }
222
223   const char* type = nullptr;
224   char *args = nullptr;
225
226   smx_process_t issuer = MC_smx_simcall_get_issuer(req);
227
228   switch (req->call) {
229
230   case SIMCALL_COMM_ISEND: {
231     type = "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));
234     if (issuer->host)
235       args =
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),
239                   p, bs);
240     else
241       args =
242           bprintf("src=(%lu)%s, buff=%s, size=%s", issuer->pid,
243                   MC_smx_process_get_name(issuer), p, bs);
244     xbt_free(bs);
245     xbt_free(p);
246     break;
247   }
248
249   case SIMCALL_COMM_IRECV: {
250     size_t* remote_size = simcall_comm_irecv__get__dst_buff_size(req);
251
252     // size_t size = size_pointer ? *size_pointer : 0;
253     size_t size = 0;
254     if (remote_size)
255       mc_model_checker->process().read_bytes(&size, sizeof(size),
256         remote(remote_size));
257
258     type = "iRecv";
259     char* p = pointer_to_string(simcall_comm_irecv__get__dst_buff(req));
260     char* bs = buff_size_to_string(size);
261     if (issuer->host)
262       args =
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),
266                   p, bs);
267     else
268       args =
269           bprintf("dst=(%lu)%s, buff=%s, size=%s", issuer->pid,
270                   MC_smx_process_get_name(issuer),
271                   p, bs);
272     xbt_free(bs);
273     xbt_free(p);
274     break;
275   }
276
277   case SIMCALL_COMM_WAIT: {
278     smx_synchro_t remote_act = simcall_comm_wait__get__comm(req);
279     char* p;
280     if (value == -1) {
281       type = "WaitTimeout";
282       p = pointer_to_string(remote_act);
283       args = bprintf("comm=%s", p);
284     } else {
285       type = "Wait";
286       p = pointer_to_string(remote_act);
287
288       s_smx_synchro_t synchro;
289       smx_synchro_t act;
290       if (use_remote_comm) {
291         mc_model_checker->process().read_bytes(&synchro,
292           sizeof(synchro), remote(remote_act));
293         act = &synchro;
294       } else
295         act = remote_act;
296
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) : "");
306     }
307     xbt_free(p);
308     break;
309   }
310
311   case SIMCALL_COMM_TEST: {
312     smx_synchro_t remote_act = simcall_comm_test__get__comm(req);
313     s_smx_synchro_t synchro;
314       smx_synchro_t act;
315       if (use_remote_comm) {
316         mc_model_checker->process().read_bytes(&synchro,
317           sizeof(synchro), remote(remote_act));
318         act = &synchro;
319       } else
320         act = remote_act;
321
322     char* p;
323     if (act->comm.src_proc == nullptr || act->comm.dst_proc == NULL) {
324       type = "Test FALSE";
325       p = pointer_to_string(remote_act);
326       args = bprintf("comm=%s", p);
327     } else {
328       type = "Test TRUE";
329       p = pointer_to_string(remote_act);
330
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,
334                      src_proc->pid,
335                      MC_smx_process_get_name(src_proc),
336                      MC_smx_process_get_host_name(src_proc),
337                      dst_proc->pid,
338                      MC_smx_process_get_name(dst_proc),
339                      MC_smx_process_get_host_name(dst_proc));
340     }
341     xbt_free(p);
342     break;
343   }
344
345   case SIMCALL_COMM_WAITANY: {
346     type = "WaitAny";
347     s_xbt_dynar_t comms;
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));
358       xbt_free(p);
359     } else
360       args = bprintf("comm at idx %d", value);
361     break;
362   }
363
364   case SIMCALL_COMM_TESTANY:
365     if (value == -1) {
366       type = "TestAny FALSE";
367       args = xbt_strdup("-");
368     } else {
369       type = "TestAny";
370       args =
371           bprintf("(%d of %zu)", value + 1,
372                   read_length(mc_model_checker->process(),
373                     simcall_comm_testany__get__comms(req)));
374     }
375     break;
376
377   case SIMCALL_MUTEX_TRYLOCK:
378   case SIMCALL_MUTEX_LOCK: {
379     if (req->call == SIMCALL_MUTEX_LOCK)
380       type = "Mutex LOCK";
381     else
382       type = "Mutex TRYLOCK";
383
384     s_smx_mutex_t mutex;
385     mc_model_checker->process().read_bytes(&mutex, sizeof(mutex),
386       remote(
387         req->call == SIMCALL_MUTEX_LOCK
388         ? simcall_mutex_lock__get__mutex(req)
389         : simcall_mutex_trylock__get__mutex(req)
390       ));
391     s_xbt_swag_t mutex_sleeping;
392     mc_model_checker->process().read_bytes(&mutex_sleeping, sizeof(mutex_sleeping),
393       remote(mutex.sleeping));
394
395     args = bprintf("locked = %d, owner = %d, sleeping = %d",
396       mutex.locked,
397       mutex.owner != nullptr ? (int) MC_smx_resolve_process(mutex.owner)->pid : -1,
398       mutex_sleeping.count);
399     break;
400   }
401
402   case SIMCALL_MC_SNAPSHOT:
403     type = "MC_SNAPSHOT";
404     args = nullptr;
405     break;
406
407   case SIMCALL_MC_COMPARE_SNAPSHOTS:
408     type = "MC_COMPARE_SNAPSHOTS";
409     args = nullptr;
410     break;
411
412   case SIMCALL_MC_RANDOM:
413     type = "MC_RANDOM";
414     args = bprintf("%d", value);
415     break;
416
417   default:
418     THROW_UNIMPLEMENTED;
419   }
420
421   char* str;
422   if (args != nullptr)
423     str =
424         bprintf("[(%lu)%s (%s)] %s(%s)", issuer->pid,
425                 MC_smx_process_get_host_name(issuer),
426                 MC_smx_process_get_name(issuer),
427                 type, args);
428   else
429     str =
430         bprintf("[(%lu)%s (%s)] %s ", issuer->pid,
431                 MC_smx_process_get_host_name(issuer),
432                 MC_smx_process_get_name(issuer),
433                 type);
434   xbt_free(args);
435   return str;
436 }
437
438 namespace simgrid {
439 namespace mc {
440
441 bool request_is_enabled_by_idx(smx_simcall_t req, unsigned int idx)
442 {
443   smx_synchro_t remote_act = nullptr;
444   switch (req->call) {
445
446   case SIMCALL_COMM_WAIT:
447     /* FIXME: check also that src and dst processes are not suspended */
448     remote_act = simcall_comm_wait__get__comm(req);
449     break;
450
451   case SIMCALL_COMM_WAITANY: {
452     read_element(
453       mc_model_checker->process(), &remote_act,
454       remote(simcall_comm_waitany__get__comms(req)),
455       idx, sizeof(remote_act));
456     }
457     break;
458
459   case SIMCALL_COMM_TESTANY: {
460     read_element(
461       mc_model_checker->process(), &remote_act,
462       remote(simcall_comm_testany__get__comms(req)),
463       idx, sizeof(remote_act));
464     }
465     break;
466
467   default:
468     return true;
469   }
470
471   s_smx_synchro_t synchro;
472   mc_model_checker->process().read_bytes(
473     &synchro, sizeof(synchro), remote(remote_act));
474   return synchro.comm.src_proc && synchro.comm.dst_proc;
475 }
476
477 bool process_is_enabled(smx_process_t process)
478 {
479   return simgrid::mc::request_is_enabled(&process->simcall);
480 }
481
482 char *request_get_dot_output(smx_simcall_t req, int value)
483 {
484   char *label = nullptr;
485
486   const smx_process_t issuer = MC_smx_simcall_get_issuer(req);
487
488   switch (req->call) {
489   case SIMCALL_COMM_ISEND:
490     if (issuer->host)
491       label =
492           bprintf("[(%lu)%s] iSend", issuer->pid,
493                   MC_smx_process_get_host_name(issuer));
494     else
495       label = bprintf("[(%lu)] iSend", issuer->pid);
496     break;
497
498   case SIMCALL_COMM_IRECV:
499     if (issuer->host)
500       label =
501           bprintf("[(%lu)%s] iRecv", issuer->pid,
502                   MC_smx_process_get_host_name(issuer));
503     else
504       label = bprintf("[(%lu)] iRecv", issuer->pid);
505     break;
506
507   case SIMCALL_COMM_WAIT: {
508     if (value == -1) {
509       if (issuer->host)
510         label =
511             bprintf("[(%lu)%s] WaitTimeout", issuer->pid,
512                     MC_smx_process_get_host_name(issuer));
513       else
514         label = bprintf("[(%lu)] WaitTimeout", issuer->pid);
515     } else {
516       smx_synchro_t remote_act = simcall_comm_wait__get__comm(req);
517       s_smx_synchro_t synchro;
518       mc_model_checker->process().read_bytes(&synchro,
519         sizeof(synchro), remote(remote_act));
520
521       smx_process_t src_proc = MC_smx_resolve_process(synchro.comm.src_proc);
522       smx_process_t dst_proc = MC_smx_resolve_process(synchro.comm.dst_proc);
523       if (issuer->host)
524         label =
525             bprintf("[(%lu)%s] Wait [(%lu)->(%lu)]", issuer->pid,
526                     MC_smx_process_get_host_name(issuer),
527                     src_proc ? src_proc->pid : 0,
528                     dst_proc ? dst_proc->pid : 0);
529       else
530         label =
531             bprintf("[(%lu)] Wait [(%lu)->(%lu)]", issuer->pid,
532                     src_proc ? src_proc->pid : 0,
533                     dst_proc ? dst_proc->pid : 0);
534     }
535     break;
536   }
537
538   case SIMCALL_COMM_TEST: {
539     smx_synchro_t remote_act = simcall_comm_test__get__comm(req);
540     s_smx_synchro_t synchro;
541     mc_model_checker->process().read_bytes(&synchro,
542       sizeof(synchro), remote(remote_act));
543     if (synchro.comm.src_proc == nullptr || synchro.comm.dst_proc == NULL) {
544       if (issuer->host)
545         label =
546             bprintf("[(%lu)%s] Test FALSE", issuer->pid,
547                     MC_smx_process_get_host_name(issuer));
548       else
549         label = bprintf("[(%lu)] Test FALSE", issuer->pid);
550     } else {
551       if (issuer->host)
552         label =
553             bprintf("[(%lu)%s] Test TRUE", issuer->pid,
554                     MC_smx_process_get_host_name(issuer));
555       else
556         label = bprintf("[(%lu)] Test TRUE", issuer->pid);
557     }
558     break;
559   }
560
561   case SIMCALL_COMM_WAITANY: {
562     unsigned long comms_size = read_length(
563       mc_model_checker->process(), remote(simcall_comm_waitany__get__comms(req)));
564     if (issuer->host)
565       label =
566           bprintf("[(%lu)%s] WaitAny [%d of %lu]", issuer->pid,
567                   MC_smx_process_get_host_name(issuer), value + 1,
568                   comms_size);
569     else
570       label =
571           bprintf("[(%lu)] WaitAny [%d of %lu]", issuer->pid, value + 1,
572                   comms_size);
573     break;
574   }
575
576   case SIMCALL_COMM_TESTANY:
577     if (value == -1) {
578       if (issuer->host)
579         label =
580             bprintf("[(%lu)%s] TestAny FALSE", issuer->pid,
581                     MC_smx_process_get_host_name(issuer));
582       else
583         label = bprintf("[(%lu)] TestAny FALSE", issuer->pid);
584     } else {
585       if (issuer->host)
586         label =
587             bprintf("[(%lu)%s] TestAny TRUE [%d of %lu]", issuer->pid,
588                     MC_smx_process_get_host_name(issuer), value + 1,
589                     xbt_dynar_length(simcall_comm_testany__get__comms(req)));
590       else
591         label =
592             bprintf("[(%lu)] TestAny TRUE [%d of %lu]", issuer->pid,
593                     value + 1,
594                     xbt_dynar_length(simcall_comm_testany__get__comms(req)));
595     }
596     break;
597
598   case SIMCALL_MUTEX_TRYLOCK:
599     label = bprintf("[(%lu)] Mutex TRYLOCK", issuer->pid);
600     break;
601
602   case SIMCALL_MUTEX_LOCK:
603     label = bprintf("[(%lu)] Mutex LOCK", issuer->pid);
604     break;
605
606   case SIMCALL_MC_RANDOM:
607     if (issuer->host)
608       label =
609           bprintf("[(%lu)%s] MC_RANDOM (%d)", issuer->pid,
610                   MC_smx_process_get_host_name(issuer), value);
611     else
612       label = bprintf("[(%lu)] MC_RANDOM (%d)", issuer->pid, value);
613     break;
614
615   case SIMCALL_MC_SNAPSHOT:
616     if (issuer->host)
617       label =
618           bprintf("[(%lu)%s] MC_SNAPSHOT", issuer->pid,
619                   MC_smx_process_get_host_name(issuer));
620     else
621       label = bprintf("[(%lu)] MC_SNAPSHOT", issuer->pid);
622     break;
623
624   case SIMCALL_MC_COMPARE_SNAPSHOTS:
625     if (issuer->host)
626       label =
627           bprintf("[(%lu)%s] MC_COMPARE_SNAPSHOTS", issuer->pid,
628                   MC_smx_process_get_host_name(issuer));
629     else
630       label = bprintf("[(%lu)] MC_COMPARE_SNAPSHOTS", issuer->pid);
631     break;
632
633   default:
634     THROW_UNIMPLEMENTED;
635   }
636
637   char* str =
638       bprintf("label = \"%s\", color = %s, fontcolor = %s", label,
639               colors[issuer->pid - 1], colors[issuer->pid - 1]);
640   xbt_free(label);
641   return str;
642
643 }
644
645 }
646 }