Rename SIMGRID_HAVE_MC into SIMGRID_HAVE_STATEFUL_MC (so that MC can be optional...

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 4fa8107..a3cc8d4 100644 (file)
--- 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 82fcc27..a0705d7 100644 (file)
--- 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 4065548..c2b3186 100644 (file)
--- 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 33f0815..2b7e823 100644 (file)
--- 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 6ef3fd7..83977db 100644 (file)
--- 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 2c0b849..5d61fb0 100644 (file)
--- a/include/smpi/mpi.h
+++ b/include/smpi/mpi.h
@@ -17,10 +17,8 @@
 
 #include <sys/time.h> /* 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 <smpi/smpi_extended_traces.h>

diff --git a/src/kernel/actor/Simcall.cpp b/src/kernel/actor/Simcall.cpp
index d34a22d..87605e4 100644 (file)
--- 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<void()> 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 13e7e9a..1f3cd31 100644 (file)
--- a/src/kernel/context/ContextSwapped.cpp
+++ b/src/kernel/context/ContextSwapped.cpp
@@ -82,8 +82,8 @@ SwappedContext::SwappedContext(std::function<void()>&& 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<unsigned char*>(xbt_malloc0(size + xbt_pagesize));
       stack_               = alloc - (reinterpret_cast<uintptr_t>(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<unsigned char**>(stack_)[-1];
 #endif

diff --git a/src/kernel/context/ContextUnix.cpp b/src/kernel/context/ContextUnix.cpp
index 7515e93..98e372d 100644 (file)
--- a/src/kernel/context/ContextUnix.cpp
+++ b/src/kernel/context/ContextUnix.cpp
@@ -61,7 +61,7 @@ UContext::UContext(std::function<void()>&& 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 3c6365c..cb9450d 100644 (file)
--- 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<char*>& 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<simgrid::mc::CheckerSide>(app_args_, need_memory_introspection);
     initial_snapshot_ = std::make_shared<simgrid::mc::Snapshot>(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 c3d0518..82a93db 100644 (file)
--- 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<simgrid::mc::Snapshot> 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 aac9c32..69fae98 100644 (file)
--- 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<simgrid::mc::Snapshot>(num_, remote_app.get_page_store(),
@@ -52,8 +52,7 @@ State::State(RemoteApp& remote_app, std::shared_ptr<State> 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<simgrid::mc::Snapshot>(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 ad39ec5..2b2a625 100644 (file)
--- 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 d2a9b1f..eb3b8e7 100644 (file)
--- 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<void(RemoteApp&)> 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 1b0f50e..3e8a45b 100644 (file)
--- 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<VisitedState> visited_state_;
 #else

diff --git a/src/mc/explo/Exploration.cpp b/src/mc/explo/Exploration.cpp
index 6efe841..5d35347 100644 (file)
--- 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 4e3fc12..700c4b9 100644 (file)
--- 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<Exploration> explo;
 
-#if SIMGRID_HAVE_MC
+#if SIMGRID_HAVE_STATEFUL_MC
   if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
     explo = std::unique_ptr<Exploration>(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 acd042d..2c0370e 100644 (file)
--- 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 7707914..35381d3 100644 (file)
--- a/src/mc/mc_config.cpp
+++ b/src/mc/mc_config.cpp
@@ -8,7 +8,7 @@
 #include "src/simgrid/sg_config.hpp"
 #include <simgrid/modelchecker.h>
 
-#if SIMGRID_HAVE_MC
+#if SIMGRID_HAVE_STATEFUL_MC
 #include <string_view>
 #endif
 
@@ -62,7 +62,7 @@ simgrid::config::Flag<std::string> _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<int> _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 bc444ff..262fa72 100644 (file)
--- 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<double> 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 4e14c0a..a16898e 100644 (file)
--- 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 34bb539..f6b53c9 100644 (file)
--- 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 fb10475..ee2f858 100644 (file)
--- 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<char*>& 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 eeaa54e..84c70d1 100644 (file)
--- 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<event_base, decltype(&event_base_free)> base_{nullptr, &event_base_free};
-#if SIMGRID_HAVE_MC
+#if SIMGRID_HAVE_STATEFUL_MC
   std::unique_ptr<RemoteProcessMemory> 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 49331de..c6e1533 100644 (file)
--- 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 <sstream>
 

diff --git a/src/mc/transition/TransitionAny.cpp b/src/mc/transition/TransitionAny.cpp
index 0f10bb1..4813a00 100644 (file)
--- 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 <sstream>
 

diff --git a/src/simgrid/sg_version.cpp b/src/simgrid/sg_version.cpp
index 3452c3b..1428132 100644 (file)
--- 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 614a00e..84f6edc 100644 (file)
--- a/src/smpi/internals/smpi_config.cpp
+++ b/src/smpi/internals/smpi_config.cpp
@@ -33,10 +33,8 @@
 #include <boost/algorithm/string.hpp> /* trim */
 #include <boost/tokenizer.hpp>
 
-#if SIMGRID_HAVE_MC
 #include "src/mc/mc_config.hpp"
 #include "src/mc/mc_replay.hpp"
-#endif
 
 #if defined(__APPLE__)
 # include <AvailabilityMacros.h>
@@ -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<int>("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 1abeed4..dbd5479 100644 (file)
--- 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 53e2835..5ef4600 100644 (file)
--- 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 a20edb3..9e2200f 100644 (file)
--- 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 ce7d830..21e0c24 100644 (file)
--- 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})