code simplification in MC start sequence

diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp
index f50fac1..4250bff 100644 (file)
--- a/src/mc/ModelChecker.cpp
+++ b/src/mc/ModelChecker.cpp
@@ -53,8 +53,6 @@ ModelChecker::~ModelChecker() {
 
 void ModelChecker::start()
 {
 
 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)
   {
   base_ = event_base_new();
   event_callback_fn event_callback = [](evutil_socket_t fd, short events, void *arg)
   {


@@ -72,6 +70,8 @@ void ModelChecker::start()
   int status;
 
   // The model-checked process SIGSTOP itself to signal it's ready:
   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");
   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");

diff --git a/src/mc/Session.cpp b/src/mc/Session.cpp
index 87ed0f5..4d73338 100644 (file)
--- a/src/mc/Session.cpp
+++ b/src/mc/Session.cpp
@@ -77,16 +77,35 @@ pid_t do_fork(F code)
   }
 }
 
   }
 }
 

-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
 
 #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)));
   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();
   xbt_assert(mc_model_checker == nullptr);
   mc_model_checker = model_checker_.get();
   mc_model_checker->start();


@@ -129,47 +148,6 @@ void Session::log_state()
   }
 }
 
   }
 }
 

-// 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;
 void Session::close()
 {
   initial_snapshot_ = nullptr;

diff --git a/src/mc/Session.hpp b/src/mc/Session.hpp
index 283366c..3a79387 100644 (file)
--- a/src/mc/Session.hpp
+++ b/src/mc/Session.hpp
@@ -26,13 +26,20 @@ private:
   std::unique_ptr<ModelChecker> model_checker_;
   std::shared_ptr<simgrid::mc::Snapshot> initial_snapshot_;
 
   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:
   // 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();
 
   ~Session();
   void close();
 


@@ -41,31 +48,6 @@ public:
   void log_state();
 
   void restore_initial_state();
   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 :)
 };
 
 // Temporary :)

diff --git a/src/mc/checker/simgrid_mc.cpp b/src/mc/checker/simgrid_mc.cpp
index 0a713b8..0c59749 100644 (file)
--- a/src/mc/checker/simgrid_mc.cpp
+++ b/src/mc/checker/simgrid_mc.cpp
@@ -12,6 +12,7 @@
 
 #include <cstring>
 #include <memory>
 
 #include <cstring>
 #include <memory>

+#include <unistd.h>

 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_main, mc, "Entry point for simgrid-mc");
 
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_main, mc, "Entry point for simgrid-mc");
 


@@ -52,12 +53,12 @@ int main(int argc, char** argv)
     xbt_log_init(&argc, argv);
     sg_config_init(&argc, argv);
 
     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;
 
     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();
     int res = SIMGRID_MC_EXIT_SUCCESS;
     try {
       checker->run();


@@ -69,7 +70,7 @@ int main(int argc, char** argv)
       res = SIMGRID_MC_EXIT_LIVENESS;
     }
     checker = nullptr;
       res = SIMGRID_MC_EXIT_LIVENESS;
     }
     checker = nullptr;

-    session->close();
+    simgrid::mc::session->close();

     return res;
   }
   catch(std::exception& e) {
     return res;
   }
   catch(std::exception& e) {