Only compile stateless MC when libevent is found

diff --git a/CMakeLists.txt b/CMakeLists.txt
index a3cc8d4..4acad42 100644 (file)
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -355,48 +355,46 @@ if(enable_model-checking AND minimal-bindings)
   message(FATAL_ERROR "Compile-time option 'minimal-bindings' cannot be enabled with 'model-checking'")
 endif()
 
-if(HAVE_MMAP)
-  SET(HAVE_MMALLOC 1)
-else()
-  SET(HAVE_MMALLOC 0)
-  if(enable_model-checking)
-    message(STATUS "Warning: support for model-checking has been disabled because you are missing either mmap or __thread.")
-  endif()
-  SET(enable_model-checking 0)
-endif()
-
 if(enable_mallocators)
   SET(SIMGRID_HAVE_MALLOCATOR 1)
 else()
   SET(SIMGRID_HAVE_MALLOCATOR 0)
 endif()
 
-find_package(Libevent REQUIRED)
-include_directories(${LIBEVENT_INCLUDE_DIR})
-set(SIMGRID_DEP "${SIMGRID_DEP} ${LIBEVENT_LIBRARIES}")
+SET(SIMGRID_HAVE_MC 0)
+SET(SIMGRID_HAVE_STATEFUL_MC 0)
+SET(HAVE_MMALLOC 0)
+
+find_package(Libevent)
+if(Libevent_FOUND)
+  message(STATUS "Found libevent. Stateless model-checking can be enabled.")
+  include_directories(${LIBEVENT_INCLUDE_DIR})
+  set(SIMGRID_DEP "${SIMGRID_DEP} ${LIBEVENT_LIBRARIES}")
+  SET(SIMGRID_HAVE_MC 1)
+else()
+  message(STATUS "libevent not found. Please install libevent-dev to enable the SimGrid model checker.")
+endif()
 
 if(enable_model-checking)
   include(FindLibunwind)
-  if(HAVE_LIBUNWIND)
-    SET(SIMGRID_DEP "${SIMGRID_DEP} ${LIBUNWIND_LIBRARIES}")
+  find_package(Libdw)
+  find_package(Libelf)
+  if(HAVE_MMAP AND HAVE_LIBUNWIND AND Libdw_FOUND AND Libelf_FOUND)
+    SET(SIMGRID_HAVE_STATEFUL_MC 1)
+    SET(HAVE_MMALLOC 1)
+    SET(SIMGRID_DEP "${SIMGRID_DEP} ${LIBUNWIND_LIBRARIES} ${LIBELF_LIBRARIES} ${LIBDW_LIBRARIES}")
+    include_directories(${LIBDW_INCLUDE_DIR} ${LIBELF_INCLUDE_DIR})
+    set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -gdwarf-4")
+    set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -gdwarf-4")
   else()
-    message(FATAL_ERROR "Please install libunwind-dev libdw-dev libelf-dev if you want to compile the SimGrid model checker.")
+    message(STATUS "Please install libunwind-dev libdw-dev libelf-dev if you want to compile the SimGrid model checker.")
+    set(HAVE_MMALLOC 0)
   endif()
-  find_package(Libdw REQUIRED)
-  find_package(Libelf REQUIRED)
-  include_directories(${LIBDW_INCLUDE_DIR} ${LIBELF_INCLUDE_DIR})
-  set(SIMGRID_DEP "${SIMGRID_DEP} ${LIBELF_LIBRARIES} ${LIBDW_LIBRARIES}")
-  set(SIMGRID_HAVE_STATEFUL_MC 1)
-  set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -gdwarf-4")
-  set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -gdwarf-4")
-else()
-  SET(SIMGRID_HAVE_STATEFUL_MC 0)
-  set(HAVE_MMALLOC 0)
 endif()
 mark_as_advanced(PATH_LIBDW_H)
 mark_as_advanced(PATH_LIBDW_LIB)
 
-if (enable_model-checking AND enable_ns3)
+if (SIMGRID_HAVE_MC AND enable_ns3) 
   message(WARNING "Activating both model-checking and ns-3 bindings is considered experimental.")
 endif()
 
@@ -938,6 +936,7 @@ message("        Compile Boost.Context support: ${HAVE_BOOST_CONTEXTS}")
 message("")
 message("        Maintainer mode .............: ${enable_maintainer_mode}")
 message("        Documentation ...............: ${enable_documentation}")
