Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Remove the stateful model-checking from the archive. It's not working anymore
authorMartin Quinson <martin.quinson@ens-rennes.fr>
Sun, 5 Nov 2023 02:04:45 +0000 (03:04 +0100)
committerMartin Quinson <martin.quinson@ens-rennes.fr>
Sun, 5 Nov 2023 02:12:11 +0000 (03:12 +0100)
commit5f5a10db6fc4552782638abb4817041223e17775
treedbe0321a993368c0422919ce18a02c1ab8afaa1e
parent9a4ec91cc24a9a54ff3a060cc2828ac54d0c0c26
Remove the stateful model-checking from the archive. It's not working anymore

It's a real pity to remove all this great code, as it was doing very
audacious things, but I need to do so to move forward. This code is
very fragile and badly tested, making it very difficult to build upon.

The next time this is implemented (if any), I guess that a
compiler-approach (e.g. a clang plugin providing a full introspection
over the compiled program) would be more robust than a fully runtime
approach tricking with the debug information to get the info. That's
too difficult and fragile.

Again, I'm deeply sorry I had to remove this code, as it requires me
to admit that I failed to maintain this great code over the years.
But facts are stubborn.
152 files changed:
.github/workflows/git.yml
CMakeLists.txt
MANIFEST.in
docs/source/Configuring_SimGrid.rst
docs/source/Installing_SimGrid.rst
docs/source/Tutorial_Model-checking.rst
examples/cpp/CMakeLists.txt
examples/cpp/mc-bugged1-liveness/promela_bugged1_liveness [deleted file]
examples/cpp/mc-bugged1-liveness/s4u-mc-bugged1-liveness-stack-cleaner [deleted file]
examples/cpp/mc-bugged1-liveness/s4u-mc-bugged1-liveness-visited.tesh [deleted file]
examples/cpp/mc-bugged1-liveness/s4u-mc-bugged1-liveness.cpp [deleted file]
examples/cpp/mc-bugged1-liveness/s4u-mc-bugged1-liveness.tesh [deleted file]
examples/cpp/mc-bugged2-liveness/promela_bugged2_liveness [deleted file]
examples/cpp/mc-bugged2-liveness/s4u-mc-bugged2-liveness.cpp [deleted file]
examples/cpp/mc-bugged2-liveness/s4u-mc-bugged2-liveness.tesh [deleted file]
examples/cpp/mc-failing-assert/s4u-mc-failing-assert-statequality.tesh [deleted file]
examples/cpp/synchro-mutex/s4u-mc-synchro-mutex-stateful.tesh [deleted file]
examples/smpi/CMakeLists.txt
examples/smpi/mc/bugged1_liveness.c [deleted file]
examples/smpi/mc/hostfile_bugged1_liveness [deleted file]
examples/smpi/mc/hostfile_non_termination [deleted file]
examples/smpi/mc/mutual_exclusion.c
examples/smpi/mc/non_termination1.c [deleted file]
examples/smpi/mc/non_termination2.c [deleted file]
examples/smpi/mc/non_termination3.c [deleted file]
examples/smpi/mc/non_termination4.c [deleted file]
examples/smpi/mc/promela_bugged1_liveness [deleted file]
examples/sthread/CMakeLists.txt
examples/sthread/pthread-mc-mutex-recursive.tesh
examples/sthread/pthread-mc-mutex-simple.tesh
examples/sthread/pthread-mc-mutex-simpledeadlock.tesh
examples/sthread/pthread-mc-producer-consumer.tesh
include/simgrid/config.h.in
include/simgrid/modelchecker.h
include/smpi/smpi_extended_traces.h
include/smpi/smpi_extended_traces_fortran.h
src/internal_config.h.in
src/kernel/activity/CommImpl.cpp
src/kernel/activity/CommImpl.hpp
src/kernel/activity/MailboxImpl.hpp
src/kernel/context/Context.cpp
src/kernel/context/Context.hpp
src/kernel/context/ContextRaw.cpp
src/kernel/context/ContextSwapped.cpp
src/kernel/context/ContextUnix.cpp
src/mc/AddressSpace.hpp [deleted file]
src/mc/VisitedState.cpp [deleted file]
src/mc/VisitedState.hpp [deleted file]
src/mc/api/RemoteApp.cpp
src/mc/api/RemoteApp.hpp
src/mc/api/State.cpp
src/mc/api/State.hpp
src/mc/compare.cpp [deleted file]
src/mc/explo/CommunicationDeterminismChecker.cpp
src/mc/explo/DFSExplorer.cpp
src/mc/explo/DFSExplorer.hpp
src/mc/explo/Exploration.cpp
src/mc/explo/Exploration.hpp
src/mc/explo/LivenessChecker.cpp [deleted file]
src/mc/explo/LivenessChecker.hpp [deleted file]
src/mc/explo/UdporChecker.cpp
src/mc/explo/simgrid_mc.cpp
src/mc/inspect/DwarfExpression.cpp [deleted file]
src/mc/inspect/DwarfExpression.hpp [deleted file]
src/mc/inspect/Frame.cpp [deleted file]
src/mc/inspect/Frame.hpp [deleted file]
src/mc/inspect/LocationList.cpp [deleted file]
src/mc/inspect/LocationList.hpp [deleted file]
src/mc/inspect/ObjectInformation.cpp [deleted file]
src/mc/inspect/ObjectInformation.hpp [deleted file]
src/mc/inspect/Type.hpp [deleted file]
src/mc/inspect/Variable.hpp [deleted file]
src/mc/inspect/mc_dwarf.cpp [deleted file]
src/mc/inspect/mc_dwarf.hpp [deleted file]
src/mc/inspect/mc_dwarf_attrnames.cpp [deleted file]
src/mc/inspect/mc_dwarf_tagnames.cpp [deleted file]
src/mc/inspect/mc_member.cpp [deleted file]
src/mc/inspect/mc_unw.cpp [deleted file]
src/mc/inspect/mc_unw.hpp [deleted file]
src/mc/inspect/mc_unw_vmread.cpp [deleted file]
src/mc/mc_base.cpp
src/mc/mc_client_api.cpp
src/mc/mc_config.cpp
src/mc/mc_config.hpp
src/mc/mc_environ.h
src/mc/mc_global.cpp
src/mc/remote/AppSide.cpp
src/mc/remote/AppSide.hpp
src/mc/remote/CheckerSide.cpp
src/mc/remote/CheckerSide.hpp
src/mc/remote/mc_protocol.h
src/mc/sosp/ChunkedData.cpp [deleted file]
src/mc/sosp/ChunkedData.hpp [deleted file]
src/mc/sosp/PageStore.cpp [deleted file]
src/mc/sosp/PageStore.hpp [deleted file]
src/mc/sosp/PageStore_test.cpp [deleted file]
src/mc/sosp/Region.cpp [deleted file]
src/mc/sosp/Region.hpp [deleted file]
src/mc/sosp/RemoteProcessMemory.cpp [deleted file]
src/mc/sosp/RemoteProcessMemory.hpp [deleted file]
src/mc/sosp/Snapshot.cpp [deleted file]
src/mc/sosp/Snapshot.hpp [deleted file]
src/mc/sosp/Snapshot_test.cpp [deleted file]
src/simgrid/sg_config.cpp
src/simgrid/sg_version.cpp
src/smpi/internals/smpi_actor.cpp
src/smpi/mpi/smpi_datatype.cpp
src/xbt/mmalloc/mfree.c [deleted file]
src/xbt/mmalloc/mm.c [deleted file]
src/xbt/mmalloc/mm_interface.c [deleted file]
src/xbt/mmalloc/mm_legacy.c [deleted file]
src/xbt/mmalloc/mm_module.c [deleted file]
src/xbt/mmalloc/mmalloc.c [deleted file]
src/xbt/mmalloc/mmalloc.h [deleted file]
src/xbt/mmalloc/mmalloc.info [deleted file]
src/xbt/mmalloc/mmalloc.texi [deleted file]
src/xbt/mmalloc/mmorecore.c [deleted file]
src/xbt/mmalloc/mmprivate.h [deleted file]
src/xbt/mmalloc/mrealloc.c [deleted file]
src/xbt/mmalloc/swag.c [deleted file]
src/xbt/mmalloc/swag.h [deleted file]
teshsuite/mc/CMakeLists.txt
teshsuite/mc/dwarf-expression/dwarf-expression.cpp [deleted file]
teshsuite/mc/dwarf-expression/dwarf-expression.tesh [deleted file]
teshsuite/mc/dwarf/dwarf.cpp [deleted file]
teshsuite/mc/dwarf/dwarf.tesh [deleted file]
teshsuite/mc/mcmini/barber_shop_deadlock.tesh
teshsuite/mc/mcmini/barber_shop_ok.tesh
teshsuite/mc/mcmini/philosophers_mutex_deadlock.tesh
teshsuite/mc/mcmini/philosophers_mutex_ok.tesh
teshsuite/mc/mcmini/philosophers_semaphores_deadlock.tesh
teshsuite/mc/mcmini/philosophers_semaphores_ok.tesh
teshsuite/mc/mcmini/producer_consumer_deadlock.tesh
teshsuite/mc/mcmini/producer_consumer_ok.tesh
teshsuite/mc/random-bug/random-bug.tesh
teshsuite/xbt/CMakeLists.txt
teshsuite/xbt/mmalloc/mmalloc_32.tesh [deleted file]
teshsuite/xbt/mmalloc/mmalloc_64.tesh [deleted file]
teshsuite/xbt/mmalloc/mmalloc_test.cpp [deleted file]
tools/CMakeLists.txt
tools/cmake/CTestConfig.cmake
tools/cmake/DefinePackages.cmake
tools/cmake/MakeLib.cmake
tools/cmake/Modules/FindLibdw.cmake [deleted file]
tools/cmake/Modules/FindLibelf.cmake [deleted file]
tools/cmake/Modules/FindLibunwind.cmake [deleted file]
tools/cmake/Option.cmake
tools/cmake/Tests.cmake
tools/docker/Dockerfile.build-deps
tools/docker/Dockerfile.tuto-mc
tools/generate-dwarf-functions [deleted file]
tools/simgrid.supp