void ModelChecker::start()
{
- const pid_t pid = process_->pid();
-
base_ = event_base_new();
event_callback_fn event_callback = [](evutil_socket_t fd, short events, void *arg)
{
int status;
// The model-checked process SIGSTOP itself to signal it's ready:
+ const pid_t pid = process_->pid();
+
pid_t res = waitpid(pid, &status, WAITPID_CHECKED_FLAGS);
if (res < 0 || not WIFSTOPPED(status) || WSTOPSIG(status) != SIGSTOP)
xbt_die("Could not wait model-checked process");
}
}
-Session::Session(pid_t pid, int socket)
+Session::Session(const std::function<void()>& code)
{
- std::unique_ptr<simgrid::mc::RemoteClient> process(new simgrid::mc::RemoteClient(pid, socket));
-
#if HAVE_SMPI
xbt_assert(smpi_privatize_global_variables != SmpiPrivStrategies::MMAP,
"Please use the dlopen privatization schema when model-checking SMPI code");
#endif
+ // Create a AF_LOCAL socketpair used for exchanging messages
+ // between the model-checker process (ourselves) and the model-checked
+ // process:
+ int res;
+ int sockets[2];
+ res = socketpair(AF_LOCAL, SOCK_SEQPACKET | SOCK_CLOEXEC, 0, sockets);
+ if (res == -1)
+ throw simgrid::xbt::errno_error("Could not create socketpair");
+
+ pid_t pid = do_fork([sockets, &code] {
+ ::close(sockets[1]);
+ setup_child_environment(sockets[0]);
+ code();
+ xbt_die("The model-checked process failed to exec()");
+ });
+
+ // Parent (model-checker):
+ ::close(sockets[0]);
+
+ std::unique_ptr<simgrid::mc::RemoteClient> process(new simgrid::mc::RemoteClient(pid, sockets[1]));
model_checker_.reset(new simgrid::mc::ModelChecker(std::move(process)));
+
xbt_assert(mc_model_checker == nullptr);
mc_model_checker = model_checker_.get();
mc_model_checker->start();
}
}
-// static
-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
- // process:
- int res;
- int sockets[2];
- res = socketpair(AF_LOCAL, SOCK_SEQPACKET | SOCK_CLOEXEC, 0, sockets);
- if (res == -1)
- throw simgrid::xbt::errno_error("Could not create socketpair");
-
- pid_t pid = do_fork([sockets, &code] {
- ::close(sockets[1]);
- setup_child_environment(sockets[0]);
- code();
- xbt_die("The model-checked process failed to exec()");
- });
-
- // Parent (model-checker):
- ::close(sockets[0]);
-
- return new Session(pid, sockets[1]);
-}
-
-// static
-Session* Session::spawnv(const char *path, char *const argv[])
-{
- return Session::fork([path, argv] {
- execv(path, argv);
- });
-}
-
-// static
-Session* Session::spawnvp(const char *file, char *const argv[])
-{
- return Session::fork([file, argv] {
- execvp(file, argv);
- });
-}
-
void Session::close()
{
initial_snapshot_ = nullptr;
std::unique_ptr<ModelChecker> model_checker_;
std::shared_ptr<simgrid::mc::Snapshot> initial_snapshot_;
- Session(pid_t pid, int socket);
-
// No copy:
Session(Session const&) = delete;
Session& operator=(Session const&) = delete;
public:
+ /** Create a new session by executing the provided code in a fork()
+ *
+ * This sets up the environment for the model-checked process
+ * (environment variables, sockets, etc.).
+ *
+ * The code is expected to `exec` the model-checked application.
+ */
+ Session(const std::function<void()>& code);
+
~Session();
void close();
void log_state();
void restore_initial_state();
-
- // static constructors
-
- /** Create a new session by forking
- *
- * This sets up the environment for the model-checked process
- * (environment variables, sockets, etc.).
- *
- * The code is expected to `exec` the model-checker program.
- */
- static Session* fork(const std::function<void()>& code);
-
- /** Spawn a model-checked process
- *
- * @param path full path of the executable
- * @param argv arguments for the model-checked process (NULL-terminated)
- */
- static Session* spawnv(const char *path, char *const argv[]);
-
- /** Spawn a model-checked process (using PATH)
- *
- * @param file file name of the executable (found using `PATH`)
- * @param argv arguments for the model-checked process (NULL-terminated)
- */
- static Session* spawnvp(const char *file, char *const argv[]);
};
// Temporary :)
#include <cstring>
#include <memory>
+#include <unistd.h>
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_main, mc, "Entry point for simgrid-mc");
xbt_log_init(&argc, argv);
sg_config_init(&argc, argv);
- std::unique_ptr<Session> session =
- std::unique_ptr<Session>(Session::spawnvp(argv_copy[1], argv_copy+1));
+ simgrid::mc::session = new Session([argv_copy] {
+ execvp(argv_copy[1], argv_copy+1);
+ });
delete[] argv_copy;
- simgrid::mc::session = session.get();
- std::unique_ptr<simgrid::mc::Checker> checker = createChecker(*session);
+ std::unique_ptr<simgrid::mc::Checker> checker = createChecker(*simgrid::mc::session);
int res = SIMGRID_MC_EXIT_SUCCESS;
try {
checker->run();
res = SIMGRID_MC_EXIT_LIVENESS;
}
checker = nullptr;
- session->close();
+ simgrid::mc::session->close();
return res;
}
catch(std::exception& e) {