From: Martin Quinson Date: Tue, 4 May 2021 22:24:10 +0000 (+0200) Subject: MC: Start implementing the dependency functions on the AppSide (TBC) X-Git-Tag: v3.28~327 X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/33adf3c6e189e468c9a55f1f7bc7d891b0700e1a MC: Start implementing the dependency functions on the AppSide (TBC) (code committed to gather feedback: it's not used yet) Instead of one big function handling the dependencies for every kind of transition on the CheckerSide, we will split that logic between the observer subclasses and execute it on the AppSide. This will induce more latencies, but hopefully this will make the code more managable. This commit introduces a MutexSimcall observer, as we want to group MutexLock and MutexUnlock together when computing the dependencies. But we cannot use it yet, as we need to have asynchronous locks for the existing independence theorems to be usable. --- diff --git a/src/kernel/actor/ActorImpl.hpp b/src/kernel/actor/ActorImpl.hpp index aa4ec1b970..d32bea829f 100644 --- a/src/kernel/actor/ActorImpl.hpp +++ b/src/kernel/actor/ActorImpl.hpp @@ -71,6 +71,7 @@ public: activity::ActivityImplPtr waiting_synchro_ = nullptr; /* the current blocking synchro if any */ std::list activities_; /* the current non-blocking synchros */ s_smx_simcall simcall_; + std::vector observer_stack_; /* list of functions executed when the process dies */ std::shared_ptr>> on_exit = std::make_shared>>(); diff --git a/src/kernel/actor/SimcallObserver.cpp b/src/kernel/actor/SimcallObserver.cpp index 11e9e2ce6f..8ecb3ee221 100644 --- a/src/kernel/actor/SimcallObserver.cpp +++ b/src/kernel/actor/SimcallObserver.cpp @@ -14,6 +14,38 @@ 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(), @@ -60,9 +92,10 @@ std::string MutexUnlockSimcall::dot_label() const 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 += "(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; } @@ -74,7 +107,7 @@ std::string MutexLockSimcall::dot_label() const bool MutexLockSimcall::is_enabled() const { - return not blocking_ || mutex_->get_owner() == nullptr || mutex_->get_owner() == get_issuer(); + return not blocking_ || get_mutex()->get_owner() == nullptr || get_mutex()->get_owner() == get_issuer(); } std::string ConditionWaitSimcall::to_string(int times_considered) const diff --git a/src/kernel/actor/SimcallObserver.hpp b/src/kernel/actor/SimcallObserver.hpp index f2fea44594..ccc4c7b736 100644 --- a/src/kernel/actor/SimcallObserver.hpp +++ b/src/kernel/actor/SimcallObserver.hpp @@ -48,9 +48,14 @@ public: { /* Nothing to do by default */ } + /** We need to save the observer of simcalls as they get executed to later compute their dependencies in classical + * DPOR */ virtual SimcallObserver* clone() = 0; - /** Some simcalls may only be observable under some circumstances. + /** Computes the dependency relation */ + virtual bool depends(SimcallObserver* other); + + /** Some simcalls may only be observable under some conditions. * Most simcalls are not visible from the MC because they don't have an observer at all. */ virtual bool is_visible() const { return true; } virtual std::string to_string(int times_considered) const = 0; @@ -73,42 +78,50 @@ class RandomSimcall : public SimcallObserver { public: RandomSimcall(smx_actor_t actor, int min, int max) : SimcallObserver(actor), min_(min), max_(max) {} - int get_max_consider() const override; - void prepare(int times_considered) override; - std::string to_string(int times_considered) const override; - std::string dot_label() const override; - int get_value() const { return next_value_; } SimcallObserver* clone() override { auto res = new RandomSimcall(get_issuer(), min_, max_); res->next_value_ = next_value_; return res; } + int get_max_consider() const override; + void prepare(int times_considered) override; + std::string to_string(int times_considered) const override; + std::string dot_label() const override; + int get_value() const { return next_value_; } + bool depends(SimcallObserver* other) override; }; -class MutexUnlockSimcall : public SimcallObserver { - using SimcallObserver::SimcallObserver; +class MutexSimcall : public SimcallObserver { + activity::MutexImpl* const mutex_; public: - SimcallObserver* clone() override { return new MutexUnlockSimcall(get_issuer()); } + MutexSimcall(smx_actor_t actor, activity::MutexImpl* mutex) : SimcallObserver(actor), mutex_(mutex) {} + activity::MutexImpl* get_mutex() const { return mutex_; } + bool depends(SimcallObserver* other) override; +}; + +class MutexUnlockSimcall : public MutexSimcall { + using MutexSimcall::MutexSimcall; + +public: + SimcallObserver* clone() override { return new MutexUnlockSimcall(get_issuer(), get_mutex()); } std::string to_string(int times_considered) const override; std::string dot_label() const override; }; -class MutexLockSimcall : public SimcallObserver { - activity::MutexImpl* const mutex_; +class MutexLockSimcall : public MutexSimcall { const bool blocking_; public: MutexLockSimcall(smx_actor_t actor, activity::MutexImpl* mutex, bool blocking = true) - : SimcallObserver(actor), mutex_(mutex), blocking_(blocking) + : MutexSimcall(actor, mutex), blocking_(blocking) { } - SimcallObserver* clone() override { return new MutexLockSimcall(get_issuer(), mutex_, blocking_); } + SimcallObserver* clone() override { return new MutexLockSimcall(get_issuer(), get_mutex(), blocking_); } bool is_enabled() const override; std::string to_string(int times_considered) const override; std::string dot_label() const override; - activity::MutexImpl* get_mutex() const { return mutex_; } }; class ConditionWaitSimcall : public ResultingSimcall { diff --git a/src/mc/remote/AppSide.cpp b/src/mc/remote/AppSide.cpp index 88da091dbd..8622f6a175 100644 --- a/src/mc/remote/AppSide.cpp +++ b/src/mc/remote/AppSide.cpp @@ -99,9 +99,11 @@ void AppSide::handle_deadlock_check(const s_mc_message_t*) const } void AppSide::handle_simcall_execute(const s_mc_message_simcall_handle_t* message) const { - kernel::actor::ActorImpl* process = kernel::actor::ActorImpl::by_pid(message->aid_); - xbt_assert(process != nullptr, "Invalid pid %ld", message->aid_); - process->simcall_handle(message->times_considered_); + kernel::actor::ActorImpl* actor = kernel::actor::ActorImpl::by_pid(message->aid_); + xbt_assert(actor != nullptr, "Invalid pid %ld", message->aid_); + if (actor->simcall_.observer_ != nullptr) + actor->observer_stack_.push_back(actor->simcall_.observer_->clone()); + actor->simcall_handle(message->times_considered_); xbt_assert(channel_.send(MessageType::WAITING) == 0, "Could not send MESSAGE_WAITING to model-checker"); } diff --git a/src/s4u/s4u_Mutex.cpp b/src/s4u/s4u_Mutex.cpp index 832c8fb9f1..b4b29a4eef 100644 --- a/src/s4u/s4u_Mutex.cpp +++ b/src/s4u/s4u_Mutex.cpp @@ -27,7 +27,7 @@ void Mutex::lock() void Mutex::unlock() { kernel::actor::ActorImpl* issuer = kernel::actor::ActorImpl::self(); - kernel::actor::MutexUnlockSimcall observer{issuer}; + kernel::actor::MutexUnlockSimcall observer{issuer, pimpl_}; kernel::actor::simcall([this, issuer] { this->pimpl_->unlock(issuer); }, &observer); } diff --git a/src/simix/popping_private.hpp b/src/simix/popping_private.hpp index 745d0e614b..f02203c975 100644 --- a/src/simix/popping_private.hpp +++ b/src/simix/popping_private.hpp @@ -48,7 +48,8 @@ struct s_smx_simcall { smx_actor_t issuer_ = nullptr; smx_timer_t timeout_cb_ = nullptr; // Callback to timeouts simgrid::kernel::actor::SimcallObserver* observer_ = nullptr; // makes that simcall observable by the MC - unsigned int mc_max_consider_ = 0; // How many times this simcall should be used. If >1, this will be a fork. + unsigned int mc_max_consider_ = + 0; // How many times this simcall should be used. If >1, this will be a fork in the state space. int mc_value_ = 0; std::array args_ = {}; u_smx_scalar result_ = {};