Merge branch 'odpor-implementation' into 'master'

[simgrid.git] / src / mc / remote / CheckerSide.cpp

diff --git a/src/mc/remote/CheckerSide.cpp b/src/mc/remote/CheckerSide.cpp
index b88d7e2ba0ad418f267a17ce057f8777845ac014..211995b856f07d1ff1b986543493ea72d9001c9d 100644 (file)
--- a/src/mc/remote/CheckerSide.cpp
+++ b/src/mc/remote/CheckerSide.cpp
@@ -5,6 +5,7 @@
 
 #include "src/mc/remote/CheckerSide.hpp"
 #include "src/mc/explo/Exploration.hpp"
+#include "src/mc/mc_environ.h"
 #include "xbt/config.hpp"
 #include "xbt/system_error.hpp"
 
@@ -56,7 +57,7 @@ XBT_ATTRIB_NORETURN static void run_child_process(int socket, const std::vector<
 
   setenv(MC_ENV_SOCKET_FD, std::to_string(socket).c_str(), 1);
   if (need_ptrace)
-    setenv("MC_NEED_PTRACE", "1", 1);
+    setenv(MC_ENV_NEED_PTRACE, "1", 1);
 
   /* Setup the tokenizer that parses the cfg:model-check/setenv parameter */
   using Tokenizer = boost::tokenizer<boost::char_separator<char>>;
@@ -130,7 +131,6 @@ void CheckerSide::setup_events(bool socket_only)
         auto checker = static_cast<simgrid::mc::CheckerSide*>(arg);
         if (events == EV_READ) {
           do {
-
             std::array<char, MC_MESSAGE_LENGTH> buffer;
             ssize_t size = checker->get_channel().receive(buffer.data(), buffer.size(), MSG_DONTWAIT);
             if (size == -1) {
@@ -182,7 +182,14 @@ CheckerSide::CheckerSide(const std::vector<char*>& args, bool need_memory_info)
   // Create an AF_UNIX socketpair used for exchanging messages between the model-checker process (ancestor)
   // and the application process (child)
   int sockets[2];
-  xbt_assert(socketpair(AF_UNIX, SOCK_STREAM, 0, sockets) != -1, "Could not create socketpair: %s", strerror(errno));
+  xbt_assert(socketpair(AF_UNIX,
+#ifdef __APPLE__
+                        SOCK_STREAM, /* Mac OSX does not have AF_UNIX + SOCK_SEQPACKET, even if that's faster */
+#else
+                        SOCK_SEQPACKET,
+#endif
+                        0, sockets) != -1,
+             "Could not create socketpair: %s", strerror(errno));
 
   pid_ = fork();
   xbt_assert(pid_ >= 0, "Could not fork application process");
@@ -251,11 +258,12 @@ CheckerSide::CheckerSide(int socket, CheckerSide* child_checker)
   wait_for_requests();
 }
 
-std::unique_ptr<CheckerSide> CheckerSide::clone(int master_socket)
+std::unique_ptr<CheckerSide> CheckerSide::clone(int master_socket, const std::string& master_socket_name)
 {
-  s_mc_message_int_t m = {};
-  m.type               = MessageType::FORK;
-  m.value              = getpid();
+  s_mc_message_fork_t m = {};
+  m.type                = MessageType::FORK;
+  xbt_assert(master_socket_name.size() == MC_SOCKET_NAME_LEN);
+  std::copy_n(begin(master_socket_name), MC_SOCKET_NAME_LEN, begin(m.socket_name));
   xbt_assert(get_channel().send(m) == 0, "Could not ask the app to fork on need.");
 
   int sock = accept(master_socket, nullptr /* I know who's connecting*/, nullptr);
@@ -280,7 +288,7 @@ void CheckerSide::finalize(bool terminate_asap)
              (int)answer.type, (int)MessageType::FINALIZE_REPLY);
 }
 
-void CheckerSide::dispatch_events()
+void CheckerSide::dispatch_events() const
 {
   event_base_dispatch(base_.get());
 }
@@ -387,6 +395,8 @@ bool CheckerSide::handle_message(const char* buffer, ssize_t size)
       return false;
 
     case MessageType::ASSERTION_FAILED:
+      // report_assertion_failure() is NORETURN, but it may change when we report more than one error per run,
+      // so please keep the consumed computation even if clang-static detects it as a dead affectation.
       consumed = sizeof(s_mc_message_t);
       Exploration::get_instance()->report_assertion_failure();
       break;
@@ -479,7 +489,6 @@ void CheckerSide::handle_waitpid()
     }
 
   } else { // Ask our proxy to wait for us
-
     s_mc_message_int_t request = {};
     request.type               = MessageType::WAIT_CHILD;
     request.value              = pid_;