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")
- 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``
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 <install_src_deps>` to activate this option.
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
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.
# 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)
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()
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)
# 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()
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
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)
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})
#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"
#include <boost/algorithm/string/predicate.hpp>
#include <dlfcn.h>
-#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 {
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;
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
}
RemoteApp::RemoteApp(const std::vector<char*>& args, bool need_memory_introspection) : app_args_(args)
{
if (need_memory_introspection) {
+#if SIMGRID_HAVE_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
+ 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));
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
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
*/
class XBT_PUBLIC RemoteApp {
private:
- std::unique_ptr<CheckerSide> checker_side_;
+#if SIMGRID_HAVE_MC
PageStore page_store_{500};
std::shared_ptr<simgrid::mc::Snapshot> initial_snapshot_;
+#else
+ void* initial_snapshot_ = nullptr; // The code tests it to decide whether to use the refork exec path
+#endif
+ std::unique_ptr<CheckerSide> checker_side_;
std::unique_ptr<CheckerSide> application_factory_; // when no meminfo, create checker_side_ by cloning this one
int master_socket_ = -1;
/** 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
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<simgrid::mc::Snapshot>(num_, remote_app.get_page_store(),
*remote_app.get_remote_process_memory());
+#endif
}
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 ((_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());
+#endif
/* If we want sleep set reduction, copy the sleep set and eventually removes things from it */
if (_sg_mc_sleep_set) {
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())) {
throw TerminationError();
}
}
+#endif
}
RecordTrace DFSExplorer::get_record_trace() // override
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));
// 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());
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();
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);
std::unique_ptr<Exploration> explo;
+#if SIMGRID_HAVE_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)
explo = std::unique_ptr<Exploration>(create_udpor_checker(argv_copy));
- else if (_sg_mc_property_file.get().empty())
- explo = std::unique_ptr<Exploration>(create_dfs_exploration(argv_copy, cfg_use_DPOR()));
- else
+ else if (not _sg_mc_property_file.get().empty())
explo = std::unique_ptr<Exploration>(create_liveness_checker(argv_copy));
+ else
+#endif
+ explo = std::unique_ptr<Exploration>(create_dfs_exploration(argv_copy, cfg_use_DPOR()));
try {
explo->run();
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);
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) {
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()
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
}
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) */
MC_record_path() = value;
}};
-#if SIMGRID_HAVE_MC
simgrid::config::Flag<bool> _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());
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<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 "
"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<std::string> _sg_mc_buffering{
"smpi/buffering",
}
return cfg_mc_reduction.get() == "dpor";
}
-
-#endif
}
}
-#if SIMGRID_HAVE_MC
-
std::string simgrid::mc::RecordTrace::to_string() const
{
std::ostringstream stream;
}
return stream.str();
}
-
-#endif
-
} // namespace simgrid::mc
}
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
{
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
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 = {};
}
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
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
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");
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
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 = {};
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
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_);
/* We now have enough info to create the memory address space */
remote_memory_ = std::make_unique<simgrid::mc::RemoteProcessMemory>(pid_, answer.mmalloc_default_mdp);
+#else
+ xbt_die("Cannot introspect memory without MC support");
+#endif
}
wait_for_requests();
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");
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));
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;
}
void CheckerSide::clear_memory_cache()
{
+#if SIMGRID_HAVE_MC
if (remote_memory_)
remote_memory_->clear_cache();
+#endif
}
void CheckerSide::handle_dead_child(int status)
event* socket_event_;
event* signal_event_;
std::unique_ptr<event_base, decltype(&event_base_free)> base_{nullptr, &event_base_free};
+#if SIMGRID_HAVE_MC
std::unique_ptr<RemoteProcessMemory> remote_memory_;
+#endif
Channel channel_;
bool running_ = false;
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
#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"
#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 <sstream>
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);
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
#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 <sstream>
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)
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
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
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
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
