X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/33adf3c6e189e468c9a55f1f7bc7d891b0700e1a..8d0b1f2f1840a16bb9551f1cfd74f2488599f95b:/src/kernel/actor/SimcallObserver.cpp diff --git a/src/kernel/actor/SimcallObserver.cpp b/src/kernel/actor/SimcallObserver.cpp index 8ecb3ee221..d7657a4bcd 100644 --- a/src/kernel/actor/SimcallObserver.cpp +++ b/src/kernel/actor/SimcallObserver.cpp @@ -1,72 +1,30 @@ -/* Copyright (c) 2019-2021. The SimGrid Team. All rights reserved. */ +/* Copyright (c) 2019-2023. The SimGrid Team. All rights reserved. */ /* This program is free software; you can redistribute it and/or modify it * under the terms of the license (GNU LGPL) which comes with this package. */ #include "src/kernel/actor/SimcallObserver.hpp" #include "simgrid/s4u/Host.hpp" +#include "src/kernel/activity/CommImpl.hpp" +#include "src/kernel/activity/MailboxImpl.hpp" #include "src/kernel/activity/MutexImpl.hpp" #include "src/kernel/actor/ActorImpl.hpp" +#include "src/mc/mc_config.hpp" -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; +#include - /* 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()); -} +XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_observer, mc, "Logging specific to MC simcall observation"); -std::string SimcallObserver::dot_label() const -{ - if (issuer_->get_host()) - return xbt::string_printf("[(%ld)%s] ", issuer_->get_pid(), issuer_->get_cname()); - return xbt::string_printf("[(%ld)] ", issuer_->get_pid()); -} +namespace simgrid::kernel::actor { -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) + ")"; + stream << (short)mc::Transition::Type::RANDOM << ' '; + stream << min_ << ' ' << max_; } - -std::string RandomSimcall::dot_label() const +std::string RandomSimcall::to_string() const { - return SimcallObserver::dot_label() + "MC_RANDOM(" + std::to_string(next_value_) + ")"; + return "Random(min:" + std::to_string(min_) + " max:" + std::to_string(max_) + ")"; } void RandomSimcall::prepare(int times_considered) @@ -80,104 +38,50 @@ int RandomSimcall::get_max_consider() const return max_ - min_ + 1; } -std::string MutexUnlockSimcall::to_string(int times_considered) const -{ - return SimcallObserver::to_string(times_considered) + "Mutex UNLOCK"; -} - -std::string MutexUnlockSimcall::dot_label() const -{ - return SimcallObserver::dot_label() + "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() const -{ - return SimcallObserver::dot_label() + (blocking_ ? "Mutex LOCK" : "Mutex TRYLOCK"); -} - -bool MutexLockSimcall::is_enabled() const +ActorJoinSimcall::ActorJoinSimcall(ActorImpl* actor, ActorImpl* other, double timeout) + : SimcallObserver(actor), other_(s4u::ActorPtr(other->get_iface())), timeout_(timeout) { - return not blocking_ || get_mutex()->get_owner() == nullptr || get_mutex()->get_owner() == get_issuer(); } - -std::string ConditionWaitSimcall::to_string(int times_considered) const +bool ActorJoinSimcall::is_enabled() { - std::string res = SimcallObserver::to_string(times_considered) + "Condition WAIT"; - res += "(" + (timeout_ == -1.0 ? "" : std::to_string(timeout_)) + ")"; - return res; + return other_->get_impl()->wannadie(); } - -std::string ConditionWaitSimcall::dot_label() const -{ - return SimcallObserver::dot_label() + "Condition WAIT"; -} - -bool ConditionWaitSimcall::is_enabled() const +void ActorJoinSimcall::serialize(std::stringstream& stream) const { - static bool warned = false; - if (not warned) { - XBT_INFO("Using condition variables in model-checked code is still experimental. Use at your own risk"); - warned = true; - } - return true; + stream << (short)mc::Transition::Type::ACTOR_JOIN << ' '; + stream << other_->get_pid() << ' ' << (timeout_ > 0); } - -std::string SemAcquireSimcall::to_string(int times_considered) const +std::string ActorJoinSimcall::to_string() const { - std::string res = SimcallObserver::to_string(times_considered) + "Sem ACQUIRE"; - res += "(" + (timeout_ == -1.0 ? "" : std::to_string(timeout_)) + ")"; - return res; + return "ActorJoin(pid:" + std::to_string(other_->get_pid()) + ")"; } - -std::string SemAcquireSimcall::dot_label() const +void ActorSleepSimcall::serialize(std::stringstream& stream) const { - return SimcallObserver::dot_label() + "Sem ACQUIRE"; + stream << (short)mc::Transition::Type::ACTOR_SLEEP; } -bool SemAcquireSimcall::is_enabled() const +std::string ActorSleepSimcall::to_string() 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; + return "ActorSleep()"; } -std::string ExecutionWaitanySimcall::to_string(int times_considered) const +void ObjectAccessSimcallObserver::serialize(std::stringstream& stream) const { - std::string res = SimcallObserver::to_string(times_considered) + "Execution WAITANY"; - res += "(" + (timeout_ == -1.0 ? "" : std::to_string(timeout_)) + ")"; - return res; + stream << (short)mc::Transition::Type::OBJECT_ACCESS << ' '; + stream << object_ << ' ' << get_owner()->get_pid(); } - -std::string ExecutionWaitanySimcall::dot_label() const +std::string ObjectAccessSimcallObserver::to_string() const { - return SimcallObserver::dot_label() + "Execution WAITANY"; + return "ObjectAccess(obj:" + ptr_to_id(object_) + + " owner:" + std::to_string(get_owner()->get_pid()) + ")"; } - -std::string IoWaitanySimcall::to_string(int times_considered) const +bool ObjectAccessSimcallObserver::is_visible() const { - std::string res = SimcallObserver::to_string(times_considered) + "I/O WAITANY"; - res += "(" + (timeout_ == -1.0 ? "" : std::to_string(timeout_)) + ")"; - return res; + return get_owner() != get_issuer(); } - -std::string IoWaitanySimcall::dot_label() const +ActorImpl* ObjectAccessSimcallObserver::get_owner() const { - return SimcallObserver::dot_label() + "I/O WAITANY"; + return object_->simcall_owner_; } -} // namespace actor -} // namespace kernel -} // namespace simgrid +} // namespace simgrid::kernel::actor