+message("        Stateless model checking ....: ${SIMGRID_HAVE_MC}")
 message("        Stateful model checking .....: ${SIMGRID_HAVE_STATEFUL_MC}")
 message("        Graphviz mode ...............: ${HAVE_GRAPHVIZ}")
 message("        Mallocators .................: ${enable_mallocators}")

diff --git a/examples/cpp/CMakeLists.txt b/examples/cpp/CMakeLists.txt
index a0705d7..777817c 100644 (file)
--- a/examples/cpp/CMakeLists.txt
+++ b/examples/cpp/CMakeLists.txt
@@ -16,15 +16,21 @@ set(_actor-stacksize_factories "^thread") # Threads ignore modifications of the
 # The maestro-set example only works for threads
 set(_maestro-set_factories "thread")
 
-# These tests timeout with threads, not sure why
-foreach(example mc-bugged1 mc-bugged2 mc-failing-assert mc-electric-fence)
-   set(_${example}_factories "^thread") # Timeout
-   add_dependencies(tests-mc s4u-${example})
-endforeach()
+if(SIMGRID_HAVE_MC)
+  # These tests timeout with threads, not sure why
+  foreach(example mc-bugged1 mc-bugged2 mc-failing-assert mc-electric-fence)
+    set(_${example}_factories "^thread") # Timeout
+    add_dependencies(tests-mc s4u-${example})
+  endforeach()
 
-if(enable_coverage)
-  foreach (example mc-bugged1 mc-bugged2 mc-electric-fence mc-failing-assert)
-    ADD_TEST(cover-${example} ${CMAKE_CURRENT_BINARY_DIR}/${example}/s4u-${example} ${CMAKE_HOME_DIRECTORY}/examples/platforms/model_checker_platform.xml)
+  if(enable_coverage)
+    foreach (example mc-bugged1 mc-bugged2 mc-electric-fence mc-failing-assert)
+      ADD_TEST(cover-${example} ${CMAKE_CURRENT_BINARY_DIR}/${example}/s4u-${example} ${CMAKE_HOME_DIRECTORY}/examples/platforms/model_checker_platform.xml)
+    endforeach()
+  endif()
+else()
+  foreach (example mc-bugged1 mc-bugged2  mc-centralized-mutex mc-failing-assert mc-electric-fence)
+    set(_${example}_disable 1)
   endforeach()
 endif()
 
@@ -81,21 +87,25 @@ endif()
 foreach (example synchro-barrier synchro-mutex synchro-semaphore)
   set(tesh_files ${tesh_files} ${CMAKE_CURRENT_SOURCE_DIR}/${example}/s4u-mc-${example}.tesh)
 
-  ADD_TESH(s4u-mc-${example}
-            --setenv bindir=${CMAKE_CURRENT_BINARY_DIR}/${example}
-            --setenv libdir=${CMAKE_BINARY_DIR}/lib
-            --setenv platfdir=${CMAKE_HOME_DIRECTORY}/examples/platforms
-            --setenv srcdir=${CMAKE_CURRENT_SOURCE_DIR}/${example}
-            --cd ${CMAKE_CURRENT_SOURCE_DIR}/${example}
-            ${CMAKE_HOME_DIRECTORY}/examples/cpp/${example}/s4u-mc-${example}.tesh)
+  if (SIMGRID_HAVE_MC)
+    ADD_TESH(s4u-mc-${example}
+              --setenv bindir=${CMAKE_CURRENT_BINARY_DIR}/${example}
+              --setenv libdir=${CMAKE_BINARY_DIR}/lib
+              --setenv platfdir=${CMAKE_HOME_DIRECTORY}/examples/platforms
+              --setenv srcdir=${CMAKE_CURRENT_SOURCE_DIR}/${example}
+              --cd ${CMAKE_CURRENT_SOURCE_DIR}/${example}
+              ${CMAKE_HOME_DIRECTORY}/examples/cpp/${example}/s4u-mc-${example}.tesh)
 
-  add_dependencies(tests-mc s4u-${example})
+    add_dependencies(tests-mc s4u-${example})
+  endif()
 endforeach()
 
-# Dependency on the regular tests
-foreach(example mc-centralized-mutex)
-  add_dependencies(tests-mc s4u-${example})
-endforeach()
+if (SIMGRID_HAVE_MC)
+  # Dependency on the regular tests
+  foreach(example mc-centralized-mutex)
+    add_dependencies(tests-mc s4u-${example})
+  endforeach()
+endif()
 
 if(NOT HAVE_GRAPHVIZ)
   set(_dag-from-dot_disable 1)
