Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
continue to mess with MC
[simgrid.git] / src / kernel / actor / SimcallObserver.cpp
1 /* Copyright (c) 2019-2022. The SimGrid Team. All rights reserved.          */
2
3 /* This program is free software; you can redistribute it and/or modify it
4  * under the terms of the license (GNU LGPL) which comes with this package. */
5
6 #include "src/kernel/actor/SimcallObserver.hpp"
7 #include "simgrid/s4u/Host.hpp"
8 #include "src/kernel/activity/CommImpl.hpp"
9 #include "src/kernel/activity/MutexImpl.hpp"
10 #include "src/kernel/actor/ActorImpl.hpp"
11 #include "src/mc/mc_config.hpp"
12
13 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_observer, mc, "Logging specific to MC simcall observation");
14
15 namespace simgrid {
16 namespace kernel {
17 namespace actor {
18
19 bool SimcallObserver::depends(SimcallObserver* other)
20 {
21   THROW_UNIMPLEMENTED;
22 }
23 /* Random is only dependent when issued by the same actor (ie, always independent) */
24 bool RandomSimcall::depends(SimcallObserver* other)
25 {
26   return get_issuer() == other->get_issuer();
27 }
28 bool MutexSimcall::depends(SimcallObserver* other)
29 {
30   if (dynamic_cast<RandomSimcall*>(other) != nullptr)
31     return other->depends(this); /* Other is random, that is very permissive. Use that relation instead. */
32
33 #if 0 /* This code is currently broken and shouldn't be used. We must implement asynchronous locks before */
34   MutexSimcall* that = dynamic_cast<MutexSimcall*>(other);
35   if (that == nullptr)
36     return true; // Depends on anything we don't know
37
38   /* Theorem 4.4.7: Any pair of synchronization actions of distinct actors concerning distinct mutexes are independent */
39   if (this->get_issuer() != that->get_issuer() && this->get_mutex() != that->get_mutex())
40     return false;
41
42   /* Theorem 4.4.8 An AsyncMutexLock is independent with a MutexUnlock of another actor */
43   if (((dynamic_cast<MutexLockSimcall*>(this) != nullptr && dynamic_cast<MutexUnlockSimcall*>(that)) ||
44        (dynamic_cast<MutexLockSimcall*>(that) != nullptr && dynamic_cast<MutexUnlockSimcall*>(this))) &&
45       get_issuer() != other->get_issuer())
46     return false;
47 #endif
48   return true; // Depend on things we don't know for sure that they are independent
49 }
50
51 std::string SimcallObserver::to_string(int /*times_considered*/) const
52 {
53   return simgrid::xbt::string_printf("[(%ld)%s (%s)] ", issuer_->get_pid(), issuer_->get_host()->get_cname(),
54                                      issuer_->get_cname());
55 }
56
57 std::string SimcallObserver::dot_label(int /*times_considered*/) const
58 {
59   if (issuer_->get_host())
60     return xbt::string_printf("[(%ld)%s] ", issuer_->get_pid(), issuer_->get_host()->get_cname());
61   return xbt::string_printf("[(%ld)] ", issuer_->get_pid());
62 }
63
64 std::string RandomSimcall::to_string(int times_considered) const
65 {
66   return SimcallObserver::to_string(times_considered) + "MC_RANDOM(" + std::to_string(times_considered) + ")";
67 }
68
69 std::string RandomSimcall::dot_label(int times_considered) const
70 {
71   return SimcallObserver::dot_label(times_considered) + "MC_RANDOM(" + std::to_string(next_value_) + ")";
72 }
73
74 void RandomSimcall::prepare(int times_considered)
75 {
76   next_value_ = min_ + times_considered;
77   XBT_DEBUG("MC_RANDOM(%d, %d) will return %d after %d times", min_, max_, next_value_, times_considered);
78 }
79
80 int RandomSimcall::get_max_consider() const
81 {
82   return max_ - min_ + 1;
83 }
84
85 std::string MutexUnlockSimcall::to_string(int times_considered) const
86 {
87   return SimcallObserver::to_string(times_considered) + "Mutex UNLOCK";
88 }
89
90 std::string MutexUnlockSimcall::dot_label(int times_considered) const
91 {
92   return SimcallObserver::dot_label(times_considered) + "Mutex UNLOCK";
93 }
94
95 std::string MutexLockSimcall::to_string(int times_considered) const
96 {
97   auto mutex      = get_mutex();
98   std::string res = SimcallObserver::to_string(times_considered) + (blocking_ ? "Mutex LOCK" : "Mutex TRYLOCK");
99   res += "(locked = " + std::to_string(mutex->is_locked());
100   res += ", owner = " + std::to_string(mutex->get_owner() ? mutex->get_owner()->get_pid() : -1);
101   res += ", sleeping = n/a)";
102   return res;
103 }
104
105 std::string MutexLockSimcall::dot_label(int times_considered) const
106 {
107   return SimcallObserver::dot_label(times_considered) + (blocking_ ? "Mutex LOCK" : "Mutex TRYLOCK");
108 }
109
110 bool MutexLockSimcall::is_enabled() const
111 {
112   return not blocking_ || get_mutex()->get_owner() == nullptr || get_mutex()->get_owner() == get_issuer();
113 }
114
115 std::string ConditionWaitSimcall::to_string(int times_considered) const
116 {
117   std::string res = SimcallObserver::to_string(times_considered) + "Condition WAIT";
118   res += "(" + (timeout_ == -1.0 ? "" : std::to_string(timeout_)) + ")";
119   return res;
120 }
121
122 std::string ConditionWaitSimcall::dot_label(int times_considered) const
123 {
124   return SimcallObserver::dot_label(times_considered) + "Condition WAIT";
125 }
126
127 bool ConditionWaitSimcall::is_enabled() const
128 {
129   static bool warned = false;
130   if (not warned) {
131     XBT_INFO("Using condition variables in model-checked code is still experimental. Use at your own risk");
132     warned = true;
133   }
134   return true;
135 }
136
137 std::string SemAcquireSimcall::to_string(int times_considered) const
138 {
139   std::string res = SimcallObserver::to_string(times_considered) + "Sem ACQUIRE";
140   res += "(" + (timeout_ == -1.0 ? "" : std::to_string(timeout_)) + ")";
141   return res;
142 }
143
144 std::string SemAcquireSimcall::dot_label(int times_considered) const
145 {
146   return SimcallObserver::dot_label(times_considered) + "Sem ACQUIRE";
147 }
148
149 bool SemAcquireSimcall::is_enabled() const
150 {
151   static bool warned = false;
152   if (not warned) {
153     XBT_INFO("Using semaphore in model-checked code is still experimental. Use at your own risk");
154     warned = true;
155   }
156   return true;
157 }
158
159 int ActivityTestanySimcall::get_max_consider() const
160 {
161   // Only Comms are of interest to MC for now. When all types of activities can be consider, this function can simply
162   // return the size of activities_.
163   int count = 0;
164   for (const auto& act : activities_)
165     if (dynamic_cast<activity::CommImpl*>(act) != nullptr)
166       count++;
167   return count;
168 }
169
170 void ActivityTestanySimcall::prepare(int times_considered)
171 {
172   next_value_ = times_considered;
173 }
174
175 std::string ActivityTestanySimcall::to_string(int times_considered) const
176 {
177   std::string res = SimcallObserver::to_string(times_considered);
178   if (times_considered == -1) {
179     res += "TestAny FALSE(-)";
180   } else {
181     res += "TestAny(" + xbt::string_printf("(%d of %zu)", times_considered + 1, activities_.size());
182   }
183
184   return res;
185 }
186
187 std::string ActivityTestanySimcall::dot_label(int times_considered) const
188 {
189   std::string res = SimcallObserver::dot_label(times_considered) + "TestAny ";
190   if (times_considered == -1) {
191     res += "FALSE";
192   } else {
193     res += xbt::string_printf("TRUE [%d of %zu]", times_considered + 1, activities_.size());
194   }
195   return res;
196 }
197
198 bool ActivityTestSimcall::depends(SimcallObserver* other)
199 {
200   if (get_issuer() == other->get_issuer())
201     return false;
202
203   if (dynamic_cast<ActivityTestSimcall*>(other))
204     return true;
205
206   auto* comm1 = dynamic_cast<activity::CommImpl*>(activity_);
207   if (comm1 == nullptr)
208     return false;
209
210   if (dynamic_cast<ActivityWaitSimcall*>(other) != nullptr &&
211       (comm1->src_actor_.get() == nullptr || comm1->dst_actor_.get() == nullptr))
212     return false;
213
214   if (comm1->src_buff_ == nullptr || comm1->dst_buff_ == nullptr)
215     return false;
216
217   if (auto* test = dynamic_cast<ActivityTestSimcall*>(other)) {
218     auto* comm2 = dynamic_cast<activity::CommImpl*>(test->get_activity());
219     if (comm2 == nullptr)
220       return false;
221     else if (comm2->src_buff_ == nullptr || comm2->dst_buff_ == nullptr)
222       return false;
223   }
224
225   if (auto* wait = dynamic_cast<ActivityWaitSimcall*>(other)) {
226     auto* comm2 = dynamic_cast<activity::CommImpl*>(wait->get_activity());
227     if (comm2 == nullptr)
228       return false;
229     if (comm1->src_buff_ == comm2->src_buff_ && comm1->dst_buff_ == comm2->dst_buff_)
230       return false;
231     if (comm1->src_buff_ != nullptr && comm1->dst_buff_ != nullptr && comm2->src_buff_ != nullptr &&
232         comm2->dst_buff_ != nullptr && comm1->dst_buff_ != comm2->src_buff_ && comm1->dst_buff_ != comm2->dst_buff_ &&
233         comm2->dst_buff_ != comm1->src_buff_)
234       return false;
235   }
236
237   return true;
238 }
239
240 std::string ActivityTestSimcall::to_string(int times_considered) const
241 {
242   std::string res = SimcallObserver::to_string(times_considered) + "Test ";
243   auto* comm      = dynamic_cast<activity::CommImpl*>(activity_);
244   if (comm) {
245     if (comm->src_actor_.get() == nullptr || comm->dst_actor_.get() == nullptr) {
246       res += "FALSE(comm=";
247       res += XBT_LOG_ISENABLED(mc_observer, xbt_log_priority_verbose) ? xbt::string_printf("%p)", comm)
248                                                                       : "(verbose only))";
249     } else {
250       res += "TRUE(comm=";
251
252       auto src = comm->src_actor_;
253       auto dst = comm->dst_actor_;
254       res +=
255           XBT_LOG_ISENABLED(mc_observer, xbt_log_priority_verbose) ? xbt::string_printf("%p", comm) : "(verbose only) ";
256       res += xbt::string_printf("[(%ld)%s (%s) ", src->get_pid(), src->get_host()->get_cname(), src->get_cname()) +
257              "-> " +
258              xbt::string_printf("(%ld)%s (%s)])", dst->get_pid(), dst->get_host()->get_cname(), dst->get_cname());
259     }
260   } else
261     xbt_die("Only Comms are supported here for now");
262   return res;
263 }
264
265 std::string ActivityTestSimcall::dot_label(int times_considered) const
266 {
267   std::string res = SimcallObserver::dot_label(times_considered) + "Test ";
268   auto* comm      = dynamic_cast<activity::CommImpl*>(activity_);
269   if (comm && (comm->src_actor_.get() == nullptr || comm->dst_actor_.get() == nullptr)) {
270     res += "FALSE";
271   } else {
272     res += "TRUE";
273   }
274   return res;
275 }
276
277 bool ActivityWaitSimcall::is_enabled() const
278 {
279   /* FIXME: check also that src and dst processes are not suspended */
280   const auto* comm = dynamic_cast<activity::CommImpl*>(activity_);
281   if (comm == nullptr)
282     xbt_die("Only Comms are supported here for now");
283
284   if (comm->src_timeout_ || comm->dst_timeout_) {
285     /* If it has a timeout it will be always be enabled (regardless of who declared the timeout),
286      * because even if the communication is not ready, it can timeout and won't block. */
287     if (_sg_mc_timeout == 1)
288       return true;
289   }
290   /* On the other hand if it hasn't a timeout, check if the comm is ready.*/
291   else if (comm->detached() && comm->src_actor_ == nullptr && comm->get_state() == activity::State::READY)
292     return (comm->dst_actor_ != nullptr);
293   return (comm->src_actor_ && comm->dst_actor_);
294 }
295
296 bool ActivityWaitSimcall::depends(SimcallObserver* other)
297 {
298   if (get_issuer() == other->get_issuer())
299     return false;
300
301   /* Timeouts in wait transitions are not considered by the independence theorem, thus assumed dependent */
302   if (auto* wait = dynamic_cast<ActivityWaitSimcall*>(other)) {
303     if (timeout_ > 0 || wait->get_timeout() > 0)
304       return true;
305     auto* comm1 = dynamic_cast<activity::CommImpl*>(activity_);
306     auto* comm2 = dynamic_cast<activity::CommImpl*>(wait->get_activity());
307
308     if (comm1 == nullptr || comm2 == nullptr) // One wait at least in not on a Comm
309       return true;
310
311     if (comm1->src_buff_ == comm2->src_buff_ && comm1->dst_buff_ == comm2->dst_buff_)
312       return false;
313     if (comm1->src_buff_ != nullptr && comm1->dst_buff_ != nullptr && comm2->src_buff_ != nullptr &&
314         comm2->dst_buff_ != nullptr && comm1->dst_buff_ != comm2->src_buff_ && comm1->dst_buff_ != comm2->dst_buff_ &&
315         comm2->dst_buff_ != comm1->src_buff_)
316       return false;
317   }
318
319   return true;
320 }
321
322 std::string ActivityWaitSimcall::to_string(int times_considered) const
323 {
324   std::string res = SimcallObserver::to_string(times_considered);
325   auto* comm      = dynamic_cast<activity::CommImpl*>(activity_);
326   if (comm == nullptr)
327     xbt_die("Only Comms are supported here for now");
328
329   if (times_considered == -1) {
330     res += "WaitTimeout(comm=" + (XBT_LOG_ISENABLED(mc_observer, xbt_log_priority_verbose)
331                                       ? xbt::string_printf("%p)", comm)
332                                       : "(verbose only))");
333   } else {
334     res += "Wait(comm=";
335
336     auto src = comm->src_actor_;
337     auto dst = comm->dst_actor_;
338     res +=
339         XBT_LOG_ISENABLED(mc_observer, xbt_log_priority_verbose) ? xbt::string_printf("%p", comm) : "(verbose only) ";
340     res += xbt::string_printf("[(%ld)%s (%s) ", src->get_pid(), src->get_host()->get_cname(), src->get_cname()) +
341            "-> " + xbt::string_printf("(%ld)%s (%s)])", dst->get_pid(), dst->get_host()->get_cname(), dst->get_cname());
342   }
343   return res;
344 }
345
346 std::string ActivityWaitSimcall::dot_label(int times_considered) const
347 {
348   std::string res = SimcallObserver::dot_label(times_considered);
349   res += (times_considered == -1) ? "WaitTimeout " : "Wait ";
350
351   auto* comm = dynamic_cast<activity::CommImpl*>(activity_);
352   if (comm) {
353     auto src = comm->src_actor_;
354     auto dst = comm->dst_actor_;
355     res += " [(" + std::to_string(src ? src->get_pid() : 0) + ")";
356     res += "->(" + std::to_string(dst ? dst->get_pid() : 0) + ")]";
357   } else
358     xbt_die("Only Comms are supported here for now");
359   return res;
360 }
361
362 std::string ActivityWaitanySimcall::dot_label(int times_considered) const
363 {
364   return SimcallObserver::dot_label(times_considered) +
365          xbt::string_printf("WaitAny [%d of %zu]", times_considered + 1, activities_.size());
366 }
367
368 bool ActivityWaitanySimcall::is_enabled() const
369 {
370   // FIXME: deal with other kind of activities (Exec and I/Os)
371   // FIXME: Can be factored with ActivityWaitSimcall::is_enabled()
372   const auto* comm = dynamic_cast<activity::CommImpl*>(activities_[next_value_]);
373   if (comm == nullptr)
374     xbt_die("Only Comms are supported here for now");
375   if (comm->src_timeout_ || comm->dst_timeout_) {
376     /* If it has a timeout it will be always be enabled (regardless of who declared the timeout),
377      * because even if the communication is not ready, it can timeout and won't block. */
378     if (_sg_mc_timeout == 1)
379       return true;
380   }
381   /* On the other hand if it hasn't a timeout, check if the comm is ready.*/
382   else if (comm->detached() && comm->src_actor_ == nullptr && comm->get_state() == activity::State::READY)
383     return (comm->dst_actor_ != nullptr);
384   return (comm->src_actor_ && comm->dst_actor_);
385 }
386
387 int ActivityWaitanySimcall::get_max_consider() const
388 {
389   return static_cast<int>(activities_.size());
390 }
391
392 void ActivityWaitanySimcall::prepare(int times_considered)
393 {
394   next_value_ = times_considered;
395 }
396
397 std::string ActivityWaitanySimcall::to_string(int times_considered) const
398 {
399   std::string res = SimcallObserver::to_string(times_considered) + "WaitAny(";
400   size_t count    = activities_.size();
401   if (count > 0) {
402     if (auto* comm = dynamic_cast<kernel::activity::CommImpl*>(activities_[times_considered]))
403       res += "comm=" +
404              (XBT_LOG_ISENABLED(mc_observer, xbt_log_priority_verbose) ? xbt::string_printf("%p", comm)
405                                                                        : "(verbose only)") +
406              xbt::string_printf("(%d of %zu))", times_considered + 1, count);
407     else
408       xbt_die("Only Comms are supported here for now");
409   } else
410     res += "comm at idx " + std::to_string(times_considered) + ")";
411   return res;
412 }
413
414 bool CommIsendSimcall::depends(SimcallObserver* other)
415 {
416   if (get_issuer() == other->get_issuer())
417     return false;
418
419   if (auto* other_isend = dynamic_cast<CommIsendSimcall*>(other))
420     return mbox_ == other_isend->get_mailbox();
421
422   // FIXME: Not in the former dependency check because of the ordering but seems logical to add it
423   if (dynamic_cast<CommIrecvSimcall*>(other) != nullptr)
424     return false;
425
426 #if SIMGRID_HAVE_MC // FIXME needed to access mbox_cpy
427   if (auto* wait = dynamic_cast<ActivityWaitSimcall*>(other)) {
428     if (auto* comm2 = dynamic_cast<activity::CommImpl*>(wait->get_activity())) { // this is a Comm::wait_for
429       auto* mbox1 = mbox_;
430       auto* mbox2 = comm2->mbox_cpy;
431
432       if (mbox1 != mbox2 && wait->get_timeout() <= 0)
433         return false;
434
435       if ((get_issuer() != comm2->src_actor_.get()) && (get_issuer() != comm2->dst_actor_.get()) &&
436           wait->get_timeout() <= 0)
437         return false;
438
439       if (comm2->type_ == activity::CommImpl::Type::SEND && comm2->src_buff_ != src_buff_ && wait->get_timeout() <= 0)
440         return false;
441     }
442   }
443 #endif
444   /* FIXME: the following rule assumes that the result of the isend/irecv call is not stored in a buffer used in the
445    * test call. */
446 #if 0
447   if (dynamic_cast<ActivityTestSimcall*>(other))
448     return false;
449 #endif
450
451   return true;
452 }
453
454 std::string CommIsendSimcall::to_string(int times_considered) const
455 {
456   std::string res = SimcallObserver::to_string(times_considered) + "iSend(";
457   res += xbt::string_printf("src=[(%ld)%s (%s)]", get_issuer()->get_pid(), get_issuer()->get_host()->get_cname(),
458                             get_issuer()->get_cname());
459   res += XBT_LOG_ISENABLED(mc_observer, xbt_log_priority_verbose) ? xbt::string_printf(", buff=%p", src_buff_)
460                                                                   : "(verbose only)";
461   res += ", size=" +
462          (XBT_LOG_ISENABLED(mc_observer, xbt_log_priority_verbose) ? std::to_string(src_buff_size_) : "(verbose only)");
463   res += ")";
464   return res;
465 }
466
467 bool CommIrecvSimcall::depends(SimcallObserver* other)
468 {
469   if (get_issuer() == other->get_issuer())
470     return false;
471
472   if (auto* other_irecv = dynamic_cast<CommIrecvSimcall*>(other))
473     return mbox_ == other_irecv->get_mailbox();
474
475   if (dynamic_cast<CommIsendSimcall*>(other) != nullptr)
476     return false;
477
478 #if SIMGRID_HAVE_MC // FIXME needed to access mbox_cpy
479   if (auto* wait = dynamic_cast<ActivityWaitSimcall*>(other)) {
480     if (auto* comm2 = dynamic_cast<activity::CommImpl*>(wait->get_activity())) { // this is a Comm::wait_for
481       auto* mbox1 = mbox_;
482       auto* mbox2 = comm2->mbox_cpy;
483
484       if (mbox1 != mbox2 && wait->get_timeout() <= 0)
485         return false;
486
487       if ((get_issuer() != comm2->src_actor_.get()) && (get_issuer() != comm2->dst_actor_.get()) &&
488           wait->get_timeout() <= 0)
489         return false;
490
491       if (comm2->type_ == activity::CommImpl::Type::RECEIVE && comm2->dst_buff_ != dst_buff_ &&
492           wait->get_timeout() <= 0)
493         return false;
494     }
495   }
496 #endif
497   /* FIXME: the following rule assumes that the result of the isend/irecv call is not stored in a buffer used in the
498    * test call. */
499 #if 0
500   if (dynamic_cast<ActivityTestSimcall*>(other))
501     return false;
502 #endif
503
504   return true;
505 }
506
507 std::string CommIrecvSimcall::to_string(int times_considered) const
508 {
509   std::string res = SimcallObserver::to_string(times_considered) + "iRecv(";
510   res += xbt::string_printf("dst=[(%ld)%s (%s)]", get_issuer()->get_pid(), get_issuer()->get_host()->get_cname(),
511                             get_issuer()->get_cname());
512   res += XBT_LOG_ISENABLED(mc_observer, xbt_log_priority_verbose) ? xbt::string_printf(", buff=%p", dst_buff_)
513                                                                   : "(verbose only)";
514   res += ", size=" + (XBT_LOG_ISENABLED(mc_observer, xbt_log_priority_verbose) ? std::to_string(*dst_buff_size_)
515                                                                                : "(verbose only)");
516   res += ")";
517   return res;
518 }
519
520 } // namespace actor
521 } // namespace kernel
522 } // namespace simgrid