From: Martin Quinson Date: Wed, 23 Feb 2022 23:41:10 +0000 (+0100) Subject: MC: Support Mutexes in DPOR X-Git-Tag: v3.31~328 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/0724fac3d997ae2f307992beb5f976fa9dec4102 MC: Support Mutexes in DPOR Fixes https://github.com/simgrid/simgrid/issues/151 --- diff --git a/ChangeLog b/ChangeLog index 6cb9aa8d8e..9776b48a65 100644 --- a/ChangeLog +++ b/ChangeLog @@ -4,6 +4,7 @@ MC: - 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: @@ -22,6 +23,7 @@ Fixed bugs (FG#.. -> FramaGit bugs; FG!.. -> FG merge requests) (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. ---------------------------------------------------------------------------- diff --git a/MANIFEST.in b/MANIFEST.in index ee5ec51a47..c66a0b18c1 100644 --- a/MANIFEST.in +++ b/MANIFEST.in @@ -2420,6 +2420,8 @@ include src/mc/transition/TransitionComm.cpp 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 diff --git a/examples/cpp/mc-centralized-mutex/s4u-mc-centralized-mutex.cpp b/examples/cpp/mc-centralized-mutex/s4u-mc-centralized-mutex.cpp index 8614d2d262..281efc177d 100644 --- a/examples/cpp/mc-centralized-mutex/s4u-mc-centralized-mutex.cpp +++ b/examples/cpp/mc-centralized-mutex/s4u-mc-centralized-mutex.cpp @@ -1,8 +1,7 @@ -/* 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. */ diff --git a/examples/cpp/synchro-mutex/s4u-synchro-mutex.cpp b/examples/cpp/synchro-mutex/s4u-synchro-mutex.cpp index f96dd70f90..9c9f45dafd 100644 --- a/examples/cpp/synchro-mutex/s4u-synchro-mutex.cpp +++ b/examples/cpp/synchro-mutex/s4u-synchro-mutex.cpp @@ -3,10 +3,12 @@ /* 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 /* 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 /* 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"); @@ -62,6 +64,10 @@ static void master() 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(); diff --git a/src/kernel/actor/MutexObserver.cpp b/src/kernel/actor/MutexObserver.cpp index 37902a0837..763ab54806 100644 --- a/src/kernel/actor/MutexObserver.cpp +++ b/src/kernel/actor/MutexObserver.cpp @@ -42,21 +42,21 @@ bool MutexSimcall::depends(SimcallObserver* other) } #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 diff --git a/src/kernel/actor/MutexObserver.hpp b/src/kernel/actor/MutexObserver.hpp index bb83761e3c..6b46645e56 100644 --- a/src/kernel/actor/MutexObserver.hpp +++ b/src/kernel/actor/MutexObserver.hpp @@ -17,38 +17,19 @@ namespace simgrid { 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 diff --git a/src/mc/transition/Transition.cpp b/src/mc/transition/Transition.cpp index 010e23b6b9..29d08ec1ba 100644 --- a/src/mc/transition/Transition.cpp +++ b/src/mc/transition/Transition.cpp @@ -13,6 +13,7 @@ #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 @@ -79,6 +80,13 @@ Transition* deserialize_transition(aid_t issuer, int times_considered, std::stri 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); } diff --git a/src/mc/transition/Transition.hpp b/src/mc/transition/Transition.hpp index eddd4045d7..96f19ca14b 100644 --- a/src/mc/transition/Transition.hpp +++ b/src/mc/transition/Transition.hpp @@ -32,7 +32,10 @@ class Transition { 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; diff --git a/src/mc/transition/TransitionSynchro.cpp b/src/mc/transition/TransitionSynchro.cpp new file mode 100644 index 0000000000..98710f84e4 --- /dev/null +++ b/src/mc/transition/TransitionSynchro.cpp @@ -0,0 +1,70 @@ +/* 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 +#include + +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(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 diff --git a/src/mc/transition/TransitionSynchro.hpp b/src/mc/transition/TransitionSynchro.hpp new file mode 100644 index 0000000000..412c0ce148 --- /dev/null +++ b/src/mc/transition/TransitionSynchro.hpp @@ -0,0 +1,27 @@ +/* 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 diff --git a/src/s4u/s4u_Mutex.cpp b/src/s4u/s4u_Mutex.cpp index 783b6c8c40..c91f07c171 100644 --- a/src/s4u/s4u_Mutex.cpp +++ b/src/s4u/s4u_Mutex.cpp @@ -19,10 +19,10 @@ void Mutex::lock() 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); @@ -38,7 +38,7 @@ void Mutex::lock() 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); } @@ -46,7 +46,7 @@ void Mutex::unlock() 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); } diff --git a/tools/cmake/DefinePackages.cmake b/tools/cmake/DefinePackages.cmake index 3a18f94d4f..4dc8fa998e 100644 --- a/tools/cmake/DefinePackages.cmake +++ b/tools/cmake/DefinePackages.cmake @@ -638,6 +638,8 @@ set(MC_SRC 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 )