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/MutexObserver.hpp"
7 #include "simgrid/s4u/Host.hpp"
8 #include "src/kernel/activity/MutexImpl.hpp"
9 #include "src/kernel/actor/ActorImpl.hpp"
10 #include "src/mc/mc_config.hpp"
14 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(obs_mutex, mc_observer, "Logging specific to mutex simcalls observation");
21 bool MutexSimcall::depends(SimcallObserver* other)
23 if (dynamic_cast<RandomSimcall*>(other) != nullptr)
24 return other->depends(this); /* Other is random, that is very permissive. Use that relation instead. */
26 #if 0 /* This code is currently broken and shouldn't be used. We must implement asynchronous locks before */
27 MutexSimcall* that = dynamic_cast<MutexSimcall*>(other);
29 return true; // Depends on anything we don't know
31 /* Theorem 4.4.7: Any pair of synchronization actions of distinct actors concerning distinct mutexes are independent */
32 if (this->get_issuer() != that->get_issuer() && this->get_mutex() != that->get_mutex())
35 /* Theorem 4.4.8 An AsyncMutexLock is independent with a MutexUnlock of another actor */
36 if (((dynamic_cast<MutexLockSimcall*>(this) != nullptr && dynamic_cast<MutexUnlockSimcall*>(that)) ||
37 (dynamic_cast<MutexLockSimcall*>(that) != nullptr && dynamic_cast<MutexUnlockSimcall*>(this))) &&
38 get_issuer() != other->get_issuer())
41 return true; // Depend on things we don't know for sure that they are independent
45 MutexObserver::MutexObserver(ActorImpl* actor, mc::Transition::Type type, activity::MutexImpl* mutex)
46 : SimcallObserver(actor), type_(type), mutex_(mutex)
50 void MutexObserver::serialize(std::stringstream& stream) const
52 auto* owner = get_mutex()->get_owner();
53 stream << (short)type_ << ' ' << (uintptr_t)get_mutex() << ' ' << (owner != nullptr ? owner->get_pid() : -1);
56 bool MutexObserver::is_enabled()
58 // Only wait can be disabled
59 return type_ != mc::Transition::Type::MUTEX_WAIT || mutex_->get_owner() == get_issuer();
64 } // namespace simgrid