#include "src/mc/mc_record.hpp"
#include "src/mc/mc_request.hpp"
#include "src/mc/mc_smx.hpp"
+#include "src/mc/mc_api.hpp"
#include "src/xbt/mmalloc/mmprivate.h"
+using mcapi = simgrid::mc::mc_api;
+
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_safety, mc, "Logging specific to MC safety verification ");
namespace simgrid {
XBT_INFO("Check a safety property. Reduction is: %s.",
(reductionMode_ == ReductionMode::none ? "none"
: (reductionMode_ == ReductionMode::dpor ? "dpor" : "unknown")));
- session->initialize();
+
+ mcapi::get().s_initialize();
XBT_DEBUG("Starting the safety algorithm");
XBT_DEBUG("Initial state");
/* Get an enabled actor and insert it in the interleave set of the initial state */
- for (auto& actor : mc_model_checker->get_remote_simulation().actors())
- if (actor_is_enabled(actor.copy.get_buffer())) {
+ auto actors = mcapi::get().get_actors();
+ for (auto& actor : actors)
+ if (mcapi::get().actor_is_enabled(actor.copy.get_buffer()->get_pid())) {
initial_state->add_interleaving_set(actor.copy.get_buffer());
if (reductionMode_ != ReductionMode::none)
break;
#include "src/mc/mc_config.hpp"
#include "src/mc/mc_exit.hpp"
#include "src/internal_config.h"
+#include "src/mc/mc_api.hpp"
#if HAVE_SMPI
#include "smpi/smpi.h"
#include <memory>
#include <unistd.h>
+using mcapi = simgrid::mc::mc_api;
+
static inline
char** argvdup(int argc, char** argv)
{
smpi_init_options(); // only performed once
#endif
sg_config_init(&argc, argv);
- simgrid::mc::session = new simgrid::mc::Session([argv_copy] {
- int i = 1;
- while (argv_copy[i] != nullptr && argv_copy[i][0] == '-')
- i++;
- xbt_assert(argv_copy[i] != nullptr,
- "Unable to find a binary to exec on the command line. Did you only pass config flags?");
- execvp(argv_copy[i], argv_copy + i);
- xbt_die("The model-checked process failed to exec(): %s", strerror(errno));
- });
+ mcapi::get().initialize(argv_copy);
delete[] argv_copy;
auto checker = create_checker(*simgrid::mc::session);
res = SIMGRID_MC_EXIT_LIVENESS;
}
checker = nullptr;
- simgrid::mc::session->close();
+ mcapi::get().s_close();
return res;
}
--- /dev/null
+#include "mc_api.hpp"
+
+#include "src/mc/Session.hpp"
+#include "src/mc/mc_private.hpp"
+#include "src/mc/remote/RemoteSimulation.hpp"
+#include <xbt/asserts.h>
+#include <xbt/log.h>
+
+XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_api, mc, "Logging specific to MC Fasade APIs ");
+
+namespace simgrid {
+namespace mc {
+
+void mc_api::initialize(char** argv)
+{
+ simgrid::mc::session = new simgrid::mc::Session([argv] {
+ int i = 1;
+ while (argv[i] != nullptr && argv[i][0] == '-')
+ i++;
+ xbt_assert(argv[i] != nullptr,
+ "Unable to find a binary to exec on the command line. Did you only pass config flags?");
+ execvp(argv[i], argv + i);
+ xbt_die("The model-checked process failed to exec(): %s", strerror(errno));
+ });
+}
+
+void mc_api::s_initialize() const
+{
+ session->initialize();
+}
+
+void mc_api::create_model_checker(std::unique_ptr<RemoteSimulation> remote_simulation, int sockfd)
+{
+
+}
+
+ModelChecker* mc_api::get_model_checker() const
+{
+ return mc_model_checker;
+}
+
+void mc_api::mc_inc_visited_states() const
+{
+ mc_model_checker->visited_states++;
+}
+
+void mc_api::mc_inc_executed_trans() const
+{
+ mc_model_checker->executed_transitions++;
+}
+
+unsigned long mc_api::mc_get_visited_states() const
+{
+ return mc_model_checker->visited_states;
+}
+
+unsigned long mc_api::mc_get_executed_trans() const
+{
+ return mc_model_checker->executed_transitions;
+}
+
+bool mc_api::mc_check_deadlock() const
+{
+ return mc_model_checker->checkDeadlock();
+}
+
+std::vector<simgrid::mc::ActorInformation>& mc_api::get_actors() const
+{
+ return mc_model_checker->get_remote_simulation().actors();
+}
+
+bool mc_api::actor_is_enabled(aid_t pid) const
+{
+ return session->actor_is_enabled(pid);
+}
+
+void mc_api::mc_assert(bool notNull, const char* message) const
+{
+ if (notNull)
+ xbt_assert(mc_model_checker == nullptr, message);
+ else
+ xbt_assert(mc_model_checker != nullptr, message);
+}
+
+bool mc_api::mc_is_null() const
+{
+ auto is_null = (mc_model_checker == nullptr) ? true : false;
+ return is_null;
+}
+
+Checker* mc_api::mc_get_checker() const
+{
+ return mc_model_checker->getChecker();
+}
+
+RemoteSimulation& mc_api::mc_get_remote_simulation() const
+{
+ return mc_model_checker->get_remote_simulation();
+}
+
+void mc_api::handle_simcall(Transition const& transition) const
+{
+ mc_model_checker->handle_simcall(transition);
+}
+
+void mc_api::mc_wait_for_requests() const
+{
+ mc_model_checker->wait_for_requests();
+}
+
+void mc_api::mc_exit(int status) const
+{
+ mc_model_checker->exit(status);
+}
+
+std::string const& mc_api::mc_get_host_name(std::string const& hostname) const
+{
+ return mc_model_checker->get_host_name(hostname);
+}
+
+PageStore& mc_api::mc_page_store() const
+{
+ return mc_model_checker->page_store();
+}
+
+void mc_api::mc_cleanup()
+{
+}
+
+void mc_api::s_close() const
+{
+ session->close();
+}
+
+void mc_api::s_restore_initial_state() const
+{
+ session->restore_initial_state();
+}
+
+void mc_api::execute(Transition const& transition)
+{
+ session->execute(transition);
+}
+
+void mc_api::s_log_state() const
+{
+ session->log_state();
+}
+
+} // namespace mc
+} // namespace simgrid
--- /dev/null
+#ifndef SIMGRID_MC_API_HPP
+#define SIMGRID_MC_API_HPP
+
+#include <memory>
+#include <vector>
+
+#include "simgrid/forward.h"
+#include "src/mc/mc_forward.hpp"
+#include "xbt/base.h"
+
+namespace simgrid {
+namespace mc {
+
+/*
+** This class aimes to implement FACADE APIs for simgrid. The FACADE layer sits between the CheckerSide
+** (Unfolding_Checker, DPOR, ...) layer and the
+** AppSide layer. The goal is to drill down into the entagled details in the CheckerSide layer and break down the
+** detailes in a way that the CheckerSide eventually
+** be capable to acquire the required information through the FACADE layer rather than the direct access to the AppSide.
+*/
+
+class mc_api {
+private:
+ mc_api() = default;
+
+public:
+ // No copy:
+ mc_api(mc_api const&) = delete;
+ void operator=(mc_api const&) = delete;
+
+ static mc_api& get()
+ {
+ static mc_api mcapi;
+ return mcapi;
+ }
+
+ void initialize(char** argv);
+
+ // MODEL_CHECKER FUNCTIONS
+ void create_model_checker(std::unique_ptr<RemoteSimulation> remote_simulation, int sockfd);
+ ModelChecker* get_model_checker() const;
+ void mc_inc_visited_states() const;
+ void mc_inc_executed_trans() const;
+ unsigned long mc_get_visited_states() const;
+ unsigned long mc_get_executed_trans() const;
+ bool mc_check_deadlock() const;
+ std::vector<simgrid::mc::ActorInformation>& get_actors() const;
+ bool actor_is_enabled(aid_t pid) const;
+ void mc_assert(bool notNull, const char* message = "") const;
+ bool mc_is_null() const;
+ Checker* mc_get_checker() const;
+ RemoteSimulation& mc_get_remote_simulation() const;
+ void handle_simcall(Transition const& transition) const;
+ void mc_wait_for_requests() const;
+ void mc_exit(int status) const;
+ std::string const& mc_get_host_name(std::string const& hostname) const;
+ PageStore& mc_page_store() const;
+ void mc_cleanup();
+
+ // SESSION FUNCTIONS
+ void s_initialize() const;
+ void s_close() const;
+ void s_restore_initial_state() const;
+ void execute(Transition const& transition);
+ void s_log_state() const;
+};
+
+} // namespace mc
+} // namespace simgrid
+
+#endif
\ No newline at end of file
// Called from both MCer and MCed:
bool actor_is_enabled(smx_actor_t actor)
{
+// #del
#if SIMGRID_HAVE_MC
// If in the MCer, ask the client app since it has all the data
if (mc_model_checker != nullptr) {
return simgrid::mc::session->actor_is_enabled(actor->get_pid());
}
#endif
+// #
// Now, we are in the client app, no need for remote memory reading.
smx_simcall_t req = &actor->simcall_;
src/mc/checker/SimcallInspector.hpp
src/mc/checker/LivenessChecker.cpp
src/mc/checker/LivenessChecker.hpp
-
+
src/mc/inspect/DwarfExpression.hpp
src/mc/inspect/DwarfExpression.cpp
src/mc/inspect/Frame.hpp
src/mc/mc_comm_pattern.cpp
src/mc/mc_comm_pattern.hpp
src/mc/compare.cpp
+ src/mc/mc_api.cpp
+ src/mc/mc_api.hpp
src/mc/mc_hash.hpp
src/mc/mc_hash.cpp
src/mc/mc_ignore.hpp
