mc/remote: switch to socket type SOCK_SEQPACKET to detect when the peer disconnected.

diff --git a/doc/doxygen/uhood.doc b/doc/doxygen/uhood.doc
index 7a750df..67632a5 100644 (file)
--- a/doc/doxygen/uhood.doc
+++ b/doc/doxygen/uhood.doc
@@ -208,7 +208,7 @@ The current implementation of the model-checker uses two distinct processes:
  - it spaws a child process for the SimGrid simulator/maestro and the simulated
    processes.
 
-They communicate using a `AF_UNIX` `SOCK_DGRAM` socket and exchange messages
+They communicate using a `AF_UNIX` `SOCK_SEQPACKET` socket and exchange messages
 defined in `mc_protocol.h`. The `SIMGRID_MC_SOCKET_FD` environment variable it
 set to the file descriptor of this socket in the child process.
 

diff --git a/src/mc/Session.cpp b/src/mc/Session.cpp
index 810351b..92b8d63 100644 (file)
--- a/src/mc/Session.cpp
+++ b/src/mc/Session.cpp
@@ -140,7 +140,7 @@ Session* Session::fork(std::function<void()> code)
   // process:
   int res;
   int sockets[2];
-  res = socketpair(AF_LOCAL, SOCK_DGRAM | SOCK_CLOEXEC, 0, sockets);
+  res = socketpair(AF_LOCAL, SOCK_SEQPACKET, 0, sockets);
   if (res == -1)
     throw simgrid::xbt::errno_error("Could not create socketpair");
 

diff --git a/src/mc/remote/Channel.hpp b/src/mc/remote/Channel.hpp
index c3fb006..c9de6d6 100644 (file)
--- a/src/mc/remote/Channel.hpp
+++ b/src/mc/remote/Channel.hpp
@@ -19,7 +19,7 @@ namespace mc {
 /** A channel for exchanging messages between model-checker and model-checked
  *
  *  This abstracts away the way the messages are transferred. Currently, they
- *  are sent over a (connected) `SOCK_DGRAM` socket.
+ *  are sent over a (connected) `SOCK_SEQPACKET` socket.
  */
 class Channel {
   int socket_ = -1;

diff --git a/src/mc/remote/Client.cpp b/src/mc/remote/Client.cpp
index 20b9c2d..93f0bc0 100644 (file)
--- a/src/mc/remote/Client.cpp
+++ b/src/mc/remote/Client.cpp
@@ -61,7 +61,7 @@ Client* Client::initialize()
   socklen_t socklen = sizeof(type);
   if (getsockopt(fd, SOL_SOCKET, SO_TYPE, &type, &socklen) != 0)
     xbt_die("Could not check socket type");
-  if (type != SOCK_DGRAM)
+  if (type != SOCK_SEQPACKET)
     xbt_die("Unexpected socket type %i", type);
   XBT_DEBUG("Model-checked application found expected socket type");
 

diff --git a/src/mc/remote/mc_protocol.h b/src/mc/remote/mc_protocol.h
index bac7981..8a2a089 100644 (file)
--- a/src/mc/remote/mc_protocol.h
+++ b/src/mc/remote/mc_protocol.h
@@ -51,7 +51,7 @@ typedef enum {
 /** Basic structure for a MC message
  *
  *  The current version of the client/server protocol sends C structures over `AF_LOCAL`
- *  `SOCK_DGRAM` sockets. This means that the protocol is ABI/architecture specific:
+ *  `SOCK_SEQPACKET` sockets. This means that the protocol is ABI/architecture specific:
  *  we currently can't model-check a x86 process from a x86_64 process.
  *
  *  Moreover the protocol is not stable. The same version of the library should be used