include src/mc/AddressSpace.hpp
include src/mc/ModelChecker.cpp
include src/mc/ModelChecker.hpp
-include src/mc/Session.cpp
-include src/mc/Session.hpp
include src/mc/VisitedState.cpp
include src/mc/VisitedState.hpp
include src/mc/api.cpp
include src/mc/api.hpp
include src/mc/api/ActorState.hpp
+include src/mc/api/RemoteApp.cpp
+include src/mc/api/RemoteApp.hpp
include src/mc/api/State.cpp
include src/mc/api/State.hpp
include src/mc/compare.cpp
for (auto const& s : mc_model_checker->get_exploration()->get_textual_trace())
XBT_INFO(" %s", s.c_str());
XBT_INFO("Path = %s", mc_model_checker->get_exploration()->get_record_trace().to_string().c_str());
- Api::get().get_session().log_state();
+ Api::get().get_remote_app().log_state();
if (xbt_log_no_loc) {
XBT_INFO("Stack trace not displayed because you passed --log=no_loc");
} else {
for (auto const& s : get_exploration()->get_textual_trace())
XBT_INFO(" %s", s.c_str());
XBT_INFO("Path = %s", get_exploration()->get_record_trace().to_string().c_str());
- Api::get().get_session().log_state();
+ Api::get().get_remote_app().log_state();
this->exit(SIMGRID_MC_EXIT_SAFETY);
#include "src/kernel/activity/MailboxImpl.hpp"
#include "src/kernel/activity/MutexImpl.hpp"
#include "src/kernel/actor/SimcallObserver.hpp"
-#include "src/mc/Session.hpp"
+#include "src/mc/api/RemoteApp.hpp"
#include "src/mc/explo/Exploration.hpp"
#include "src/mc/mc_base.hpp"
#include "src/mc/mc_exit.hpp"
simgrid::mc::Exploration* Api::initialize(char** argv, const std::unordered_map<std::string, std::string>& env,
simgrid::mc::ExplorationAlgorithm algo)
{
- session_ = std::make_unique<simgrid::mc::Session>([argv, &env] {
+ remote_app_ = std::make_unique<simgrid::mc::RemoteApp>([argv, &env] {
int i = 1;
while (argv[i] != nullptr && argv[i][0] == '-')
i++;
simgrid::mc::Exploration* explo;
switch (algo) {
case ExplorationAlgorithm::CommDeterminism:
- explo = simgrid::mc::create_communication_determinism_checker(session_.get());
+ explo = simgrid::mc::create_communication_determinism_checker(remote_app_.get());
break;
case ExplorationAlgorithm::UDPOR:
- explo = simgrid::mc::create_udpor_checker(session_.get());
+ explo = simgrid::mc::create_udpor_checker(remote_app_.get());
break;
case ExplorationAlgorithm::Safety:
- explo = simgrid::mc::create_dfs_exploration(session_.get());
+ explo = simgrid::mc::create_dfs_exploration(remote_app_.get());
break;
case ExplorationAlgorithm::Liveness:
- explo = simgrid::mc::create_liveness_checker(session_.get());
+ explo = simgrid::mc::create_liveness_checker(remote_app_.get());
break;
default:
void Api::s_close()
{
- session_.reset();
+ remote_app_.reset();
if (simgrid::mc::property_automaton != nullptr) {
xbt_automaton_free(simgrid::mc::property_automaton);
simgrid::mc::property_automaton = nullptr;
#include <vector>
#include "simgrid/forward.h"
-#include "src/mc/Session.hpp"
+#include "src/mc/api/RemoteApp.hpp"
#include "src/mc/api/State.hpp"
#include "src/mc/mc_forward.hpp"
#include "src/mc/mc_record.hpp"
}
};
- std::unique_ptr<simgrid::mc::Session> session_;
+ std::unique_ptr<simgrid::mc::RemoteApp> remote_app_;
public:
// No copy:
simgrid::mc::Snapshot* take_snapshot(long num_state) const;
// SESSION APIs
- simgrid::mc::Session const& get_session() const { return *session_; }
+ simgrid::mc::RemoteApp const& get_remote_app() const { return *remote_app_; }
void s_close();
// AUTOMATION APIs
/* 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 "src/mc/Session.hpp"
+#include "src/mc/api/RemoteApp.hpp"
#include "src/internal_config.h" // HAVE_SMPI
#include "src/mc/explo/Exploration.hpp"
#include "src/mc/mc_config.hpp"
#ifdef __linux__
// Make sure we do not outlive our parent
sigset_t mask;
- sigemptyset (&mask);
+ sigemptyset(&mask);
xbt_assert(sigprocmask(SIG_SETMASK, &mask, nullptr) >= 0, "Could not unblock signals");
xbt_assert(prctl(PR_SET_PDEATHSIG, SIGHUP) == 0, "Could not PR_SET_PDEATHSIG");
#endif
code();
}
-Session::Session(const std::function<void()>& code)
+RemoteApp::RemoteApp(const std::function<void()>& code)
{
#if HAVE_SMPI
- smpi_init_options();//only performed once
+ smpi_init_options(); // only performed once
xbt_assert(smpi_cfg_privatization() != SmpiPrivStrategies::MMAP,
"Please use the dlopen privatization schema when model-checking SMPI code");
#endif
model_checker_->start();
}
-Session::~Session()
+RemoteApp::~RemoteApp()
{
this->close();
}
/** The application must be stopped. */
-void Session::take_initial_snapshot()
+void RemoteApp::take_initial_snapshot()
{
xbt_assert(initial_snapshot_ == nullptr);
model_checker_->wait_for_requests();
initial_snapshot_ = std::make_shared<simgrid::mc::Snapshot>(0);
}
-void Session::restore_initial_state() const
+void RemoteApp::restore_initial_state() const
{
this->initial_snapshot_->restore(&model_checker_->get_remote_process());
}
-void Session::log_state() const
+void RemoteApp::log_state() const
{
model_checker_->get_exploration()->log_state();
fprintf(dot_output, "}\n");
fclose(dot_output);
}
- if (getenv("SIMGRID_MC_SYSTEM_STATISTICS")){
- int ret=system("free");
+ if (getenv("SIMGRID_MC_SYSTEM_STATISTICS")) {
+ int ret = system("free");
if (ret != 0)
XBT_WARN("Call to system(free) did not return 0, but %d", ret);
}
}
-void Session::close()
+void RemoteApp::close()
{
initial_snapshot_ = nullptr;
if (model_checker_) {
}
}
-void
Session::get_actors_status(std::map<aid_t, ActorState>& whereto)
+void
RemoteApp::get_actors_status(std::map<aid_t, ActorState>& whereto)
{
s_mc_message_t msg;
memset(&msg, 0, sizeof msg);
whereto.insert(std::make_pair(actor.aid, ActorState(actor.aid, actor.enabled, actor.max_considered)));
}
-void Session::check_deadlock() const
+void RemoteApp::check_deadlock() const
{
xbt_assert(model_checker_->channel().send(MessageType::DEADLOCK_CHECK) == 0, "Could not check deadlock state");
s_mc_message_int_t message;
/* 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. */
-#ifndef SIMGRID_MC_SESSION_HPP
-#define SIMGRID_MC_SESSION_HPP
+#ifndef SIMGRID_MC_REMOTE_APP_HPP
+#define SIMGRID_MC_REMOTE_APP_HPP
#include "simgrid/forward.h"
#include "src/mc/ModelChecker.hpp"
namespace simgrid::mc {
-/** A model-checking session
+/** High-level view of the verified application, from the model-checker POV
*
* This is expected to become the interface used by model-checking
* algorithms to control the execution of the model-checked process
* algorithms should be able to be written in high-level languages
* (e.g. Python) using bindings on this interface.
*/
-class XBT_PUBLIC Session {
+class XBT_PUBLIC RemoteApp {
private:
std::unique_ptr<ModelChecker> model_checker_;
std::shared_ptr<simgrid::mc::Snapshot> initial_snapshot_;
// No copy:
- Session(Session const&) = delete;
- Session& operator=(Session const&) = delete;
+ RemoteApp(RemoteApp const&) = delete;
+ RemoteApp& operator=(RemoteApp const&) = delete;
public:
/** Create a new session by executing the provided code in a fork()
*
* The code is expected to `exec` the model-checked application.
*/
- explicit Session(const std::function<void()>& code);
+ explicit RemoteApp(const std::function<void()>& code);
- ~Session();
+ ~RemoteApp();
void close();
void take_initial_snapshot();
long State::expended_states_ = 0;
-State::State(Session& session) : num_(++expended_states_)
+State::State(RemoteApp& remote_app) : num_(++expended_states_)
{
- session.get_actors_status(actors_to_run_);
+ remote_app.get_actors_status(actors_to_run_);
transition_.reset(new Transition());
/* Stateful model checking */
#define SIMGRID_MC_STATE_HPP
#include "src/mc/api/ActorState.hpp"
+#include "src/mc/api/RemoteApp.hpp"
#include "src/mc/sosp/Snapshot.hpp"
#include "src/mc/transition/Transition.hpp"
std::shared_ptr<Snapshot> system_state_;
public:
- explicit State(Session& session);
+ explicit State(RemoteApp& remote_app);
/* Returns a positive number if there is another transition to pick, or -1 if not */
aid_t next_transition() const;
XBT_INFO("***** Non-send-deterministic communications pattern *****");
XBT_INFO("*********************************************************");
XBT_INFO("%s", send_diff.c_str());
- Api::get().get_session().log_state();
+ Api::get().get_remote_app().log_state();
Api::get().mc_exit(SIMGRID_MC_EXIT_NON_DETERMINISM);
} else if (_sg_mc_comms_determinism && (not send_deterministic && not recv_deterministic)) {
XBT_INFO("****************************************************");
XBT_INFO("%s", send_diff.c_str());
if (not recv_diff.empty())
XBT_INFO("%s", recv_diff.c_str());
- Api::get().get_session().log_state();
+ Api::get().get_remote_app().log_state();
Api::get().mc_exit(SIMGRID_MC_EXIT_NON_DETERMINISM);
}
}
}
*/
-Exploration* create_communication_determinism_checker(Session* session)
+Exploration* create_communication_determinism_checker(RemoteApp* remote_app)
{
CommDetExtension::EXTENSION_ID = simgrid::mc::Exploration::extension_create<CommDetExtension>();
StateCommDet::EXTENSION_ID = simgrid::mc::State::extension_create<StateCommDet>();
delete extension;
});
- return new DFSExplorer(session);
+ return new DFSExplorer(remote_app);
}
} // namespace simgrid::mc
state->get_transition()->to_string().c_str(), stack_.size(), state->get_num(), state->count_todo());
/* Create the new expanded state (copy the state of MCed into our MCer data) */
- auto next_state = std::make_unique<State>(get_session());
+ auto next_state = std::make_unique<State>(get_remote_app());
on_state_creation_signal(next_state.get());
if (_sg_mc_termination)
on_backtracking_signal();
stack_.pop_back();
- get_session().check_deadlock();
+ get_remote_app().check_deadlock();
/* Traverse the stack backwards until a state with a non empty interleave set is found, deleting all the states that
* have it empty in the way. For each deleted state, check if the request that has generated it (from its
}
/* if no snapshot, we need to restore the initial state and replay the transitions */
- get_session().restore_initial_state();
+ get_remote_app().restore_initial_state();
on_restore_initial_state_signal();
/* Traverse the stack from the state at position start and re-execute the transitions */
}
}
-DFSExplorer::DFSExplorer(Session* session) : Exploration(session)
+DFSExplorer::DFSExplorer(RemoteApp* remote_app) : Exploration(remote_app)
{
reductionMode_ = reduction_mode;
if (_sg_mc_termination)
(reductionMode_ == ReductionMode::none ? "none"
: (reductionMode_ == ReductionMode::dpor ? "dpor" : "unknown")));
- get_session().take_initial_snapshot();
+ get_remote_app().take_initial_snapshot();
XBT_DEBUG("Starting the DFS exploration");
- auto initial_state = std::make_unique<State>(get_session());
+ auto initial_state = std::make_unique<State>(get_remote_app());
XBT_DEBUG("**************************************************");
stack_.push_back(std::move(initial_state));
}
-Exploration* create_dfs_exploration(Session* session)
+Exploration* create_dfs_exploration(RemoteApp* remote_app)
{
- return new DFSExplorer(session);
+ return new DFSExplorer(remote_app);
}
} // namespace simgrid::mc
static xbt::signal<void()> on_log_state_signal;
public:
- explicit DFSExplorer(Session* session);
+ explicit DFSExplorer(RemoteApp* remote_app);
void run() override;
RecordTrace get_record_trace() override;
std::vector<std::string> get_textual_trace() override;
-/* Copyright (c) 2016-2022. The SimGrid Team.
- * All rights reserved. */
+/* Copyright (c) 2016-2022. 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. */
* you might be able to write your model-checking algorithm as plain
* imperative code instead.
*
- * It is expected to interact with the model-checking core through the
- * `Session` interface (but currently the `Session` interface does not
- * have all the necessary features). */
+ * It is expected to interact with the model-checked application through the
+ * `RemoteApp` interface (that is currently not perfectly sufficient to that extend). */
// abstract
class Exploration : public xbt::Extendable<Exploration> {
- Session* session_;
+ RemoteApp* remote_app_;
public:
- explicit Exploration(Session* session) : session_(session) {}
+ explicit Exploration(RemoteApp* remote_app) : remote_app_(remote_app) {}
// No copy:
Exploration(Exploration const&) = delete;
/** Log additional information about the state of the model-checker */
virtual void log_state() = 0;
- Session& get_session() { return *session_; }
+ RemoteApp& get_remote_app() { return *remote_app_; }
};
// External constructors so that the types (and the types of their content) remain hidden
-XBT_PUBLIC Exploration* create_liveness_checker(Session* session);
-XBT_PUBLIC Exploration* create_dfs_exploration(Session* session);
-XBT_PUBLIC Exploration* create_communication_determinism_checker(Session* session);
-XBT_PUBLIC Exploration* create_udpor_checker(Session* session);
+XBT_PUBLIC Exploration* create_liveness_checker(RemoteApp* remote_app);
+XBT_PUBLIC Exploration* create_dfs_exploration(RemoteApp* remote_app);
+XBT_PUBLIC Exploration* create_communication_determinism_checker(RemoteApp* remote_app);
+XBT_PUBLIC Exploration* create_udpor_checker(RemoteApp* remote_app);
} // namespace simgrid::mc
* under the terms of the license (GNU LGPL) which comes with this package. */
#include "src/mc/explo/LivenessChecker.hpp"
-#include "src/mc/Session.hpp"
+#include "src/mc/api/RemoteApp.hpp"
#include "src/mc/mc_config.hpp"
#include "src/mc/mc_exit.hpp"
#include "src/mc/mc_private.hpp"
}
}
- get_session().restore_initial_state();
+ get_remote_app().restore_initial_state();
/* Traverse the stack from the initial state and re-execute the transitions */
int depth = 1;
}
}
-LivenessChecker::LivenessChecker(Session* session) : Exploration(session) {}
+LivenessChecker::LivenessChecker(RemoteApp* remote_app) : Exploration(remote_app) {}
RecordTrace LivenessChecker::get_record_trace() // override
{
++expanded_pairs_count_;
auto next_pair = std::make_shared<Pair>(expanded_pairs_count_);
next_pair->prop_state_ = state;
- next_pair->app_state_ = std::make_shared<State>(get_session());
+ next_pair->app_state_ = std::make_shared<State>(get_remote_app());
next_pair->atomic_propositions = std::move(propositions);
if (current_pair)
next_pair->depth = current_pair->depth + 1;
Api::get().automaton_load(_sg_mc_property_file.get().c_str());
XBT_DEBUG("Starting the liveness algorithm");
- get_session().take_initial_snapshot();
+ get_remote_app().take_initial_snapshot();
/* Initialize */
this->previous_pair_ = 0;
log_state();
}
-Exploration* create_liveness_checker(Session* session)
+Exploration* create_liveness_checker(RemoteApp* remote_app)
{
- return new LivenessChecker(session);
+ return new LivenessChecker(remote_app);
}
} // namespace simgrid::mc
class XBT_PRIVATE LivenessChecker : public Exploration {
public:
- explicit LivenessChecker(Session* session);
+ explicit LivenessChecker(RemoteApp* remote_app);
void run() override;
RecordTrace get_record_trace() override;
std::vector<std::string> get_textual_trace() override;
namespace simgrid::mc {
-UdporChecker::UdporChecker(Session* session) : Exploration(session) {}
+UdporChecker::UdporChecker(RemoteApp* remote_app) : Exploration(remote_app) {}
void UdporChecker::run() {}
void UdporChecker::log_state() {}
-Exploration* create_udpor_checker(Session* session)
+Exploration* create_udpor_checker(RemoteApp* remote_app)
{
- return new UdporChecker(session);
+ return new UdporChecker(remote_app);
}
} // namespace simgrid::mc
class XBT_PRIVATE UdporChecker : public Exploration {
public:
- explicit UdporChecker(Session* session);
+ explicit UdporChecker(RemoteApp* remote_app);
void run() override;
RecordTrace get_record_trace() override;
std::vector<std::string> get_textual_trace() override;
#if SIMGRID_HAVE_MC
#include "src/mc/ModelChecker.hpp"
-#include "src/mc/Session.hpp"
+#include "src/mc/api/RemoteApp.hpp"
#include "src/mc/remote/RemoteProcess.hpp"
#endif
#include "src/kernel/actor/ActorImpl.hpp"
#if SIMGRID_HAVE_MC
-#include "src/mc/Session.hpp"
+#include "src/mc/api/RemoteApp.hpp"
#include "src/mc/explo/Exploration.hpp"
#include "src/mc/inspect/mc_unw.hpp"
#include "src/mc/mc_config.hpp"
#include <simgrid/config.h>
#if SIMGRID_HAVE_MC
#include "src/mc/ModelChecker.hpp"
-#include "src/mc/Session.hpp"
+#include "src/mc/api/RemoteApp.hpp"
#include "src/mc/api/State.hpp"
#endif
#include <simgrid/config.h>
#if SIMGRID_HAVE_MC
#include "src/mc/ModelChecker.hpp"
-#include "src/mc/Session.hpp"
+#include "src/mc/api/RemoteApp.hpp"
#include "src/mc/api/State.hpp"
#endif
src/mc/AddressSpace.hpp
src/mc/ModelChecker.cpp
src/mc/ModelChecker.hpp
- src/mc/Session.cpp
- src/mc/Session.hpp
src/mc/VisitedState.cpp
src/mc/VisitedState.hpp
src/mc/api.cpp
src/mc/api.hpp
+ src/mc/api/ActorState.hpp
src/mc/api/State.cpp
src/mc/api/State.hpp
- src/mc/api/ActorState.hpp
+ src/mc/api/RemoteApp.cpp
+ src/mc/api/RemoteApp.hpp
src/mc/compare.cpp
src/mc/mc_client_api.cpp
src/mc/mc_exit.hpp
