1 /* Copyright (c) 2019-2022. The SimGrid Team. All rights reserved. */
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. */
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"
13 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_observer, mc, "Logging specific to MC simcall observation");
19 bool SimcallObserver::depends(SimcallObserver* other)
23 /* Random is only dependent when issued by the same actor (ie, always independent) */
24 bool RandomSimcall::depends(SimcallObserver* other)
26 return get_issuer() == other->get_issuer();
28 bool MutexSimcall::depends(SimcallObserver* other)
30 if (dynamic_cast<RandomSimcall*>(other) != nullptr)
31 return other->depends(this); /* Other is random, that is very permissive. Use that relation instead. */
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);
36 return true; // Depends on anything we don't know
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())
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())
48 return true; // Depend on things we don't know for sure that they are independent
51 std::string SimcallObserver::to_string(int /*times_considered*/) const
53 return simgrid::xbt::string_printf("[(%ld)%s (%s)] ", issuer_->get_pid(), issuer_->get_host()->get_cname(),
54 issuer_->get_cname());
57 std::string SimcallObserver::dot_label(int /*times_considered*/) const
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());
64 std::string RandomSimcall::to_string(int times_considered) const
66 return SimcallObserver::to_string(times_considered) + "MC_RANDOM(" + std::to_string(times_considered) + ")";
69 std::string RandomSimcall::dot_label(int times_considered) const
71 return SimcallObserver::dot_label(times_considered) + "MC_RANDOM(" + std::to_string(next_value_) + ")";
74 void RandomSimcall::prepare(int times_considered)
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);
80 int RandomSimcall::get_max_consider() const
82 return max_ - min_ + 1;
85 std::string MutexUnlockSimcall::to_string(int times_considered) const
87 return SimcallObserver::to_string(times_considered) + "Mutex UNLOCK";
90 std::string MutexUnlockSimcall::dot_label(int times_considered) const
92 return SimcallObserver::dot_label(times_considered) + "Mutex UNLOCK";
95 std::string MutexLockSimcall::to_string(int times_considered) const
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)";
105 std::string MutexLockSimcall::dot_label(int times_considered) const
107 return SimcallObserver::dot_label(times_considered) + (blocking_ ? "Mutex LOCK" : "Mutex TRYLOCK");
110 bool MutexLockSimcall::is_enabled() const
112 return not blocking_ || get_mutex()->get_owner() == nullptr || get_mutex()->get_owner() == get_issuer();
115 std::string ConditionWaitSimcall::to_string(int times_considered) const
117 std::string res = SimcallObserver::to_string(times_considered) + "Condition WAIT";
118 res += "(" + (timeout_ == -1.0 ? "" : std::to_string(timeout_)) + ")";
122 std::string ConditionWaitSimcall::dot_label(int times_considered) const
124 return SimcallObserver::dot_label(times_considered) + "Condition WAIT";
127 bool ConditionWaitSimcall::is_enabled() const
129 static bool warned = false;
131 XBT_INFO("Using condition variables in model-checked code is still experimental. Use at your own risk");
137 std::string SemAcquireSimcall::to_string(int times_considered) const
139 std::string res = SimcallObserver::to_string(times_considered) + "Sem ACQUIRE";
140 res += "(" + (timeout_ == -1.0 ? "" : std::to_string(timeout_)) + ")";
144 std::string SemAcquireSimcall::dot_label(int times_considered) const
146 return SimcallObserver::dot_label(times_considered) + "Sem ACQUIRE";
149 bool SemAcquireSimcall::is_enabled() const
151 static bool warned = false;
153 XBT_INFO("Using semaphore in model-checked code is still experimental. Use at your own risk");
159 int ActivityTestanySimcall::get_max_consider() const
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_.
164 for (const auto& act : activities_)
165 if (dynamic_cast<activity::CommImpl*>(act) != nullptr)
170 void ActivityTestanySimcall::prepare(int times_considered)
172 next_value_ = times_considered;
175 std::string ActivityTestanySimcall::to_string(int times_considered) const
177 std::string res = SimcallObserver::to_string(times_considered);
178 if (times_considered == -1) {
179 res += "TestAny FALSE(-)";
181 res += "TestAny(" + xbt::string_printf("(%d of %zu)", times_considered + 1, activities_.size());
187 std::string ActivityTestanySimcall::dot_label(int times_considered) const
189 std::string res = SimcallObserver::dot_label(times_considered) + "TestAny ";
190 if (times_considered == -1) {
193 res += xbt::string_printf("TRUE [%d of %zu]", times_considered + 1, activities_.size());
198 bool ActivityTestSimcall::depends(SimcallObserver* other)
200 if (get_issuer() == other->get_issuer())
203 if (dynamic_cast<ActivityTestSimcall*>(other))
206 auto* comm1 = dynamic_cast<activity::CommImpl*>(activity_);
207 if (comm1 == nullptr)
210 if (dynamic_cast<ActivityWaitSimcall*>(other) != nullptr &&
211 (comm1->src_actor_.get() == nullptr || comm1->dst_actor_.get() == nullptr))
214 if (comm1->src_buff_ == nullptr || comm1->dst_buff_ == nullptr)
217 if (auto* test = dynamic_cast<ActivityTestSimcall*>(other)) {
218 auto* comm2 = dynamic_cast<activity::CommImpl*>(test->get_activity());
219 if (comm2 == nullptr)
221 else if (comm2->src_buff_ == nullptr || comm2->dst_buff_ == nullptr)
225 if (auto* wait = dynamic_cast<ActivityWaitSimcall*>(other)) {
226 auto* comm2 = dynamic_cast<activity::CommImpl*>(wait->get_activity());
227 if (comm2 == nullptr)
229 if (comm1->src_buff_ == comm2->src_buff_ && comm1->dst_buff_ == comm2->dst_buff_)
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_)
240 std::string ActivityTestSimcall::to_string(int times_considered) const
242 std::string res = SimcallObserver::to_string(times_considered) + "Test ";
243 auto* comm = dynamic_cast<activity::CommImpl*>(activity_);
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)
252 auto src = comm->src_actor_;
253 auto dst = comm->dst_actor_;
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()) +
258 xbt::string_printf("(%ld)%s (%s)])", dst->get_pid(), dst->get_host()->get_cname(), dst->get_cname());
261 xbt_die("Only Comms are supported here for now");
265 std::string ActivityTestSimcall::dot_label(int times_considered) const
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)) {
277 bool ActivityWaitSimcall::is_enabled() const
279 /* FIXME: check also that src and dst processes are not suspended */
280 const auto* comm = dynamic_cast<activity::CommImpl*>(activity_);
282 xbt_die("Only Comms are supported here for now");
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)
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_);
296 bool ActivityWaitSimcall::depends(SimcallObserver* other)
298 if (get_issuer() == other->get_issuer())
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)
305 auto* comm1 = dynamic_cast<activity::CommImpl*>(activity_);
306 auto* comm2 = dynamic_cast<activity::CommImpl*>(wait->get_activity());
308 if (comm1 == nullptr || comm2 == nullptr) // One wait at least in not on a Comm
311 if (comm1->src_buff_ == comm2->src_buff_ && comm1->dst_buff_ == comm2->dst_buff_)
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_)
321 std::string ActivityWaitSimcall::to_string(int times_considered) const
323 std::string res = SimcallObserver::to_string(times_considered);
324 auto* comm = dynamic_cast<activity::CommImpl*>(activity_);
326 xbt_die("Only Comms are supported here for now");
328 if (times_considered == -1) {
329 res += "WaitTimeout(comm=" + (XBT_LOG_ISENABLED(mc_observer, xbt_log_priority_verbose)
330 ? xbt::string_printf("%p)", comm)
331 : "(verbose only))");
335 auto src = comm->src_actor_;
336 auto dst = comm->dst_actor_;
338 XBT_LOG_ISENABLED(mc_observer, xbt_log_priority_verbose) ? xbt::string_printf("%p", comm) : "(verbose only) ";
339 res += xbt::string_printf("[(%ld)%s (%s) ", src->get_pid(), src->get_host()->get_cname(), src->get_cname()) +
340 "-> " + xbt::string_printf("(%ld)%s (%s)])", dst->get_pid(), dst->get_host()->get_cname(), dst->get_cname());
345 std::string ActivityWaitSimcall::dot_label(int times_considered) const
347 std::string res = SimcallObserver::dot_label(times_considered);
348 res += (times_considered == -1) ? "WaitTimeout " : "Wait ";
350 auto* comm = dynamic_cast<activity::CommImpl*>(activity_);
352 auto src = comm->src_actor_;
353 auto dst = comm->dst_actor_;
354 res += " [(" + std::to_string(src ? src->get_pid() : 0) + ")";
355 res += "->(" + std::to_string(dst ? dst->get_pid() : 0) + ")]";
357 xbt_die("Only Comms are supported here for now");
361 std::string ActivityWaitanySimcall::dot_label(int times_considered) const
363 return SimcallObserver::dot_label(times_considered) +
364 xbt::string_printf("WaitAny [%d of %zu]", times_considered + 1, activities_.size());
367 bool ActivityWaitanySimcall::is_enabled() const
369 // FIXME: deal with other kind of activities (Exec and I/Os)
370 // FIXME: Can be factored with ActivityWaitSimcall::is_enabled()
371 const auto* comm = dynamic_cast<activity::CommImpl*>(activities_[next_value_]);
373 xbt_die("Only Comms are supported here for now");
374 if (comm->src_timeout_ || comm->dst_timeout_) {
375 /* If it has a timeout it will be always be enabled (regardless of who declared the timeout),
376 * because even if the communication is not ready, it can timeout and won't block. */
377 if (_sg_mc_timeout == 1)
380 /* On the other hand if it hasn't a timeout, check if the comm is ready.*/
381 else if (comm->detached() && comm->src_actor_ == nullptr && comm->get_state() == activity::State::READY)
382 return (comm->dst_actor_ != nullptr);
383 return (comm->src_actor_ && comm->dst_actor_);
386 int ActivityWaitanySimcall::get_max_consider() const
388 return static_cast<int>(activities_.size());
391 void ActivityWaitanySimcall::prepare(int times_considered)
393 next_value_ = times_considered;
396 std::string ActivityWaitanySimcall::to_string(int times_considered) const
398 std::string res = SimcallObserver::to_string(times_considered) + "WaitAny(";
399 size_t count = activities_.size();
401 if (auto* comm = dynamic_cast<kernel::activity::CommImpl*>(activities_[times_considered]))
403 (XBT_LOG_ISENABLED(mc_observer, xbt_log_priority_verbose) ? xbt::string_printf("%p", comm)
404 : "(verbose only)") +
405 xbt::string_printf("(%d of %zu))", times_considered + 1, count);
407 xbt_die("Only Comms are supported here for now");
409 res += "comm at idx " + std::to_string(times_considered) + ")";
414 } // namespace kernel
415 } // namespace simgrid