activity::ActivityImplPtr waiting_synchro_ = nullptr; /* the current blocking synchro if any */
std::list<activity::ActivityImplPtr> activities_; /* the current non-blocking synchros */
s_smx_simcall simcall_;
+ std::vector<SimcallObserver*> observer_stack_;
/* list of functions executed when the process dies */
std::shared_ptr<std::vector<std::function<void(bool)>>> on_exit =
std::make_shared<std::vector<std::function<void(bool)>>>();
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<RandomSimcall*>(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<MutexSimcall*>(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<MutexLockSimcall*>(this) != nullptr && dynamic_cast<MutexUnlockSimcall*>(that)) ||
+ (dynamic_cast<MutexLockSimcall*>(that) != nullptr && dynamic_cast<MutexUnlockSimcall*>(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(),
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;
}
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
{ /* 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;
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<bool> {
}
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");
}
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);
}
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<u_smx_scalar, 11> args_ = {};
u_smx_scalar result_ = {};
