From 72265dbbfe57521bfa1b77cb4498afac9c3438c4 Mon Sep 17 00:00:00 2001 From: Martin Quinson Date: Sat, 1 Apr 2023 02:30:43 +0200 Subject: [PATCH] Only compile stateless MC when libevent is found --- CMakeLists.txt | 53 +++++++++++++------------- examples/cpp/CMakeLists.txt | 64 +++++++++++++++++++------------- examples/sthread/CMakeLists.txt | 18 ++++++--- include/simgrid/config.h.in | 2 + src/kernel/EngineImpl.cpp | 11 +++++- src/mc/mc_base.cpp | 5 ++- src/mc/mc_client_api.cpp | 13 +++++++ src/mc/transition/Transition.cpp | 14 ++++++- teshsuite/mc/CMakeLists.txt | 15 ++++---- teshsuite/smpi/CMakeLists.txt | 2 +- tools/cmake/DefinePackages.cmake | 9 ++++- tools/cmake/MakeLib.cmake | 24 ++++++------ tools/cmake/Option.cmake | 2 +- 13 files changed, 146 insertions(+), 86 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index a3cc8d467a..4acad42269 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -355,48 +355,46 @@ if(enable_model-checking AND minimal-bindings) message(FATAL_ERROR "Compile-time option 'minimal-bindings' cannot be enabled with 'model-checking'") endif() -if(HAVE_MMAP) - SET(HAVE_MMALLOC 1) -else() - SET(HAVE_MMALLOC 0) - if(enable_model-checking) - message(STATUS "Warning: support for model-checking has been disabled because you are missing either mmap or __thread.") - endif() - SET(enable_model-checking 0) -endif() - if(enable_mallocators) SET(SIMGRID_HAVE_MALLOCATOR 1) else() SET(SIMGRID_HAVE_MALLOCATOR 0) endif() -find_package(Libevent REQUIRED) -include_directories(${LIBEVENT_INCLUDE_DIR}) -set(SIMGRID_DEP "${SIMGRID_DEP} ${LIBEVENT_LIBRARIES}") +SET(SIMGRID_HAVE_MC 0) +SET(SIMGRID_HAVE_STATEFUL_MC 0) +SET(HAVE_MMALLOC 0) + +find_package(Libevent) +if(Libevent_FOUND) + message(STATUS "Found libevent. Stateless model-checking can be enabled.") + include_directories(${LIBEVENT_INCLUDE_DIR}) + set(SIMGRID_DEP "${SIMGRID_DEP} ${LIBEVENT_LIBRARIES}") + SET(SIMGRID_HAVE_MC 1) +else() + message(STATUS "libevent not found. Please install libevent-dev to enable the SimGrid model checker.") +endif() if(enable_model-checking) include(FindLibunwind) - if(HAVE_LIBUNWIND) - SET(SIMGRID_DEP "${SIMGRID_DEP} ${LIBUNWIND_LIBRARIES}") + find_package(Libdw) + find_package(Libelf) + if(HAVE_MMAP AND HAVE_LIBUNWIND AND Libdw_FOUND AND Libelf_FOUND) + SET(SIMGRID_HAVE_STATEFUL_MC 1) + SET(HAVE_MMALLOC 1) + SET(SIMGRID_DEP "${SIMGRID_DEP} ${LIBUNWIND_LIBRARIES} ${LIBELF_LIBRARIES} ${LIBDW_LIBRARIES}") + include_directories(${LIBDW_INCLUDE_DIR} ${LIBELF_INCLUDE_DIR}) + set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -gdwarf-4") + set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -gdwarf-4") else() - message(FATAL_ERROR "Please install libunwind-dev libdw-dev libelf-dev if you want to compile the SimGrid model checker.") + message(STATUS "Please install libunwind-dev libdw-dev libelf-dev if you want to compile the SimGrid model checker.") + set(HAVE_MMALLOC 0) endif() - find_package(Libdw REQUIRED) - find_package(Libelf REQUIRED) - include_directories(${LIBDW_INCLUDE_DIR} ${LIBELF_INCLUDE_DIR}) - set(SIMGRID_DEP "${SIMGRID_DEP} ${LIBELF_LIBRARIES} ${LIBDW_LIBRARIES}") - set(SIMGRID_HAVE_STATEFUL_MC 1) - set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -gdwarf-4") - set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -gdwarf-4") -else() - SET(SIMGRID_HAVE_STATEFUL_MC 0) - set(HAVE_MMALLOC 0) endif() mark_as_advanced(PATH_LIBDW_H) mark_as_advanced(PATH_LIBDW_LIB) -if (enable_model-checking AND enable_ns3) +if (SIMGRID_HAVE_MC AND enable_ns3) message(WARNING "Activating both model-checking and ns-3 bindings is considered experimental.") endif() @@ -938,6 +936,7 @@ message(" Compile Boost.Context support: ${HAVE_BOOST_CONTEXTS}") message("") message(" Maintainer mode .............: ${enable_maintainer_mode}") message(" Documentation ...............: ${enable_documentation}") +message(" Stateless model checking ....: ${SIMGRID_HAVE_MC}") message(" Stateful model checking .....: ${SIMGRID_HAVE_STATEFUL_MC}") message(" Graphviz mode ...............: ${HAVE_GRAPHVIZ}") message(" Mallocators .................: ${enable_mallocators}") diff --git a/examples/cpp/CMakeLists.txt b/examples/cpp/CMakeLists.txt index a0705d7032..777817c075 100644 --- a/examples/cpp/CMakeLists.txt +++ b/examples/cpp/CMakeLists.txt @@ -16,15 +16,21 @@ set(_actor-stacksize_factories "^thread") # Threads ignore modifications of the # The maestro-set example only works for threads set(_maestro-set_factories "thread") -# These tests timeout with threads, not sure why -foreach(example mc-bugged1 mc-bugged2 mc-failing-assert mc-electric-fence) - set(_${example}_factories "^thread") # Timeout - add_dependencies(tests-mc s4u-${example}) -endforeach() +if(SIMGRID_HAVE_MC) + # These tests timeout with threads, not sure why + foreach(example mc-bugged1 mc-bugged2 mc-failing-assert mc-electric-fence) + set(_${example}_factories "^thread") # Timeout + add_dependencies(tests-mc s4u-${example}) + endforeach() -if(enable_coverage) - foreach (example mc-bugged1 mc-bugged2 mc-electric-fence mc-failing-assert) - ADD_TEST(cover-${example} ${CMAKE_CURRENT_BINARY_DIR}/${example}/s4u-${example} ${CMAKE_HOME_DIRECTORY}/examples/platforms/model_checker_platform.xml) + if(enable_coverage) + foreach (example mc-bugged1 mc-bugged2 mc-electric-fence mc-failing-assert) + ADD_TEST(cover-${example} ${CMAKE_CURRENT_BINARY_DIR}/${example}/s4u-${example} ${CMAKE_HOME_DIRECTORY}/examples/platforms/model_checker_platform.xml) + endforeach() + endif() +else() + foreach (example mc-bugged1 mc-bugged2 mc-centralized-mutex mc-failing-assert mc-electric-fence) + set(_${example}_disable 1) endforeach() endif() @@ -81,21 +87,25 @@ endif() foreach (example synchro-barrier synchro-mutex synchro-semaphore) set(tesh_files ${tesh_files} ${CMAKE_CURRENT_SOURCE_DIR}/${example}/s4u-mc-${example}.tesh) - ADD_TESH(s4u-mc-${example} - --setenv bindir=${CMAKE_CURRENT_BINARY_DIR}/${example} - --setenv libdir=${CMAKE_BINARY_DIR}/lib - --setenv platfdir=${CMAKE_HOME_DIRECTORY}/examples/platforms - --setenv srcdir=${CMAKE_CURRENT_SOURCE_DIR}/${example} - --cd ${CMAKE_CURRENT_SOURCE_DIR}/${example} - ${CMAKE_HOME_DIRECTORY}/examples/cpp/${example}/s4u-mc-${example}.tesh) + if (SIMGRID_HAVE_MC) + ADD_TESH(s4u-mc-${example} + --setenv bindir=${CMAKE_CURRENT_BINARY_DIR}/${example} + --setenv libdir=${CMAKE_BINARY_DIR}/lib + --setenv platfdir=${CMAKE_HOME_DIRECTORY}/examples/platforms + --setenv srcdir=${CMAKE_CURRENT_SOURCE_DIR}/${example} + --cd ${CMAKE_CURRENT_SOURCE_DIR}/${example} + ${CMAKE_HOME_DIRECTORY}/examples/cpp/${example}/s4u-mc-${example}.tesh) - add_dependencies(tests-mc s4u-${example}) + add_dependencies(tests-mc s4u-${example}) + endif() endforeach() -# Dependency on the regular tests -foreach(example mc-centralized-mutex) - add_dependencies(tests-mc s4u-${example}) -endforeach() +if (SIMGRID_HAVE_MC) + # Dependency on the regular tests + foreach(example mc-centralized-mutex) + add_dependencies(tests-mc s4u-${example}) + endforeach() +endif() if(NOT HAVE_GRAPHVIZ) set(_dag-from-dot_disable 1) @@ -228,12 +238,14 @@ foreach(example mc-failing-assert) # ${CMAKE_HOME_DIRECTORY}/examples/cpp/${example}/s4u-${example}-statequality.tesh) # endif() - ADD_TESH(s4u-${example}-nodpor --setenv bindir=${CMAKE_CURRENT_BINARY_DIR}/${example} - --setenv libdir=${CMAKE_BINARY_DIR}/lib - --setenv platfdir=${CMAKE_HOME_DIRECTORY}/examples/platforms - --setenv srcdir=${CMAKE_CURRENT_SOURCE_DIR}/${example} - --cd ${CMAKE_CURRENT_SOURCE_DIR}/${example} - ${CMAKE_HOME_DIRECTORY}/examples/cpp/${example}/s4u-${example}-nodpor.tesh) + if(SIMGRID_HAVE_MC) + ADD_TESH(s4u-${example}-nodpor --setenv bindir=${CMAKE_CURRENT_BINARY_DIR}/${example} + --setenv libdir=${CMAKE_BINARY_DIR}/lib + --setenv platfdir=${CMAKE_HOME_DIRECTORY}/examples/platforms + --setenv srcdir=${CMAKE_CURRENT_SOURCE_DIR}/${example} + --cd ${CMAKE_CURRENT_SOURCE_DIR}/${example} + ${CMAKE_HOME_DIRECTORY}/examples/cpp/${example}/s4u-${example}-nodpor.tesh) + endif() set(tesh_files ${tesh_files} ${CMAKE_HOME_DIRECTORY}/examples/cpp/${example}/s4u-${example}-statequality.tesh) set(tesh_files ${tesh_files} ${CMAKE_HOME_DIRECTORY}/examples/cpp/${example}/s4u-${example}-nodpor.tesh) endforeach() diff --git a/examples/sthread/CMakeLists.txt b/examples/sthread/CMakeLists.txt index 2b7e8234dc..98811c23ad 100644 --- a/examples/sthread/CMakeLists.txt +++ b/examples/sthread/CMakeLists.txt @@ -19,8 +19,10 @@ foreach(x add_dependencies(tests pthread-${x}) ADD_TESH_FACTORIES(pthread-${x} "^thread" --setenv libdir=${CMAKE_BINARY_DIR}/lib --cd ${CMAKE_BINARY_DIR}/examples/sthread ${CMAKE_CURRENT_SOURCE_DIR}/pthread-${x}.tesh) - add_dependencies(tests-mc pthread-${x}) - ADD_TESH_FACTORIES(pthread-mc-${x} "^thread" --setenv libdir=${CMAKE_BINARY_DIR}/lib --cd ${CMAKE_BINARY_DIR}/examples/sthread ${CMAKE_CURRENT_SOURCE_DIR}/pthread-mc-${x}.tesh) + if(SIMGRID_HAVE_MC) + add_dependencies(tests-mc pthread-${x}) + ADD_TESH_FACTORIES(pthread-mc-${x} "^thread" --setenv libdir=${CMAKE_BINARY_DIR}/lib --cd ${CMAKE_BINARY_DIR}/examples/sthread ${CMAKE_CURRENT_SOURCE_DIR}/pthread-mc-${x}.tesh) + endif() endif() set(tesh_files ${tesh_files} ${CMAKE_CURRENT_SOURCE_DIR}/pthread-${x}.tesh @@ -44,8 +46,10 @@ foreach(x target_link_libraries(pthread-${x} PUBLIC "-Wl,-znorelro -Wl,-znoseparate-code") # TODO: convert to target_link_option once CMAKE_VERSION is >3.13 endif() - add_dependencies(tests-mc pthread-${x}) - ADD_TESH_FACTORIES(pthread-mc-${x} "^thread" --setenv libdir=${CMAKE_BINARY_DIR}/lib --cd ${CMAKE_BINARY_DIR}/examples/sthread ${CMAKE_CURRENT_SOURCE_DIR}/pthread-mc-${x}.tesh) + if(SIMGRID_HAVE_MC) + add_dependencies(tests-mc pthread-${x}) + ADD_TESH_FACTORIES(pthread-mc-${x} "^thread" --setenv libdir=${CMAKE_BINARY_DIR}/lib --cd ${CMAKE_BINARY_DIR}/examples/sthread ${CMAKE_CURRENT_SOURCE_DIR}/pthread-mc-${x}.tesh) + endif() endif() set(tesh_files ${tesh_files} ${CMAKE_CURRENT_SOURCE_DIR}/pthread-mc-${x}.tesh) @@ -68,8 +72,10 @@ foreach(example endif() set_target_properties(${example} PROPERTIES RUNTIME_OUTPUT_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR}/${example}) - add_dependencies(tests-mc ${example}) - ADD_TESH_FACTORIES(sthread-mc-${example} "^thread" --setenv libdir=${CMAKE_BINARY_DIR}/lib --cd ${CMAKE_BINARY_DIR}/examples/sthread/${example} ${CMAKE_CURRENT_SOURCE_DIR}/${example}/${example}.tesh) + if(SIMGRID_HAVE_MC) + add_dependencies(tests-mc ${example}) + ADD_TESH_FACTORIES(sthread-mc-${example} "^thread" --setenv libdir=${CMAKE_BINARY_DIR}/lib --cd ${CMAKE_BINARY_DIR}/examples/sthread/${example} ${CMAKE_CURRENT_SOURCE_DIR}/${example}/${example}.tesh) + endif() endif() set(tesh_files ${tesh_files} ${CMAKE_CURRENT_SOURCE_DIR}/${example}/${example}.tesh) diff --git a/include/simgrid/config.h.in b/include/simgrid/config.h.in index 83977db9ed..bb4f27e346 100644 --- a/include/simgrid/config.h.in +++ b/include/simgrid/config.h.in @@ -11,6 +11,8 @@ /* Were mallocators (object pools) compiled in? */ #cmakedefine01 SIMGRID_HAVE_MALLOCATOR +/* Was the model-checking compiled in? */ +#cmakedefine01 SIMGRID_HAVE_MC /* Was the stateful model-checking compiled in? */ #cmakedefine01 SIMGRID_HAVE_STATEFUL_MC /* Was the ns-3 support compiled in? */ diff --git a/src/kernel/EngineImpl.cpp b/src/kernel/EngineImpl.cpp index d8ce61fac3..5a6dd12129 100644 --- a/src/kernel/EngineImpl.cpp +++ b/src/kernel/EngineImpl.cpp @@ -16,11 +16,14 @@ #include "src/mc/mc.h" #include "src/mc/mc_record.hpp" #include "src/mc/mc_replay.hpp" -#include "src/mc/remote/AppSide.hpp" #include "src/simgrid/math_utils.h" #include "src/simgrid/sg_config.hpp" #include "src/smpi/include/smpi_actor.hpp" +#if SIMGRID_HAVE_MC +#include "src/mc/remote/AppSide.hpp" +#endif + #include "xbt/log.hpp" #include @@ -168,10 +171,12 @@ void EngineImpl::initialize(int* argc, char** argv) xbt_assert(EngineImpl::instance_ == nullptr, "It is currently forbidden to create more than one instance of kernel::EngineImpl"); EngineImpl::instance_ = this; +#if SIMGRID_HAVE_MC // The communication initialization is done ASAP, as we need to get some init parameters from the MC for different // layers. But instance_ needs to be created, as we send the address of some of its fields to the MC that wants to // read them directly. simgrid::mc::AppSide::initialize(); +#endif if (static bool inited = false; not inited) { inited = true; @@ -600,7 +605,11 @@ void EngineImpl::run(double max_date) seal_platform(); if (MC_is_active()) { +#if SIMGRID_HAVE_MC mc::AppSide::get()->main_loop(); +#else + xbt_die("MC_is_active() is not supposed to return true in non-MC settings"); +#endif THROW_IMPOSSIBLE; // main_loop never returns } diff --git a/src/mc/mc_base.cpp b/src/mc/mc_base.cpp index 2c0370ec3a..8d8b66e985 100644 --- a/src/mc/mc_base.cpp +++ b/src/mc/mc_base.cpp @@ -8,11 +8,12 @@ #include "src/kernel/activity/CommImpl.hpp" #include "src/kernel/activity/MutexImpl.hpp" #include "src/kernel/actor/SimcallObserver.hpp" -#include "src/mc/api/RemoteApp.hpp" + #include "src/mc/mc.h" #include "src/mc/mc_config.hpp" #include "src/mc/mc_replay.hpp" -#include "src/mc/remote/AppSide.hpp" +/*#include "src/mc/api/RemoteApp.hpp" +#include "src/mc/remote/AppSide.hpp"*/ #if SIMGRID_HAVE_STATEFUL_MC #include "src/mc/sosp/RemoteProcessMemory.hpp" diff --git a/src/mc/mc_client_api.cpp b/src/mc/mc_client_api.cpp index fe18e7bf75..57e28cfb46 100644 --- a/src/mc/mc_client_api.cpp +++ b/src/mc/mc_client_api.cpp @@ -33,12 +33,17 @@ void MC_assert(int prop) // Cannot used xbt_assert here, or it would be an infinite recursion. xbt_assert(simgrid::mc::model_checking_mode != simgrid::mc::ModelCheckingMode::CHECKER_SIDE, "This should be called from the client side"); +#if SIMGRID_HAVE_MC if (not prop) { if (MC_is_active()) simgrid::mc::AppSide::get()->report_assertion_failure(); if (MC_record_replay_is_active()) xbt_die("MC assertion failed"); } +#else + if (not prop) + xbt_die("Safety property violation detected without the model-checker"); +#endif } int MC_is_active() @@ -49,28 +54,36 @@ int MC_is_active() void MC_automaton_new_propositional_symbol_pointer(const char *name, int* value) { +#if SIMGRID_HAVE_MC xbt_assert(simgrid::mc::model_checking_mode != simgrid::mc::ModelCheckingMode::CHECKER_SIDE, "This should be called from the client side"); simgrid::mc::AppSide::get()->declare_symbol(name, value); +#endif } void MC_ignore(void* addr, size_t size) { +#if SIMGRID_HAVE_MC xbt_assert(simgrid::mc::model_checking_mode != simgrid::mc::ModelCheckingMode::CHECKER_SIDE, "This should be called from the client side"); simgrid::mc::AppSide::get()->ignore_memory(addr, size); +#endif } void MC_ignore_heap(void *address, size_t size) { +#if SIMGRID_HAVE_MC xbt_assert(simgrid::mc::model_checking_mode != simgrid::mc::ModelCheckingMode::CHECKER_SIDE, "This should be called from the client side"); simgrid::mc::AppSide::get()->ignore_heap(address, size); +#endif } void MC_unignore_heap(void* address, size_t size) { +#if SIMGRID_HAVE_MC xbt_assert(simgrid::mc::model_checking_mode != simgrid::mc::ModelCheckingMode::CHECKER_SIDE, "This should be called from the client side"); simgrid::mc::AppSide::get()->unignore_heap(address, size); +#endif } diff --git a/src/mc/transition/Transition.cpp b/src/mc/transition/Transition.cpp index 4a8025167c..84ad991fd5 100644 --- a/src/mc/transition/Transition.cpp +++ b/src/mc/transition/Transition.cpp @@ -5,6 +5,11 @@ #include "src/mc/transition/Transition.hpp" #include "src/kernel/actor/Simcall.hpp" +#include "xbt/asserts.h" +#include "xbt/string.hpp" +#include + +#if SIMGRID_HAVE_MC #include "src/mc/explo/Exploration.hpp" #include "src/mc/transition/TransitionActorJoin.hpp" #include "src/mc/transition/TransitionAny.hpp" @@ -12,8 +17,7 @@ #include "src/mc/transition/TransitionObjectAccess.hpp" #include "src/mc/transition/TransitionRandom.hpp" #include "src/mc/transition/TransitionSynchro.hpp" -#include "xbt/asserts.h" -#include "xbt/string.hpp" +#endif #include @@ -43,12 +47,15 @@ std::string Transition::dot_string() const void Transition::replay(RemoteApp& app) const { replayed_transitions_++; +#if SIMGRID_HAVE_MC app.handle_simcall(aid_, times_considered_, false); app.wait_for_requests(); +#endif } Transition* deserialize_transition(aid_t issuer, int times_considered, std::stringstream& stream) { +#if SIMGRID_HAVE_MC short type; xbt_assert(stream >> type); @@ -101,6 +108,9 @@ Transition* deserialize_transition(aid_t issuer, int times_considered, std::stri xbt_die("Invalid transition type %d received. Did you implement a new observer in the app without implementing the " "corresponding transition in the checker?", type); +#else + xbt_die("Deserializing transitions is only interesting in MC mode."); +#endif } } // namespace simgrid::mc diff --git a/teshsuite/mc/CMakeLists.txt b/teshsuite/mc/CMakeLists.txt index dbd5479188..7addb33912 100644 --- a/teshsuite/mc/CMakeLists.txt +++ b/teshsuite/mc/CMakeLists.txt @@ -40,18 +40,19 @@ set(teshsuite_src ${teshsuite_src} set(tesh_files ${tesh_files} ${CMAKE_CURRENT_SOURCE_DIR}/random-bug/random-bug-replay.tesh ${CMAKE_CURRENT_SOURCE_DIR}/mutex-handling/without-mutex-handling.tesh PARENT_SCOPE) +ADD_TESH(mc-random-bug-replay --setenv platfdir=${CMAKE_HOME_DIRECTORY}/examples/platforms --setenv bindir=${CMAKE_BINARY_DIR}/teshsuite/mc/random-bug --cd ${CMAKE_HOME_DIRECTORY}/teshsuite/mc/random-bug random-bug-replay.tesh) +IF(SIMGRID_HAVE_MC) + ADD_TESH(tesh-mc-mutex-handling --setenv bindir=${CMAKE_BINARY_DIR}/teshsuite/mc/mutex-handling --setenv srcdir=${CMAKE_HOME_DIRECTORY} --cd ${CMAKE_HOME_DIRECTORY}/teshsuite/mc/mutex-handling mutex-handling.tesh --cfg=model-check/reduction:none) + ADD_TESH(tesh-mc-mutex-handling-dpor --setenv bindir=${CMAKE_BINARY_DIR}/teshsuite/mc/mutex-handling --setenv srcdir=${CMAKE_HOME_DIRECTORY} --cd ${CMAKE_HOME_DIRECTORY}/teshsuite/mc/mutex-handling mutex-handling.tesh --cfg=model-check/reduction:dpor) + ADD_TESH(tesh-mc-without-mutex-handling --setenv bindir=${CMAKE_BINARY_DIR}/teshsuite/mc/mutex-handling --setenv srcdir=${CMAKE_HOME_DIRECTORY} --cd ${CMAKE_HOME_DIRECTORY}/teshsuite/mc/mutex-handling without-mutex-handling.tesh --cfg=model-check/reduction:none) + ADD_TESH(tesh-mc-without-mutex-handling-dpor --setenv bindir=${CMAKE_BINARY_DIR}/teshsuite/mc/mutex-handling --setenv srcdir=${CMAKE_HOME_DIRECTORY} --cd ${CMAKE_HOME_DIRECTORY}/teshsuite/mc/mutex-handling without-mutex-handling.tesh --cfg=model-check/reduction:dpor) + ADD_TESH(mc-random-bug --setenv platfdir=${CMAKE_HOME_DIRECTORY}/examples/platforms --setenv bindir=${CMAKE_BINARY_DIR}/teshsuite/mc/random-bug --cd ${CMAKE_HOME_DIRECTORY}/teshsuite/mc/random-bug random-bug.tesh) +ENDIF() IF(SIMGRID_HAVE_STATEFUL_MC) ADD_TESH(tesh-mc-dwarf --setenv bindir=${CMAKE_BINARY_DIR}/teshsuite/mc/dwarf --cd ${CMAKE_HOME_DIRECTORY}/teshsuite/mc/dwarf dwarf.tesh) ADD_TESH(tesh-mc-dwarf-expression --setenv bindir=${CMAKE_BINARY_DIR}/teshsuite/mc/dwarf-expression --cd ${CMAKE_HOME_DIRECTORY}/teshsuite/mc/dwarf-expression dwarf-expression.tesh) ENDIF() -ADD_TESH(tesh-mc-mutex-handling --setenv bindir=${CMAKE_BINARY_DIR}/teshsuite/mc/mutex-handling --setenv srcdir=${CMAKE_HOME_DIRECTORY} --cd ${CMAKE_HOME_DIRECTORY}/teshsuite/mc/mutex-handling mutex-handling.tesh --cfg=model-check/reduction:none) -ADD_TESH(tesh-mc-mutex-handling-dpor --setenv bindir=${CMAKE_BINARY_DIR}/teshsuite/mc/mutex-handling --setenv srcdir=${CMAKE_HOME_DIRECTORY} --cd ${CMAKE_HOME_DIRECTORY}/teshsuite/mc/mutex-handling mutex-handling.tesh --cfg=model-check/reduction:dpor) -ADD_TESH(tesh-mc-without-mutex-handling --setenv bindir=${CMAKE_BINARY_DIR}/teshsuite/mc/mutex-handling --setenv srcdir=${CMAKE_HOME_DIRECTORY} --cd ${CMAKE_HOME_DIRECTORY}/teshsuite/mc/mutex-handling without-mutex-handling.tesh --cfg=model-check/reduction:none) -ADD_TESH(tesh-mc-without-mutex-handling-dpor --setenv bindir=${CMAKE_BINARY_DIR}/teshsuite/mc/mutex-handling --setenv srcdir=${CMAKE_HOME_DIRECTORY} --cd ${CMAKE_HOME_DIRECTORY}/teshsuite/mc/mutex-handling without-mutex-handling.tesh --cfg=model-check/reduction:dpor) -ADD_TESH(mc-random-bug --setenv platfdir=${CMAKE_HOME_DIRECTORY}/examples/platforms --setenv bindir=${CMAKE_BINARY_DIR}/teshsuite/mc/random-bug --cd ${CMAKE_HOME_DIRECTORY}/teshsuite/mc/random-bug random-bug.tesh) -ADD_TESH(mc-random-bug-replay --setenv platfdir=${CMAKE_HOME_DIRECTORY}/examples/platforms --setenv bindir=${CMAKE_BINARY_DIR}/teshsuite/mc/random-bug --cd ${CMAKE_HOME_DIRECTORY}/teshsuite/mc/random-bug random-bug-replay.tesh) - if(enable_coverage) ADD_TEST(cover-mc-mutex-handling ${CMAKE_CURRENT_BINARY_DIR}/mutex-handling/mutex-handling ${CMAKE_HOME_DIRECTORY}/examples/platforms/small_platform.xml) endif() diff --git a/teshsuite/smpi/CMakeLists.txt b/teshsuite/smpi/CMakeLists.txt index be774532ff..ce735edf2a 100644 --- a/teshsuite/smpi/CMakeLists.txt +++ b/teshsuite/smpi/CMakeLists.txt @@ -141,7 +141,7 @@ if(enable_smpi) if (NOT HAVE_SANITIZER_ADDRESS) ADD_TESH(tesh-smpi-coll-allreduce-with-leaks --setenv platfdir=${CMAKE_HOME_DIRECTORY}/examples/platforms --setenv bindir=${CMAKE_BINARY_DIR}/teshsuite/smpi/coll-allreduce-with-leaks --cd ${CMAKE_BINARY_DIR}/teshsuite/smpi/coll-allreduce-with-leaks ${CMAKE_HOME_DIRECTORY}/teshsuite/smpi/coll-allreduce-with-leaks/coll-allreduce-with-leaks.tesh) set_target_properties(coll-allreduce-with-leaks PROPERTIES COMPILE_FLAGS "-trace-call-location") - if(enable_model-checking) + if(SIMGRID_HAVE_MC) add_dependencies(tests-mc coll-allreduce-with-leaks) ADD_TESH(tesh-mc-smpi-coll-allreduce-with-leaks --setenv platfdir=${CMAKE_HOME_DIRECTORY}/examples/platforms --setenv bindir=${CMAKE_BINARY_DIR}/teshsuite/smpi/coll-allreduce-with-leaks --cd ${CMAKE_BINARY_DIR}/teshsuite/smpi/coll-allreduce-with-leaks ${CMAKE_HOME_DIRECTORY}/teshsuite/smpi/coll-allreduce-with-leaks/mc-coll-allreduce-with-leaks.tesh) endif() diff --git a/tools/cmake/DefinePackages.cmake b/tools/cmake/DefinePackages.cmake index 9e2200f21f..8492f25db9 100644 --- a/tools/cmake/DefinePackages.cmake +++ b/tools/cmake/DefinePackages.cmake @@ -518,13 +518,15 @@ set(MC_SRC_BASE src/mc/mc_record.hpp src/mc/mc_replay.hpp src/mc/transition/Transition.cpp - + ) + +set(MC_SRC_STATELESS src/mc/api/ActorState.hpp src/mc/api/State.cpp src/mc/api/State.hpp src/mc/api/RemoteApp.cpp src/mc/api/RemoteApp.hpp - + src/mc/explo/DFSExplorer.cpp src/mc/explo/DFSExplorer.hpp src/mc/explo/Exploration.cpp @@ -769,6 +771,9 @@ if(enable_smpi) set(simgrid_sources ${simgrid_sources} ${SMPI_SRC}) endif() +if(SIMGRID_HAVE_MC) + set(simgrid_sources ${simgrid_sources} ${MC_SRC_STATELESS}) +endif() if(SIMGRID_HAVE_STATEFUL_MC) set(simgrid_sources ${simgrid_sources} ${MC_SRC_STATEFUL}) endif() diff --git a/tools/cmake/MakeLib.cmake b/tools/cmake/MakeLib.cmake index 5575bb7188..f41f3b70af 100644 --- a/tools/cmake/MakeLib.cmake +++ b/tools/cmake/MakeLib.cmake @@ -42,17 +42,19 @@ if(HAVE_MMALLOC) APPEND PROPERTY INCLUDE_DIRECTORIES "${INTERNAL_INCLUDES}") endif() -add_executable(simgrid-mc ${MC_SIMGRID_MC_SRC}) -target_link_libraries(simgrid-mc simgrid) -set_target_properties(simgrid-mc - PROPERTIES RUNTIME_OUTPUT_DIRECTORY "${CMAKE_BINARY_DIR}/bin") -set_property(TARGET simgrid-mc - APPEND PROPERTY INCLUDE_DIRECTORIES "${INTERNAL_INCLUDES}") -install(TARGETS simgrid-mc # install that binary without breaking the rpath on Mac - RUNTIME DESTINATION ${CMAKE_INSTALL_BINDIR}/) -add_dependencies(tests-mc simgrid-mc) -if("${CMAKE_SYSTEM}" MATCHES "Linux") - add_dependencies(tests-mc sthread) +if(SIMGRID_HAVE_MC) + add_executable(simgrid-mc ${MC_SIMGRID_MC_SRC}) + target_link_libraries(simgrid-mc simgrid) + set_target_properties(simgrid-mc + PROPERTIES RUNTIME_OUTPUT_DIRECTORY "${CMAKE_BINARY_DIR}/bin") + set_property(TARGET simgrid-mc + APPEND PROPERTY INCLUDE_DIRECTORIES "${INTERNAL_INCLUDES}") + install(TARGETS simgrid-mc # install that binary without breaking the rpath on Mac + RUNTIME DESTINATION ${CMAKE_INSTALL_BINDIR}/) + add_dependencies(tests-mc simgrid-mc) + if("${CMAKE_SYSTEM}" MATCHES "Linux") + add_dependencies(tests-mc sthread) + endif() endif() # Compute the dependencies of SimGrid diff --git a/tools/cmake/Option.cmake b/tools/cmake/Option.cmake index 0ff2fcca26..19e3248d71 100644 --- a/tools/cmake/Option.cmake +++ b/tools/cmake/Option.cmake @@ -38,7 +38,7 @@ endif() option(minimal-bindings "Whether to compile the Python bindings libraries with the minimal dependency set" off) mark_as_advanced(minimal-bindings) -option(enable_model-checking "Turn this on to experiment with our prototype of model-checker (hinders the simulation's performance even if turned off at runtime)" off) +option(enable_model-checking "Turn this on to experiment with our prototype of model-checker" on) option(enable-model-checking "Please set 'enable_model-checking' instead" off) mark_as_advanced(enable-model-checking) if(enable-model-checking) -- 2.20.1