@@ -228,12 +238,14 @@ foreach(example mc-failing-assert)
 #                                      ${CMAKE_HOME_DIRECTORY}/examples/cpp/${example}/s4u-${example}-statequality.tesh)
 #  endif()
 
-  ADD_TESH(s4u-${example}-nodpor    --setenv bindir=${CMAKE_CURRENT_BINARY_DIR}/${example}
-                                    --setenv libdir=${CMAKE_BINARY_DIR}/lib
-                                    --setenv platfdir=${CMAKE_HOME_DIRECTORY}/examples/platforms
-                                    --setenv srcdir=${CMAKE_CURRENT_SOURCE_DIR}/${example}
-                                    --cd ${CMAKE_CURRENT_SOURCE_DIR}/${example}
-                                    ${CMAKE_HOME_DIRECTORY}/examples/cpp/${example}/s4u-${example}-nodpor.tesh)
+  if(SIMGRID_HAVE_MC)
+    ADD_TESH(s4u-${example}-nodpor    --setenv bindir=${CMAKE_CURRENT_BINARY_DIR}/${example}
+                                      --setenv libdir=${CMAKE_BINARY_DIR}/lib
+                                      --setenv platfdir=${CMAKE_HOME_DIRECTORY}/examples/platforms
+                                      --setenv srcdir=${CMAKE_CURRENT_SOURCE_DIR}/${example}
+                                      --cd ${CMAKE_CURRENT_SOURCE_DIR}/${example}
+                                      ${CMAKE_HOME_DIRECTORY}/examples/cpp/${example}/s4u-${example}-nodpor.tesh)
+  endif()                                    
   set(tesh_files    ${tesh_files}   ${CMAKE_HOME_DIRECTORY}/examples/cpp/${example}/s4u-${example}-statequality.tesh)
   set(tesh_files    ${tesh_files}   ${CMAKE_HOME_DIRECTORY}/examples/cpp/${example}/s4u-${example}-nodpor.tesh)
 endforeach()

