namespace kernel {
namespace activity {
+/* -------- Acquisition -------- */
+
bool MutexAcquisitionImpl::test(actor::ActorImpl*)
{
return mutex_->owner_ == issuer_;
simcall->issuer_->simcall_answer();
}
+/* -------- Mutex -------- */
+
unsigned MutexImpl::next_id_ = 0;
MutexAcquisitionImplPtr MutexImpl::lock_async(actor::ActorImpl* issuer)
#include "src/kernel/activity/SemaphoreImpl.hpp"
#include "src/kernel/activity/Synchro.hpp"
-#include "src/kernel/actor/SimcallObserver.hpp"
+#include "src/kernel/actor/SynchroObserver.hpp"
#include "src/kernel/resource/CpuImpl.hpp"
#include <cmath> // std::isfinite
namespace kernel {
namespace activity {
+/* -------- Acquisition -------- */
+
void SemAcquisitionImpl::wait_for(actor::ActorImpl* issuer, double timeout)
{
xbt_assert(std::isfinite(timeout), "timeout is not finite!");
cancel(); // Unregister the acquisition from the semaphore
/* Return to the englobing simcall that the wait_for timeouted */
- auto* observer = dynamic_cast<kernel::actor::SemAcquireSimcall*>(get_issuer()->simcall_.observer_);
+ auto* observer = dynamic_cast<kernel::actor::SemaphoreAcquisitionObserver*>(get_issuer()->simcall_.observer_);
xbt_assert(observer != nullptr);
observer->set_result(true);
}
"Cannot find myself in the waiting queue that I have to leave");
semaphore_->ongoing_acquisitions_.erase(it);
}
+
+/* -------- Semaphore -------- */
+unsigned SemaphoreImpl::next_id_ = 0;
+
SemAcquisitionImplPtr SemaphoreImpl::acquire_async(actor::ActorImpl* issuer)
{
auto res = SemAcquisitionImplPtr(new kernel::activity::SemAcquisitionImpl(issuer, this), true);
#include "simgrid/s4u/Semaphore.hpp"
#include "src/kernel/actor/ActorImpl.hpp"
+#include "src/kernel/actor/SynchroObserver.hpp"
namespace simgrid {
namespace kernel {
bool granted_ = false;
friend SemaphoreImpl;
+ friend actor::SemaphoreAcquisitionObserver;
public:
SemAcquisitionImpl(actor::ActorImpl* issuer, SemaphoreImpl* sem) : issuer_(issuer), semaphore_(sem) {}
unsigned int value_;
std::deque<SemAcquisitionImplPtr> ongoing_acquisitions_;
+ static unsigned next_id_;
+ unsigned id_ = next_id_++;
+
friend SemAcquisitionImpl;
+ friend actor::SemaphoreObserver;
public:
explicit SemaphoreImpl(unsigned int value) : piface_(this), value_(value){};
delete sem;
}
}
+ unsigned get_id() { return id_; }
s4u::Semaphore& sem() { return piface_; }
};
}
return true;
}
-
-bool SemAcquireSimcall::is_enabled()
-{
- 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;
-}
-
} // namespace actor
} // namespace kernel
} // namespace simgrid
double get_timeout() const { return timeout_; }
};
-class SemAcquireSimcall : public ResultingSimcall<bool> {
- activity::SemaphoreImpl* const sem_;
- const double timeout_;
-
-public:
- SemAcquireSimcall(ActorImpl* actor, activity::SemaphoreImpl* sem, double timeout = -1.0)
- : ResultingSimcall(actor, false), sem_(sem), timeout_(timeout)
- {
- }
- bool is_enabled() override;
- bool is_visible() const override { return false; }
- activity::SemaphoreImpl* get_sem() const { return sem_; }
- double get_timeout() const { return timeout_; }
-};
-
} // namespace actor
} // namespace kernel
} // namespace simgrid
#include "src/kernel/actor/SynchroObserver.hpp"
#include "simgrid/s4u/Host.hpp"
#include "src/kernel/activity/MutexImpl.hpp"
+#include "src/kernel/activity/SemaphoreImpl.hpp"
#include "src/kernel/actor/ActorImpl.hpp"
#include "src/mc/mc_config.hpp"
return type_ != mc::Transition::Type::MUTEX_WAIT || mutex_->get_owner() == get_issuer();
}
+SemaphoreObserver::SemaphoreObserver(ActorImpl* actor, mc::Transition::Type type, activity::SemaphoreImpl* sem)
+ : SimcallObserver(actor), type_(type), sem_(sem)
+{
+ xbt_assert(sem_);
+}
+
+void SemaphoreObserver::serialize(std::stringstream& stream) const
+{
+ stream << (short)type_ << ' ' << get_sem()->get_id() << ' ' << false /* Granted is ignored for LOCK/UNLOCK */;
+}
+
+SemaphoreAcquisitionObserver::SemaphoreAcquisitionObserver(ActorImpl* actor, mc::Transition::Type type,
+ activity::SemAcquisitionImpl* acqui, double timeout)
+ : ResultingSimcall(actor, false), type_(type), acquisition_(acqui), timeout_(timeout)
+{
+}
+bool SemaphoreAcquisitionObserver::is_enabled()
+{
+ return acquisition_->granted_;
+}
+void SemaphoreAcquisitionObserver::serialize(std::stringstream& stream) const
+{
+ stream << (short)type_ << ' ' << acquisition_->semaphore_->get_id() << ' ' << acquisition_->granted_;
+}
+
} // namespace actor
} // namespace kernel
} // namespace simgrid
MutexObserver(ActorImpl* actor, mc::Transition::Type type, activity::MutexImpl* mutex);
void serialize(std::stringstream& stream) const override;
+ bool is_enabled() override;
+
activity::MutexImpl* get_mutex() const { return mutex_; }
+};
+
+/* This observer is used for SEM_LOCK and SEM_UNLOCK (only) */
+class SemaphoreObserver : public SimcallObserver {
+ mc::Transition::Type type_;
+ activity::SemaphoreImpl* const sem_;
+
+public:
+ SemaphoreObserver(ActorImpl* actor, mc::Transition::Type type, activity::SemaphoreImpl* sem);
+
+ void serialize(std::stringstream& stream) const override;
+
+ activity::SemaphoreImpl* get_sem() const { return sem_; }
+};
+
+/* This observer is ued for SEM_WAIT, that is returning and needs the acquisition (in MC mode) */
+class SemaphoreAcquisitionObserver : public ResultingSimcall<bool> {
+ mc::Transition::Type type_;
+ activity::SemAcquisitionImpl* const acquisition_;
+ const double timeout_;
+
+public:
+ SemaphoreAcquisitionObserver(ActorImpl* actor, mc::Transition::Type type, activity::SemAcquisitionImpl* acqui,
+ double timeout = -1.0);
+
+ void serialize(std::stringstream& stream) const override;
bool is_enabled() override;
+
+ double get_timeout() const { return timeout_; }
};
} // namespace actor
case Transition::Type::MUTEX_UNLOCK:
return new MutexTransition(issuer, times_considered, simcall, stream);
+ case Transition::Type::SEM_LOCK:
+ case Transition::Type::SEM_UNLOCK:
+ case Transition::Type::SEM_WAIT:
+ return new SemaphoreTransition(issuer, times_considered, simcall, stream);
+
case Transition::Type::UNKNOWN:
return new Transition(Transition::Type::UNKNOWN, issuer, times_considered);
}
TESTANY, WAITANY, /* high priority because they can rewrite themselves to *_WAIT */
COMM_RECV, COMM_SEND, COMM_TEST, COMM_WAIT, /* Alphabetical ordering of COMM_* */
MUTEX_LOCK, MUTEX_TEST, MUTEX_TRYLOCK, MUTEX_UNLOCK, MUTEX_WAIT, /* alphabetical */
+ SEM_LOCK, SEM_UNLOCK, SEM_WAIT, /* alphabetical ordering of SEM transitions */
/* UNKNOWN must be last */ UNKNOWN);
Type type_ = Type::UNKNOWN;
#include "src/mc/transition/TransitionSynchro.hpp"
#include "xbt/asserts.h"
+#include "xbt/ex.h"
#include "xbt/string.hpp"
#include <inttypes.h>
return false;
// FIXME: UNLOCK indep WAIT/TEST iff wait/test are not first in the waiting queue
+ return true;
}
- return true; // FIXME: TODO
+ return false; // mutexes are INDEP with non-mutex transitions
+}
+
+std::string SemaphoreTransition::to_string(bool verbose) const
+{
+ if (type_ == Type::SEM_LOCK || type_ == Type::SEM_UNLOCK)
+ return xbt::string_printf("%s(semaphore: %" PRIxPTR ")", Transition::to_c_str(type_), sem_);
+ if (type_ == Type::SEM_WAIT)
+ return xbt::string_printf("%s(semaphore: %" PRIxPTR ", granted: %s)", Transition::to_c_str(type_), sem_,
+ granted_ ? "yes" : "no");
+ THROW_IMPOSSIBLE;
+}
+SemaphoreTransition::SemaphoreTransition(aid_t issuer, int times_considered, Type type, std::stringstream& stream)
+ : Transition(type, issuer, times_considered)
+{
+ xbt_assert(stream >> sem_ >> granted_);
+}
+bool SemaphoreTransition::depends(const Transition* o) const
+{
+ if (o->type_ < type_)
+ return o->depends(this);
+
+ if (auto* other = dynamic_cast<const SemaphoreTransition*>(o)) {
+ if (sem_ != other->sem_)
+ return false;
+
+ // LOCK indep UNLOCK: pop_front and push_back are independent.
+ if (type_ == Type::SEM_LOCK && other->type_ == Type::SEM_UNLOCK)
+ return false;
+
+ // LOCK indep WAIT: If both enabled, ordering has no impact on the result. If WAIT is not enabled, LOCK won't enable
+ // it.
+ if (type_ == Type::SEM_LOCK && other->type_ == Type::SEM_WAIT)
+ return false;
+
+ // UNLOCK indep UNLOCK: ordering of two pop_front has no impact
+ if (type_ == Type::SEM_UNLOCK && other->type_ == Type::SEM_UNLOCK)
+ return false;
+
+ // WAIT indep WAIT:
+ // if both enabled (may happen in the initial value is sufficient), the ordering has no impact on the result.
+ // If only one enabled, the other won't be enabled by the first one.
+ // If none enabled, well, nothing will change.
+ if (type_ == Type::SEM_WAIT && other->type_ == Type::SEM_WAIT)
+ return false;
+
+ return true; // Other semaphore cases are dependent
+ }
+
+ return false; // semaphores are INDEP with non-semaphore transitions
}
} // namespace mc
bool depends(const Transition* other) const override;
};
+class SemaphoreTransition : public Transition {
+ uintptr_t sem_;
+ bool granted_;
+
+public:
+ std::string to_string(bool verbose) const override;
+ SemaphoreTransition(aid_t issuer, int times_considered, Type type, std::stringstream& stream);
+ bool depends(const Transition* other) const override;
+};
+
} // namespace mc
} // namespace simgrid
#include <simgrid/modelchecker.h>
#include <simgrid/mutex.h>
#include <simgrid/s4u/Mutex.hpp>
-#include <src/kernel/activity/MutexImpl.hpp>
-#include <src/kernel/actor/SynchroObserver.hpp>
-#include <src/mc/mc_replay.hpp>
+
+#include "src/kernel/activity/MutexImpl.hpp"
+#include "src/kernel/actor/SynchroObserver.hpp"
+#include "src/mc/mc_replay.hpp"
namespace simgrid {
namespace s4u {
/* 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 <simgrid/modelchecker.h>
#include <simgrid/s4u/Semaphore.hpp>
#include <simgrid/semaphore.h>
#include "src/kernel/activity/SemaphoreImpl.hpp"
-#include "src/kernel/actor/SimcallObserver.hpp"
+#include "src/kernel/actor/SynchroObserver.hpp"
+#include "src/mc/mc_replay.hpp"
namespace simgrid {
namespace s4u {
void Semaphore::acquire()
{
- kernel::actor::ActorImpl* issuer = kernel::actor::ActorImpl::self();
- kernel::actor::SemAcquireSimcall observer{issuer, pimpl_};
- kernel::actor::simcall_blocking([this, issuer] { pimpl_->acquire_async(issuer)->wait_for(issuer, -1.0); }, &observer);
+ acquire_timeout(-1);
}
bool Semaphore::acquire_timeout(double timeout)
{
kernel::actor::ActorImpl* issuer = kernel::actor::ActorImpl::self();
- kernel::actor::SemAcquireSimcall observer{issuer, pimpl_, timeout};
- return kernel::actor::simcall_blocking(
- [this, issuer, timeout] { pimpl_->acquire_async(issuer)->wait_for(issuer, timeout); }, &observer);
+
+ if (MC_is_active() || MC_record_replay_is_active()) { // Split in 2 simcalls for transition persistency
+ kernel::actor::SemaphoreObserver lock_observer{issuer, mc::Transition::Type::SEM_LOCK, pimpl_};
+ auto acquisition =
+ kernel::actor::simcall_answered([issuer, this] { return pimpl_->acquire_async(issuer); }, &lock_observer);
+
+ kernel::actor::SemaphoreAcquisitionObserver wait_observer{issuer, mc::Transition::Type::SEM_WAIT, acquisition.get(),
+ timeout};
+ return kernel::actor::simcall_blocking(
+ [issuer, acquisition, timeout] { return acquisition->wait_for(issuer, timeout); }, &wait_observer);
+
+ } else { // Do it in one simcall only and without observer
+ kernel::actor::SemaphoreAcquisitionObserver observer{issuer, mc::Transition::Type::SEM_WAIT, nullptr, timeout};
+ return kernel::actor::simcall_blocking(
+ [this, issuer, timeout] { return pimpl_->acquire_async(issuer)->wait_for(issuer, timeout); }, &observer);
+ }
}
void Semaphore::release()
{
- kernel::actor::simcall_answered([this] { pimpl_->release(); });
+ kernel::actor::ActorImpl* issuer = kernel::actor::ActorImpl::self();
+ kernel::actor::SemaphoreObserver observer{issuer, mc::Transition::Type::SEM_UNLOCK, pimpl_};
+
+ kernel::actor::simcall_answered([this] { pimpl_->release(); }, &observer);
}
int Semaphore::get_capacity() const
{
- return kernel::actor::simcall_answered([this] { return pimpl_->get_capacity(); });
+ return pimpl_->get_capacity();
}
bool Semaphore::would_block() const
{
- return kernel::actor::simcall_answered([this] { return pimpl_->would_block(); });
+ return pimpl_->would_block();
}
/* refcounting of the intrusive_ptr is delegated to the implementation object */
