1 /* Copyright (c) 2019-2021. 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/mc/checker/SimcallObserver.hpp"
7 #include "simgrid/s4u/Host.hpp"
8 #include "src/kernel/activity/MutexImpl.hpp"
9 #include "src/kernel/actor/ActorImpl.hpp"
11 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_observer, mc, "Logging specific to MC simcall observation");
16 std::string SimcallObserver::to_string(int /*time_considered*/) const
18 return simgrid::xbt::string_printf("[(%ld)%s (%s)] ", issuer_->get_pid(), issuer_->get_host()->get_cname(),
19 issuer_->get_cname());
22 std::string SimcallObserver::dot_label() const
24 if (issuer_->get_host())
25 return xbt::string_printf("[(%ld)%s] ", issuer_->get_pid(), issuer_->get_cname());
26 return xbt::string_printf("[(%ld)] ", issuer_->get_pid());
29 std::string RandomSimcall::to_string(int time_considered) const
31 return SimcallObserver::to_string(time_considered) + "MC_RANDOM(" + std::to_string(time_considered) + ")";
34 std::string RandomSimcall::dot_label() const
36 return SimcallObserver::dot_label() + "MC_RANDOM(" + std::to_string(next_value_) + ")";
39 void RandomSimcall::prepare(int times_considered)
41 next_value_ = min_ + times_considered;
42 XBT_DEBUG("MC_RANDOM(%d, %d) will return %d after %d times", min_, max_, next_value_, times_considered);
45 int RandomSimcall::get_max_consider() const
47 return max_ - min_ + 1;
50 std::string MutexUnlockSimcall::to_string(int time_considered) const
52 return SimcallObserver::to_string(time_considered) + "Mutex UNLOCK";
55 std::string MutexUnlockSimcall::dot_label() const
57 return SimcallObserver::dot_label() + "Mutex UNLOCK";
60 std::string MutexLockSimcall::to_string(int time_considered) const
62 std::string res = SimcallObserver::to_string(time_considered) + (blocking_ ? "Mutex LOCK" : "Mutex TRYLOCK");
63 res += "(locked = " + std::to_string(mutex_->is_locked());
64 res += ", owner = " + std::to_string(mutex_->get_owner() ? mutex_->get_owner()->get_pid() : -1);
65 res += ", sleeping = n/a)";
69 std::string MutexLockSimcall::dot_label() const
71 return SimcallObserver::dot_label() + (blocking_ ? "Mutex LOCK" : "Mutex TRYLOCK");
74 bool MutexLockSimcall::is_enabled() const
76 return not blocking_ || mutex_->get_owner() == nullptr || mutex_->get_owner() == get_issuer();
79 std::string ConditionWaitSimcall::to_string(int time_considered) const
81 std::string res = SimcallObserver::to_string(time_considered) + "Condition WAIT";
82 res += "(" + (timeout_ == -1.0 ? "" : std::to_string(timeout_)) + ")";
86 std::string ConditionWaitSimcall::dot_label() const
88 return SimcallObserver::dot_label() + "Condition WAIT";
91 bool ConditionWaitSimcall::is_enabled() const
93 static bool warned = false;
95 XBT_INFO("Using condition variables in model-checked code is still experimental. Use at your own risk");
101 std::string SemAcquireSimcall::to_string(int time_considered) const
103 std::string res = SimcallObserver::to_string(time_considered) + "Sem ACQUIRE";
104 res += "(" + (timeout_ == -1.0 ? "" : std::to_string(timeout_)) + ")";
108 std::string SemAcquireSimcall::dot_label() const
110 return SimcallObserver::dot_label() + "Sem ACQUIRE";
113 bool SemAcquireSimcall::is_enabled() const
115 static bool warned = false;
117 XBT_INFO("Using semaphore in model-checked code is still experimental. Use at your own risk");
123 std::string ExecutionWaitanySimcall::to_string(int time_considered) const
125 std::string res = SimcallObserver::to_string(time_considered) + "Execution WAITANY";
126 res += "(" + (timeout_ == -1.0 ? "" : std::to_string(timeout_)) + ")";
130 std::string ExecutionWaitanySimcall::dot_label() const
132 return SimcallObserver::dot_label() + "Execution WAITANY";
135 } // namespace simgrid