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 std::string ActivityTestanySimcall::to_string(int times_considered) const
172 std::string res = SimcallObserver::to_string(times_considered);
173 if (times_considered == -1) {
174 res += "TestAny FALSE(-)";
176 res += "TestAny(" + xbt::string_printf("(%d of %zu)", times_considered + 1, activities_.size());
182 std::string ActivityTestanySimcall::dot_label(int times_considered) const
184 std::string res = SimcallObserver::dot_label(times_considered) + "TestAny ";
185 if (times_considered == -1) {
188 res += xbt::string_printf("TRUE [%d of %zu]", times_considered + 1, activities_.size());
193 std::string ActivityTestSimcall::to_string(int times_considered) const
195 std::string res = SimcallObserver::to_string(times_considered) + "Test ";
196 auto* comm = dynamic_cast<activity::CommImpl*>(activity_);
198 if (comm->src_actor_.get() == nullptr || comm->dst_actor_.get() == nullptr) {
199 res += "FALSE(comm=";
200 res += XBT_LOG_ISENABLED(mc_observer, xbt_log_priority_verbose) ? xbt::string_printf("%p)", comm)
205 auto src = comm->src_actor_;
206 auto dst = comm->dst_actor_;
208 XBT_LOG_ISENABLED(mc_observer, xbt_log_priority_verbose) ? xbt::string_printf("%p", comm) : "(verbose only) ";
209 res += xbt::string_printf("[(%ld)%s (%s) ", src->get_pid(), src->get_host()->get_cname(), src->get_cname()) +
211 xbt::string_printf("(%ld)%s (%s)])", dst->get_pid(), dst->get_host()->get_cname(), dst->get_cname());
217 std::string ActivityTestSimcall::dot_label(int times_considered) const
219 std::string res = SimcallObserver::dot_label(times_considered) + "Test ";
220 auto* comm = dynamic_cast<activity::CommImpl*>(activity_);
221 if (comm && (comm->src_actor_.get() == nullptr || comm->dst_actor_.get() == nullptr)) {
229 std::string ActivityWaitSimcall::to_string(int times_considered) const
231 std::string res = SimcallObserver::to_string(times_considered);
232 auto* comm = dynamic_cast<activity::CommImpl*>(activity_);
235 if (times_considered == -1) {
236 res += "WaitTimeout(comm=" + XBT_LOG_ISENABLED(mc_observer, xbt_log_priority_verbose)
237 ? xbt::string_printf("%p)", comm)
242 auto src = comm->src_actor_;
243 auto dst = comm->dst_actor_;
245 XBT_LOG_ISENABLED(mc_observer, xbt_log_priority_verbose) ? xbt::string_printf("%p", comm) : "(verbose only) ";
246 res += xbt::string_printf("[(%ld)%s (%s) ", src->get_pid(), src->get_host()->get_cname(), src->get_cname()) +
247 "-> " + xbt::string_printf("(%ld)%s (%s)])", dst->get_pid(), dst->get_host()->get_cname(), dst->get_cname());
252 std::string ActivityWaitSimcall::dot_label(int times_considered) const
254 std::string res = SimcallObserver::dot_label(times_considered);
255 res += (times_considered == -1) ? "WaitTimeout " : "Wait ";
257 auto* comm = dynamic_cast<activity::CommImpl*>(activity_);
259 auto src = comm->src_actor_;
260 auto dst = comm->dst_actor_;
261 res += " [(" + std::to_string(src ? src->get_pid() : 0) + ")";
262 res += "->(" + std::to_string(dst ? dst->get_pid() : 0) + ")]";
267 bool ActivityWaitSimcall::is_enabled() const
269 /* FIXME: check also that src and dst processes are not suspended */
270 const auto* comm = dynamic_cast<activity::CommImpl*>(activity_);
274 if (comm->src_timeout_ || comm->dst_timeout_) {
275 /* If it has a timeout it will be always be enabled (regardless of who declared the timeout),
276 * because even if the communication is not ready, it can timeout and won't block. */
277 if (_sg_mc_timeout == 1)
280 /* On the other hand if it hasn't a timeout, check if the comm is ready.*/
281 else if (comm->detached() && comm->src_actor_ == nullptr && comm->get_state() == activity::State::READY)
282 return (comm->dst_actor_ != nullptr);
283 return (comm->src_actor_ && comm->dst_actor_);
286 std::string ActivityWaitanySimcall::dot_label(int times_considered) const
288 return SimcallObserver::dot_label(times_considered) +
289 xbt::string_printf("WaitAny [%d of %zu]", times_considered + 1, activities_.size());
292 bool ActivityWaitanySimcall::is_enabled() const
294 // FIXME: deal with other kind of activities (Exec and I/Os)
295 for (auto act : activities_) {
296 const auto* comm = dynamic_cast<activity::CommImpl*>(act);
297 if (comm != nullptr && comm->src_actor_ && comm->dst_actor_)
303 int ActivityWaitanySimcall::get_max_consider() const
305 // Only Comms are of interest to MC for now. When all types of activities can be consider, this function can simply
306 // return the size of activities_.
308 for (const auto& act : activities_)
309 if (dynamic_cast<activity::CommImpl*>(act) != nullptr)
314 std::string ActivityWaitanySimcall::to_string(int times_considered) const
316 std::string res = SimcallObserver::to_string(times_considered) + "WaitAny(";
317 size_t count = activities_.size();
319 if (auto* comm = dynamic_cast<kernel::activity::CommImpl*>(activities_[times_considered]))
320 res += "comm=" + XBT_LOG_ISENABLED(mc_observer, xbt_log_priority_verbose)
321 ? xbt::string_printf("%p", comm)
322 : "(verbose only)" + xbt::string_printf("(%d of %zu))", times_considered + 1, count);
324 res += "comm at idx " + std::to_string(times_considered) + ")";
329 } // namespace kernel
330 } // namespace simgrid