From: Martin Quinson Date: Fri, 31 Mar 2023 21:48:26 +0000 (+0200) Subject: Compile the safe part of MC in default mode too X-Git-Tag: v3.34~237 X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/7a1d9713c8dd8a96686f75acb428b2e4dcb08c1f Compile the safe part of MC in default mode too Safety properties (with no checkpointing) are not requiring anything weird nowadays. Liveness properties, communication determinism and state-equality reductions are not considered safe as they still need some memory introspection black magic. --- diff --git a/CMakeLists.txt b/CMakeLists.txt index 5123dba877..4fa8107700 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -371,18 +371,21 @@ else() SET(SIMGRID_HAVE_MALLOCATOR 0) endif() +find_package(Libevent REQUIRED) +include_directories(${LIBEVENT_INCLUDE_DIR}) +set(SIMGRID_DEP "${SIMGRID_DEP} ${LIBEVENT_LIBRARIES}") + if(enable_model-checking) include(FindLibunwind) if(HAVE_LIBUNWIND) SET(SIMGRID_DEP "${SIMGRID_DEP} ${LIBUNWIND_LIBRARIES}") else() - message(FATAL_ERROR "Please install libunwind-dev libdw-dev libelf-dev libevent-dev if you want to compile the SimGrid model checker.") + message(FATAL_ERROR "Please install libunwind-dev libdw-dev libelf-dev if you want to compile the SimGrid model checker.") endif() find_package(Libdw REQUIRED) find_package(Libelf REQUIRED) - find_package(Libevent REQUIRED) - include_directories(${LIBDW_INCLUDE_DIR} ${LIBELF_INCLUDE_DIR} ${LIBEVENT_INCLUDE_DIR}) - set(SIMGRID_DEP "${SIMGRID_DEP} ${LIBEVENT_LIBRARIES} ${LIBELF_LIBRARIES} ${LIBDW_LIBRARIES}") + include_directories(${LIBDW_INCLUDE_DIR} ${LIBELF_INCLUDE_DIR}) + set(SIMGRID_DEP "${SIMGRID_DEP} ${LIBELF_LIBRARIES} ${LIBDW_LIBRARIES}") set(SIMGRID_HAVE_MC 1) set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -gdwarf-4") set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -gdwarf-4") diff --git a/docs/source/Installing_SimGrid.rst b/docs/source/Installing_SimGrid.rst index 4751ceb890..c58f470e35 100644 --- a/docs/source/Installing_SimGrid.rst +++ b/docs/source/Installing_SimGrid.rst @@ -100,8 +100,10 @@ boost recommended components (optional). - On Debian / Ubuntu: ``apt install libboost-context-dev libboost-stacktrace-dev`` python bindings (optional): - On Debian / Ubuntu: ``apt install pybind11-dev python3-dev`` -Model-checking dependencies (optional) - - On Debian / Ubuntu: ``apt install libunwind-dev libdw-dev libelf-dev libevent-dev`` +Model-checking mandatory dependencies + - On Debian / Ubuntu: ``apt install libevent-dev`` +Model-checking optional dependencies + - On Debian / Ubuntu: ``apt install libunwind-dev libdw-dev libelf-dev`` Eigen3 (optional) - On Debian / Ubuntu: ``apt install libeigen3-dev`` - On CentOS / Fedora: ``dnf install eigen3-devel`` @@ -242,7 +244,7 @@ enable_mallocators (ON/off) code, but it may fool the debuggers. enable_model-checking (on/OFF) - Activates the formal verification mode. This will hinder simulation speed even when the model checker is not activated at run + Activates the liveness verification mode. This will hinder simulation speed even when the model checker is not activated at run time, because some optimizations such as LTO must be disabled at compile time. You need to have the :ref:`required build-dependencies ` to activate this option. @@ -399,7 +401,7 @@ Windows-specific instructions ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ The best solution to get SimGrid working on windows is to install the -Ubuntu subsystem of Windows 10. All of SimGrid (but the model checker) +Ubuntu subsystem of Windows 10. All of SimGrid (but the liveness model checker) works in this setting. Native builds never really worked, and they are disabled starting with SimGrid v3.33. diff --git a/examples/cpp/CMakeLists.txt b/examples/cpp/CMakeLists.txt index 10fd24ae3b..82fcc276c8 100644 --- a/examples/cpp/CMakeLists.txt +++ b/examples/cpp/CMakeLists.txt @@ -16,13 +16,19 @@ set(_actor-stacksize_factories "^thread") # Threads ignore modifications of the # The maestro-set example only works for threads set(_maestro-set_factories "thread") -if(SIMGRID_HAVE_MC) - # These tests timeout with threads, maybe because of dwarf parsing? not sure - foreach(example mc-bugged1 mc-bugged2 mc-failing-assert mc-electric-fence) - set(_${example}_factories "^thread") # Timeout - add_dependencies(tests-mc s4u-${example}) +# 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) endforeach() +endif() +if(SIMGRID_HAVE_MC) if(HAVE_C_STACK_CLEANER) add_executable (s4u-mc-bugged1-liveness-cleaner-on EXCLUDE_FROM_ALL s4u-mc-bugged1-liveness/s4u-mc-bugged1-liveness.cpp) target_link_libraries(s4u-mc-bugged1-liveness-cleaner-on simgrid) @@ -62,15 +68,11 @@ if(SIMGRID_HAVE_MC) endif() 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() ADD_TEST(cover-mc-bugged1-liveness ${CMAKE_CURRENT_BINARY_DIR}/mc-bugged1-liveness/s4u-mc-bugged1-liveness ${CMAKE_HOME_DIRECTORY}/examples/platforms/small_platform.xml 1 1001) endif() else() - foreach (example mc-bugged1 mc-bugged2 mc-centralized-mutex mc-failing-assert mc-electric-fence - mc-bugged1-liveness mc-bugged2-liveness) + foreach (example mc-bugged1-liveness mc-bugged2-liveness) set(_${example}_disable 1) endforeach() endif() @@ -79,25 +81,21 @@ endif() foreach (example synchro-barrier synchro-mutex synchro-semaphore) set(tesh_files ${tesh_files} ${CMAKE_CURRENT_SOURCE_DIR}/${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_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}) - endif() + 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() +# Dependency on the regular tests +foreach(example mc-centralized-mutex) + add_dependencies(tests-mc s4u-${example}) +endforeach() if(NOT HAVE_GRAPHVIZ) set(_dag-from-dot_disable 1) @@ -217,25 +215,25 @@ endforeach() # Test non-DPOR reductions on a given MC test foreach(example mc-failing-assert) - if(SIMGRID_HAVE_MC) # State equality is not tested because it would take about 15 hours to run that test on my machine. # We should first optimize mmalloc_heap_differ() which takes ~4sec for each pair to compare (maybe {175 x 174/ 2} pairs here) # See the comment on mmalloc_heap_differ() in compare.cpp for more info on why it's hard to optimize. # +# if(SIMGRID_HAVE_MC) # ADD_TESH(s4u-${example}-statequality --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}-statequality.tesh) - - 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() +# 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) 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 3159ccce2e..33f0815199 100644 --- a/examples/sthread/CMakeLists.txt +++ b/examples/sthread/CMakeLists.txt @@ -12,15 +12,15 @@ foreach(x add_executable (pthread-${x} EXCLUDE_FROM_ALL pthread-${x}.c) set_target_properties(pthread-${x} PROPERTIES RUNTIME_OUTPUT_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR}) target_link_libraries(pthread-${x} PRIVATE Threads::Threads) - target_link_libraries(pthread-${x} PUBLIC "-Wl,-znorelro -Wl,-znoseparate-code") # TODO: convert to target_link_option once CMAKE_VERSION is >3.13 + if(SIMGRID_HAVE_MC) # Only needed to introspect the binary + 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 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) - 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() + 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() set(tesh_files ${tesh_files} ${CMAKE_CURRENT_SOURCE_DIR}/pthread-${x}.tesh @@ -35,12 +35,14 @@ endforeach() foreach(x mutex-simpledeadlock) - if(SIMGRID_HAVE_MC AND ("${CMAKE_SYSTEM}" MATCHES "Linux")) # sthread is linux-only + if("${CMAKE_SYSTEM}" MATCHES "Linux") # sthread is linux-only add_executable (pthread-${x} EXCLUDE_FROM_ALL pthread-${x}.c) set_target_properties(pthread-${x} PROPERTIES RUNTIME_OUTPUT_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR}) target_link_libraries(pthread-${x} PRIVATE Threads::Threads) - target_link_libraries(pthread-${x} PUBLIC "-Wl,-znorelro -Wl,-znoseparate-code") # TODO: convert to target_link_option once CMAKE_VERSION is >3.13 + if(SIMGRID_HAVE_MC) # Only needed to introspect the binary + 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) @@ -56,12 +58,14 @@ endforeach() foreach(example stdobject) - if(SIMGRID_HAVE_MC AND ("${CMAKE_SYSTEM}" MATCHES "Linux")) # sthread is linux-only + if("${CMAKE_SYSTEM}" MATCHES "Linux") # sthread is linux-only add_executable (${example} EXCLUDE_FROM_ALL ${CMAKE_CURRENT_SOURCE_DIR}/${example}/${example}.cpp) set_target_properties(${example} PROPERTIES RUNTIME_OUTPUT_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR}) target_link_libraries(${example} PRIVATE Threads::Threads) - target_link_libraries(${example} PUBLIC "-fPIC -Wl,-znorelro -Wl,-znoseparate-code") # TODO: convert to target_link_option once CMAKE_VERSION is >3.13 + if(SIMGRID_HAVE_MC) # Only needed to introspect the binary + target_link_libraries(${example} PUBLIC "-fPIC -Wl,-znorelro -Wl,-znoseparate-code") # TODO: convert to target_link_option once CMAKE_VERSION is >3.13 + endif() set_target_properties(${example} PROPERTIES RUNTIME_OUTPUT_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR}/${example}) add_dependencies(tests-mc ${example}) diff --git a/src/kernel/EngineImpl.cpp b/src/kernel/EngineImpl.cpp index f7af9b41ad..d8ce61fac3 100644 --- a/src/kernel/EngineImpl.cpp +++ b/src/kernel/EngineImpl.cpp @@ -16,6 +16,7 @@ #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" @@ -25,10 +26,6 @@ #include #include -#if SIMGRID_HAVE_MC -#include "src/mc/remote/AppSide.hpp" -#endif - XBT_LOG_NEW_DEFAULT_CATEGORY(ker_engine, "Logging specific to Engine (kernel)"); namespace simgrid::kernel { @@ -171,12 +168,10 @@ 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; @@ -605,11 +600,7 @@ 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/api/RemoteApp.cpp b/src/mc/api/RemoteApp.cpp index fc496adfd8..3c6365c895 100644 --- a/src/mc/api/RemoteApp.cpp +++ b/src/mc/api/RemoteApp.cpp @@ -41,8 +41,12 @@ static void cleanup_master_socket() RemoteApp::RemoteApp(const std::vector& args, bool need_memory_introspection) : app_args_(args) { if (need_memory_introspection) { +#if SIMGRID_HAVE_MC checker_side_ = std::make_unique(app_args_, need_memory_introspection); initial_snapshot_ = std::make_shared(0, page_store_, *checker_side_->get_remote_memory()); +#else + xbt_die("SimGrid was compiled without MC support."); +#endif } else { master_socket_ = socket(AF_LOCAL, SOCK_SEQPACKET | SOCK_CLOEXEC, 0); xbt_assert(master_socket_ != -1, "Cannot create the master socket: %s", strerror(errno)); @@ -66,16 +70,17 @@ RemoteApp::RemoteApp(const std::vector& args, bool need_memory_introspect RemoteApp::~RemoteApp() { - initial_snapshot_ = nullptr; checker_side_ = nullptr; } void RemoteApp::restore_initial_state() { - if (initial_snapshot_ == nullptr) { // No memory introspection + if (initial_snapshot_ == nullptr) // No memory introspection checker_side_ = application_factory_->clone(master_socket_); - } else +#if SIMGRID_HAVE_MC + else initial_snapshot_->restore(*checker_side_->get_remote_memory()); +#endif } unsigned long RemoteApp::get_maxpid() const @@ -184,8 +189,10 @@ Transition* RemoteApp::handle_simcall(aid_t aid, int times_considered, bool new_ m.times_considered_ = times_considered; checker_side_->get_channel().send(m); +#if SIMGRID_HAVE_MC if (auto* memory = get_remote_process_memory(); memory != nullptr) memory->clear_cache(); +#endif if (checker_side_->running()) checker_side_->dispatch_events(); // The app may send messages while processing the transition diff --git a/src/mc/api/RemoteApp.hpp b/src/mc/api/RemoteApp.hpp index 693a2202a7..c3d051840b 100644 --- a/src/mc/api/RemoteApp.hpp +++ b/src/mc/api/RemoteApp.hpp @@ -26,9 +26,13 @@ namespace simgrid::mc { */ class XBT_PUBLIC RemoteApp { private: - std::unique_ptr checker_side_; +#if SIMGRID_HAVE_MC PageStore page_store_{500}; std::shared_ptr initial_snapshot_; +#else + void* initial_snapshot_ = nullptr; // The code tests it to decide whether to use the refork exec path +#endif + std::unique_ptr checker_side_; std::unique_ptr application_factory_; // when no meminfo, create checker_side_ by cloning this one int master_socket_ = -1; @@ -68,10 +72,12 @@ public: /** Take a transition. A new Transition is created iff the last parameter is true */ Transition* handle_simcall(aid_t aid, int times_considered, bool new_transition); +#if SIMGRID_HAVE_MC /* Get the memory of the remote process */ RemoteProcessMemory* get_remote_process_memory() { return checker_side_->get_remote_memory(); } PageStore& get_page_store() { return page_store_; } +#endif }; } // namespace simgrid::mc diff --git a/src/mc/api/State.cpp b/src/mc/api/State.cpp index c2478cb9dd..aac9c32f90 100644 --- a/src/mc/api/State.cpp +++ b/src/mc/api/State.cpp @@ -29,10 +29,12 @@ State::State(RemoteApp& remote_app) : num_(++expended_states_) remote_app.get_actors_status(strategy_->actors_to_run_); +#if SIMGRID_HAVE_MC /* Stateful model checking */ if ((_sg_mc_checkpoint > 0 && (num_ % _sg_mc_checkpoint == 0)) || _sg_mc_termination) system_state_ = std::make_shared(num_, remote_app.get_page_store(), *remote_app.get_remote_process_memory()); +#endif } State::State(RemoteApp& remote_app, std::shared_ptr parent_state) @@ -51,9 +53,11 @@ State::State(RemoteApp& remote_app, std::shared_ptr parent_state) remote_app.get_actors_status(strategy_->actors_to_run_); /* Stateful model checking */ +#if SIMGRID_HAVE_MC if ((_sg_mc_checkpoint > 0 && (num_ % _sg_mc_checkpoint == 0)) || _sg_mc_termination) system_state_ = std::make_shared(num_, remote_app.get_page_store(), *remote_app.get_remote_process_memory()); +#endif /* If we want sleep set reduction, copy the sleep set and eventually removes things from it */ if (_sg_mc_sleep_set) { diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp index 8f1fe11789..a51cbd7a07 100644 --- a/src/mc/explo/DFSExplorer.cpp +++ b/src/mc/explo/DFSExplorer.cpp @@ -41,6 +41,7 @@ xbt::signal DFSExplorer::on_log_state_signal; void DFSExplorer::check_non_termination(const State* current_state) { +#if SIMGRID_HAVE_MC for (auto const& state : stack_) { if (state->get_system_state()->equals_to(*current_state->get_system_state(), *get_remote_app().get_remote_process_memory())) { @@ -59,6 +60,7 @@ void DFSExplorer::check_non_termination(const State* current_state) throw TerminationError(); } } +#endif } RecordTrace DFSExplorer::get_record_trace() // override @@ -240,9 +242,11 @@ void DFSExplorer::run() if (_sg_mc_termination) this->check_non_termination(next_state.get()); +#if SIMGRID_HAVE_MC /* Check whether we already explored next_state in the past (but only if interested in state-equality reduction) */ if (_sg_mc_max_visited_states > 0) visited_state_ = visited_states_.addVisitedState(next_state->get_num(), next_state.get(), get_remote_app()); +#endif stack_.push_back(std::move(next_state)); @@ -294,6 +298,8 @@ void DFSExplorer::backtrack() // We found a real backtracking point, let's go to it backtrack_count_++; XBT_DEBUG("Backtracking to state#%ld", backtracking_point->get_num()); + +#if SIMGRID_HAVE_MC /* If asked to rollback on a state that has a snapshot, restore it */ if (const auto* system_state = backtracking_point->get_system_state()) { system_state->restore(*get_remote_app().get_remote_process_memory()); @@ -301,6 +307,7 @@ void DFSExplorer::backtrack() this->restore_stack(backtracking_point); return; } +#endif /* if no snapshot, we need to restore the initial state and replay the transitions */ get_remote_app().restore_initial_state(); diff --git a/src/mc/explo/Exploration.cpp b/src/mc/explo/Exploration.cpp index 061a9b4473..6b8366ef34 100644 --- a/src/mc/explo/Exploration.cpp +++ b/src/mc/explo/Exploration.cpp @@ -88,13 +88,14 @@ XBT_ATTRIB_NORETURN void Exploration::report_crash(int status) if (xbt_log_no_loc) { XBT_INFO("Stack trace not displayed because you passed --log=no_loc"); } else { +#if SIMGRID_HAVE_MC const auto* memory = get_remote_app().get_remote_process_memory(); if (memory) { XBT_INFO("Stack trace:"); memory->dump_stack(); - } else { + } else +#endif XBT_INFO("Stack trace not shown because there is no memory introspection."); - } } system_exit(SIMGRID_MC_EXIT_PROGRAM_CRASH); diff --git a/src/mc/explo/simgrid_mc.cpp b/src/mc/explo/simgrid_mc.cpp index f1525fee99..4e3fc12eae 100644 --- a/src/mc/explo/simgrid_mc.cpp +++ b/src/mc/explo/simgrid_mc.cpp @@ -35,14 +35,16 @@ int main(int argc, char** argv) std::unique_ptr explo; +#if SIMGRID_HAVE_MC if (_sg_mc_comms_determinism || _sg_mc_send_determinism) explo = std::unique_ptr(create_communication_determinism_checker(argv_copy, cfg_use_DPOR())); else if (_sg_mc_unfolding_checker) explo = std::unique_ptr(create_udpor_checker(argv_copy)); - else if (_sg_mc_property_file.get().empty()) - explo = std::unique_ptr(create_dfs_exploration(argv_copy, cfg_use_DPOR())); - else + else if (not _sg_mc_property_file.get().empty()) explo = std::unique_ptr(create_liveness_checker(argv_copy)); + else +#endif + explo = std::unique_ptr(create_dfs_exploration(argv_copy, cfg_use_DPOR())); try { explo->run(); diff --git a/src/mc/mc_client_api.cpp b/src/mc/mc_client_api.cpp index c257a7603c..fe18e7bf75 100644 --- a/src/mc/mc_client_api.cpp +++ b/src/mc/mc_client_api.cpp @@ -17,10 +17,9 @@ int MC_random(int min, int max) { -#if SIMGRID_HAVE_MC xbt_assert(simgrid::mc::model_checking_mode != simgrid::mc::ModelCheckingMode::CHECKER_SIDE, "This should be called from the client side"); -#endif + if (not MC_is_active() && not MC_record_replay_is_active()) { // no need to do a simcall in this case static simgrid::xbt::random::XbtRandom prng; return prng.uniform_int(min, max); @@ -32,7 +31,6 @@ int MC_random(int min, int max) void MC_assert(int prop) { // Cannot used xbt_assert here, or it would be an infinite recursion. -#if SIMGRID_HAVE_MC xbt_assert(simgrid::mc::model_checking_mode != simgrid::mc::ModelCheckingMode::CHECKER_SIDE, "This should be called from the client side"); if (not prop) { @@ -41,10 +39,6 @@ void MC_assert(int prop) 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() @@ -55,36 +49,28 @@ 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/mc_config.cpp b/src/mc/mc_config.cpp index f219a1175a..7707914061 100644 --- a/src/mc/mc_config.cpp +++ b/src/mc/mc_config.cpp @@ -18,14 +18,10 @@ simgrid::mc::ModelCheckingMode simgrid::mc::model_checking_mode = simgrid::mc::M static void _mc_cfg_cb_check(const char* spec, bool more_check = true) { -#if SIMGRID_HAVE_MC xbt_assert(_sg_cfg_init_status == 0 || MC_is_active() || MC_record_replay_is_active() || not more_check, "Specifying a %s is only allowed within the model-checker. Please use simgrid-mc, or specify this option " "after the replay path.", spec); -#else - xbt_die("Specifying a %s is only allowed within the model-checker. Please enable it before the compilation.", spec); -#endif } /* Replay (this part is enabled even if MC it disabled) */ @@ -41,7 +37,6 @@ simgrid::config::Flag _sg_mc_record_path{ MC_record_path() = value; }}; -#if SIMGRID_HAVE_MC simgrid::config::Flag _sg_mc_timeout{ "model-check/timeout", "Whether to enable timeouts for wait requests", false, [](bool) { _mc_cfg_cb_check("value to enable/disable timeout for wait requests", not MC_record_replay_is_active()); @@ -67,6 +62,7 @@ simgrid::config::Flag _sg_mc_strategy{ xbt_die("configuration option 'model-check/guided-mc' can only take 'none' or 'nb_wait' as a value"); }}; +#if SIMGRID_HAVE_MC simgrid::config::Flag _sg_mc_checkpoint{ "model-check/checkpoint", "Specify the amount of steps between checkpoints during stateful model-checking " "(default: 0 => stateless verification). If value=1, one checkpoint is saved for each " @@ -99,6 +95,7 @@ simgrid::config::Flag _sg_mc_unfolding_checker{ "Whether to enable the unfolding-based dynamic partial order reduction to MPI programs", false, [](bool) { _mc_cfg_cb_check("value to to enable/disable the unfolding-based dynamic partial order reduction to MPI programs"); }}; +#endif simgrid::config::Flag _sg_mc_buffering{ "smpi/buffering", @@ -136,5 +133,3 @@ bool simgrid::mc::cfg_use_DPOR() } return cfg_mc_reduction.get() == "dpor"; } - -#endif diff --git a/src/mc/mc_record.cpp b/src/mc/mc_record.cpp index 6f1d32f486..4e14c0ad8e 100644 --- a/src/mc/mc_record.cpp +++ b/src/mc/mc_record.cpp @@ -100,8 +100,6 @@ simgrid::mc::RecordTrace::RecordTrace(const char* data) } } -#if SIMGRID_HAVE_MC - std::string simgrid::mc::RecordTrace::to_string() const { std::ostringstream stream; @@ -114,7 +112,4 @@ std::string simgrid::mc::RecordTrace::to_string() const } return stream.str(); } - -#endif - } // namespace simgrid::mc diff --git a/src/mc/remote/AppSide.cpp b/src/mc/remote/AppSide.cpp index a5d5ffaa3e..9efa3081d6 100644 --- a/src/mc/remote/AppSide.cpp +++ b/src/mc/remote/AppSide.cpp @@ -190,11 +190,15 @@ void AppSide::handle_wait_child(const s_mc_message_int_t* msg) } void AppSide::handle_need_meminfo() { +#if SIMGRID_HAVE_MC this->need_memory_info_ = true; s_mc_message_need_meminfo_reply_t answer = {}; answer.type = MessageType::NEED_MEMINFO_REPLY; answer.mmalloc_default_mdp = mmalloc_get_current_heap(); xbt_assert(channel_.send(answer) == 0, "Could not send response to the request for meminfo."); +#else + xbt_die("SimGrid was compiled without MC suppport, so liveness and similar features are not available."); +#endif } void AppSide::handle_actors_status() const { @@ -365,11 +369,15 @@ void AppSide::ignore_memory(void* addr, std::size_t size) const if (not MC_is_active() || not need_memory_info_) return; +#if SIMGRID_HAVE_MC s_mc_message_ignore_memory_t message = {}; message.type = MessageType::IGNORE_MEMORY; message.addr = (std::uintptr_t)addr; message.size = size; xbt_assert(channel_.send(message) == 0, "Could not send IGNORE_MEMORY message to model-checker"); +#else + xbt_die("Cannot really call ignore_heap() in non-SIMGRID_MC mode."); +#endif } void AppSide::ignore_heap(void* address, std::size_t size) const @@ -377,6 +385,7 @@ void AppSide::ignore_heap(void* address, std::size_t size) const if (not MC_is_active() || not need_memory_info_) return; +#if SIMGRID_HAVE_MC const s_xbt_mheap_t* heap = mmalloc_get_current_heap(); s_mc_message_ignore_heap_t message = {}; @@ -393,6 +402,9 @@ void AppSide::ignore_heap(void* address, std::size_t size) const } xbt_assert(channel_.send(message) == 0, "Could not send ignored region to MCer"); +#else + xbt_die("Cannot really call ignore_heap() in non-SIMGRID_MC mode."); +#endif } void AppSide::unignore_heap(void* address, std::size_t size) const @@ -400,11 +412,15 @@ void AppSide::unignore_heap(void* address, std::size_t size) const if (not MC_is_active() || not need_memory_info_) return; +#if SIMGRID_HAVE_MC s_mc_message_ignore_memory_t message = {}; message.type = MessageType::UNIGNORE_HEAP; message.addr = (std::uintptr_t)address; message.size = size; xbt_assert(channel_.send(message) == 0, "Could not send IGNORE_HEAP message to model-checker"); +#else + xbt_die("Cannot really call unignore_heap() in non-SIMGRID_MC mode."); +#endif } void AppSide::declare_symbol(const char* name, int* value) const @@ -414,6 +430,7 @@ void AppSide::declare_symbol(const char* name, int* value) const return; } +#if SIMGRID_HAVE_MC s_mc_message_register_symbol_t message = {}; message.type = MessageType::REGISTER_SYMBOL; xbt_assert(strlen(name) + 1 <= message.name.size(), "Symbol is too long"); @@ -421,6 +438,9 @@ void AppSide::declare_symbol(const char* name, int* value) const message.callback = nullptr; message.data = value; xbt_assert(channel_.send(message) == 0, "Could send REGISTER_SYMBOL message to model-checker"); +#else + xbt_die("Cannot really call declare_symbol() in non-SIMGRID_MC mode."); +#endif } /** Register a stack in the model checker @@ -434,6 +454,7 @@ void AppSide::declare_stack(void* stack, size_t size, ucontext_t* context) const if (not MC_is_active() || not need_memory_info_) return; +#if SIMGRID_HAVE_MC const s_xbt_mheap_t* heap = mmalloc_get_current_heap(); s_stack_region_t region = {}; @@ -446,5 +467,8 @@ void AppSide::declare_stack(void* stack, size_t size, ucontext_t* context) const message.type = MessageType::STACK_REGION; message.stack_region = region; xbt_assert(channel_.send(message) == 0, "Could not send STACK_REGION to model-checker"); +#else + xbt_die("Cannot really call declare_stack() in non-SIMGRID_MC mode."); +#endif } } // namespace simgrid::mc diff --git a/src/mc/remote/CheckerSide.cpp b/src/mc/remote/CheckerSide.cpp index a19f0934e0..3937d28955 100644 --- a/src/mc/remote/CheckerSide.cpp +++ b/src/mc/remote/CheckerSide.cpp @@ -193,6 +193,7 @@ CheckerSide::CheckerSide(const std::vector& args, bool need_memory_info) setup_events(false); /* we need a signal handler too */ if (need_memory_info) { +#if SIMGRID_HAVE_MC // setup ptrace and sync with the app wait_application_process(pid_); @@ -208,6 +209,9 @@ CheckerSide::CheckerSide(const std::vector& args, bool need_memory_info) /* We now have enough info to create the memory address space */ remote_memory_ = std::make_unique(pid_, answer.mmalloc_default_mdp); +#else + xbt_die("Cannot introspect memory without MC support"); +#endif } wait_for_requests(); @@ -288,6 +292,7 @@ bool CheckerSide::handle_message(const char* buffer, ssize_t size) switch (base_message.type) { case MessageType::IGNORE_HEAP: { +#if SIMGRID_HAVE_MC if (remote_memory_ != nullptr) { s_mc_message_ignore_heap_t message; xbt_assert(size == sizeof(message), "Broken message"); @@ -299,49 +304,53 @@ bool CheckerSide::handle_message(const char* buffer, ssize_t size) region.address = message.address; region.size = message.size; get_remote_memory()->ignore_heap(region); - } else { + } else +#endif XBT_INFO("Ignoring a IGNORE_HEAP message because we don't need to introspect memory."); - } break; } case MessageType::UNIGNORE_HEAP: { +#if SIMGRID_HAVE_MC if (remote_memory_ != nullptr) { s_mc_message_ignore_memory_t message; xbt_assert(size == sizeof(message), "Broken message"); memcpy(&message, buffer, sizeof(message)); get_remote_memory()->unignore_heap((void*)message.addr, message.size); - } else { + } else +#endif XBT_INFO("Ignoring an UNIGNORE_HEAP message because we don't need to introspect memory."); - } break; } case MessageType::IGNORE_MEMORY: { +#if SIMGRID_HAVE_MC if (remote_memory_ != nullptr) { s_mc_message_ignore_memory_t message; xbt_assert(size == sizeof(message), "Broken message"); memcpy(&message, buffer, sizeof(message)); get_remote_memory()->ignore_region(message.addr, message.size); - } else { + } else +#endif XBT_INFO("Ignoring an IGNORE_MEMORY message because we don't need to introspect memory."); - } break; } case MessageType::STACK_REGION: { +#if SIMGRID_HAVE_MC if (remote_memory_ != nullptr) { s_mc_message_stack_region_t message; xbt_assert(size == sizeof(message), "Broken message"); memcpy(&message, buffer, sizeof(message)); get_remote_memory()->stack_areas().push_back(message.stack_region); - } else { + } else +#endif XBT_INFO("Ignoring an STACK_REGION message because we don't need to introspect memory."); - } break; } case MessageType::REGISTER_SYMBOL: { +#if SIMGRID_HAVE_MC s_mc_message_register_symbol_t message; xbt_assert(size == sizeof(message), "Broken message"); memcpy(&message, buffer, sizeof(message)); @@ -349,6 +358,9 @@ bool CheckerSide::handle_message(const char* buffer, ssize_t size) XBT_DEBUG("Received symbol: %s", message.name.data()); LivenessChecker::automaton_register_symbol(*get_remote_memory(), message.name.data(), remote((int*)message.data)); +#else + xbt_die("Please don't use liveness properties when MC is compiled out."); +#endif break; } @@ -378,8 +390,10 @@ void CheckerSide::wait_for_requests() void CheckerSide::clear_memory_cache() { +#if SIMGRID_HAVE_MC if (remote_memory_) remote_memory_->clear_cache(); +#endif } void CheckerSide::handle_dead_child(int status) diff --git a/src/mc/remote/CheckerSide.hpp b/src/mc/remote/CheckerSide.hpp index a3cb6a6eda..eeaa54e623 100644 --- a/src/mc/remote/CheckerSide.hpp +++ b/src/mc/remote/CheckerSide.hpp @@ -21,7 +21,9 @@ class CheckerSide { event* socket_event_; event* signal_event_; std::unique_ptr base_{nullptr, &event_base_free}; +#if SIMGRID_HAVE_MC std::unique_ptr remote_memory_; +#endif Channel channel_; bool running_ = false; @@ -64,7 +66,9 @@ public: pid_t get_pid() const { return pid_; } bool running() const { return running_; } void terminate() { running_ = false; } +#if SIMGRID_HAVE_MC RemoteProcessMemory* get_remote_memory() { return remote_memory_.get(); } +#endif }; } // namespace simgrid::mc diff --git a/src/mc/transition/Transition.cpp b/src/mc/transition/Transition.cpp index 84ad991fd5..4a8025167c 100644 --- a/src/mc/transition/Transition.cpp +++ b/src/mc/transition/Transition.cpp @@ -5,11 +5,6 @@ #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" @@ -17,7 +12,8 @@ #include "src/mc/transition/TransitionObjectAccess.hpp" #include "src/mc/transition/TransitionRandom.hpp" #include "src/mc/transition/TransitionSynchro.hpp" -#endif +#include "xbt/asserts.h" +#include "xbt/string.hpp" #include @@ -47,15 +43,12 @@ 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); @@ -108,9 +101,6 @@ 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/src/mc/transition/TransitionComm.cpp b/src/mc/transition/TransitionComm.cpp index de0ec2b67a..8ae9d207e1 100644 --- a/src/mc/transition/TransitionComm.cpp +++ b/src/mc/transition/TransitionComm.cpp @@ -5,12 +5,10 @@ #include "src/mc/transition/TransitionComm.hpp" #include "simgrid/config.h" -#include "xbt/asserts.h" -#include "xbt/string.hpp" -#if SIMGRID_HAVE_MC #include "src/mc/api/RemoteApp.hpp" #include "src/mc/api/State.hpp" -#endif +#include "xbt/asserts.h" +#include "xbt/string.hpp" #include diff --git a/teshsuite/mc/CMakeLists.txt b/teshsuite/mc/CMakeLists.txt index 129923dd6b..1abeed4b37 100644 --- a/teshsuite/mc/CMakeLists.txt +++ b/teshsuite/mc/CMakeLists.txt @@ -43,14 +43,14 @@ set(tesh_files ${tesh_files} ${CMAKE_CURRENT_SOURCE_DIR}/random-bug/rando IF(SIMGRID_HAVE_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) - 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() -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) +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) diff --git a/tools/cmake/DefinePackages.cmake b/tools/cmake/DefinePackages.cmake index ce4633f4a1..a20edb328a 100644 --- a/tools/cmake/DefinePackages.cmake +++ b/tools/cmake/DefinePackages.cmake @@ -518,14 +518,44 @@ set(MC_SRC_BASE src/mc/mc_record.hpp src/mc/mc_replay.hpp src/mc/transition/Transition.cpp - ) -set(MC_SRC - src/mc/explo/CommunicationDeterminismChecker.cpp + 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 src/mc/explo/Exploration.hpp + + src/mc/remote/AppSide.cpp + src/mc/remote/AppSide.hpp + src/mc/remote/Channel.cpp + src/mc/remote/Channel.hpp + src/mc/remote/CheckerSide.cpp + src/mc/remote/CheckerSide.hpp + src/mc/remote/RemotePtr.hpp + src/mc/remote/mc_protocol.h + + src/mc/transition/Transition.hpp + src/mc/transition/TransitionActorJoin.cpp + src/mc/transition/TransitionActorJoin.hpp + src/mc/transition/TransitionAny.cpp + src/mc/transition/TransitionAny.hpp + src/mc/transition/TransitionComm.cpp + src/mc/transition/TransitionComm.hpp + src/mc/transition/TransitionObjectAccess.cpp + src/mc/transition/TransitionObjectAccess.hpp + src/mc/transition/TransitionRandom.cpp + src/mc/transition/TransitionRandom.hpp + src/mc/transition/TransitionSynchro.cpp + src/mc/transition/TransitionSynchro.hpp + ) + +set(MC_SRC + src/mc/explo/CommunicationDeterminismChecker.cpp src/mc/explo/LivenessChecker.cpp src/mc/explo/LivenessChecker.hpp src/mc/explo/UdporChecker.cpp @@ -565,15 +595,6 @@ set(MC_SRC src/mc/inspect/mc_unw.cpp src/mc/inspect/mc_unw.hpp src/mc/inspect/mc_unw_vmread.cpp - - src/mc/remote/AppSide.cpp - src/mc/remote/AppSide.hpp - src/mc/remote/Channel.cpp - src/mc/remote/Channel.hpp - src/mc/remote/CheckerSide.cpp - src/mc/remote/CheckerSide.hpp - src/mc/remote/RemotePtr.hpp - src/mc/remote/mc_protocol.h src/mc/sosp/ChunkedData.cpp src/mc/sosp/ChunkedData.hpp @@ -586,26 +607,6 @@ set(MC_SRC src/mc/sosp/Snapshot.cpp src/mc/sosp/Snapshot.hpp - src/mc/transition/Transition.hpp - src/mc/transition/TransitionActorJoin.cpp - src/mc/transition/TransitionActorJoin.hpp - src/mc/transition/TransitionAny.cpp - src/mc/transition/TransitionAny.hpp - src/mc/transition/TransitionComm.cpp - src/mc/transition/TransitionComm.hpp - src/mc/transition/TransitionObjectAccess.cpp - src/mc/transition/TransitionObjectAccess.hpp - src/mc/transition/TransitionRandom.cpp - src/mc/transition/TransitionRandom.hpp - src/mc/transition/TransitionSynchro.cpp - src/mc/transition/TransitionSynchro.hpp - - 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/AddressSpace.hpp src/mc/VisitedState.cpp src/mc/VisitedState.hpp diff --git a/tools/cmake/MakeLib.cmake b/tools/cmake/MakeLib.cmake index 11cf6b9c28..5575bb7188 100644 --- a/tools/cmake/MakeLib.cmake +++ b/tools/cmake/MakeLib.cmake @@ -42,19 +42,17 @@ if(HAVE_MMALLOC) APPEND PROPERTY INCLUDE_DIRECTORIES "${INTERNAL_INCLUDES}") endif() -if(enable_model-checking) - 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() +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() # Compute the dependencies of SimGrid