Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
[mc] Remove redundant 'mc_mode' global variable
[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_mbox(smx_simcall_t r)
44 {
45   switch(r->call) {
46   case SIMCALL_COMM_ISEND:
47     return simcall_comm_isend__get__mbox(r);
48   case SIMCALL_COMM_IRECV:
49     return simcall_comm_irecv__get__mbox(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 mbox = MC_get_mbox(r1);
77
78     if (mbox != synchro2->comm.mbox_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 0
105   if((r1->call == SIMCALL_COMM_ISEND || r1->call == SIMCALL_COMM_IRECV)
106      &&  r2->call == SIMCALL_COMM_TEST)
107      return FALSE;
108 #endif
109
110   if (r1->call == SIMCALL_COMM_WAIT
111       && (r2->call == SIMCALL_COMM_WAIT || r2->call == SIMCALL_COMM_TEST)
112       && (synchro1->comm.src_proc == nullptr || synchro1->comm.dst_proc == nullptr))
113     return false;
114
115   if (r1->call == SIMCALL_COMM_TEST &&
116       (simcall_comm_test__get__comm(r1) == nullptr
117        || synchro1->comm.src_buff == nullptr
118        || synchro1->comm.dst_buff == nullptr))
119     return false;
120
121   if (r1->call == SIMCALL_COMM_TEST && r2->call == SIMCALL_COMM_WAIT
122       && synchro1->comm.src_buff == synchro2->comm.src_buff
123       && synchro1->comm.dst_buff == synchro2->comm.dst_buff)
124     return false;
125
126   if (r1->call == SIMCALL_COMM_WAIT && r2->call == SIMCALL_COMM_TEST
127       && synchro1->comm.src_buff != nullptr
128       && synchro1->comm.dst_buff != nullptr
129       && synchro2->comm.src_buff != nullptr
130       && synchro2->comm.dst_buff != nullptr
131       && synchro1->comm.dst_buff != synchro2->comm.src_buff
132       && synchro1->comm.dst_buff != synchro2->comm.dst_buff
133       && synchro2->comm.dst_buff != synchro1->comm.src_buff)
134     return false;
135
136   return true;
137 }
138
139 // Those are internal_req
140 bool request_depend(smx_simcall_t r1, smx_simcall_t r2)
141 {
142   if (r1->issuer == r2->issuer)
143     return false;
144
145   /* Wait with timeout transitions are not considered by the independance theorem, thus we consider them as dependant with all other transitions */
146   if ((r1->call == SIMCALL_COMM_WAIT && simcall_comm_wait__get__timeout(r1) > 0)
147       || (r2->call == SIMCALL_COMM_WAIT
148           && simcall_comm_wait__get__timeout(r2) > 0))
149     return TRUE;
150
151   if (r1->call != r2->call)
152     return request_depend_asymmetric(r1, r2)
153       && request_depend_asymmetric(r2, r1);
154
155   // Those are internal requests, we do not need indirection
156   // because those objects are copies:
157   smx_synchro_t synchro1 = MC_get_comm(r1);
158   smx_synchro_t synchro2 = MC_get_comm(r2);
159
160   switch(r1->call) {
161   case SIMCALL_COMM_ISEND:
162     return simcall_comm_isend__get__mbox(r1) == simcall_comm_isend__get__mbox(r2);
163   case SIMCALL_COMM_IRECV:
164     return simcall_comm_irecv__get__mbox(r1) == simcall_comm_irecv__get__mbox(r2);
165   case SIMCALL_COMM_WAIT:
166     if (synchro1->comm.src_buff == synchro2->comm.src_buff
167         && synchro1->comm.dst_buff == synchro2->comm.dst_buff)
168       return false;
169     else if (synchro1->comm.src_buff != nullptr
170         && synchro1->comm.dst_buff != nullptr
171         && synchro2->comm.src_buff != nullptr
172         && synchro2->comm.dst_buff != nullptr
173         && synchro1->comm.dst_buff != synchro2->comm.src_buff
174         && synchro1->comm.dst_buff != synchro2->comm.dst_buff
175         && synchro2->comm.dst_buff != synchro1->comm.src_buff)
176       return false;
177     else
178       return true;
179   default:
180     return true;
181   }
182 }
183
184 }
185 }
186
187 static char *pointer_to_string(void *pointer)
188 {
189
190   if (XBT_LOG_ISENABLED(mc_request, xbt_log_priority_verbose))
191     return bprintf("%p", pointer);
192
193   return xbt_strdup("(verbose only)");
194 }
195
196 static char *buff_size_to_string(size_t buff_size)
197 {
198
199   if (XBT_LOG_ISENABLED(mc_request, xbt_log_priority_verbose))
200     return bprintf("%zu", buff_size);
201
202   return xbt_strdup("(verbose only)");
203 }
204
205
206 std::string simgrid::mc::request_to_string(smx_simcall_t req, int value, simgrid::mc::RequestType request_type)
207 {
208   xbt_assert(mc_model_checker != nullptr);
209
210   bool use_remote_comm = true;
211   switch(request_type) {
212   case simgrid::mc::RequestType::simix:
213     use_remote_comm = true;
214     break;
215   case simgrid::mc::RequestType::executed:
216   case simgrid::mc::RequestType::internal:
217     use_remote_comm = false;
218     break;
219   }
220
221   const char* type = nullptr;
222   char *args = nullptr;
223
224   smx_process_t issuer = MC_smx_simcall_get_issuer(req);
225
226   switch (req->call) {
227
228   case SIMCALL_COMM_ISEND: {
229     type = "iSend";
230     char* p = pointer_to_string(simcall_comm_isend__get__src_buff(req));
231     char* bs = buff_size_to_string(simcall_comm_isend__get__src_buff_size(req));
232     if (issuer->host)
233       args =
234           bprintf("src=(%lu)%s (%s), buff=%s, size=%s", issuer->pid,
235                   MC_smx_process_get_host_name(issuer),
236                   MC_smx_process_get_name(issuer),
237                   p, bs);
238     else
239       args =
240           bprintf("src=(%lu)%s, buff=%s, size=%s", issuer->pid,
241                   MC_smx_process_get_name(issuer), p, bs);
242     xbt_free(bs);
243     xbt_free(p);
244     break;
245   }
246
247   case SIMCALL_COMM_IRECV: {
248     size_t* remote_size = simcall_comm_irecv__get__dst_buff_size(req);
249
250     // size_t size = size_pointer ? *size_pointer : 0;
251     size_t size = 0;
252     if (remote_size)
253       mc_model_checker->process().read_bytes(&size, sizeof(size),
254         remote(remote_size));
255
256     type = "iRecv";
257     char* p = pointer_to_string(simcall_comm_irecv__get__dst_buff(req));
258     char* bs = buff_size_to_string(size);
259     if (issuer->host)
260       args =
261           bprintf("dst=(%lu)%s (%s), buff=%s, size=%s", issuer->pid,
262                   MC_smx_process_get_host_name(issuer),
263                   MC_smx_process_get_name(issuer),
264                   p, bs);
265     else
266       args =
267           bprintf("dst=(%lu)%s, buff=%s, size=%s", issuer->pid,
268                   MC_smx_process_get_name(issuer),
269                   p, bs);
270     xbt_free(bs);
271     xbt_free(p);
272     break;
273   }
274
275   case SIMCALL_COMM_WAIT: {
276     smx_synchro_t remote_act = simcall_comm_wait__get__comm(req);
277     char* p;
278     if (value == -1) {
279       type = "WaitTimeout";
280       p = pointer_to_string(remote_act);
281       args = bprintf("comm=%s", p);
282     } else {
283       type = "Wait";
284       p = pointer_to_string(remote_act);
285
286       s_smx_synchro_t synchro;
287       smx_synchro_t act;
288       if (use_remote_comm) {
289         mc_model_checker->process().read_bytes(&synchro,
290           sizeof(synchro), remote(remote_act));
291         act = &synchro;
292       } else
293         act = remote_act;
294
295       smx_process_t src_proc = mc_model_checker->process().resolveProcess(
296         simgrid::mc::remote(act->comm.src_proc));
297       smx_process_t dst_proc = mc_model_checker->process().resolveProcess(
298         simgrid::mc::remote(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 == nullptr) {
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_model_checker->process().resolveProcess(
332         simgrid::mc::remote(act->comm.src_proc));
333       smx_process_t dst_proc = mc_model_checker->process().resolveProcess(
334         simgrid::mc::remote(act->comm.dst_proc));
335       args = bprintf("comm=%s [(%lu)%s (%s) -> (%lu)%s (%s)]", p,
336                      src_proc->pid,
337                      MC_smx_process_get_name(src_proc),
338                      MC_smx_process_get_host_name(src_proc),
339                      dst_proc->pid,
340                      MC_smx_process_get_name(dst_proc),
341                      MC_smx_process_get_host_name(dst_proc));
342     }
343     xbt_free(p);
344     break;
345   }
346
347   case SIMCALL_COMM_WAITANY: {
348     type = "WaitAny";
349     s_xbt_dynar_t comms;
350     mc_model_checker->process().read_bytes(
351       &comms, sizeof(comms), remote(simcall_comm_waitany__get__comms(req)));
352     if (!xbt_dynar_is_empty(&comms)) {
353       smx_synchro_t remote_sync;
354       read_element(mc_model_checker->process(),
355         &remote_sync, remote(simcall_comm_waitany__get__comms(req)), value,
356         sizeof(remote_sync));
357       char* p = pointer_to_string(remote_sync);
358       args = bprintf("comm=%s (%d of %lu)",
359         p, value + 1, xbt_dynar_length(&comms));
360       xbt_free(p);
361     } else
362       args = bprintf("comm at idx %d", value);
363     break;
364   }
365
366   case SIMCALL_COMM_TESTANY:
367     if (value == -1) {
368       type = "TestAny FALSE";
369       args = xbt_strdup("-");
370     } else {
371       type = "TestAny";
372       args =
373           bprintf("(%d of %zu)", value + 1,
374                   read_length(mc_model_checker->process(),
375                     simcall_comm_testany__get__comms(req)));
376     }
377     break;
378
379   case SIMCALL_MUTEX_TRYLOCK:
380   case SIMCALL_MUTEX_LOCK: {
381     if (req->call == SIMCALL_MUTEX_LOCK)
382       type = "Mutex LOCK";
383     else
384       type = "Mutex TRYLOCK";
385
386     s_smx_mutex_t mutex;
387     mc_model_checker->process().read_bytes(&mutex, sizeof(mutex),
388       remote(
389         req->call == SIMCALL_MUTEX_LOCK
390         ? simcall_mutex_lock__get__mutex(req)
391         : simcall_mutex_trylock__get__mutex(req)
392       ));
393     s_xbt_swag_t mutex_sleeping;
394     mc_model_checker->process().read_bytes(&mutex_sleeping, sizeof(mutex_sleeping),
395       remote(mutex.sleeping));
396
397     args = bprintf("locked = %d, owner = %d, sleeping = %d",
398       mutex.locked,
399       mutex.owner != nullptr ? (int) mc_model_checker->process().resolveProcess(
400         simgrid::mc::remote(mutex.owner))->pid : -1,
401       mutex_sleeping.count);
402     break;
403   }
404
405   case SIMCALL_MC_RANDOM:
406     type = "MC_RANDOM";
407     args = bprintf("%d", value);
408     break;
409
410   default:
411     THROW_UNIMPLEMENTED;
412   }
413
414   std::string str;
415   if (args != nullptr)
416     str = simgrid::xbt::string_printf("[(%lu)%s (%s)] %s(%s)", issuer->pid,
417                 MC_smx_process_get_host_name(issuer),
418                 MC_smx_process_get_name(issuer),
419                 type, args);
420   else
421     str = simgrid::xbt::string_printf("[(%lu)%s (%s)] %s ", issuer->pid,
422                 MC_smx_process_get_host_name(issuer),
423                 MC_smx_process_get_name(issuer),
424                 type);
425   xbt_free(args);
426   return str;
427 }
428
429 namespace simgrid {
430 namespace mc {
431
432 bool request_is_enabled_by_idx(smx_simcall_t req, unsigned int idx)
433 {
434   smx_synchro_t remote_act = nullptr;
435   switch (req->call) {
436
437   case SIMCALL_COMM_WAIT:
438     /* FIXME: check also that src and dst processes are not suspended */
439     remote_act = simcall_comm_wait__get__comm(req);
440     break;
441
442   case SIMCALL_COMM_WAITANY: {
443     read_element(
444       mc_model_checker->process(), &remote_act,
445       remote(simcall_comm_waitany__get__comms(req)),
446       idx, sizeof(remote_act));
447     }
448     break;
449
450   case SIMCALL_COMM_TESTANY: {
451     read_element(
452       mc_model_checker->process(), &remote_act,
453       remote(simcall_comm_testany__get__comms(req)),
454       idx, sizeof(remote_act));
455     }
456     break;
457
458   default:
459     return true;
460   }
461
462   s_smx_synchro_t synchro;
463   mc_model_checker->process().read_bytes(
464     &synchro, sizeof(synchro), remote(remote_act));
465   return synchro.comm.src_proc && synchro.comm.dst_proc;
466 }
467
468 bool process_is_enabled(smx_process_t process)
469 {
470   return simgrid::mc::request_is_enabled(&process->simcall);
471 }
472
473 static const char* colors[] = {
474   "blue",
475   "red",
476   "green3",
477   "goldenrod",
478   "brown",
479   "purple",
480   "magenta",
481   "turquoise4",
482   "gray25",
483   "forestgreen",
484   "hotpink",
485   "lightblue",
486   "tan",
487 };
488
489 static inline const char* get_color(int id)
490 {
491   return colors[id % (sizeof(colors) / sizeof(colors[0])) ];
492 }
493
494 std::string request_get_dot_output(smx_simcall_t req, int value)
495 {
496   std::string label;
497
498   const smx_process_t issuer = MC_smx_simcall_get_issuer(req);
499
500   switch (req->call) {
501   case SIMCALL_COMM_ISEND:
502     if (issuer->host)
503       label = simgrid::xbt::string_printf("[(%lu)%s] iSend", issuer->pid,
504                   MC_smx_process_get_host_name(issuer));
505     else
506       label = bprintf("[(%lu)] iSend", issuer->pid);
507     break;
508
509   case SIMCALL_COMM_IRECV:
510     if (issuer->host)
511       label = simgrid::xbt::string_printf("[(%lu)%s] iRecv", issuer->pid,
512                   MC_smx_process_get_host_name(issuer));
513     else
514       label = simgrid::xbt::string_printf("[(%lu)] iRecv", issuer->pid);
515     break;
516
517   case SIMCALL_COMM_WAIT: {
518     if (value == -1) {
519       if (issuer->host)
520         label = simgrid::xbt::string_printf("[(%lu)%s] WaitTimeout", issuer->pid,
521                     MC_smx_process_get_host_name(issuer));
522       else
523         label = simgrid::xbt::string_printf("[(%lu)] WaitTimeout", issuer->pid);
524     } else {
525       smx_synchro_t remote_act = simcall_comm_wait__get__comm(req);
526       s_smx_synchro_t synchro;
527       mc_model_checker->process().read_bytes(&synchro,
528         sizeof(synchro), remote(remote_act));
529
530       smx_process_t src_proc = mc_model_checker->process().resolveProcess(
531         simgrid::mc::remote(synchro.comm.src_proc));
532       smx_process_t dst_proc = mc_model_checker->process().resolveProcess(
533         simgrid::mc::remote(synchro.comm.dst_proc));
534       if (issuer->host)
535         label = simgrid::xbt::string_printf("[(%lu)%s] Wait [(%lu)->(%lu)]",
536                     issuer->pid,
537                     MC_smx_process_get_host_name(issuer),
538                     src_proc ? src_proc->pid : 0,
539                     dst_proc ? dst_proc->pid : 0);
540       else
541         label = simgrid::xbt::string_printf("[(%lu)] Wait [(%lu)->(%lu)]",
542                     issuer->pid,
543                     src_proc ? src_proc->pid : 0,
544                     dst_proc ? dst_proc->pid : 0);
545     }
546     break;
547   }
548
549   case SIMCALL_COMM_TEST: {
550     smx_synchro_t remote_act = simcall_comm_test__get__comm(req);
551     s_smx_synchro_t synchro;
552     mc_model_checker->process().read_bytes(&synchro,
553       sizeof(synchro), remote(remote_act));
554     if (synchro.comm.src_proc == nullptr || synchro.comm.dst_proc == nullptr) {
555       if (issuer->host)
556         label = simgrid::xbt::string_printf("[(%lu)%s] Test FALSE",
557                     issuer->pid,
558                     MC_smx_process_get_host_name(issuer));
559       else
560         label = bprintf("[(%lu)] Test FALSE", issuer->pid);
561     } else {
562       if (issuer->host)
563         label = simgrid::xbt::string_printf("[(%lu)%s] Test TRUE", issuer->pid,
564                     MC_smx_process_get_host_name(issuer));
565       else
566         label = simgrid::xbt::string_printf("[(%lu)] Test TRUE", issuer->pid);
567     }
568     break;
569   }
570
571   case SIMCALL_COMM_WAITANY: {
572     unsigned long comms_size = read_length(
573       mc_model_checker->process(), remote(simcall_comm_waitany__get__comms(req)));
574     if (issuer->host)
575       label = simgrid::xbt::string_printf("[(%lu)%s] WaitAny [%d of %lu]",
576                   issuer->pid,
577                   MC_smx_process_get_host_name(issuer), value + 1,
578                   comms_size);
579     else
580       label = simgrid::xbt::string_printf("[(%lu)] WaitAny [%d of %lu]",
581                   issuer->pid, value + 1, comms_size);
582     break;
583   }
584
585   case SIMCALL_COMM_TESTANY:
586     if (value == -1) {
587       if (issuer->host)
588         label = simgrid::xbt::string_printf("[(%lu)%s] TestAny FALSE",
589                     issuer->pid, MC_smx_process_get_host_name(issuer));
590       else
591         label = simgrid::xbt::string_printf("[(%lu)] TestAny FALSE", issuer->pid);
592     } else {
593       if (issuer->host)
594         label = simgrid::xbt::string_printf("[(%lu)%s] TestAny TRUE [%d of %lu]",
595                     issuer->pid,
596                     MC_smx_process_get_host_name(issuer), value + 1,
597                     xbt_dynar_length(simcall_comm_testany__get__comms(req)));
598       else
599         label = simgrid::xbt::string_printf("[(%lu)] TestAny TRUE [%d of %lu]",
600                     issuer->pid,
601                     value + 1,
602                     xbt_dynar_length(simcall_comm_testany__get__comms(req)));
603     }
604     break;
605
606   case SIMCALL_MUTEX_TRYLOCK:
607     label = simgrid::xbt::string_printf("[(%lu)] Mutex TRYLOCK", issuer->pid);
608     break;
609
610   case SIMCALL_MUTEX_LOCK:
611     label = simgrid::xbt::string_printf("[(%lu)] Mutex LOCK", issuer->pid);
612     break;
613
614   case SIMCALL_MC_RANDOM:
615     if (issuer->host)
616       label = simgrid::xbt::string_printf("[(%lu)%s] MC_RANDOM (%d)",
617                   issuer->pid, MC_smx_process_get_host_name(issuer), value);
618     else
619       label = simgrid::xbt::string_printf("[(%lu)] MC_RANDOM (%d)", issuer->pid, value);
620     break;
621
622   default:
623     THROW_UNIMPLEMENTED;
624   }
625
626   const char* color = get_color(issuer->pid - 1);
627   return  simgrid::xbt::string_printf(
628         "label = \"%s\", color = %s, fontcolor = %s", label.c_str(),
629         color, color);
630 }
631
632 }
633 }