Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Test the dependencies of Mutex transitions
authorMartin Quinson <martin.quinson@ens-rennes.fr>
Thu, 24 Feb 2022 12:46:20 +0000 (13:46 +0100)
committerMartin Quinson <martin.quinson@ens-rennes.fr>
Thu, 24 Feb 2022 13:01:21 +0000 (14:01 +0100)
commit2e20b9d63d8a9ca26f8b508b5cab294acc3b608a
tree48a1a79b58b5271094b0284ae8ccee5f72236ab9
parent238ba443a8fb93bf6a0d5e14265a93f443b1adab
Test the dependencies of Mutex transitions

- give each mutex an ID so that we can get reproducible debug messages.
  This is arguably a waste of resource in non-MC setups. Patch welcome.
- give one mutex per pair of actors in the test, to make the test more
  interesting for the reduction
- rework a bit the verbose output of the safety explorer
MANIFEST.in
examples/cpp/CMakeLists.txt
examples/cpp/synchro-mutex/s4u-mc-synchro-mutex.tesh
examples/cpp/synchro-mutex/s4u-synchro-mutex.cpp
src/kernel/activity/MutexImpl.cpp
src/kernel/activity/MutexImpl.hpp
src/kernel/actor/MutexObserver.cpp
src/mc/explo/SafetyChecker.cpp
src/mc/transition/TransitionSynchro.cpp