diff --git a/examples/sthread/CMakeLists.txt b/examples/sthread/CMakeLists.txt
index 2b7e823..98811c2 100644 (file)
--- a/examples/sthread/CMakeLists.txt
+++ b/examples/sthread/CMakeLists.txt
@@ -19,8 +19,10 @@ foreach(x
     add_dependencies(tests pthread-${x})
     ADD_TESH_FACTORIES(pthread-${x} "^thread" --setenv libdir=${CMAKE_BINARY_DIR}/lib --cd ${CMAKE_BINARY_DIR}/examples/sthread ${CMAKE_CURRENT_SOURCE_DIR}/pthread-${x}.tesh)
 
-    add_dependencies(tests-mc pthread-${x})
-    ADD_TESH_FACTORIES(pthread-mc-${x} "^thread" --setenv libdir=${CMAKE_BINARY_DIR}/lib --cd ${CMAKE_BINARY_DIR}/examples/sthread ${CMAKE_CURRENT_SOURCE_DIR}/pthread-mc-${x}.tesh)
+    if(SIMGRID_HAVE_MC)
+      add_dependencies(tests-mc pthread-${x})
+      ADD_TESH_FACTORIES(pthread-mc-${x} "^thread" --setenv libdir=${CMAKE_BINARY_DIR}/lib --cd ${CMAKE_BINARY_DIR}/examples/sthread ${CMAKE_CURRENT_SOURCE_DIR}/pthread-mc-${x}.tesh)
+    endif()
   endif()
 
   set(tesh_files    ${tesh_files}    ${CMAKE_CURRENT_SOURCE_DIR}/pthread-${x}.tesh
@@ -44,8 +46,10 @@ foreach(x
       target_link_libraries(pthread-${x} PUBLIC "-Wl,-znorelro -Wl,-znoseparate-code") # TODO: convert to target_link_option once CMAKE_VERSION is >3.13
     endif()
 
-    add_dependencies(tests-mc pthread-${x})
-    ADD_TESH_FACTORIES(pthread-mc-${x} "^thread" --setenv libdir=${CMAKE_BINARY_DIR}/lib --cd ${CMAKE_BINARY_DIR}/examples/sthread ${CMAKE_CURRENT_SOURCE_DIR}/pthread-mc-${x}.tesh)
+    if(SIMGRID_HAVE_MC)
+      add_dependencies(tests-mc pthread-${x})
+      ADD_TESH_FACTORIES(pthread-mc-${x} "^thread" --setenv libdir=${CMAKE_BINARY_DIR}/lib --cd ${CMAKE_BINARY_DIR}/examples/sthread ${CMAKE_CURRENT_SOURCE_DIR}/pthread-mc-${x}.tesh)
+    endif()
   endif()
 
   set(tesh_files    ${tesh_files}    ${CMAKE_CURRENT_SOURCE_DIR}/pthread-mc-${x}.tesh)
@@ -68,8 +72,10 @@ foreach(example
     endif()
     set_target_properties(${example} PROPERTIES RUNTIME_OUTPUT_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR}/${example})
 
-    add_dependencies(tests-mc ${example})
-    ADD_TESH_FACTORIES(sthread-mc-${example} "^thread" --setenv libdir=${CMAKE_BINARY_DIR}/lib --cd ${CMAKE_BINARY_DIR}/examples/sthread/${example} ${CMAKE_CURRENT_SOURCE_DIR}/${example}/${example}.tesh)
+    if(SIMGRID_HAVE_MC)
+      add_dependencies(tests-mc ${example})
+      ADD_TESH_FACTORIES(sthread-mc-${example} "^thread" --setenv libdir=${CMAKE_BINARY_DIR}/lib --cd ${CMAKE_BINARY_DIR}/examples/sthread/${example} ${CMAKE_CURRENT_SOURCE_DIR}/${example}/${example}.tesh)
+    endif()
   endif()
 
   set(tesh_files    ${tesh_files}    ${CMAKE_CURRENT_SOURCE_DIR}/${example}/${example}.tesh)

diff --git a/include/simgrid/config.h.in b/include/simgrid/config.h.in
index 83977db..bb4f27e 100644 (file)
--- a/include/simgrid/config.h.in
+++ b/include/simgrid/config.h.in
@@ -11,6 +11,8 @@
 
 /* Were mallocators (object pools) compiled in? */
 #cmakedefine01 SIMGRID_HAVE_MALLOCATOR
+/* Was the model-checking compiled in? */
+#cmakedefine01 SIMGRID_HAVE_MC
 /* Was the stateful model-checking compiled in? */
 #cmakedefine01 SIMGRID_HAVE_STATEFUL_MC
 /* Was the ns-3 support compiled in? */

diff --git a/src/kernel/EngineImpl.cpp b/src/kernel/EngineImpl.cpp
index d8ce61f..5a6dd12 100644 (file)
--- a/src/kernel/EngineImpl.cpp
+++ b/src/kernel/EngineImpl.cpp
@@ -16,11 +16,14 @@
 #include "src/mc/mc.h"
 #include "src/mc/mc_record.hpp"
 #include "src/mc/mc_replay.hpp"
-#include "src/mc/remote/AppSide.hpp"
 #include "src/simgrid/math_utils.h"
 #include "src/simgrid/sg_config.hpp"
 #include "src/smpi/include/smpi_actor.hpp"
 
+#if SIMGRID_HAVE_MC
+#include "src/mc/remote/AppSide.hpp"
+#endif
+
 #include "xbt/log.hpp"
 
 #include <boost/algorithm/string/predicate.hpp>
@@ -168,10 +171,12 @@ void EngineImpl::initialize(int* argc, char** argv)
   xbt_assert(EngineImpl::instance_ == nullptr,
              "It is currently forbidden to create more than one instance of kernel::EngineImpl");
   EngineImpl::instance_ = this;
+#if SIMGRID_HAVE_MC
   // The communication initialization is done ASAP, as we need to get some init parameters from the MC for different
   // layers. But instance_ needs to be created, as we send the address of some of its fields to the MC that wants to
   // read them directly.
   simgrid::mc::AppSide::initialize();
+#endif
 
   if (static bool inited = false; not inited) {
     inited = true;
@@ -600,7 +605,11 @@ void EngineImpl::run(double max_date)
   seal_platform();
 
   if (MC_is_active()) {
+#if SIMGRID_HAVE_MC
     mc::AppSide::get()->main_loop();
+#else
+    xbt_die("MC_is_active() is not supposed to return true in non-MC settings");
+#endif
     THROW_IMPOSSIBLE; // main_loop never returns
   }
 

diff --git a/src/mc/mc_base.cpp b/src/mc/mc_base.cpp
index 2c0370e..8d8b66e 100644 (file)
--- a/src/mc/mc_base.cpp
+++ b/src/mc/mc_base.cpp
@@ -8,11 +8,12 @@
 #include "src/kernel/activity/CommImpl.hpp"
 #include "src/kernel/activity/MutexImpl.hpp"
 #include "src/kernel/actor/SimcallObserver.hpp"
-#include "src/mc/api/RemoteApp.hpp"
+
 #include "src/mc/mc.h"
 #include "src/mc/mc_config.hpp"
 #include "src/mc/mc_replay.hpp"
-#include "src/mc/remote/AppSide.hpp"
+/*#include "src/mc/api/RemoteApp.hpp"
+#include "src/mc/remote/AppSide.hpp"*/
 
 #if SIMGRID_HAVE_STATEFUL_MC
 #include "src/mc/sosp/RemoteProcessMemory.hpp"

diff --git a/src/mc/mc_client_api.cpp b/src/mc/mc_client_api.cpp
index fe18e7b..57e28cf 100644 (file)
--- a/src/mc/mc_client_api.cpp
+++ b/src/mc/mc_client_api.cpp
@@ -33,12 +33,17 @@ void MC_assert(int prop)
   // Cannot used xbt_assert here, or it would be an infinite recursion.
   xbt_assert(simgrid::mc::model_checking_mode != simgrid::mc::ModelCheckingMode::CHECKER_SIDE,
              "This should be called from the client side");
+#if SIMGRID_HAVE_MC
   if (not prop) {
     if (MC_is_active())
       simgrid::mc::AppSide::get()->report_assertion_failure();
     if (MC_record_replay_is_active())
       xbt_die("MC assertion failed");
   }
+#else
+  if (not prop)
+    xbt_die("Safety property violation detected without the model-checker");
+#endif
 }
 
 int MC_is_active()
@@ -49,28 +54,36 @@ int MC_is_active()
 
 void MC_automaton_new_propositional_symbol_pointer(const char *name, int* value)
 {
+#if SIMGRID_HAVE_MC
   xbt_assert(simgrid::mc::model_checking_mode != simgrid::mc::ModelCheckingMode::CHECKER_SIDE,
              "This should be called from the client side");
   simgrid::mc::AppSide::get()->declare_symbol(name, value);
+#endif
 }
 
 void MC_ignore(void* addr, size_t size)
 {
+#if SIMGRID_HAVE_MC
   xbt_assert(simgrid::mc::model_checking_mode != simgrid::mc::ModelCheckingMode::CHECKER_SIDE,
              "This should be called from the client side");
   simgrid::mc::AppSide::get()->ignore_memory(addr, size);
+#endif
 }
 
 void MC_ignore_heap(void *address, size_t size)
 {
+#if SIMGRID_HAVE_MC
   xbt_assert(simgrid::mc::model_checking_mode != simgrid::mc::ModelCheckingMode::CHECKER_SIDE,
              "This should be called from the client side");
   simgrid::mc::AppSide::get()->ignore_heap(address, size);
+#endif
 }
 
 void MC_unignore_heap(void* address, size_t size)
 {
+#if SIMGRID_HAVE_MC
   xbt_assert(simgrid::mc::model_checking_mode != simgrid::mc::ModelCheckingMode::CHECKER_SIDE,
              "This should be called from the client side");
   simgrid::mc::AppSide::get()->unignore_heap(address, size);
+#endif
 }

diff --git a/src/mc/transition/Transition.cpp b/src/mc/transition/Transition.cpp
index 4a80251..84ad991 100644 (file)
--- a/src/mc/transition/Transition.cpp
+++ b/src/mc/transition/Transition.cpp
@@ -5,6 +5,11 @@
 
 #include "src/mc/transition/Transition.hpp"
 #include "src/kernel/actor/Simcall.hpp"
+#include "xbt/asserts.h"
+#include "xbt/string.hpp"
+#include <simgrid/config.h>
+
+#if SIMGRID_HAVE_MC
 #include "src/mc/explo/Exploration.hpp"
 #include "src/mc/transition/TransitionActorJoin.hpp"
 #include "src/mc/transition/TransitionAny.hpp"
@@ -12,8 +17,7 @@
 #include "src/mc/transition/TransitionObjectAccess.hpp"
 #include "src/mc/transition/TransitionRandom.hpp"
 #include "src/mc/transition/TransitionSynchro.hpp"
-#include "xbt/asserts.h"
-#include "xbt/string.hpp"
+#endif
 
 #include <sstream>
 
@@ -43,12 +47,15 @@ std::string Transition::dot_string() const
 void Transition::replay(RemoteApp& app) const
 {
   replayed_transitions_++;
+#if SIMGRID_HAVE_MC
   app.handle_simcall(aid_, times_considered_, false);
   app.wait_for_requests();
+#endif
 }
 
 Transition* deserialize_transition(aid_t issuer, int times_considered, std::stringstream& stream)
 {
+#if SIMGRID_HAVE_MC
   short type;
   xbt_assert(stream >> type);
 
@@ -101,6 +108,9 @@ Transition* deserialize_transition(aid_t issuer, int times_considered, std::stri
   xbt_die("Invalid transition type %d received. Did you implement a new observer in the app without implementing the "
           "corresponding transition in the checker?",
           type);
+#else
+  xbt_die("Deserializing transitions is only interesting in MC mode.");
+#endif
 }
 
 } // namespace simgrid::mc

diff --git a/teshsuite/mc/CMakeLists.txt b/teshsuite/mc/CMakeLists.txt
index dbd5479..7addb33 100644 (file)
--- a/teshsuite/mc/CMakeLists.txt
+++ b/teshsuite/mc/CMakeLists.txt
@@ -40,18 +40,19 @@ set(teshsuite_src  ${teshsuite_src}
 set(tesh_files     ${tesh_files}    ${CMAKE_CURRENT_SOURCE_DIR}/random-bug/random-bug-replay.tesh
                                     ${CMAKE_CURRENT_SOURCE_DIR}/mutex-handling/without-mutex-handling.tesh PARENT_SCOPE)
 
+ADD_TESH(mc-random-bug-replay                --setenv platfdir=${CMAKE_HOME_DIRECTORY}/examples/platforms --setenv bindir=${CMAKE_BINARY_DIR}/teshsuite/mc/random-bug --cd ${CMAKE_HOME_DIRECTORY}/teshsuite/mc/random-bug random-bug-replay.tesh)
+IF(SIMGRID_HAVE_MC)
+  ADD_TESH(tesh-mc-mutex-handling              --setenv bindir=${CMAKE_BINARY_DIR}/teshsuite/mc/mutex-handling --setenv srcdir=${CMAKE_HOME_DIRECTORY} --cd ${CMAKE_HOME_DIRECTORY}/teshsuite/mc/mutex-handling mutex-handling.tesh --cfg=model-check/reduction:none)
+  ADD_TESH(tesh-mc-mutex-handling-dpor         --setenv bindir=${CMAKE_BINARY_DIR}/teshsuite/mc/mutex-handling --setenv srcdir=${CMAKE_HOME_DIRECTORY} --cd ${CMAKE_HOME_DIRECTORY}/teshsuite/mc/mutex-handling mutex-handling.tesh --cfg=model-check/reduction:dpor)
+  ADD_TESH(tesh-mc-without-mutex-handling      --setenv bindir=${CMAKE_BINARY_DIR}/teshsuite/mc/mutex-handling --setenv srcdir=${CMAKE_HOME_DIRECTORY} --cd ${CMAKE_HOME_DIRECTORY}/teshsuite/mc/mutex-handling without-mutex-handling.tesh --cfg=model-check/reduction:none)
+  ADD_TESH(tesh-mc-without-mutex-handling-dpor --setenv bindir=${CMAKE_BINARY_DIR}/teshsuite/mc/mutex-handling --setenv srcdir=${CMAKE_HOME_DIRECTORY} --cd ${CMAKE_HOME_DIRECTORY}/teshsuite/mc/mutex-handling without-mutex-handling.tesh --cfg=model-check/reduction:dpor)
+  ADD_TESH(mc-random-bug                       --setenv platfdir=${CMAKE_HOME_DIRECTORY}/examples/platforms --setenv bindir=${CMAKE_BINARY_DIR}/teshsuite/mc/random-bug --cd ${CMAKE_HOME_DIRECTORY}/teshsuite/mc/random-bug random-bug.tesh)
+ENDIF()
 IF(SIMGRID_HAVE_STATEFUL_MC)
   ADD_TESH(tesh-mc-dwarf                       --setenv bindir=${CMAKE_BINARY_DIR}/teshsuite/mc/dwarf            --cd ${CMAKE_HOME_DIRECTORY}/teshsuite/mc/dwarf dwarf.tesh)
   ADD_TESH(tesh-mc-dwarf-expression            --setenv bindir=${CMAKE_BINARY_DIR}/teshsuite/mc/dwarf-expression --cd ${CMAKE_HOME_DIRECTORY}/teshsuite/mc/dwarf-expression dwarf-expression.tesh)
 ENDIF()
 
-ADD_TESH(tesh-mc-mutex-handling              --setenv bindir=${CMAKE_BINARY_DIR}/teshsuite/mc/mutex-handling --setenv srcdir=${CMAKE_HOME_DIRECTORY} --cd ${CMAKE_HOME_DIRECTORY}/teshsuite/mc/mutex-handling mutex-handling.tesh --cfg=model-check/reduction:none)
-ADD_TESH(tesh-mc-mutex-handling-dpor         --setenv bindir=${CMAKE_BINARY_DIR}/teshsuite/mc/mutex-handling --setenv srcdir=${CMAKE_HOME_DIRECTORY} --cd ${CMAKE_HOME_DIRECTORY}/teshsuite/mc/mutex-handling mutex-handling.tesh --cfg=model-check/reduction:dpor)
-ADD_TESH(tesh-mc-without-mutex-handling      --setenv bindir=${CMAKE_BINARY_DIR}/teshsuite/mc/mutex-handling --setenv srcdir=${CMAKE_HOME_DIRECTORY} --cd ${CMAKE_HOME_DIRECTORY}/teshsuite/mc/mutex-handling without-mutex-handling.tesh --cfg=model-check/reduction:none)
-ADD_TESH(tesh-mc-without-mutex-handling-dpor --setenv bindir=${CMAKE_BINARY_DIR}/teshsuite/mc/mutex-handling --setenv srcdir=${CMAKE_HOME_DIRECTORY} --cd ${CMAKE_HOME_DIRECTORY}/teshsuite/mc/mutex-handling without-mutex-handling.tesh --cfg=model-check/reduction:dpor)
-ADD_TESH(mc-random-bug                       --setenv platfdir=${CMAKE_HOME_DIRECTORY}/examples/platforms --setenv bindir=${CMAKE_BINARY_DIR}/teshsuite/mc/random-bug --cd ${CMAKE_HOME_DIRECTORY}/teshsuite/mc/random-bug random-bug.tesh)
-ADD_TESH(mc-random-bug-replay                --setenv platfdir=${CMAKE_HOME_DIRECTORY}/examples/platforms --setenv bindir=${CMAKE_BINARY_DIR}/teshsuite/mc/random-bug --cd ${CMAKE_HOME_DIRECTORY}/teshsuite/mc/random-bug random-bug-replay.tesh)
-
 if(enable_coverage)
   ADD_TEST(cover-mc-mutex-handling ${CMAKE_CURRENT_BINARY_DIR}/mutex-handling/mutex-handling ${CMAKE_HOME_DIRECTORY}/examples/platforms/small_platform.xml)
 endif()

diff --git a/teshsuite/smpi/CMakeLists.txt b/teshsuite/smpi/CMakeLists.txt
index be77453..ce735ed 100644 (file)
--- a/teshsuite/smpi/CMakeLists.txt
+++ b/teshsuite/smpi/CMakeLists.txt
@@ -141,7 +141,7 @@ if(enable_smpi)
   if (NOT HAVE_SANITIZER_ADDRESS)
     ADD_TESH(tesh-smpi-coll-allreduce-with-leaks --setenv platfdir=${CMAKE_HOME_DIRECTORY}/examples/platforms --setenv bindir=${CMAKE_BINARY_DIR}/teshsuite/smpi/coll-allreduce-with-leaks --cd ${CMAKE_BINARY_DIR}/teshsuite/smpi/coll-allreduce-with-leaks ${CMAKE_HOME_DIRECTORY}/teshsuite/smpi/coll-allreduce-with-leaks/coll-allreduce-with-leaks.tesh)
     set_target_properties(coll-allreduce-with-leaks PROPERTIES COMPILE_FLAGS "-trace-call-location")
-    if(enable_model-checking)
+    if(SIMGRID_HAVE_MC)
       add_dependencies(tests-mc coll-allreduce-with-leaks)
       ADD_TESH(tesh-mc-smpi-coll-allreduce-with-leaks --setenv platfdir=${CMAKE_HOME_DIRECTORY}/examples/platforms --setenv bindir=${CMAKE_BINARY_DIR}/teshsuite/smpi/coll-allreduce-with-leaks --cd ${CMAKE_BINARY_DIR}/teshsuite/smpi/coll-allreduce-with-leaks ${CMAKE_HOME_DIRECTORY}/teshsuite/smpi/coll-allreduce-with-leaks/mc-coll-allreduce-with-leaks.tesh)
     endif()

diff --git a/tools/cmake/DefinePackages.cmake b/tools/cmake/DefinePackages.cmake
index 9e2200f..8492f25 100644 (file)
--- a/tools/cmake/DefinePackages.cmake
+++ b/tools/cmake/DefinePackages.cmake
@@ -518,13 +518,15 @@ set(MC_SRC_BASE
   src/mc/mc_record.hpp
   src/mc/mc_replay.hpp
   src/mc/transition/Transition.cpp
-
+  )
+  
+set(MC_SRC_STATELESS
   src/mc/api/ActorState.hpp
   src/mc/api/State.cpp
   src/mc/api/State.hpp
   src/mc/api/RemoteApp.cpp
   src/mc/api/RemoteApp.hpp
-
+  
   src/mc/explo/DFSExplorer.cpp
   src/mc/explo/DFSExplorer.hpp
   src/mc/explo/Exploration.cpp
@@ -769,6 +771,9 @@ if(enable_smpi)
   set(simgrid_sources  ${simgrid_sources}  ${SMPI_SRC})
 endif()
 
+if(SIMGRID_HAVE_MC)
+  set(simgrid_sources  ${simgrid_sources}  ${MC_SRC_STATELESS})
+endif()
 if(SIMGRID_HAVE_STATEFUL_MC)
   set(simgrid_sources  ${simgrid_sources}  ${MC_SRC_STATEFUL})
 endif()

diff --git a/tools/cmake/MakeLib.cmake b/tools/cmake/MakeLib.cmake
index 5575bb7..f41f3b7 100644 (file)
--- a/tools/cmake/MakeLib.cmake
+++ b/tools/cmake/MakeLib.cmake
@@ -42,17 +42,19 @@ if(HAVE_MMALLOC)
                 APPEND PROPERTY INCLUDE_DIRECTORIES "${INTERNAL_INCLUDES}")
 endif()
 
-add_executable(simgrid-mc ${MC_SIMGRID_MC_SRC})
-target_link_libraries(simgrid-mc simgrid)
-set_target_properties(simgrid-mc
-                      PROPERTIES RUNTIME_OUTPUT_DIRECTORY "${CMAKE_BINARY_DIR}/bin")
-set_property(TARGET simgrid-mc
-              APPEND PROPERTY INCLUDE_DIRECTORIES "${INTERNAL_INCLUDES}")
-install(TARGETS simgrid-mc # install that binary without breaking the rpath on Mac
-  RUNTIME DESTINATION ${CMAKE_INSTALL_BINDIR}/)
-add_dependencies(tests-mc simgrid-mc)
-if("${CMAKE_SYSTEM}" MATCHES "Linux")
-  add_dependencies(tests-mc sthread)
+if(SIMGRID_HAVE_MC)
+  add_executable(simgrid-mc ${MC_SIMGRID_MC_SRC})
+  target_link_libraries(simgrid-mc simgrid)
+  set_target_properties(simgrid-mc
+                        PROPERTIES RUNTIME_OUTPUT_DIRECTORY "${CMAKE_BINARY_DIR}/bin")
+  set_property(TARGET simgrid-mc
+                APPEND PROPERTY INCLUDE_DIRECTORIES "${INTERNAL_INCLUDES}")
+  install(TARGETS simgrid-mc # install that binary without breaking the rpath on Mac
+    RUNTIME DESTINATION ${CMAKE_INSTALL_BINDIR}/)
+  add_dependencies(tests-mc simgrid-mc)
+  if("${CMAKE_SYSTEM}" MATCHES "Linux")
+    add_dependencies(tests-mc sthread)
+  endif()
 endif()
 
 # Compute the dependencies of SimGrid

diff --git a/tools/cmake/Option.cmake b/tools/cmake/Option.cmake
index 0ff2fcc..19e3248 100644 (file)
--- a/tools/cmake/Option.cmake
+++ b/tools/cmake/Option.cmake
@@ -38,7 +38,7 @@ endif()
 option(minimal-bindings      "Whether to compile the Python bindings libraries with the minimal dependency set" off)
 mark_as_advanced(minimal-bindings)
 
-option(enable_model-checking "Turn this on to experiment with our prototype of model-checker (hinders the simulation's performance even if turned off at runtime)" off)
+option(enable_model-checking "Turn this on to experiment with our prototype of model-checker" on)
 option(enable-model-checking "Please set 'enable_model-checking' instead" off)
 mark_as_advanced(enable-model-checking)
 if(enable-model-checking)