Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
[mc] Fix #includes
[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 #include <xbt/swag.h>
14
15 #include "src/mc/mc_request.h"
16 #include "src/mc/mc_safety.h"
17 #include "src/mc/mc_private.h"
18 #include "src/mc/mc_smx.h"
19 #include "src/mc/mc_xbt.hpp"
20
21 using simgrid::mc::remote;
22
23 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_request, mc,
24                                 "Logging specific to MC (request)");
25
26 static char *pointer_to_string(void *pointer);
27 static char *buff_size_to_string(size_t size);
28
29 static inline
30 smx_synchro_t MC_get_comm(smx_simcall_t r)
31 {
32   switch (r->call ) {
33   case SIMCALL_COMM_WAIT:
34     return simcall_comm_wait__get__comm(r);
35   case SIMCALL_COMM_TEST:
36     return simcall_comm_test__get__comm(r);
37   default:
38     return nullptr;
39   }
40 }
41
42 static inline
43 smx_mailbox_t MC_get_rdv(smx_simcall_t r)
44 {
45   switch(r->call) {
46   case SIMCALL_COMM_ISEND:
47     return simcall_comm_isend__get__rdv(r);
48   case SIMCALL_COMM_IRECV:
49     return simcall_comm_irecv__get__rdv(r);
50   default:
51     return nullptr;
52   }
53 }
54
55 namespace simgrid {
56 namespace mc {
57
58 // Does half the job
59 static inline
60 bool request_depend_asymmetric(smx_simcall_t r1, smx_simcall_t r2)
61 {
62   if (r1->call == SIMCALL_COMM_ISEND && r2->call == SIMCALL_COMM_IRECV)
63     return false;
64
65   if (r1->call == SIMCALL_COMM_IRECV && r2->call == SIMCALL_COMM_ISEND)
66     return false;
67
68   // Those are internal requests, we do not need indirection
69   // because those objects are copies:
70   smx_synchro_t synchro1 = MC_get_comm(r1);
71   smx_synchro_t synchro2 = MC_get_comm(r2);
72
73   if ((r1->call == SIMCALL_COMM_ISEND || r1->call == SIMCALL_COMM_IRECV)
74       && r2->call == SIMCALL_COMM_WAIT) {
75
76     smx_mailbox_t rdv = MC_get_rdv(r1);
77
78     if (rdv != synchro2->comm.rdv_cpy
79         && simcall_comm_wait__get__timeout(r2) <= 0)
80       return false;
81
82     if ((r1->issuer != synchro2->comm.src_proc)
83         && (r1->issuer != synchro2->comm.dst_proc)
84         && simcall_comm_wait__get__timeout(r2) <= 0)
85       return false;
86
87     if ((r1->call == SIMCALL_COMM_ISEND)
88         && (synchro2->comm.type == SIMIX_COMM_SEND)
89         && (synchro2->comm.src_buff !=
90             simcall_comm_isend__get__src_buff(r1))
91         && simcall_comm_wait__get__timeout(r2) <= 0)
92       return false;
93
94     if ((r1->call == SIMCALL_COMM_IRECV)
95         && (synchro2->comm.type == SIMIX_COMM_RECEIVE)
96         && (synchro2->comm.dst_buff != simcall_comm_irecv__get__dst_buff(r1))
97         && simcall_comm_wait__get__timeout(r2) <= 0)
98       return false;
99   }
100
101   /* FIXME: the following rule assumes that the result of the
102    * isend/irecv call is not stored in a buffer used in the
103    * test call. */
104   /*if(   (r1->call == SIMCALL_COMM_ISEND || r1->call == SIMCALL_COMM_IRECV)
105      &&  r2->call == SIMCALL_COMM_TEST)
106      return FALSE; */
107
108   if (r1->call == SIMCALL_COMM_WAIT
109       && (r2->call == SIMCALL_COMM_WAIT || r2->call == SIMCALL_COMM_TEST)
110       && (synchro1->comm.src_proc == nullptr || synchro1->comm.dst_proc == NULL))
111     return false;
112
113   if (r1->call == SIMCALL_COMM_TEST &&
114       (simcall_comm_test__get__comm(r1) == nullptr
115        || synchro1->comm.src_buff == nullptr
116        || synchro1->comm.dst_buff == nullptr))
117     return false;
118
119   if (r1->call == SIMCALL_COMM_TEST && r2->call == SIMCALL_COMM_WAIT
120       && synchro1->comm.src_buff == synchro2->comm.src_buff
121       && synchro1->comm.dst_buff == synchro2->comm.dst_buff)
122     return false;
123
124   if (r1->call == SIMCALL_COMM_WAIT && r2->call == SIMCALL_COMM_TEST
125       && synchro1->comm.src_buff != nullptr
126       && synchro1->comm.dst_buff != nullptr
127       && synchro2->comm.src_buff != nullptr
128       && synchro2->comm.dst_buff != nullptr
129       && synchro1->comm.dst_buff != synchro2->comm.src_buff
130       && synchro1->comm.dst_buff != synchro2->comm.dst_buff
131       && synchro2->comm.dst_buff != synchro1->comm.src_buff)
132     return false;
133
134   return true;
135 }
136
137 // Those are MC_state_get_internal_request(state)
138 bool request_depend(smx_simcall_t r1, smx_simcall_t r2)
139 {
140   if (r1->issuer == r2->issuer)
141     return false;
142
143   /* Wait with timeout transitions are not considered by the independance theorem, thus we consider them as dependant with all other transitions */
144   if ((r1->call == SIMCALL_COMM_WAIT && simcall_comm_wait__get__timeout(r1) > 0)
145       || (r2->call == SIMCALL_COMM_WAIT
146           && simcall_comm_wait__get__timeout(r2) > 0))
147     return TRUE;
148
149   if (r1->call != r2->call)
150     return request_depend_asymmetric(r1, r2)
151       && request_depend_asymmetric(r2, r1);
152
153   // Those are internal requests, we do not need indirection
154   // because those objects are copies:
155   smx_synchro_t synchro1 = MC_get_comm(r1);
156   smx_synchro_t synchro2 = MC_get_comm(r2);
157
158   switch(r1->call) {
159   case SIMCALL_COMM_ISEND:
160     return simcall_comm_isend__get__rdv(r1) == simcall_comm_isend__get__rdv(r2);
161   case SIMCALL_COMM_IRECV:
162     return simcall_comm_irecv__get__rdv(r1) == simcall_comm_irecv__get__rdv(r2);
163   case SIMCALL_COMM_WAIT:
164     if (synchro1->comm.src_buff == synchro2->comm.src_buff
165         && synchro1->comm.dst_buff == synchro2->comm.dst_buff)
166       return false;
167     else if (synchro1->comm.src_buff != nullptr
168         && synchro1->comm.dst_buff != nullptr
169         && synchro2->comm.src_buff != nullptr
170         && synchro2->comm.dst_buff != nullptr
171         && synchro1->comm.dst_buff != synchro2->comm.src_buff
172         && synchro1->comm.dst_buff != synchro2->comm.dst_buff
173         && synchro2->comm.dst_buff != synchro1->comm.src_buff)
174       return false;
175     else
176       return true;
177   default:
178     return true;
179   }
180 }
181
182 }
183 }
184
185 static char *pointer_to_string(void *pointer)
186 {
187
188   if (XBT_LOG_ISENABLED(mc_request, xbt_log_priority_verbose))
189     return bprintf("%p", pointer);
190
191   return xbt_strdup("(verbose only)");
192 }
193
194 static char *buff_size_to_string(size_t buff_size)
195 {
196
197   if (XBT_LOG_ISENABLED(mc_request, xbt_log_priority_verbose))
198     return bprintf("%zu", buff_size);
199
200   return xbt_strdup("(verbose only)");
201 }
202
203
204 std::string simgrid::mc::request_to_string(smx_simcall_t req, int value, simgrid::mc::RequestType request_type)
205 {
206   bool use_remote_comm = true;
207   switch(request_type) {
208   case simgrid::mc::RequestType::simix:
209     use_remote_comm = true;
210     break;
211   case simgrid::mc::RequestType::executed:
212   case simgrid::mc::RequestType::internal:
213     use_remote_comm = false;
214     break;
215   }
216
217   const char* type = nullptr;
218   char *args = nullptr;
219
220   smx_process_t issuer = MC_smx_simcall_get_issuer(req);
221
222   switch (req->call) {
223
224   case SIMCALL_COMM_ISEND: {
225     type = "iSend";
226     char* p = pointer_to_string(simcall_comm_isend__get__src_buff(req));
227     char* bs = buff_size_to_string(simcall_comm_isend__get__src_buff_size(req));
228     if (issuer->host)
229       args =
230           bprintf("src=(%lu)%s (%s), buff=%s, size=%s", issuer->pid,
231                   MC_smx_process_get_host_name(issuer),
232                   MC_smx_process_get_name(issuer),
233                   p, bs);
234     else
235       args =
236           bprintf("src=(%lu)%s, buff=%s, size=%s", issuer->pid,
237                   MC_smx_process_get_name(issuer), p, bs);
238     xbt_free(bs);
239     xbt_free(p);
240     break;
241   }
242
243   case SIMCALL_COMM_IRECV: {
244     size_t* remote_size = simcall_comm_irecv__get__dst_buff_size(req);
245
246     // size_t size = size_pointer ? *size_pointer : 0;
247     size_t size = 0;
248     if (remote_size)
249       mc_model_checker->process().read_bytes(&size, sizeof(size),
250         remote(remote_size));
251
252     type = "iRecv";
253     char* p = pointer_to_string(simcall_comm_irecv__get__dst_buff(req));
254     char* bs = buff_size_to_string(size);
255     if (issuer->host)
256       args =
257           bprintf("dst=(%lu)%s (%s), buff=%s, size=%s", issuer->pid,
258                   MC_smx_process_get_host_name(issuer),
259                   MC_smx_process_get_name(issuer),
260                   p, bs);
261     else
262       args =
263           bprintf("dst=(%lu)%s, buff=%s, size=%s", issuer->pid,
264                   MC_smx_process_get_name(issuer),
265                   p, bs);
266     xbt_free(bs);
267     xbt_free(p);
268     break;
269   }
270
271   case SIMCALL_COMM_WAIT: {
272     smx_synchro_t remote_act = simcall_comm_wait__get__comm(req);
273     char* p;
274     if (value == -1) {
275       type = "WaitTimeout";
276       p = pointer_to_string(remote_act);
277       args = bprintf("comm=%s", p);
278     } else {
279       type = "Wait";
280       p = pointer_to_string(remote_act);
281
282       s_smx_synchro_t synchro;
283       smx_synchro_t act;
284       if (use_remote_comm) {
285         mc_model_checker->process().read_bytes(&synchro,
286           sizeof(synchro), remote(remote_act));
287         act = &synchro;
288       } else
289         act = remote_act;
290
291       smx_process_t src_proc = MC_smx_resolve_process(act->comm.src_proc);
292       smx_process_t dst_proc = MC_smx_resolve_process(act->comm.dst_proc);
293       args = bprintf("comm=%s [(%lu)%s (%s)-> (%lu)%s (%s)]", p,
294                      src_proc ? src_proc->pid : 0,
295                      src_proc ? MC_smx_process_get_host_name(src_proc) : "",
296                      src_proc ? MC_smx_process_get_name(src_proc) : "",
297                      dst_proc ? dst_proc->pid : 0,
298                      dst_proc ? MC_smx_process_get_host_name(dst_proc) : "",
299                      dst_proc ? MC_smx_process_get_name(dst_proc) : "");
300     }
301     xbt_free(p);
302     break;
303   }
304
305   case SIMCALL_COMM_TEST: {
306     smx_synchro_t remote_act = simcall_comm_test__get__comm(req);
307     s_smx_synchro_t synchro;
308       smx_synchro_t act;
309       if (use_remote_comm) {
310         mc_model_checker->process().read_bytes(&synchro,
311           sizeof(synchro), remote(remote_act));
312         act = &synchro;
313       } else
314         act = remote_act;
315
316     char* p;
317     if (act->comm.src_proc == nullptr || act->comm.dst_proc == NULL) {
318       type = "Test FALSE";
319       p = pointer_to_string(remote_act);
320       args = bprintf("comm=%s", p);
321     } else {
322       type = "Test TRUE";
323       p = pointer_to_string(remote_act);
324
325       smx_process_t src_proc = MC_smx_resolve_process(act->comm.src_proc);
326       smx_process_t dst_proc = MC_smx_resolve_process(act->comm.dst_proc);
327       args = bprintf("comm=%s [(%lu)%s (%s) -> (%lu)%s (%s)]", p,
328                      src_proc->pid,
329                      MC_smx_process_get_name(src_proc),
330                      MC_smx_process_get_host_name(src_proc),
331                      dst_proc->pid,
332                      MC_smx_process_get_name(dst_proc),
333                      MC_smx_process_get_host_name(dst_proc));
334     }
335     xbt_free(p);
336     break;
337   }
338
339   case SIMCALL_COMM_WAITANY: {
340     type = "WaitAny";
341     s_xbt_dynar_t comms;
342     mc_model_checker->process().read_bytes(
343       &comms, sizeof(comms), remote(simcall_comm_waitany__get__comms(req)));
344     if (!xbt_dynar_is_empty(&comms)) {
345       smx_synchro_t remote_sync;
346       read_element(mc_model_checker->process(),
347         &remote_sync, remote(simcall_comm_waitany__get__comms(req)), value,
348         sizeof(remote_sync));
349       char* p = pointer_to_string(remote_sync);
350       args = bprintf("comm=%s (%d of %lu)",
351         p, value + 1, xbt_dynar_length(&comms));
352       xbt_free(p);
353     } else
354       args = bprintf("comm at idx %d", value);
355     break;
356   }
357
358   case SIMCALL_COMM_TESTANY:
359     if (value == -1) {
360       type = "TestAny FALSE";
361       args = xbt_strdup("-");
362     } else {
363       type = "TestAny";
364       args =
365           bprintf("(%d of %zu)", value + 1,
366                   read_length(mc_model_checker->process(),
367                     simcall_comm_testany__get__comms(req)));
368     }
369     break;
370
371   case SIMCALL_MUTEX_TRYLOCK:
372   case SIMCALL_MUTEX_LOCK: {
373     if (req->call == SIMCALL_MUTEX_LOCK)
374       type = "Mutex LOCK";
375     else
376       type = "Mutex TRYLOCK";
377
378     s_smx_mutex_t mutex;
379     mc_model_checker->process().read_bytes(&mutex, sizeof(mutex),
380       remote(
381         req->call == SIMCALL_MUTEX_LOCK
382         ? simcall_mutex_lock__get__mutex(req)
383         : simcall_mutex_trylock__get__mutex(req)
384       ));
385     s_xbt_swag_t mutex_sleeping;
386     mc_model_checker->process().read_bytes(&mutex_sleeping, sizeof(mutex_sleeping),
387       remote(mutex.sleeping));
388
389     args = bprintf("locked = %d, owner = %d, sleeping = %d",
390       mutex.locked,
391       mutex.owner != nullptr ? (int) MC_smx_resolve_process(mutex.owner)->pid : -1,
392       mutex_sleeping.count);
393     break;
394   }
395
396   case SIMCALL_MC_RANDOM:
397     type = "MC_RANDOM";
398     args = bprintf("%d", value);
399     break;
400
401   default:
402     THROW_UNIMPLEMENTED;
403   }
404
405   std::string str;
406   if (args != nullptr)
407     str = simgrid::xbt::string_printf("[(%lu)%s (%s)] %s(%s)", issuer->pid,
408                 MC_smx_process_get_host_name(issuer),
409                 MC_smx_process_get_name(issuer),
410                 type, args);
411   else
412     str = simgrid::xbt::string_printf("[(%lu)%s (%s)] %s ", issuer->pid,
413                 MC_smx_process_get_host_name(issuer),
414                 MC_smx_process_get_name(issuer),
415                 type);
416   xbt_free(args);
417   return str;
418 }
419
420 namespace simgrid {
421 namespace mc {
422
423 bool request_is_enabled_by_idx(smx_simcall_t req, unsigned int idx)
424 {
425   smx_synchro_t remote_act = nullptr;
426   switch (req->call) {
427
428   case SIMCALL_COMM_WAIT:
429     /* FIXME: check also that src and dst processes are not suspended */
430     remote_act = simcall_comm_wait__get__comm(req);
431     break;
432
433   case SIMCALL_COMM_WAITANY: {
434     read_element(
435       mc_model_checker->process(), &remote_act,
436       remote(simcall_comm_waitany__get__comms(req)),
437       idx, sizeof(remote_act));
438     }
439     break;
440
441   case SIMCALL_COMM_TESTANY: {
442     read_element(
443       mc_model_checker->process(), &remote_act,
444       remote(simcall_comm_testany__get__comms(req)),
445       idx, sizeof(remote_act));
446     }
447     break;
448
449   default:
450     return true;
451   }
452
453   s_smx_synchro_t synchro;
454   mc_model_checker->process().read_bytes(
455     &synchro, sizeof(synchro), remote(remote_act));
456   return synchro.comm.src_proc && synchro.comm.dst_proc;
457 }
458
459 bool process_is_enabled(smx_process_t process)
460 {
461   return simgrid::mc::request_is_enabled(&process->simcall);
462 }
463
464 static const char* colors[] = {
465   "blue",
466   "red",
467   "green3",
468   "goldenrod",
469   "brown",
470   "purple",
471   "magenta",
472   "turquoise4",
473   "gray25",
474   "forestgreen",
475   "hotpink",
476   "lightblue",
477   "tan",
478 };
479
480 static inline const char* get_color(int id)
481 {
482   return colors[id % (sizeof(colors) / sizeof(colors[0])) ];
483 }
484
485 std::string request_get_dot_output(smx_simcall_t req, int value)
486 {
487   std::string label;
488
489   const smx_process_t issuer = MC_smx_simcall_get_issuer(req);
490
491   switch (req->call) {
492   case SIMCALL_COMM_ISEND:
493     if (issuer->host)
494       label = simgrid::xbt::string_printf("[(%lu)%s] iSend", issuer->pid,
495                   MC_smx_process_get_host_name(issuer));
496     else
497       label = bprintf("[(%lu)] iSend", issuer->pid);
498     break;
499
500   case SIMCALL_COMM_IRECV:
501     if (issuer->host)
502       label = simgrid::xbt::string_printf("[(%lu)%s] iRecv", issuer->pid,
503                   MC_smx_process_get_host_name(issuer));
504     else
505       label = simgrid::xbt::string_printf("[(%lu)] iRecv", issuer->pid);
506     break;
507
508   case SIMCALL_COMM_WAIT: {
509     if (value == -1) {
510       if (issuer->host)
511         label = simgrid::xbt::string_printf("[(%lu)%s] WaitTimeout", issuer->pid,
512                     MC_smx_process_get_host_name(issuer));
513       else
514         label = simgrid::xbt::string_printf("[(%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 = simgrid::xbt::string_printf("[(%lu)%s] Wait [(%lu)->(%lu)]",
525                     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 = simgrid::xbt::string_printf("[(%lu)] Wait [(%lu)->(%lu)]",
531                     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 = simgrid::xbt::string_printf("[(%lu)%s] Test FALSE",
546                     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 = simgrid::xbt::string_printf("[(%lu)%s] Test TRUE", issuer->pid,
553                     MC_smx_process_get_host_name(issuer));
554       else
555         label = simgrid::xbt::string_printf("[(%lu)] Test TRUE", issuer->pid);
556     }
557     break;
558   }
559
560   case SIMCALL_COMM_WAITANY: {
561     unsigned long comms_size = read_length(
562       mc_model_checker->process(), remote(simcall_comm_waitany__get__comms(req)));
563     if (issuer->host)
564       label = simgrid::xbt::string_printf("[(%lu)%s] WaitAny [%d of %lu]",
565                   issuer->pid,
566                   MC_smx_process_get_host_name(issuer), value + 1,
567                   comms_size);
568     else
569       label = simgrid::xbt::string_printf("[(%lu)] WaitAny [%d of %lu]",
570                   issuer->pid, value + 1, comms_size);
571     break;
572   }
573
574   case SIMCALL_COMM_TESTANY:
575     if (value == -1) {
576       if (issuer->host)
577         label = simgrid::xbt::string_printf("[(%lu)%s] TestAny FALSE",
578                     issuer->pid, MC_smx_process_get_host_name(issuer));
579       else
580         label = simgrid::xbt::string_printf("[(%lu)] TestAny FALSE", issuer->pid);
581     } else {
582       if (issuer->host)
583         label = simgrid::xbt::string_printf("[(%lu)%s] TestAny TRUE [%d of %lu]",
584                     issuer->pid,
585                     MC_smx_process_get_host_name(issuer), value + 1,
586                     xbt_dynar_length(simcall_comm_testany__get__comms(req)));
587       else
588         label = simgrid::xbt::string_printf("[(%lu)] TestAny TRUE [%d of %lu]",
589                     issuer->pid,
590                     value + 1,
591                     xbt_dynar_length(simcall_comm_testany__get__comms(req)));
592     }
593     break;
594
595   case SIMCALL_MUTEX_TRYLOCK:
596     label = simgrid::xbt::string_printf("[(%lu)] Mutex TRYLOCK", issuer->pid);
597     break;
598
599   case SIMCALL_MUTEX_LOCK:
600     label = simgrid::xbt::string_printf("[(%lu)] Mutex LOCK", issuer->pid);
601     break;
602
603   case SIMCALL_MC_RANDOM:
604     if (issuer->host)
605       label = simgrid::xbt::string_printf("[(%lu)%s] MC_RANDOM (%d)",
606                   issuer->pid, MC_smx_process_get_host_name(issuer), value);
607     else
608       label = simgrid::xbt::string_printf("[(%lu)] MC_RANDOM (%d)", issuer->pid, value);
609     break;
610
611   default:
612     THROW_UNIMPLEMENTED;
613   }
614
615   const char* color = get_color(issuer->pid - 1);
616   return  simgrid::xbt::string_printf(
617         "label = \"%s\", color = %s, fontcolor = %s", label.c_str(),
618         color, color);
619 }
620
621 }
622 }