X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/e78e6b5cb3b687215d131f7110529e037dcafd29..8f7ec2e4b08cd2b27aa34b2c9fec2af0ad79d53a:/src/kernel/actor/SimcallObserver.cpp diff --git a/src/kernel/actor/SimcallObserver.cpp b/src/kernel/actor/SimcallObserver.cpp index b5f3a36d0b..b4422d5506 100644 --- a/src/kernel/actor/SimcallObserver.cpp +++ b/src/kernel/actor/SimcallObserver.cpp @@ -6,69 +6,26 @@ #include "src/kernel/actor/SimcallObserver.hpp" #include "simgrid/s4u/Host.hpp" #include "src/kernel/activity/CommImpl.hpp" -#include "src/kernel/activity/MutexImpl.hpp" +#include "src/kernel/activity/MailboxImpl.hpp" #include "src/kernel/actor/ActorImpl.hpp" #include "src/mc/mc_config.hpp" +#include + XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_observer, mc, "Logging specific to MC simcall observation"); namespace simgrid { namespace kernel { namespace actor { -bool SimcallObserver::depends(SimcallObserver* other) -{ - THROW_UNIMPLEMENTED; -} -/* Random is only dependent when issued by the same actor (ie, always independent) */ -bool RandomSimcall::depends(SimcallObserver* other) -{ - return get_issuer() == other->get_issuer(); -} -bool MutexSimcall::depends(SimcallObserver* other) -{ - if (dynamic_cast(other) != nullptr) - return other->depends(this); /* Other is random, that is very permissive. Use that relation instead. */ - -#if 0 /* This code is currently broken and shouldn't be used. We must implement asynchronous locks before */ - MutexSimcall* that = dynamic_cast(other); - if (that == nullptr) - return true; // Depends on anything we don't know - - /* Theorem 4.4.7: Any pair of synchronization actions of distinct actors concerning distinct mutexes are independent */ - if (this->get_issuer() != that->get_issuer() && this->get_mutex() != that->get_mutex()) - return false; - - /* Theorem 4.4.8 An AsyncMutexLock is independent with a MutexUnlock of another actor */ - if (((dynamic_cast(this) != nullptr && dynamic_cast(that)) || - (dynamic_cast(that) != nullptr && dynamic_cast(this))) && - get_issuer() != other->get_issuer()) - return false; -#endif - return true; // Depend on things we don't know for sure that they are independent -} - -std::string SimcallObserver::to_string(int /*times_considered*/) const -{ - return simgrid::xbt::string_printf("[(%ld)%s (%s)] ", issuer_->get_pid(), issuer_->get_host()->get_cname(), - issuer_->get_cname()); -} - -std::string SimcallObserver::dot_label(int /*times_considered*/) const +void SimcallObserver::serialize(std::stringstream& stream) const { - if (issuer_->get_host()) - return xbt::string_printf("[(%ld)%s] ", issuer_->get_pid(), issuer_->get_host()->get_cname()); - return xbt::string_printf("[(%ld)] ", issuer_->get_pid()); + stream << (short)mc::Transition::Type::UNKNOWN; } - -std::string RandomSimcall::to_string(int times_considered) const +void RandomSimcall::serialize(std::stringstream& stream) const { - return SimcallObserver::to_string(times_considered) + "MC_RANDOM(" + std::to_string(times_considered) + ")"; -} - -std::string RandomSimcall::dot_label(int times_considered) const -{ - return SimcallObserver::dot_label(times_considered) + "MC_RANDOM(" + std::to_string(next_value_) + ")"; + stream << (short)mc::Transition::Type::RANDOM << ' '; + stream << min_ << ' ' << max_; } void RandomSimcall::prepare(int times_considered) @@ -77,255 +34,19 @@ void RandomSimcall::prepare(int times_considered) XBT_DEBUG("MC_RANDOM(%d, %d) will return %d after %d times", min_, max_, next_value_, times_considered); } -int RandomSimcall::get_max_consider() const +int RandomSimcall::get_max_consider() { return max_ - min_ + 1; } -std::string MutexUnlockSimcall::to_string(int times_considered) const +bool ConditionWaitSimcall::is_enabled() { - return SimcallObserver::to_string(times_considered) + "Mutex UNLOCK"; -} - -std::string MutexUnlockSimcall::dot_label(int times_considered) const -{ - return SimcallObserver::dot_label(times_considered) + "Mutex UNLOCK"; -} - -std::string MutexLockSimcall::to_string(int times_considered) const -{ - auto mutex = get_mutex(); - std::string res = SimcallObserver::to_string(times_considered) + (blocking_ ? "Mutex LOCK" : "Mutex TRYLOCK"); - res += "(locked = " + std::to_string(mutex->is_locked()); - res += ", owner = " + std::to_string(mutex->get_owner() ? mutex->get_owner()->get_pid() : -1); - res += ", sleeping = n/a)"; - return res; -} - -std::string MutexLockSimcall::dot_label(int times_considered) const -{ - return SimcallObserver::dot_label(times_considered) + (blocking_ ? "Mutex LOCK" : "Mutex TRYLOCK"); -} - -bool MutexLockSimcall::is_enabled() const -{ - return not blocking_ || get_mutex()->get_owner() == nullptr || get_mutex()->get_owner() == get_issuer(); -} - -std::string ConditionWaitSimcall::to_string(int times_considered) const -{ - std::string res = SimcallObserver::to_string(times_considered) + "Condition WAIT"; - res += "(" + (timeout_ == -1.0 ? "" : std::to_string(timeout_)) + ")"; - return res; -} - -std::string ConditionWaitSimcall::dot_label(int times_considered) const -{ - return SimcallObserver::dot_label(times_considered) + "Condition WAIT"; -} - -bool ConditionWaitSimcall::is_enabled() const -{ - static bool warned = false; - if (not warned) { + if (static bool warned = false; not warned) { XBT_INFO("Using condition variables in model-checked code is still experimental. Use at your own risk"); warned = true; } return true; } - -std::string SemAcquireSimcall::to_string(int times_considered) const -{ - std::string res = SimcallObserver::to_string(times_considered) + "Sem ACQUIRE"; - res += "(" + (timeout_ == -1.0 ? "" : std::to_string(timeout_)) + ")"; - return res; -} - -std::string SemAcquireSimcall::dot_label(int times_considered) const -{ - return SimcallObserver::dot_label(times_considered) + "Sem ACQUIRE"; -} - -bool SemAcquireSimcall::is_enabled() const -{ - static bool warned = false; - if (not warned) { - XBT_INFO("Using semaphore in model-checked code is still experimental. Use at your own risk"); - warned = true; - } - return true; -} - -int ActivityTestanySimcall::get_max_consider() const -{ - // Only Comms are of interest to MC for now. When all types of activities can be consider, this function can simply - // return the size of activities_. - int count = 0; - for (const auto& act : activities_) - if (dynamic_cast(act) != nullptr) - count++; - return count; -} - -std::string ActivityTestanySimcall::to_string(int times_considered) const -{ - std::string res = SimcallObserver::to_string(times_considered); - if (times_considered == -1) { - res += "TestAny FALSE(-)"; - } else { - res += "TestAny(" + xbt::string_printf("(%d of %zu)", times_considered + 1, activities_.size()); - } - - return res; -} - -std::string ActivityTestanySimcall::dot_label(int times_considered) const -{ - std::string res = SimcallObserver::dot_label(times_considered) + "TestAny "; - if (times_considered == -1) { - res += "FALSE"; - } else { - res += xbt::string_printf("TRUE [%d of %zu]", times_considered + 1, activities_.size()); - } - return res; -} - -std::string ActivityTestSimcall::to_string(int times_considered) const -{ - std::string res = SimcallObserver::to_string(times_considered) + "Test "; - auto* comm = dynamic_cast(activity_); - if (comm) { - if (comm->src_actor_.get() == nullptr || comm->dst_actor_.get() == nullptr) { - res += "FALSE(comm="; - res += XBT_LOG_ISENABLED(mc_observer, xbt_log_priority_verbose) ? xbt::string_printf("%p)", comm) - : "(verbose only))"; - } else { - res += "TRUE(comm="; - - auto src = comm->src_actor_; - auto dst = comm->dst_actor_; - res += - XBT_LOG_ISENABLED(mc_observer, xbt_log_priority_verbose) ? xbt::string_printf("%p", comm) : "(verbose only) "; - res += xbt::string_printf("[(%ld)%s (%s) ", src->get_pid(), src->get_host()->get_cname(), src->get_cname()) + - "-> " + - xbt::string_printf("(%ld)%s (%s)])", dst->get_pid(), dst->get_host()->get_cname(), dst->get_cname()); - } - } - return res; -} - -std::string ActivityTestSimcall::dot_label(int times_considered) const -{ - std::string res = SimcallObserver::dot_label(times_considered) + "Test "; - auto* comm = dynamic_cast(activity_); - if (comm && (comm->src_actor_.get() == nullptr || comm->dst_actor_.get() == nullptr)) { - res += "FALSE"; - } else { - res += "TRUE"; - } - return res; -} - -std::string ActivityWaitSimcall::to_string(int times_considered) const -{ - std::string res = SimcallObserver::to_string(times_considered); - auto* comm = dynamic_cast(activity_); - if (comm == nullptr) - return res; - if (times_considered == -1) { - res += "WaitTimeout(comm=" + (XBT_LOG_ISENABLED(mc_observer, xbt_log_priority_verbose) - ? xbt::string_printf("%p)", comm) - : "(verbose only))"); - } else { - res += "Wait(comm="; - - auto src = comm->src_actor_; - auto dst = comm->dst_actor_; - res += - XBT_LOG_ISENABLED(mc_observer, xbt_log_priority_verbose) ? xbt::string_printf("%p", comm) : "(verbose only) "; - res += xbt::string_printf("[(%ld)%s (%s) ", src->get_pid(), src->get_host()->get_cname(), src->get_cname()) + - "-> " + xbt::string_printf("(%ld)%s (%s)])", dst->get_pid(), dst->get_host()->get_cname(), dst->get_cname()); - } - return res; -} - -std::string ActivityWaitSimcall::dot_label(int times_considered) const -{ - std::string res = SimcallObserver::dot_label(times_considered); - res += (times_considered == -1) ? "WaitTimeout " : "Wait "; - - auto* comm = dynamic_cast(activity_); - if (comm) { - auto src = comm->src_actor_; - auto dst = comm->dst_actor_; - res += " [(" + std::to_string(src ? src->get_pid() : 0) + ")"; - res += "->(" + std::to_string(dst ? dst->get_pid() : 0) + ")]"; - } - return res; -} - -bool ActivityWaitSimcall::is_enabled() const -{ - /* FIXME: check also that src and dst processes are not suspended */ - const auto* comm = dynamic_cast(activity_); - if (comm == nullptr) - return true; - - if (comm->src_timeout_ || comm->dst_timeout_) { - /* If it has a timeout it will be always be enabled (regardless of who declared the timeout), - * because even if the communication is not ready, it can timeout and won't block. */ - if (_sg_mc_timeout == 1) - return true; - } - /* On the other hand if it hasn't a timeout, check if the comm is ready.*/ - else if (comm->detached() && comm->src_actor_ == nullptr && comm->get_state() == activity::State::READY) - return (comm->dst_actor_ != nullptr); - return (comm->src_actor_ && comm->dst_actor_); -} - -std::string ActivityWaitanySimcall::dot_label(int times_considered) const -{ - return SimcallObserver::dot_label(times_considered) + - xbt::string_printf("WaitAny [%d of %zu]", times_considered + 1, activities_.size()); -} - -bool ActivityWaitanySimcall::is_enabled() const -{ - // FIXME: deal with other kind of activities (Exec and I/Os) - for (auto act : activities_) { - const auto* comm = dynamic_cast(act); - if (comm != nullptr && comm->src_actor_ && comm->dst_actor_) - return true; - } - return false; -} - -int ActivityWaitanySimcall::get_max_consider() const -{ - // Only Comms are of interest to MC for now. When all types of activities can be consider, this function can simply - // return the size of activities_. - int count = 0; - for (const auto& act : activities_) - if (dynamic_cast(act) != nullptr) - count++; - return count; -} - -std::string ActivityWaitanySimcall::to_string(int times_considered) const -{ - std::string res = SimcallObserver::to_string(times_considered) + "WaitAny("; - size_t count = activities_.size(); - if (count > 0) { - if (auto* comm = dynamic_cast(activities_[times_considered])) - res += "comm=" + - (XBT_LOG_ISENABLED(mc_observer, xbt_log_priority_verbose) ? xbt::string_printf("%p", comm) - : "(verbose only)") + - xbt::string_printf("(%d of %zu))", times_considered + 1, count); - } else - res += "comm at idx " + std::to_string(times_considered) + ")"; - return res; -} - } // namespace actor } // namespace kernel } // namespace simgrid