-/* Copyright (c) 2015-2018. The SimGrid Team.
- * All rights reserved. */
+/* Copyright (c) 2015-2019. The SimGrid Team. All rights reserved. */
/* This program is free software; you can redistribute it and/or modify it
* under the terms of the license (GNU LGPL) which comes with this package. */
-#include <csignal>
-#include <fcntl.h>
-
-#include <functional>
-
-#include "xbt/log.h"
-#include "xbt/system_error.hpp"
-#include <mc/mc.h>
-#include <simgrid/modelchecker.h>
-#include <simgrid/sg_config.hpp>
-
#include "src/mc/Session.hpp"
#include "src/mc/checker/Checker.hpp"
+#include "src/mc/mc_config.hpp"
#include "src/mc/mc_private.hpp"
#include "src/mc/mc_state.hpp"
+#include "xbt/log.h"
+#include "xbt/system_error.hpp"
-#include "src/smpi/include/private.hpp"
+#include <fcntl.h>
+#ifdef __linux__
+#include <sys/prctl.h>
+#endif
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_Session, mc, "Model-checker session");
-extern std::string _sg_mc_dot_output_file;
namespace simgrid {
namespace mc {
Session::Session(pid_t pid, int socket)
{
std::unique_ptr<simgrid::mc::RemoteClient> process(new simgrid::mc::RemoteClient(pid, socket));
- // TODO, automatic detection of the config from the process
- process->privatized(smpi_privatize_global_variables != SmpiPrivStrategies::None);
- modelChecker_ = std::unique_ptr<ModelChecker>(
- new simgrid::mc::ModelChecker(std::move(process)));
+
+#if HAVE_SMPI
+ xbt_assert(smpi_privatize_global_variables != SmpiPrivStrategies::MMAP,
+ "Please use the dlopen privatization schema when model-checking SMPI code");
+#endif
+
+ model_checker_.reset(new simgrid::mc::ModelChecker(std::move(process)));
xbt_assert(mc_model_checker == nullptr);
- mc_model_checker = modelChecker_.get();
+ mc_model_checker = model_checker_.get();
mc_model_checker->start();
}
void Session::initialize()
{
- xbt_assert(initialSnapshot_ == nullptr);
+ xbt_assert(initial_snapshot_ == nullptr);
mc_model_checker->wait_for_requests();
- initialSnapshot_ = simgrid::mc::take_snapshot(0);
+ initial_snapshot_ = simgrid::mc::take_snapshot(0);
}
void Session::execute(Transition const& transition)
{
- modelChecker_->handle_simcall(transition);
- modelChecker_->wait_for_requests();
+ model_checker_->handle_simcall(transition);
+ model_checker_->wait_for_requests();
}
-void Session::restoreInitialState()
+void Session::restore_initial_state()
{
- simgrid::mc::restore_snapshot(this->initialSnapshot_);
+ this->initial_snapshot_->restore(&mc_model_checker->process());
}
-void Session::logState()
+void Session::log_state()
{
- mc_model_checker->getChecker()->logState();
+ mc_model_checker->getChecker()->log_state();
- if (not _sg_mc_dot_output_file.empty()) {
+ if (not _sg_mc_dot_output_file.get().empty()) {
fprintf(dot_output, "}\n");
fclose(dot_output);
}
}
// static
-Session* Session::fork(std::function<void()> code)
+Session* Session::fork(const std::function<void()>& code)
{
// Create a AF_LOCAL socketpair used for exchanging messages
// between the model-checker process (ourselves) and the model-checked
void Session::close()
{
- initialSnapshot_ = nullptr;
- if (modelChecker_) {
- modelChecker_->shutdown();
- modelChecker_ = nullptr;
+ initial_snapshot_ = nullptr;
+ if (model_checker_) {
+ model_checker_->shutdown();
+ model_checker_ = nullptr;
mc_model_checker = nullptr;
}
}