1 /* Copyright (c) 2019-2023. 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/SynchroObserver.hpp"
7 #include "simgrid/s4u/Host.hpp"
8 #include "src/kernel/activity/BarrierImpl.hpp"
9 #include "src/kernel/activity/MutexImpl.hpp"
10 #include "src/kernel/activity/SemaphoreImpl.hpp"
11 #include "src/kernel/actor/ActorImpl.hpp"
12 #include "src/mc/mc_config.hpp"
16 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(obs_mutex, mc_observer, "Logging specific to mutex simcalls observation");
18 namespace simgrid::kernel::actor {
20 MutexObserver::MutexObserver(ActorImpl* actor, mc::Transition::Type type, activity::MutexImpl* mutex)
21 : SimcallObserver(actor), type_(type), mutex_(mutex)
26 void MutexObserver::serialize(std::stringstream& stream) const
28 const auto* owner = get_mutex()->get_owner();
29 stream << (short)type_ << ' ' << get_mutex()->get_id() << ' ' << (owner != nullptr ? owner->get_pid() : -1);
31 std::string MutexObserver::to_string() const
33 return std::string(mc::Transition::to_c_str(type_)) + "(mutex_id:" + std::to_string(get_mutex()->get_id()) +
35 (get_mutex()->get_owner() == nullptr ? "none" : std::to_string(get_mutex()->get_owner()->get_pid())) + ")";
38 bool MutexObserver::is_enabled()
40 // Only wait can be disabled
41 return type_ != mc::Transition::Type::MUTEX_WAIT || mutex_->get_owner() == get_issuer();
44 SemaphoreObserver::SemaphoreObserver(ActorImpl* actor, mc::Transition::Type type, activity::SemaphoreImpl* sem)
45 : SimcallObserver(actor), type_(type), sem_(sem)
50 void SemaphoreObserver::serialize(std::stringstream& stream) const
52 stream << (short)type_ << ' ' << get_sem()->get_id() << ' ' << false /* Granted is ignored for LOCK/UNLOCK */ << ' '
53 << get_sem()->get_capacity();
55 std::string SemaphoreObserver::to_string() const
57 return std::string(mc::Transition::to_c_str(type_)) + "(sem_id:" + std::to_string(get_sem()->get_id()) + ")";
60 SemaphoreAcquisitionObserver::SemaphoreAcquisitionObserver(ActorImpl* actor, mc::Transition::Type type,
61 activity::SemAcquisitionImpl* acqui, double timeout)
62 : ResultingSimcall(actor, false), type_(type), acquisition_(acqui), timeout_(timeout)
65 bool SemaphoreAcquisitionObserver::is_enabled()
67 return acquisition_->granted_;
69 void SemaphoreAcquisitionObserver::serialize(std::stringstream& stream) const
71 stream << (short)type_ << ' ' << acquisition_->semaphore_->get_id() << ' ' << acquisition_->granted_ << ' '
72 << acquisition_->semaphore_->get_capacity();
74 std::string SemaphoreAcquisitionObserver::to_string() const
76 return std::string(mc::Transition::to_c_str(type_)) +
77 "(sem_id:" + std::to_string(acquisition_->semaphore_->get_id()) + ' ' +
78 (acquisition_->granted_ ? "granted)" : "not granted)");
81 BarrierObserver::BarrierObserver(ActorImpl* actor, mc::Transition::Type type, activity::BarrierImpl* bar)
82 : ResultingSimcall(actor, false), type_(type), barrier_(bar), timeout_(-1)
84 xbt_assert(type_ == mc::Transition::Type::BARRIER_ASYNC_LOCK);
86 BarrierObserver::BarrierObserver(ActorImpl* actor, mc::Transition::Type type, activity::BarrierAcquisitionImpl* acqui,
88 : ResultingSimcall(actor, false), type_(type), acquisition_(acqui), timeout_(timeout)
90 xbt_assert(type_ == mc::Transition::Type::BARRIER_WAIT);
92 void BarrierObserver::serialize(std::stringstream& stream) const
94 xbt_assert(barrier_ != nullptr || (acquisition_ != nullptr && acquisition_->barrier_ != nullptr));
95 stream << (short)type_ << ' ' << (barrier_ != nullptr ? barrier_->get_id() : acquisition_->barrier_->get_id());
97 std::string BarrierObserver::to_string() const
99 return std::string(mc::Transition::to_c_str(type_)) +
100 "(barrier_id:" + std::to_string(barrier_ != nullptr ? barrier_->get_id() : acquisition_->barrier_->get_id()) +
103 bool BarrierObserver::is_enabled()
105 return type_ == mc::Transition::Type::BARRIER_ASYNC_LOCK ||
106 (type_ == mc::Transition::Type::BARRIER_WAIT && acquisition_ != nullptr && acquisition_->granted_);
109 bool ConditionVariableObserver::is_enabled()
111 if (static bool warned = false; not warned) {
112 XBT_INFO("Using condition variables in model-checked code is still experimental. Use at your own risk");
117 void ConditionVariableObserver::serialize(std::stringstream& stream) const
121 std::string ConditionVariableObserver::to_string() const
123 return "ConditionWait(cond_id:" + ptr_to_id<activity::ConditionVariableImpl const>(get_cond()) +
124 " mutex_id:" + std::to_string(get_mutex()->get_id()) + ")";
127 } // namespace simgrid::kernel::actor