From: Martin Quinson Date: Fri, 31 Mar 2023 22:58:56 +0000 (+0200) Subject: Rename SIMGRID_HAVE_MC into SIMGRID_HAVE_STATEFUL_MC (so that MC can be optional... X-Git-Tag: v3.34~235 X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/824740eb0df1dedddb86035ff3730d87e037f356 Rename SIMGRID_HAVE_MC into SIMGRID_HAVE_STATEFUL_MC (so that MC can be optional again) --- diff --git a/CMakeLists.txt b/CMakeLists.txt index 4fa8107700..a3cc8d467a 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -386,11 +386,11 @@ if(enable_model-checking) find_package(Libelf REQUIRED) include_directories(${LIBDW_INCLUDE_DIR} ${LIBELF_INCLUDE_DIR}) set(SIMGRID_DEP "${SIMGRID_DEP} ${LIBELF_LIBRARIES} ${LIBDW_LIBRARIES}") - set(SIMGRID_HAVE_MC 1) + 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_MC 0) + SET(SIMGRID_HAVE_STATEFUL_MC 0) set(HAVE_MMALLOC 0) endif() mark_as_advanced(PATH_LIBDW_H) @@ -938,7 +938,7 @@ message(" Compile Boost.Context support: ${HAVE_BOOST_CONTEXTS}") message("") message(" Maintainer mode .............: ${enable_maintainer_mode}") message(" Documentation ...............: ${enable_documentation}") -message(" Model checking ..............: ${SIMGRID_HAVE_MC}") +message(" Stateful model checking .....: ${SIMGRID_HAVE_STATEFUL_MC}") message(" Graphviz mode ...............: ${HAVE_GRAPHVIZ}") message(" Mallocators .................: ${enable_mallocators}") message("") diff --git a/examples/cpp/CMakeLists.txt b/examples/cpp/CMakeLists.txt index 82fcc276c8..a0705d7032 100644 --- a/examples/cpp/CMakeLists.txt +++ b/examples/cpp/CMakeLists.txt @@ -28,7 +28,7 @@ if(enable_coverage) endforeach() endif() -if(SIMGRID_HAVE_MC) +if(SIMGRID_HAVE_STATEFUL_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) @@ -219,7 +219,7 @@ foreach(example mc-failing-assert) # 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) +# if(SIMGRID_HAVE_STATEFUL_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 diff --git a/examples/smpi/CMakeLists.txt b/examples/smpi/CMakeLists.txt index 406554822f..c2b3186017 100644 --- a/examples/smpi/CMakeLists.txt +++ b/examples/smpi/CMakeLists.txt @@ -6,7 +6,7 @@ set(_ampi_test_sources ${CMAKE_CURRENT_SOURCE_DIR}/ampi_test/ampi_test.cpp) set(MC_tests bugged1 bugged2 bugged1_liveness only_send_deterministic mutual_exclusion non_termination1 non_termination2 non_termination3 non_termination4 sendsend) foreach(x ${MC_tests}) - if(NOT SIMGRID_HAVE_MC) + if(NOT SIMGRID_HAVE_STATEFUL_MC) set(_${x}_disable 1) endif() set(_${x}_sources ${CMAKE_CURRENT_SOURCE_DIR}/mc/${x}.c) @@ -91,7 +91,7 @@ set(txt_files ${txt_files} ${CMAKE_CURRENT_SOURCE_DIR}/replay/actions0.t if(enable_smpi) # MC is currently broken with threads (deadlock => timeout) - if(SIMGRID_HAVE_MC) + if(SIMGRID_HAVE_STATEFUL_MC) add_dependencies(tests-mc smpimain) add_dependencies(tests-mc smpi_only_send_deterministic) ADD_TESH(smpi-mc-only-send-determinism --setenv srcdir=${CMAKE_HOME_DIRECTORY}/examples/smpi/mc --setenv platfdir=${CMAKE_HOME_DIRECTORY}/examples/platforms --cd ${CMAKE_BINARY_DIR}/examples/smpi/mc ${CMAKE_HOME_DIRECTORY}/examples/smpi/mc/only_send_deterministic.tesh) diff --git a/examples/sthread/CMakeLists.txt b/examples/sthread/CMakeLists.txt index 33f0815199..2b7e8234dc 100644 --- a/examples/sthread/CMakeLists.txt +++ b/examples/sthread/CMakeLists.txt @@ -12,7 +12,7 @@ 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) - if(SIMGRID_HAVE_MC) # Only needed to introspect the binary + if(SIMGRID_HAVE_STATEFUL_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() @@ -40,7 +40,7 @@ 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) - if(SIMGRID_HAVE_MC) # Only needed to introspect the binary + if(SIMGRID_HAVE_STATEFUL_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() @@ -63,7 +63,7 @@ foreach(example 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) - if(SIMGRID_HAVE_MC) # Only needed to introspect the binary + if(SIMGRID_HAVE_STATEFUL_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}) diff --git a/include/simgrid/config.h.in b/include/simgrid/config.h.in index 6ef3fd76b1..83977db9ed 100644 --- a/include/simgrid/config.h.in +++ b/include/simgrid/config.h.in @@ -11,8 +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? */ #cmakedefine01 SIMGRID_HAVE_NS3 #cmakedefine NS3_MINOR_VERSION @NS3_MINOR_VERSION@ diff --git a/include/smpi/mpi.h b/include/smpi/mpi.h index 2c0b849745..5d61fb047f 100644 --- a/include/smpi/mpi.h +++ b/include/smpi/mpi.h @@ -17,10 +17,8 @@ #include /* Load it before the define next line to not mess with the system headers */ -#if SIMGRID_HAVE_MC #undef assert #define assert(x) MC_assert(!!(x)) -#endif #ifdef TRACE_CALL_LOCATION /* Defined by smpicc on the command line */ #include diff --git a/src/kernel/actor/Simcall.cpp b/src/kernel/actor/Simcall.cpp index d34a22d229..87605e4d64 100644 --- a/src/kernel/actor/Simcall.cpp +++ b/src/kernel/actor/Simcall.cpp @@ -4,17 +4,14 @@ * under the terms of the license (GNU LGPL) which comes with this package. */ #include "src/kernel/actor/Simcall.hpp" +#include "simgrid/modelchecker.h" #include "simgrid/s4u/Host.hpp" #include "src/kernel/EngineImpl.hpp" #include "src/kernel/actor/ActorImpl.hpp" #include "src/kernel/actor/SimcallObserver.hpp" #include "src/kernel/context/Context.hpp" -#include "xbt/log.h" - -#if SIMGRID_HAVE_MC -#include "simgrid/modelchecker.h" #include "src/mc/mc_replay.hpp" -#endif +#include "xbt/log.h" XBT_LOG_NEW_DEFAULT_SUBCATEGORY(ker_simcall, kernel, "transmuting from user request into kernel handlers"); @@ -82,11 +79,7 @@ void simcall_run_object_access(std::function const& code, simgrid::kerne // We only need a simcall if the order of the setters is important (parallel run or MC execution). // Otherwise, just call the function with no simcall - if (simgrid::kernel::context::Context::is_parallel() -#if SIMGRID_HAVE_MC - || MC_is_active() || MC_record_replay_is_active() -#endif - ) { + if (simgrid::kernel::context::Context::is_parallel() || MC_is_active() || MC_record_replay_is_active()) { simgrid::kernel::actor::ObjectAccessSimcallObserver observer{self, item}; simcall(simgrid::kernel::actor::Simcall::Type::RUN_ANSWERED, code, &observer); item->take_ownership(); diff --git a/src/kernel/context/ContextSwapped.cpp b/src/kernel/context/ContextSwapped.cpp index 13e7e9aa9b..1f3cd31e3a 100644 --- a/src/kernel/context/ContextSwapped.cpp +++ b/src/kernel/context/ContextSwapped.cpp @@ -82,8 +82,8 @@ SwappedContext::SwappedContext(std::function&& code, actor::ActorImpl* a #endif size_t size = actor->get_stacksize() + guard_size; -#if SIMGRID_HAVE_MC - /* Cannot use posix_memalign when SIMGRID_HAVE_MC. Align stack by hand, and save the +#if SIMGRID_HAVE_STATEFUL_MC + /* Cannot use posix_memalign when SIMGRID_HAVE_STATEFUL_MC. Align stack by hand, and save the * pointer returned by xbt_malloc0. */ auto* alloc = static_cast(xbt_malloc0(size + xbt_pagesize)); stack_ = alloc - (reinterpret_cast(alloc) & (xbt_pagesize - 1)) + xbt_pagesize; @@ -146,7 +146,7 @@ SwappedContext::~SwappedContext() XBT_WARN("Failed to remove page protection: %s", strerror(errno)); /* try to pursue anyway */ } -#if SIMGRID_HAVE_MC +#if SIMGRID_HAVE_STATEFUL_MC /* Retrieve the saved pointer. See the initialization above. */ stack_ = reinterpret_cast(stack_)[-1]; #endif diff --git a/src/kernel/context/ContextUnix.cpp b/src/kernel/context/ContextUnix.cpp index 7515e93515..98e372daf3 100644 --- a/src/kernel/context/ContextUnix.cpp +++ b/src/kernel/context/ContextUnix.cpp @@ -61,7 +61,7 @@ UContext::UContext(std::function&& code, actor::ActorImpl* actor, Swappe memcpy(ctx_addr, &arg, sizeof arg); makecontext(&this->uc_, (void (*)())sysv_ctx_wrapper, 2, ctx_addr[0], ctx_addr[1]); -#if SIMGRID_HAVE_MC +#if SIMGRID_HAVE_STATEFUL_MC if (MC_is_active()) simgrid::mc::AppSide::get()->declare_stack(get_stack(), stack_size, &uc_); #endif diff --git a/src/mc/api/RemoteApp.cpp b/src/mc/api/RemoteApp.cpp index 3c6365c895..cb9450d536 100644 --- a/src/mc/api/RemoteApp.cpp +++ b/src/mc/api/RemoteApp.cpp @@ -41,7 +41,7 @@ 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 +#if SIMGRID_HAVE_STATEFUL_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 @@ -77,7 +77,7 @@ void RemoteApp::restore_initial_state() { if (initial_snapshot_ == nullptr) // No memory introspection checker_side_ = application_factory_->clone(master_socket_); -#if SIMGRID_HAVE_MC +#if SIMGRID_HAVE_STATEFUL_MC else initial_snapshot_->restore(*checker_side_->get_remote_memory()); #endif @@ -189,7 +189,7 @@ 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 SIMGRID_HAVE_STATEFUL_MC if (auto* memory = get_remote_process_memory(); memory != nullptr) memory->clear_cache(); #endif diff --git a/src/mc/api/RemoteApp.hpp b/src/mc/api/RemoteApp.hpp index c3d051840b..82a93db420 100644 --- a/src/mc/api/RemoteApp.hpp +++ b/src/mc/api/RemoteApp.hpp @@ -26,7 +26,7 @@ namespace simgrid::mc { */ class XBT_PUBLIC RemoteApp { private: -#if SIMGRID_HAVE_MC +#if SIMGRID_HAVE_STATEFUL_MC PageStore page_store_{500}; std::shared_ptr initial_snapshot_; #else @@ -72,7 +72,7 @@ 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 +#if SIMGRID_HAVE_STATEFUL_MC /* Get the memory of the remote process */ RemoteProcessMemory* get_remote_process_memory() { return checker_side_->get_remote_memory(); } diff --git a/src/mc/api/State.cpp b/src/mc/api/State.cpp index aac9c32f90..69fae98b37 100644 --- a/src/mc/api/State.cpp +++ b/src/mc/api/State.cpp @@ -29,7 +29,7 @@ State::State(RemoteApp& remote_app) : num_(++expended_states_) remote_app.get_actors_status(strategy_->actors_to_run_); -#if SIMGRID_HAVE_MC +#if SIMGRID_HAVE_STATEFUL_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(), @@ -52,8 +52,7 @@ 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 SIMGRID_HAVE_STATEFUL_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()); diff --git a/src/mc/api/State.hpp b/src/mc/api/State.hpp index ad39ec5e5d..2b2a62577b 100644 --- a/src/mc/api/State.hpp +++ b/src/mc/api/State.hpp @@ -11,7 +11,7 @@ #include "src/mc/api/strategy/Strategy.hpp" #include "src/mc/transition/Transition.hpp" -#if SIMGRID_HAVE_MC +#if SIMGRID_HAVE_STATEFUL_MC #include "src/mc/sosp/Snapshot.hpp" #endif diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp index d2a9b1f6aa..eb3b8e7ac1 100644 --- a/src/mc/explo/DFSExplorer.cpp +++ b/src/mc/explo/DFSExplorer.cpp @@ -10,7 +10,7 @@ #include "src/mc/mc_record.hpp" #include "src/mc/transition/Transition.hpp" -#if SIMGRID_HAVE_MC +#if SIMGRID_HAVE_STATEFUL_MC #include "src/mc/VisitedState.hpp" #endif @@ -44,7 +44,7 @@ xbt::signal DFSExplorer::on_log_state_signal; void DFSExplorer::check_non_termination(const State* current_state) { -#if SIMGRID_HAVE_MC +#if SIMGRID_HAVE_STATEFUL_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())) { @@ -139,7 +139,7 @@ void DFSExplorer::run() continue; } -#if SIMGRID_HAVE_MC +#if SIMGRID_HAVE_STATEFUL_MC // Backtrack if we are revisiting a state we saw previously while applying state-equality reduction if (visited_state_ != nullptr) { XBT_DEBUG("State already visited (equal to state %ld), exploration stopped on this path.", @@ -247,7 +247,7 @@ void DFSExplorer::run() if (_sg_mc_termination) this->check_non_termination(next_state.get()); -#if SIMGRID_HAVE_MC +#if SIMGRID_HAVE_STATEFUL_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()); @@ -266,7 +266,7 @@ void DFSExplorer::run() dot_output("\"%ld\" -> \"%ld\" [%s];\n", state->get_num(), stack_.back()->get_num(), state->get_transition()->dot_string().c_str()); -#if SIMGRID_HAVE_MC +#if SIMGRID_HAVE_STATEFUL_MC } else { dot_output("\"%ld\" -> \"%ld\" [%s];\n", state->get_num(), visited_state_->original_num_ == -1 ? visited_state_->num_ : visited_state_->original_num_, @@ -307,7 +307,7 @@ void DFSExplorer::backtrack() backtrack_count_++; XBT_DEBUG("Backtracking to state#%ld", backtracking_point->get_num()); -#if SIMGRID_HAVE_MC +#if SIMGRID_HAVE_STATEFUL_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()); diff --git a/src/mc/explo/DFSExplorer.hpp b/src/mc/explo/DFSExplorer.hpp index 1b0f50e75e..3e8a45be7a 100644 --- a/src/mc/explo/DFSExplorer.hpp +++ b/src/mc/explo/DFSExplorer.hpp @@ -9,7 +9,7 @@ #include "src/mc/api/State.hpp" #include "src/mc/explo/Exploration.hpp" -#if SIMGRID_HAVE_MC +#if SIMGRID_HAVE_STATEFUL_MC #include "src/mc/VisitedState.hpp" #endif @@ -104,7 +104,7 @@ private: /** Stack representing the position in the exploration graph */ stack_t stack_; -#if SIMGRID_HAVE_MC +#if SIMGRID_HAVE_STATEFUL_MC VisitedStates visited_states_; std::unique_ptr visited_state_; #else diff --git a/src/mc/explo/Exploration.cpp b/src/mc/explo/Exploration.cpp index 6efe84181f..5d35347678 100644 --- a/src/mc/explo/Exploration.cpp +++ b/src/mc/explo/Exploration.cpp @@ -8,7 +8,7 @@ #include "src/mc/mc_exit.hpp" #include "src/mc/mc_private.hpp" -#if SIMGRID_HAVE_MC +#if SIMGRID_HAVE_STATEFUL_MC #include "src/mc/sosp/RemoteProcessMemory.hpp" #endif @@ -91,7 +91,7 @@ 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 +#if SIMGRID_HAVE_STATEFUL_MC const auto* memory = get_remote_app().get_remote_process_memory(); if (memory) { XBT_INFO("Stack trace:"); diff --git a/src/mc/explo/simgrid_mc.cpp b/src/mc/explo/simgrid_mc.cpp index 4e3fc12eae..700c4b9b58 100644 --- a/src/mc/explo/simgrid_mc.cpp +++ b/src/mc/explo/simgrid_mc.cpp @@ -35,7 +35,7 @@ int main(int argc, char** argv) std::unique_ptr explo; -#if SIMGRID_HAVE_MC +#if SIMGRID_HAVE_STATEFUL_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) diff --git a/src/mc/mc_base.cpp b/src/mc/mc_base.cpp index acd042d861..2c0370ec3a 100644 --- a/src/mc/mc_base.cpp +++ b/src/mc/mc_base.cpp @@ -8,13 +8,13 @@ #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" - -#if SIMGRID_HAVE_MC -#include "src/mc/api/RemoteApp.hpp" #include "src/mc/remote/AppSide.hpp" + +#if SIMGRID_HAVE_STATEFUL_MC #include "src/mc/sosp/RemoteProcessMemory.hpp" #endif @@ -52,10 +52,8 @@ void execute_actors() */ bool actor_is_enabled(kernel::actor::ActorImpl* actor) { -#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 // Now, we are in the client app, no need for remote memory reading. kernel::actor::Simcall* req = &actor->simcall_; @@ -75,10 +73,9 @@ bool actor_is_enabled(kernel::actor::ActorImpl* actor) */ bool request_is_visible(const kernel::actor::Simcall* req) { -#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 (req->observer_ == nullptr) return false; return req->observer_->is_visible(); diff --git a/src/mc/mc_config.cpp b/src/mc/mc_config.cpp index 7707914061..35381d3cb3 100644 --- a/src/mc/mc_config.cpp +++ b/src/mc/mc_config.cpp @@ -8,7 +8,7 @@ #include "src/simgrid/sg_config.hpp" #include -#if SIMGRID_HAVE_MC +#if SIMGRID_HAVE_STATEFUL_MC #include #endif @@ -62,7 +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 +#if SIMGRID_HAVE_STATEFUL_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 " diff --git a/src/mc/mc_global.cpp b/src/mc/mc_global.cpp index bc444ffb5a..262fa72ef3 100644 --- a/src/mc/mc_global.cpp +++ b/src/mc/mc_global.cpp @@ -6,7 +6,7 @@ #include "src/kernel/actor/ActorImpl.hpp" #include "src/mc/mc.h" -#if SIMGRID_HAVE_MC +#if SIMGRID_HAVE_STATEFUL_MC #include "src/mc/api/RemoteApp.hpp" #include "src/mc/explo/Exploration.hpp" #include "src/mc/inspect/mc_unw.hpp" @@ -34,7 +34,7 @@ std::vector processes_time; } -#if SIMGRID_HAVE_MC +#if SIMGRID_HAVE_STATEFUL_MC namespace simgrid::mc { diff --git a/src/mc/mc_record.cpp b/src/mc/mc_record.cpp index 4e14c0ad8e..a16898e144 100644 --- a/src/mc/mc_record.cpp +++ b/src/mc/mc_record.cpp @@ -10,12 +10,6 @@ #include "src/mc/mc_replay.hpp" #include "src/mc/transition/Transition.hpp" -#if SIMGRID_HAVE_MC -#include "src/mc/api/State.hpp" -#include "src/mc/explo/Exploration.hpp" -#include "src/mc/mc_private.hpp" -#endif - XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_record, mc, "Logging specific to MC record/replay facility"); namespace simgrid::mc { diff --git a/src/mc/remote/AppSide.cpp b/src/mc/remote/AppSide.cpp index 34bb5391be..f6b53c9686 100644 --- a/src/mc/remote/AppSide.cpp +++ b/src/mc/remote/AppSide.cpp @@ -11,7 +11,7 @@ #include "src/kernel/actor/SimcallObserver.hpp" #include "src/mc/mc_base.hpp" #include "src/mc/mc_config.hpp" -#if SIMGRID_HAVE_MC +#if SIMGRID_HAVE_STATEFUL_MC #include "src/mc/sosp/RemoteProcessMemory.hpp" #endif #if HAVE_SMPI @@ -192,7 +192,7 @@ void AppSide::handle_wait_child(const s_mc_message_int_t* msg) } void AppSide::handle_need_meminfo() { -#if SIMGRID_HAVE_MC +#if SIMGRID_HAVE_STATEFUL_MC this->need_memory_info_ = true; s_mc_message_need_meminfo_reply_t answer = {}; answer.type = MessageType::NEED_MEMINFO_REPLY; @@ -371,7 +371,7 @@ 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 +#if SIMGRID_HAVE_STATEFUL_MC s_mc_message_ignore_memory_t message = {}; message.type = MessageType::IGNORE_MEMORY; message.addr = (std::uintptr_t)addr; @@ -387,7 +387,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 +#if SIMGRID_HAVE_STATEFUL_MC const s_xbt_mheap_t* heap = mmalloc_get_current_heap(); s_mc_message_ignore_heap_t message = {}; @@ -414,7 +414,7 @@ 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 +#if SIMGRID_HAVE_STATEFUL_MC s_mc_message_ignore_memory_t message = {}; message.type = MessageType::UNIGNORE_HEAP; message.addr = (std::uintptr_t)address; @@ -432,7 +432,7 @@ void AppSide::declare_symbol(const char* name, int* value) const return; } -#if SIMGRID_HAVE_MC +#if SIMGRID_HAVE_STATEFUL_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"); @@ -456,7 +456,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 +#if SIMGRID_HAVE_STATEFUL_MC const s_xbt_mheap_t* heap = mmalloc_get_current_heap(); s_stack_region_t region = {}; diff --git a/src/mc/remote/CheckerSide.cpp b/src/mc/remote/CheckerSide.cpp index fb10475bd4..ee2f858ac6 100644 --- a/src/mc/remote/CheckerSide.cpp +++ b/src/mc/remote/CheckerSide.cpp @@ -8,7 +8,7 @@ #include "xbt/config.hpp" #include "xbt/system_error.hpp" -#if SIMGRID_HAVE_MC +#if SIMGRID_HAVE_STATEFUL_MC #include "src/mc/explo/LivenessChecker.hpp" #include "src/mc/sosp/RemoteProcessMemory.hpp" #endif @@ -197,7 +197,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 +#if SIMGRID_HAVE_STATEFUL_MC // setup ptrace and sync with the app wait_application_process(pid_); @@ -296,7 +296,7 @@ bool CheckerSide::handle_message(const char* buffer, ssize_t size) switch (base_message.type) { case MessageType::IGNORE_HEAP: { -#if SIMGRID_HAVE_MC +#if SIMGRID_HAVE_STATEFUL_MC if (remote_memory_ != nullptr) { s_mc_message_ignore_heap_t message; xbt_assert(size == sizeof(message), "Broken message"); @@ -315,7 +315,7 @@ bool CheckerSide::handle_message(const char* buffer, ssize_t size) } case MessageType::UNIGNORE_HEAP: { -#if SIMGRID_HAVE_MC +#if SIMGRID_HAVE_STATEFUL_MC if (remote_memory_ != nullptr) { s_mc_message_ignore_memory_t message; xbt_assert(size == sizeof(message), "Broken message"); @@ -328,7 +328,7 @@ bool CheckerSide::handle_message(const char* buffer, ssize_t size) } case MessageType::IGNORE_MEMORY: { -#if SIMGRID_HAVE_MC +#if SIMGRID_HAVE_STATEFUL_MC if (remote_memory_ != nullptr) { s_mc_message_ignore_memory_t message; xbt_assert(size == sizeof(message), "Broken message"); @@ -341,7 +341,7 @@ bool CheckerSide::handle_message(const char* buffer, ssize_t size) } case MessageType::STACK_REGION: { -#if SIMGRID_HAVE_MC +#if SIMGRID_HAVE_STATEFUL_MC if (remote_memory_ != nullptr) { s_mc_message_stack_region_t message; xbt_assert(size == sizeof(message), "Broken message"); @@ -354,7 +354,7 @@ bool CheckerSide::handle_message(const char* buffer, ssize_t size) } case MessageType::REGISTER_SYMBOL: { -#if SIMGRID_HAVE_MC +#if SIMGRID_HAVE_STATEFUL_MC s_mc_message_register_symbol_t message; xbt_assert(size == sizeof(message), "Broken message"); memcpy(&message, buffer, sizeof(message)); @@ -394,7 +394,7 @@ void CheckerSide::wait_for_requests() void CheckerSide::clear_memory_cache() { -#if SIMGRID_HAVE_MC +#if SIMGRID_HAVE_STATEFUL_MC if (remote_memory_) remote_memory_->clear_cache(); #endif diff --git a/src/mc/remote/CheckerSide.hpp b/src/mc/remote/CheckerSide.hpp index eeaa54e623..84c70d1252 100644 --- a/src/mc/remote/CheckerSide.hpp +++ b/src/mc/remote/CheckerSide.hpp @@ -21,7 +21,7 @@ class CheckerSide { event* socket_event_; event* signal_event_; std::unique_ptr base_{nullptr, &event_base_free}; -#if SIMGRID_HAVE_MC +#if SIMGRID_HAVE_STATEFUL_MC std::unique_ptr remote_memory_; #endif @@ -66,7 +66,7 @@ public: pid_t get_pid() const { return pid_; } bool running() const { return running_; } void terminate() { running_ = false; } -#if SIMGRID_HAVE_MC +#if SIMGRID_HAVE_STATEFUL_MC RemoteProcessMemory* get_remote_memory() { return remote_memory_.get(); } #endif }; diff --git a/src/mc/transition/TransitionActorJoin.cpp b/src/mc/transition/TransitionActorJoin.cpp index 49331de852..c6e1533998 100644 --- a/src/mc/transition/TransitionActorJoin.cpp +++ b/src/mc/transition/TransitionActorJoin.cpp @@ -7,10 +7,6 @@ #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 diff --git a/src/mc/transition/TransitionAny.cpp b/src/mc/transition/TransitionAny.cpp index 0f10bb1080..4813a00ff8 100644 --- a/src/mc/transition/TransitionAny.cpp +++ b/src/mc/transition/TransitionAny.cpp @@ -7,10 +7,6 @@ #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 diff --git a/src/simgrid/sg_version.cpp b/src/simgrid/sg_version.cpp index 3452c3b96a..1428132895 100644 --- a/src/simgrid/sg_version.cpp +++ b/src/simgrid/sg_version.cpp @@ -50,10 +50,10 @@ void sg_version() XBT_HELP("This program was linked against %s (git: %s), found in %s.", SIMGRID_VERSION_STRING, SIMGRID_GIT_VERSION, SIMGRID_INSTALL_PREFIX); -#if SIMGRID_HAVE_MC - XBT_HELP(" Model-checking support compiled in."); +#if SIMGRID_HAVE_STATEFUL_MC + XBT_HELP(" Stateful model-checking support compiled in."); #else - XBT_HELP(" Model-checking support disabled at compilation."); + XBT_HELP(" Stateful model-checking support disabled at compilation."); #endif #if SIMGRID_HAVE_NS3 diff --git a/src/smpi/internals/smpi_config.cpp b/src/smpi/internals/smpi_config.cpp index 614a00e264..84f6edce68 100644 --- a/src/smpi/internals/smpi_config.cpp +++ b/src/smpi/internals/smpi_config.cpp @@ -33,10 +33,8 @@ #include /* trim */ #include -#if SIMGRID_HAVE_MC #include "src/mc/mc_config.hpp" #include "src/mc/mc_replay.hpp" -#endif #if defined(__APPLE__) # include @@ -308,7 +306,6 @@ void smpi_init_options_internal(bool called_by_smpi_main) void smpi_check_options() { -#if SIMGRID_HAVE_MC if (MC_is_active() || MC_record_replay_is_active()) { if (_sg_mc_buffering == "zero") simgrid::config::set_value("smpi/send-is-detached-thresh", 0); @@ -317,7 +314,6 @@ void smpi_check_options() else THROW_IMPOSSIBLE; } -#endif xbt_assert(smpi_cfg_async_small_thresh() <= smpi_cfg_detached_send_thresh(), "smpi/async-small-thresh (=%d) should be smaller or equal to smpi/send-is-detached-thresh (=%d)", @@ -336,4 +332,3 @@ void smpi_check_options() simgrid::smpi::colls::set_collectives(); simgrid::smpi::colls::smpi_coll_cleanup_callback = nullptr; } - diff --git a/teshsuite/mc/CMakeLists.txt b/teshsuite/mc/CMakeLists.txt index 1abeed4b37..dbd5479188 100644 --- a/teshsuite/mc/CMakeLists.txt +++ b/teshsuite/mc/CMakeLists.txt @@ -1,4 +1,4 @@ -if (NOT SIMGRID_HAVE_MC) +if (NOT SIMGRID_HAVE_STATEFUL_MC) set(dwarf_disable 1) set(dwarf-expression_disable 1) endif() @@ -40,7 +40,7 @@ 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) -IF(SIMGRID_HAVE_MC) +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() diff --git a/tools/cmake/CTestConfig.cmake b/tools/cmake/CTestConfig.cmake index 53e2835b78..5ef4600bd1 100644 --- a/tools/cmake/CTestConfig.cmake +++ b/tools/cmake/CTestConfig.cmake @@ -17,7 +17,7 @@ if(enable_compile_warnings AND enable_compile_optimizations) SET(BUILDNAME "FULL_FLAGS" CACHE INTERNAL "Buildname" FORCE) endif() -if(SIMGRID_HAVE_MC) +if(SIMGRID_HAVE_STATEFUL_MC) SET(BUILDNAME "MODEL-CHECKING" CACHE INTERNAL "Buildname" FORCE) endif() diff --git a/tools/cmake/DefinePackages.cmake b/tools/cmake/DefinePackages.cmake index a20edb328a..9e2200f21f 100644 --- a/tools/cmake/DefinePackages.cmake +++ b/tools/cmake/DefinePackages.cmake @@ -554,7 +554,7 @@ set(MC_SRC_BASE src/mc/transition/TransitionSynchro.hpp ) -set(MC_SRC +set(MC_SRC_STATEFUL src/mc/explo/CommunicationDeterminismChecker.cpp src/mc/explo/LivenessChecker.cpp src/mc/explo/LivenessChecker.hpp @@ -769,8 +769,8 @@ if(enable_smpi) set(simgrid_sources ${simgrid_sources} ${SMPI_SRC}) endif() -if(SIMGRID_HAVE_MC) - set(simgrid_sources ${simgrid_sources} ${MC_SRC}) +if(SIMGRID_HAVE_STATEFUL_MC) + set(simgrid_sources ${simgrid_sources} ${MC_SRC_STATEFUL}) endif() if(SIMGRID_HAVE_NS3) diff --git a/tools/cmake/Tests.cmake b/tools/cmake/Tests.cmake index ce7d830116..21e0c24a24 100644 --- a/tools/cmake/Tests.cmake +++ b/tools/cmake/Tests.cmake @@ -136,7 +136,7 @@ set(MC_UNIT_TESTS src/mc/sosp/Snapshot_test.cpp src/mc/explo/udpor/UnfoldingEvent_test.cpp src/mc/explo/udpor/History_test.cpp src/mc/explo/udpor/Configuration_test.cpp) -if (SIMGRID_HAVE_MC) +if (SIMGRID_HAVE_STATEFUL_MC) set(UNIT_TESTS ${UNIT_TESTS} ${MC_UNIT_TESTS}) else() set(EXTRA_DIST ${EXTRA_DIST} ${MC_UNIT_TESTS})