- Rework the internals, for simpler and modern code. This shall unlock many future improvements.
- You can now define plugins onto SafetyChecker (a simple DFS explorer), using the declared signals.
See CommunicationDeterminism for an example.
+ - Support mutex in DPOR reduction
- Seems to work on Arm64 architectures too.
SMPI:
(FG: issues on Framagit; GH: issues on GitHub)
- FG#100: [SMPI] Order of the message matching is not guaranteed
- FG#101: LGPL 2.1 is deprecated license
+ - GH#151: Missing mutexes for DPOR.
----------------------------------------------------------------------------
include src/mc/transition/TransitionComm.hpp
include src/mc/transition/TransitionRandom.cpp
include src/mc/transition/TransitionRandom.hpp
+include src/mc/transition/TransitionSynchro.cpp
+include src/mc/transition/TransitionSynchro.hpp
include src/mc/udpor_global.cpp
include src/mc/udpor_global.hpp
include src/msg/msg_comm.cpp
-/* Copyright (c) 2010-2022. The SimGrid Team.
- * All rights reserved. */
+/* Copyright (c) 2010-2022. The SimGrid Team. All rights reserved. */
/* 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. */
+ * under the terms of the license (GNU LGPL) which comes with this package. */
/***************** Centralized Mutual Exclusion Algorithm *********************/
/* This example implements a centralized mutual exclusion algorithm. */
/* 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 <mutex> /* std::mutex and std::lock_guard */
#include "simgrid/s4u.hpp" /* All of S4U */
+#include "simgrid/modelchecker.h" // This example is also used to test the modelchecker on mutexes
+
+#include <mutex> /* std::mutex and std::lock_guard */
-constexpr int NB_ACTOR = 6;
+int NB_ACTOR = 6;
XBT_LOG_NEW_DEFAULT_CATEGORY(s4u_test, "a sample log category");
int main(int argc, char **argv)
{
simgrid::s4u::Engine e(&argc, argv);
+
+ if (MC_is_active()) // Reduce the size of that test when running in the model-checker
+ NB_ACTOR = 2;
+
e.load_platform("../../platforms/two_hosts.xml");
simgrid::s4u::Actor::create("main", e.host_by_name("Tremblay"), master);
e.run();
}
#endif
-MutexObserver::MutexObserver(ActorImpl* actor, activity::MutexImpl* mutex) : SimcallObserver(actor), mutex_(mutex) {}
-MutexTestObserver::MutexTestObserver(ActorImpl* actor, activity::MutexImpl* mutex) : MutexObserver(actor, mutex) {}
-
-MutexLockAsyncObserver::MutexLockAsyncObserver(ActorImpl* actor, activity::MutexImpl* mutex)
- : MutexObserver(actor, mutex)
+MutexObserver::MutexObserver(ActorImpl* actor, mc::Transition::Type type, activity::MutexImpl* mutex)
+ : SimcallObserver(actor), type_(type), mutex_(mutex)
{
}
-MutexLockWaitObserver::MutexLockWaitObserver(ActorImpl* actor, activity::MutexAcquisitionImplPtr synchro)
- : MutexObserver(actor, synchro->get_mutex().get()), synchro_(synchro)
+
+void MutexObserver::serialize(std::stringstream& stream) const
{
+ auto* owner = get_mutex()->get_owner();
+ stream << (short)type_ << ' ' << (uintptr_t)get_mutex() << ' ' << (owner != nullptr ? owner->get_pid() : -1);
}
-bool MutexLockWaitObserver::is_enabled()
+bool MutexObserver::is_enabled()
{
- return synchro_->test();
+ // Only wait can be disabled
+ return type_ != mc::Transition::Type::MUTEX_WAIT || mutex_->get_owner() == get_issuer();
}
} // namespace actor
namespace kernel {
namespace actor {
-/* abstract */
+/* All the observers of Mutex transitions are very similar, so implement them all together in this class */
class MutexObserver : public SimcallObserver {
- activity::MutexImpl* const mutex_;
+ mc::Transition::Type type_;
+ activity::MutexImpl* const mutex_ = nullptr;
public:
- MutexObserver(ActorImpl* actor, activity::MutexImpl* mutex);
- virtual ~MutexObserver() = default;
- activity::MutexImpl* get_mutex() const { return mutex_; }
-};
+ MutexObserver(ActorImpl* actor, mc::Transition::Type type, activity::MutexImpl* mutex);
-class MutexTestObserver : public MutexObserver {
-public:
- MutexTestObserver(ActorImpl* actor, activity::MutexImpl* mutex);
-};
-
-class MutexLockAsyncObserver : public MutexObserver {
-public:
- MutexLockAsyncObserver(ActorImpl* actor, activity::MutexImpl* mutex);
-};
-
-class MutexLockWaitObserver : public MutexObserver {
- activity::MutexAcquisitionImplPtr synchro_;
-
-public:
- MutexLockWaitObserver(ActorImpl* actor, activity::MutexAcquisitionImplPtr synchro);
+ void serialize(std::stringstream& stream) const override;
+ activity::MutexImpl* get_mutex() const { return mutex_; }
bool is_enabled() override;
};
-class MutexUnlockObserver : public MutexObserver {
- using MutexObserver::MutexObserver;
-};
-
} // namespace actor
} // namespace kernel
} // namespace simgrid
#include "src/mc/transition/TransitionAny.hpp"
#include "src/mc/transition/TransitionComm.hpp"
#include "src/mc/transition/TransitionRandom.hpp"
+#include "src/mc/transition/TransitionSynchro.hpp"
#endif
#include <sstream>
case Transition::Type::RANDOM:
return new RandomTransition(issuer, times_considered, stream);
+ case Transition::Type::MUTEX_TRYLOCK:
+ case Transition::Type::MUTEX_LOCK:
+ case Transition::Type::MUTEX_TEST:
+ case Transition::Type::MUTEX_WAIT:
+ case Transition::Type::MUTEX_UNLOCK:
+ return new MutexTransition(issuer, times_considered, simcall, stream);
+
case Transition::Type::UNKNOWN:
return new Transition(Transition::Type::UNKNOWN, issuer, times_considered);
}
public:
/* Ordering is important here. depends() implementations only consider subsequent types in this ordering */
- XBT_DECLARE_ENUM_CLASS(Type, RANDOM, TESTANY, WAITANY, COMM_RECV, COMM_SEND, COMM_TEST, COMM_WAIT,
+ XBT_DECLARE_ENUM_CLASS(Type, RANDOM, /* First because indep with anybody */
+ 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 */
/* UNKNOWN must be last */ UNKNOWN);
Type type_ = Type::UNKNOWN;
--- /dev/null
+/* Copyright (c) 2015-2022. The SimGrid Team. All rights reserved. */
+
+/* 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 "src/mc/transition/TransitionSynchro.hpp"
+#include "xbt/asserts.h"
+#include "xbt/string.hpp"
+
+#include <inttypes.h>
+#include <sstream>
+
+XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_trans_synchro, mc_transition, "Logging specific to MC synchronization transitions");
+
+namespace simgrid {
+namespace mc {
+std::string MutexTransition::to_string(bool verbose) const
+{
+ return xbt::string_printf("%s(%" PRIxPTR ", owner:%ld)", Transition::to_c_str(type_), mutex_, owner_);
+}
+
+MutexTransition::MutexTransition(aid_t issuer, int times_considered, Type type, std::stringstream& stream)
+ : Transition(type, issuer, times_considered)
+{
+ xbt_assert(stream >> mutex_ >> owner_);
+}
+
+bool MutexTransition::depends(const Transition* o) const
+{
+
+ if (o->type_ < type_)
+ return o->depends(this);
+
+ // type_ <= other->type_ in MUTEX_LOCK, MUTEX_TEST, MUTEX_TRYLOCK, MUTEX_UNLOCK, MUTEX_WAIT,
+
+ if (auto* other = dynamic_cast<const MutexTransition*>(o)) {
+
+ // Theorem 4.4.7: Any pair of synchronization actions of distinct actors concerning distinct mutexes are independent
+ if (mutex_ != other->mutex_)
+ return false;
+
+ // Theorem 4.4.11: LOCK indep TEST/WAIT.
+ // If both enabled, the result does not depend on their order. If WAIT is not enabled, LOCK won't enable it.
+ if (type_ == Type::MUTEX_LOCK && (other->type_ == Type::MUTEX_TEST || other->type_ == Type::MUTEX_WAIT))
+ return false;
+
+ // Theorem 4.4.8: LOCK indep UNLOCK.
+ // pop_front and push_back are independent.
+ if (type_ == Type::MUTEX_LOCK && other->type_ == Type::MUTEX_UNLOCK)
+ return false;
+
+ // TEST is a pure function; TEST/WAIT won't change the owner; TRYLOCK will always fail if TEST is enabled (because a
+ // request is queued)
+ if (type_ == Type::MUTEX_TEST &&
+ (other->type_ == Type::MUTEX_TEST || other->type_ == Type::MUTEX_TRYLOCK || other->type_ == Type::MUTEX_WAIT))
+ return false;
+
+ // TRYLOCK will always fail if TEST is enabled (because a request is queued), and may not overpass the WAITed
+ // request in the queue
+ if (type_ == Type::MUTEX_TRYLOCK && other->type_ == Type::MUTEX_WAIT)
+ return false;
+
+ // FIXME: UNLOCK indep WAIT/TEST iff wait/test are not first in the waiting queue
+ }
+
+ return true; // FIXME: TODO
+}
+
+} // namespace mc
+} // namespace simgrid
--- /dev/null
+/* Copyright (c) 2015-2022. The SimGrid Team. All rights reserved. */
+
+/* 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. */
+
+#ifndef SIMGRID_MC_TRANSITION_SYNCHRO_HPP
+#define SIMGRID_MC_TRANSITION_SYNCHRO_HPP
+
+#include "src/mc/transition/Transition.hpp"
+
+namespace simgrid {
+namespace mc {
+
+class MutexTransition : public Transition {
+ uintptr_t mutex_;
+ aid_t owner_;
+
+public:
+ std::string to_string(bool verbose) const override;
+ MutexTransition(aid_t issuer, int times_considered, Type type, std::stringstream& stream);
+ bool depends(const Transition* other) const override;
+};
+
+} // namespace mc
+} // namespace simgrid
+
+#endif
kernel::actor::ActorImpl* issuer = kernel::actor::ActorImpl::self();
if (MC_is_active() || MC_record_replay_is_active()) { // Split in 2 simcalls for transition persistency
- kernel::actor::MutexLockAsyncObserver lock_observer{issuer, pimpl_};
+ kernel::actor::MutexObserver lock_observer{issuer, mc::Transition::Type::MUTEX_LOCK, pimpl_};
auto acquisition = kernel::actor::simcall([issuer, this] { return pimpl_->lock_async(issuer); }, &lock_observer);
- kernel::actor::MutexLockWaitObserver wait_observer{issuer, acquisition};
+ kernel::actor::MutexObserver wait_observer{issuer, mc::Transition::Type::MUTEX_WAIT, pimpl_};
kernel::actor::simcall_blocking([issuer, acquisition] { return acquisition->wait_for(issuer, -1); },
&wait_observer);
void Mutex::unlock()
{
kernel::actor::ActorImpl* issuer = kernel::actor::ActorImpl::self();
- kernel::actor::MutexUnlockObserver observer{issuer, pimpl_};
+ kernel::actor::MutexObserver observer{issuer, mc::Transition::Type::MUTEX_UNLOCK, pimpl_};
kernel::actor::simcall([this, issuer] { this->pimpl_->unlock(issuer); }, &observer);
}
bool Mutex::try_lock()
{
kernel::actor::ActorImpl* issuer = kernel::actor::ActorImpl::self();
- kernel::actor::MutexTestObserver observer{issuer, pimpl_};
+ kernel::actor::MutexObserver observer{issuer, mc::Transition::Type::MUTEX_TRYLOCK, pimpl_};
return kernel::actor::simcall([&observer] { return observer.get_mutex()->try_lock(observer.get_issuer()); },
&observer);
}
src/mc/transition/TransitionComm.hpp
src/mc/transition/TransitionRandom.cpp
src/mc/transition/TransitionRandom.hpp
+ src/mc/transition/TransitionSynchro.cpp
+ src/mc/transition/TransitionSynchro.hpp
src/mc/udpor_global.cpp
src/mc/udpor_global.hpp
)
