continue to split the source code of MC. Split remoting

diff --git a/src/mc/AddressSpace.hpp b/src/mc/AddressSpace.hpp
index 1fd9e49..95a938d 100644 (file)
--- a/src/mc/AddressSpace.hpp
+++ b/src/mc/AddressSpace.hpp
@@ -17,7 +17,7 @@
 #include <vector>
 
 #include "src/mc/mc_forward.hpp"
-#include "src/mc/RemotePtr.hpp"
+#include "src/mc/remote/RemotePtr.hpp"
 
 namespace simgrid {
 namespace mc {

diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp
index dc4dba8..f160216 100644 (file)
--- a/src/mc/ModelChecker.cpp
+++ b/src/mc/ModelChecker.cpp
@@ -22,15 +22,15 @@
 #include "simgrid/sg_config.h"
 
 #include "src/mc/ModelChecker.hpp"
-#include "src/mc/PageStore.hpp"
 #include "src/mc/ModelChecker.hpp"
-#include "src/mc/mc_protocol.h"
-#include "src/mc/mc_private.h"
-#include "src/mc/mc_ignore.h"
-#include "src/mc/mc_exit.h"
-#include "src/mc/mc_record.h"
+#include "src/mc/PageStore.hpp"
 #include "src/mc/Transition.hpp"
 #include "src/mc/checker/Checker.hpp"
+#include "src/mc/mc_exit.h"
+#include "src/mc/mc_ignore.h"
+#include "src/mc/mc_private.h"
+#include "src/mc/mc_record.h"
+#include "src/mc/remote/mc_protocol.h"
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_ModelChecker, mc, "ModelChecker");
 

diff --git a/src/mc/ModelChecker.hpp b/src/mc/ModelChecker.hpp
index a1138ce..82724c4 100644 (file)
--- a/src/mc/ModelChecker.hpp
+++ b/src/mc/ModelChecker.hpp
@@ -19,11 +19,11 @@
 #include <xbt/base.h>
 #include <sys/types.h>
 
-#include "src/mc/mc_forward.hpp"
-#include "src/mc/Process.hpp"
 #include "src/mc/PageStore.hpp"
-#include "src/mc/mc_protocol.h"
+#include "src/mc/Process.hpp"
 #include "src/mc/Transition.hpp"
+#include "src/mc/mc_forward.hpp"
+#include "src/mc/remote/mc_protocol.h"
 
 namespace simgrid {
 namespace mc {

diff --git a/src/mc/Process.hpp b/src/mc/Process.hpp
index 2e93cf7..a109f83 100644 (file)
--- a/src/mc/Process.hpp
+++ b/src/mc/Process.hpp
@@ -23,7 +23,9 @@
 #include <xbt/mmalloc.h>
 
 #include "src/xbt/mmalloc/mmprivate.h"
-#include "src/mc/Channel.hpp"
+
+#include "src/mc/remote/Channel.hpp"
+#include "src/mc/remote/RemotePtr.hpp"
 
 #include <simgrid/simix.h>
 #include "src/simix/popping_private.h"
@@ -31,13 +33,11 @@
 
 #include "src/xbt/memory_map.hpp"
 
-#include "src/mc/mc_forward.hpp"
-#include "src/mc/mc_base.h"
-#include "src/mc/RemotePtr.hpp"
 #include "src/mc/AddressSpace.hpp"
-#include "src/mc/mc_protocol.h"
 #include "src/mc/ObjectInformation.hpp"
-
+#include "src/mc/mc_base.h"
+#include "src/mc/mc_forward.hpp"
+#include "src/mc/remote/mc_protocol.h"
 
 namespace simgrid {
 namespace mc {

diff --git a/src/mc/RegionSnapshot.hpp b/src/mc/RegionSnapshot.hpp
index a701e41..42de5f8 100644 (file)
--- a/src/mc/RegionSnapshot.hpp
+++ b/src/mc/RegionSnapshot.hpp
@@ -15,10 +15,10 @@
 
 #include <xbt/base.h>
 
-#include "src/mc/RemotePtr.hpp"
-#include "src/mc/PageStore.hpp"
 #include "src/mc/AddressSpace.hpp"
 #include "src/mc/ChunkedData.hpp"
+#include "src/mc/PageStore.hpp"
+#include "src/mc/remote/RemotePtr.hpp"
 
 namespace simgrid {
 namespace mc {

diff --git a/src/mc/checker/CommunicationDeterminismChecker.cpp b/src/mc/checker/CommunicationDeterminismChecker.cpp
index ec9ff9e..741e7ad 100644 (file)
--- a/src/mc/checker/CommunicationDeterminismChecker.cpp
+++ b/src/mc/checker/CommunicationDeterminismChecker.cpp
@@ -10,18 +10,18 @@
 #include <xbt/log.h>
 #include <xbt/sysdep.h>
 
-#include "src/mc/mc_state.h"
+#include "src/mc/Transition.hpp"
+#include "src/mc/VisitedState.hpp"
+#include "src/mc/checker/CommunicationDeterminismChecker.hpp"
 #include "src/mc/mc_comm_pattern.h"
-#include "src/mc/mc_request.h"
-#include "src/mc/mc_safety.h"
+#include "src/mc/mc_exit.h"
 #include "src/mc/mc_private.h"
 #include "src/mc/mc_record.h"
+#include "src/mc/mc_request.h"
+#include "src/mc/mc_safety.h"
 #include "src/mc/mc_smx.h"
-#include "src/mc/Client.hpp"
-#include "src/mc/checker/CommunicationDeterminismChecker.hpp"
-#include "src/mc/mc_exit.h"
-#include "src/mc/VisitedState.hpp"
-#include "src/mc/Transition.hpp"
+#include "src/mc/mc_state.h"
+#include "src/mc/remote/Client.hpp"
 
 using simgrid::mc::remote;
 

diff --git a/src/mc/checker/LivenessChecker.cpp b/src/mc/checker/LivenessChecker.cpp
index 5f967aa..a28aa51 100644 (file)
--- a/src/mc/checker/LivenessChecker.cpp
+++ b/src/mc/checker/LivenessChecker.cpp
@@ -20,18 +20,18 @@
 #include <xbt/log.h>
 #include <xbt/sysdep.h>
 
-#include "src/mc/mc_request.h"
+#include "src/mc/Session.hpp"
+#include "src/mc/Transition.hpp"
 #include "src/mc/checker/LivenessChecker.hpp"
+#include "src/mc/mc_exit.h"
 #include "src/mc/mc_private.h"
-#include "src/mc/mc_record.h"
-#include "src/mc/mc_smx.h"
-#include "src/mc/Client.hpp"
 #include "src/mc/mc_private.h"
+#include "src/mc/mc_record.h"
 #include "src/mc/mc_replay.h"
+#include "src/mc/mc_request.h"
 #include "src/mc/mc_safety.h"
-#include "src/mc/mc_exit.h"
-#include "src/mc/Transition.hpp"
-#include "src/mc/Session.hpp"
+#include "src/mc/mc_smx.h"
+#include "src/mc/remote/Client.hpp"
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc,
                                 "Logging specific to algorithms for liveness properties verification");

diff --git a/src/mc/checker/SafetyChecker.cpp b/src/mc/checker/SafetyChecker.cpp
index 2d766e2..088841a 100644 (file)
--- a/src/mc/checker/SafetyChecker.cpp
+++ b/src/mc/checker/SafetyChecker.cpp
@@ -14,18 +14,18 @@
 #include <xbt/log.h>
 #include <xbt/sysdep.h>
 
-#include "src/mc/mc_state.h"
-#include "src/mc/mc_request.h"
-#include "src/mc/mc_safety.h"
+#include "src/mc/Session.hpp"
+#include "src/mc/Transition.hpp"
+#include "src/mc/VisitedState.hpp"
+#include "src/mc/checker/SafetyChecker.hpp"
+#include "src/mc/mc_exit.h"
 #include "src/mc/mc_private.h"
 #include "src/mc/mc_record.h"
+#include "src/mc/mc_request.h"
+#include "src/mc/mc_safety.h"
 #include "src/mc/mc_smx.h"
-#include "src/mc/Client.hpp"
-#include "src/mc/mc_exit.h"
-#include "src/mc/checker/SafetyChecker.hpp"
-#include "src/mc/VisitedState.hpp"
-#include "src/mc/Transition.hpp"
-#include "src/mc/Session.hpp"
+#include "src/mc/mc_state.h"
+#include "src/mc/remote/Client.hpp"
 
 #include "src/xbt/mmalloc/mmprivate.h"
 

diff --git a/src/mc/checker/simgrid_mc.cpp b/src/mc/checker/simgrid_mc.cpp
index 413b22d..cf5164b 100644 (file)
--- a/src/mc/checker/simgrid_mc.cpp
+++ b/src/mc/checker/simgrid_mc.cpp
@@ -19,14 +19,14 @@
 #include "simgrid/sg_config.h"
 #include "src/xbt_modinter.h"
 
+#include "src/mc/Session.hpp"
+#include "src/mc/checker/Checker.hpp"
 #include "src/mc/mc_base.h"
-#include "src/mc/mc_private.h"
-#include "src/mc/mc_protocol.h"
-#include "src/mc/mc_safety.h"
 #include "src/mc/mc_comm_pattern.h"
 #include "src/mc/mc_exit.h"
-#include "src/mc/Session.hpp"
-#include "src/mc/checker/Checker.hpp"
+#include "src/mc/mc_private.h"
+#include "src/mc/mc_safety.h"
+#include "src/mc/remote/mc_protocol.h"
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_main, mc, "Entry point for simgrid-mc");
 

diff --git a/src/mc/mc_base.cpp b/src/mc/mc_base.cpp
index 541e314..ee4462f 100644 (file)
--- a/src/mc/mc_base.cpp
+++ b/src/mc/mc_base.cpp
@@ -14,11 +14,11 @@
 
 #include <simgrid/simix.h>
 
+#include "mc/mc.h"
 #include "src/mc/mc_base.h"
-#include "src/simix/smx_private.h"
 #include "src/mc/mc_replay.h"
-#include "mc/mc.h"
-#include "src/mc/mc_protocol.h"
+#include "src/mc/remote/mc_protocol.h"
+#include "src/simix/smx_private.h"
 
 #include "src/kernel/activity/ActivityImpl.hpp"
 #include "src/kernel/activity/SynchroIo.hpp"

diff --git a/src/mc/mc_checkpoint.cpp b/src/mc/mc_checkpoint.cpp
index 6c193dc..6deee1c 100644 (file)
--- a/src/mc/mc_checkpoint.cpp
+++ b/src/mc/mc_checkpoint.cpp
@@ -32,12 +32,12 @@
 #include "src/mc/mc_private.h"
 #include <mc/mc.h>
 
-#include "src/mc/mc_snapshot.h"
+#include "src/mc/mc_hash.hpp"
 #include "src/mc/mc_mmu.h"
-#include "src/mc/mc_unw.h"
-#include "src/mc/mc_protocol.h"
 #include "src/mc/mc_smx.h"
-#include "mc_hash.hpp"
+#include "src/mc/mc_snapshot.h"
+#include "src/mc/mc_unw.h"
+#include "src/mc/remote/mc_protocol.h"
 
 #include "src/mc/RegionSnapshot.hpp"
 #include "src/mc/ObjectInformation.hpp"

diff --git a/src/mc/mc_client_api.cpp b/src/mc/mc_client_api.cpp
index 9fbd031..7fd76d2 100644 (file)
--- a/src/mc/mc_client_api.cpp
+++ b/src/mc/mc_client_api.cpp
@@ -8,12 +8,12 @@
 #include <xbt/sysdep.h>
 #include <simgrid/modelchecker.h>
 
-#include "src/mc/mc_record.h"
-#include "src/mc/mc_private.h"
-#include "src/mc/mc_ignore.h"
-#include "src/mc/mc_protocol.h"
-#include "src/mc/Client.hpp"
 #include "src/mc/ModelChecker.hpp"
+#include "src/mc/mc_ignore.h"
+#include "src/mc/mc_private.h"
+#include "src/mc/mc_record.h"
+#include "src/mc/remote/Client.hpp"
+#include "src/mc/remote/mc_protocol.h"
 
 /** @file mc_client_api.cpp
  *

diff --git a/src/mc/mc_global.cpp b/src/mc/mc_global.cpp
index 1adc80b..8418b96 100644 (file)
--- a/src/mc/mc_global.cpp
+++ b/src/mc/mc_global.cpp
@@ -41,10 +41,10 @@
 #include "src/mc/checker/Checker.hpp"
 #endif
 
-#include "src/mc/mc_record.h"
-#include "src/mc/mc_protocol.h"
-#include "src/mc/Client.hpp"
 #include "src/mc/Transition.hpp"
+#include "src/mc/mc_record.h"
+#include "src/mc/remote/Client.hpp"
+#include "src/mc/remote/mc_protocol.h"
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_global, mc, "Logging specific to MC (global)");
 

diff --git a/src/mc/mc_protocol.cpp b/src/mc/mc_protocol.cpp
deleted file mode 100644 (file)
index b420e44..0000000
--- a/src/mc/mc_protocol.cpp
+++ /dev/null
@@ -1,52 +0,0 @@
-/* Copyright (c) 2015. The SimGrid Team.
- * All rights reserved.                                                     */
-
-/* This program is free software; you can redistribute it and/or modify it
- * under the terms of the license (GNU LGPL) which comes with this package. */
-
-#include <errno.h>
-#include <string.h>
-#include <stdio.h> // perror
-#include <cstddef> // std::size_t
-
-#include <sys/types.h>
-#include <sys/socket.h>
-
-#include <xbt/log.h>
-
-#include "src/mc/mc_protocol.h"
-#include "src/mc/Client.hpp"
-
-XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_protocol, mc, "Generic MC protocol logic");
-
-const char* MC_message_type_name(e_mc_message_type type)
-{
-  switch(type) {
-  case MC_MESSAGE_NONE:
-    return "NONE";
-  case MC_MESSAGE_CONTINUE:
-    return "CONTINUE";
-  case MC_MESSAGE_IGNORE_HEAP:
-    return "IGNORE_HEAP";
-  case MC_MESSAGE_UNIGNORE_HEAP:
-    return "UNIGNORE_HEAP";
-  case MC_MESSAGE_IGNORE_MEMORY:
-    return "IGNORE_MEMORY";
-  case MC_MESSAGE_STACK_REGION:
-    return "STACK_REGION";
-  case MC_MESSAGE_REGISTER_SYMBOL:
-    return "REGISTER_SYMBOL";
-  case MC_MESSAGE_DEADLOCK_CHECK:
-    return "DEADLOCK_CHECK";
-  case MC_MESSAGE_DEADLOCK_CHECK_REPLY:
-    return "DEADLOCK_CHECK_REPLY";
-  case MC_MESSAGE_WAITING:
-    return "WAITING";
-  case MC_MESSAGE_SIMCALL_HANDLE:
-    return "SIMCALL_HANDLE";
-  case MC_MESSAGE_ASSERTION_FAILED:
-    return "ASSERTION_FAILED";
-  default:
-    return "?";
-  }
-}

diff --git a/src/mc/mc_smx.h b/src/mc/mc_smx.h
index 194cf88..c078cca 100644 (file)
--- a/src/mc/mc_smx.h
+++ b/src/mc/mc_smx.h
@@ -17,7 +17,7 @@
 #include "src/smpi/private.h"
 
 #include "src/mc/Process.hpp"
-#include "src/mc/mc_protocol.h"
+#include "src/mc/remote/mc_protocol.h"
 
 /** @file
  *  @brief (Cross-process, MCer/MCed) Access to SMX structures

diff --git a/src/mc/mc_xbt.cpp b/src/mc/mc_xbt.cpp
index b7e6f5a..00cbe6c 100644 (file)
--- a/src/mc/mc_xbt.cpp
+++ b/src/mc/mc_xbt.cpp
@@ -6,9 +6,9 @@
 
 #include <cstddef>
 
-#include "src/mc/RemotePtr.hpp"
 #include "src/mc/AddressSpace.hpp"
 #include "src/mc/mc_xbt.hpp"
+#include "src/mc/remote/RemotePtr.hpp"
 
 #include <xbt/dynar.h>
 #include <xbt/sysdep.h>

diff --git a/src/mc/mc_xbt.hpp b/src/mc/mc_xbt.hpp
index 1d9a581..14940a9 100644 (file)
--- a/src/mc/mc_xbt.hpp
+++ b/src/mc/mc_xbt.hpp
@@ -11,8 +11,8 @@
 
 #include <xbt/dynar.h>
 
-#include "src/mc/RemotePtr.hpp"
 #include "src/mc/AddressSpace.hpp"
+#include "src/mc/remote/RemotePtr.hpp"
 
 namespace simgrid {
 namespace mc {

diff --git a/src/mc/Channel.cpp b/src/mc/remote/Channel.cpp
similarity index 80%
rename from src/mc/Channel.cpp
rename to src/mc/remote/Channel.cpp
index 6902497..30ccdcd 100644 (file)
--- a/src/mc/Channel.cpp
+++ b/src/mc/remote/Channel.cpp
@@ -7,12 +7,12 @@
 #include <errno.h>
 #include <unistd.h>
 
-#include <sys/types.h>
 #include <sys/socket.h>
+#include <sys/types.h>
 
 #include <xbt/log.h>
 
-#include "src/mc/Channel.hpp"
+#include "src/mc/remote/Channel.hpp"
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_Channel, mc, "MC interprocess communication");
 
@@ -21,14 +21,13 @@ namespace mc {
 
 Channel::~Channel()
 {
-  if (this->socket_ >=0)
+  if (this->socket_ >= 0)
     close(this->socket_);
 }
 
 int Channel::send(const void* message, size_t size) const
 {
-  XBT_DEBUG("Send %s",
-    MC_message_type_name(*(e_mc_message_type*) message));
+  XBT_DEBUG("Send %s", MC_message_type_name(*(e_mc_message_type*)message));
   while (::send(this->socket_, message, size, 0) == -1)
     if (errno == EINTR)
       continue;
@@ -41,10 +40,8 @@ ssize_t Channel::receive(void* message, size_t size, bool block) const
 {
   int res = recv(this->socket_, message, size, block ? 0 : MSG_DONTWAIT);
   if (res != -1)
-    XBT_DEBUG("Receive %s",
-      MC_message_type_name(*(e_mc_message_type*) message));
+    XBT_DEBUG("Receive %s", MC_message_type_name(*(e_mc_message_type*)message));
   return res;
 }
-
 }
 }

diff --git a/src/mc/Channel.hpp b/src/mc/remote/Channel.hpp
similarity index 74%
rename from src/mc/Channel.hpp
rename to src/mc/remote/Channel.hpp
index 30e03c6..ac4fd0c 100644 (file)
--- a/src/mc/Channel.hpp
+++ b/src/mc/remote/Channel.hpp
@@ -11,7 +11,7 @@
 
 #include <type_traits>
 
-#include "src/mc/mc_protocol.h"
+#include "src/mc/remote/mc_protocol.h"
 
 namespace simgrid {
 namespace mc {
@@ -23,13 +23,12 @@ namespace mc {
  */
 class Channel {
   int socket_ = -1;
-  template<class M>
-  static constexpr bool messageType()
+  template <class M> static constexpr bool messageType()
   {
     return std::is_class<M>::value && std::is_trivial<M>::value;
   }
-public:
 
+public:
   Channel() {}
   explicit Channel(int sock) : socket_(sock) {}
   ~Channel();
@@ -39,14 +38,11 @@ public:
   Channel& operator=(Channel const&) = delete;
 
   // Move:
-  Channel(Channel&& that) : socket_(that.socket_)
-  {
-    that.socket_ = -1;
-  }
+  Channel(Channel&& that) : socket_(that.socket_) { that.socket_ = -1; }
   Channel& operator=(Channel&& that)
   {
     this->socket_ = that.socket_;
-    that.socket_ = -1;
+    that.socket_  = -1;
     return *this;
   }
 
@@ -54,32 +50,23 @@ public:
   int send(const void* message, size_t size) const;
   int send(e_mc_message_type type) const
   {
-    s_mc_message message = { type };
+    s_mc_message message = {type};
     return this->send(&message, sizeof(message));
   }
-  template<class M>
-  typename std::enable_if< messageType<M>(), int >::type
-  send(M const& m) const
+  template <class M> typename std::enable_if<messageType<M>(), int>::type send(M const& m) const
   {
     return this->send(&m, sizeof(M));
   }
 
   // Receive
   ssize_t receive(void* message, size_t size, bool block = true) const;
-  template<class M>
-  typename std::enable_if< messageType<M>(), ssize_t >::type
-  receive(M& m) const
+  template <class M> typename std::enable_if<messageType<M>(), ssize_t>::type receive(M& m) const
   {
     return this->receive(&m, sizeof(M));
   }
 
-  int getSocket() const
-  {
-    return socket_;
-  }
-
+  int getSocket() const { return socket_; }
 };
-
 }
 }
 

diff --git a/src/mc/Client.cpp b/src/mc/remote/Client.cpp
similarity index 80%
rename from src/mc/Client.cpp
rename to src/mc/remote/Client.cpp
index d28a00b..2b25c63 100644 (file)
--- a/src/mc/Client.cpp
+++ b/src/mc/remote/Client.cpp
@@ -4,25 +4,25 @@
 /* This program is free software; you can redistribute it and/or modify it
  * under the terms of the license (GNU LGPL) which comes with this package. */
 
-#include <cstdlib>
 #include <cerrno>
+#include <cstdlib>
 
-#include <sys/types.h>
 #include <sys/ptrace.h>
 #include <sys/socket.h>
+#include <sys/types.h>
 
 #include <xbt/log.h>
-#include <xbt/sysdep.h>
 #include <xbt/mmalloc.h>
 #include <xbt/swag.h>
+#include <xbt/sysdep.h>
 
 #include <simgrid/modelchecker.h>
 
 #include "src/internal_config.h"
 
-#include "src/mc/mc_protocol.h"
-#include "src/mc/Client.hpp"
 #include "src/mc/mc_request.h"
+#include "src/mc/remote/Client.hpp"
+#include "src/mc/remote/mc_protocol.h"
 
 // We won't need those once the separation MCer/MCed is complete:
 #include "src/mc/mc_ignore.h"
@@ -52,7 +52,8 @@ Client* Client::initialize()
   char* fd_env = std::getenv(MC_ENV_SOCKET_FD);
   if (!fd_env)
     xbt_die("No MC socket passed in the environment");
-  int fd = xbt_str_parse_int(fd_env, bprintf("Variable %s should contain a number but contains '%%s'", MC_ENV_SOCKET_FD));
+  int fd =
+      xbt_str_parse_int(fd_env, bprintf("Variable %s should contain a number but contains '%%s'", MC_ENV_SOCKET_FD));
   XBT_DEBUG("Model-checked application found socket FD %i", fd);
 
   // Check the socket type/validity:
@@ -73,9 +74,9 @@ Client* Client::initialize()
 #elif defined BSD
   ptrace(PT_TRACE_ME, 0, nullptr, 0);
 #else
-# error "no ptrace equivalent coded for this platform"
+#error "no ptrace equivalent coded for this platform"
 #endif
-  if(errno != 0 || raise(SIGSTOP) != 0)
+  if (errno != 0 || raise(SIGSTOP) != 0)
     xbt_die("Could not wait for the model-checker");
 
   client_->handleMessages();
@@ -94,13 +95,12 @@ void Client::handleMessages()
       xbt_die("Could not receive commands from the model-checker");
 
     s_mc_message_t message;
-    if ((size_t) s < sizeof(message))
+    if ((size_t)s < sizeof(message))
       xbt_die("Received message is too small");
     memcpy(&message, message_buffer, sizeof(message));
     switch (message.type) {
 
-    case MC_MESSAGE_DEADLOCK_CHECK:
-      {
+      case MC_MESSAGE_DEADLOCK_CHECK: {
         // Check deadlock:
         bool deadlock = false;
         smx_actor_t actor;
@@ -110,38 +110,34 @@ void Client::handleMessages()
           {
             deadlock = false;
             break;
-            }
+          }
         }
 
         // Send result:
         s_mc_int_message_t answer;
-        answer.type = MC_MESSAGE_DEADLOCK_CHECK_REPLY;
+        answer.type  = MC_MESSAGE_DEADLOCK_CHECK_REPLY;
         answer.value = deadlock;
         if (channel_.send(answer))
           xbt_die("Could not send response");
-      }
-      break;
+      } break;
 
-    case MC_MESSAGE_CONTINUE:
-      return;
+      case MC_MESSAGE_CONTINUE:
+        return;
 
-    case MC_MESSAGE_SIMCALL_HANDLE:
-      {
+      case MC_MESSAGE_SIMCALL_HANDLE: {
         s_mc_simcall_handle_message_t message;
         if (s != sizeof(message))
           xbt_die("Unexpected size for SIMCALL_HANDLE");
         memcpy(&message, message_buffer, sizeof(message));
         smx_actor_t process = SIMIX_process_from_PID(message.pid);
         if (!process)
-          xbt_die("Invalid pid %lu", (unsigned long) message.pid);
+          xbt_die("Invalid pid %lu", (unsigned long)message.pid);
         SIMIX_simcall_handle(&process->simcall, message.value);
         if (channel_.send(MC_MESSAGE_WAITING))
           xbt_die("Could not send MESSAGE_WAITING to model-checker");
-      }
-      break;
+      } break;
 
-    case MC_MESSAGE_RESTORE:
-      {
+      case MC_MESSAGE_RESTORE: {
         s_mc_restore_message_t message;
         if (s != sizeof(message))
           xbt_die("Unexpected size for SIMCALL_HANDLE");
@@ -149,14 +145,10 @@ void Client::handleMessages()
 #if HAVE_SMPI
         smpi_really_switch_data_segment(message.index);
 #endif
-      }
-      break;
-
-    default:
-      xbt_die("Received unexpected message %s (%i)",
-        MC_message_type_name(message.type),
-        message.type
-      );
+      } break;
+
+      default:
+        xbt_die("Received unexpected message %s (%i)", MC_message_type_name(message.type), message.type);
     }
   }
 }
@@ -182,7 +174,7 @@ void Client::ignoreMemory(void* addr, std::size_t size)
 {
   s_mc_ignore_memory_message_t message;
   message.type = MC_MESSAGE_IGNORE_MEMORY;
-  message.addr = (std::uintptr_t) addr;
+  message.addr = (std::uintptr_t)addr;
   message.size = size;
   if (channel_.send(message))
     xbt_die("Could not send IGNORE_MEMORY mesage to model-checker");
@@ -193,19 +185,15 @@ void Client::ignoreHeap(void* address, std::size_t size)
   xbt_mheap_t heap = mmalloc_get_current_heap();
 
   s_mc_ignore_heap_message_t message;
-  message.type = MC_MESSAGE_IGNORE_HEAP;
+  message.type    = MC_MESSAGE_IGNORE_HEAP;
   message.address = address;
-  message.size = size;
-  message.block =
-   ((char *) address -
-    (char *) heap->heapbase) / BLOCKSIZE + 1;
+  message.size    = size;
+  message.block   = ((char*)address - (char*)heap->heapbase) / BLOCKSIZE + 1;
   if (heap->heapinfo[message.block].type == 0) {
     message.fragment = -1;
     heap->heapinfo[message.block].busy_block.ignore++;
   } else {
-    message.fragment =
-        ((uintptr_t) (ADDR2UINT(address) % (BLOCKSIZE))) >>
-        heap->heapinfo[message.block].type;
+    message.fragment = ((uintptr_t)(ADDR2UINT(address) % (BLOCKSIZE))) >> heap->heapinfo[message.block].type;
     heap->heapinfo[message.block].busy_frag.ignore[message.fragment]++;
   }
 
@@ -217,13 +205,13 @@ void Client::unignoreHeap(void* address, std::size_t size)
 {
   s_mc_ignore_memory_message_t message;
   message.type = MC_MESSAGE_UNIGNORE_HEAP;
-  message.addr = (std::uintptr_t) address;
+  message.addr = (std::uintptr_t)address;
   message.size = size;
   if (channel_.send(message))
     xbt_die("Could not send IGNORE_HEAP mesasge to model-checker");
 }
 
-void Client::declareSymbol(const char *name, int* value)
+void Client::declareSymbol(const char* name, int* value)
 {
   s_mc_register_symbol_message_t message;
   message.type = MC_MESSAGE_REGISTER_SYMBOL;
@@ -231,12 +219,12 @@ void Client::declareSymbol(const char *name, int* value)
     xbt_die("Symbol is too long");
   strncpy(message.name, name, sizeof(message.name));
   message.callback = nullptr;
-  message.data = value;
+  message.data     = value;
   if (channel_.send(message))
     xbt_die("Could send REGISTER_SYMBOL message to model-checker");
 }
 
-void Client::declareStack(void *stack, size_t size, smx_actor_t process, ucontext_t* context)
+void Client::declareStack(void* stack, size_t size, smx_actor_t process, ucontext_t* context)
 {
   xbt_mheap_t heap = mmalloc_get_current_heap();
 
@@ -244,23 +232,20 @@ void Client::declareStack(void *stack, size_t size, smx_actor_t process, ucontex
   memset(&region, 0, sizeof(region));
   region.address = stack;
   region.context = context;
-  region.size = size;
-  region.block =
-      ((char *) stack -
-       (char *) heap->heapbase) / BLOCKSIZE + 1;
+  region.size    = size;
+  region.block   = ((char*)stack - (char*)heap->heapbase) / BLOCKSIZE + 1;
 #if HAVE_SMPI
   if (smpi_privatize_global_variables && process)
     region.process_index = smpi_process_index_of_smx_process(process);
   else
 #endif
-  region.process_index = -1;
+    region.process_index = -1;
 
   s_mc_stack_region_message_t message;
-  message.type = MC_MESSAGE_STACK_REGION;
+  message.type         = MC_MESSAGE_STACK_REGION;
   message.stack_region = region;
   if (channel_.send(message))
     xbt_die("Coule not send STACK_REGION to model-checker");
 }
-
 }
 }

diff --git a/src/mc/Client.hpp b/src/mc/remote/Client.hpp
similarity index 85%
rename from src/mc/Client.hpp
rename to src/mc/remote/Client.hpp
index 6de722c..ead07fe 100644 (file)
--- a/src/mc/Client.hpp
+++ b/src/mc/remote/Client.hpp
@@ -16,8 +16,8 @@
 
 #include <simgrid/simix.h>
 
-#include "src/mc/mc_protocol.h"
-#include "src/mc/Channel.hpp"
+#include "src/mc/remote/Channel.hpp"
+#include "src/mc/remote/mc_protocol.h"
 
 namespace simgrid {
 namespace mc {
@@ -31,6 +31,7 @@ private:
   bool active_ = false;
   Channel channel_;
   static std::unique_ptr<Client> client_;
+
 public:
   Client();
   explicit Client(int fd) : active_(true), channel_(fd) {}
@@ -42,20 +43,16 @@ public:
   void ignoreMemory(void* addr, std::size_t size);
   void ignoreHeap(void* addr, std::size_t size);
   void unignoreHeap(void* addr, std::size_t size);
-  void declareSymbol(const char *name, int* value);
+  void declareSymbol(const char* name, int* value);
 #if HAVE_UCONTEXT_H
-  void declareStack(void *stack, size_t size, smx_actor_t process, ucontext_t* context);
+  void declareStack(void* stack, size_t size, smx_actor_t process, ucontext_t* context);
 #endif
 
   // Singleton :/
   // TODO, remove the singleton antipattern.
   static Client* initialize();
-  static Client* get()
-  {
-    return client_.get();
-  }
+  static Client* get() { return client_.get(); }
 };
-
 }
 }
 

diff --git a/src/mc/RemotePtr.hpp b/src/mc/remote/RemotePtr.hpp
similarity index 66%
rename from src/mc/RemotePtr.hpp
rename to src/mc/remote/RemotePtr.hpp
index e69af01..3622eac 100644 (file)
--- a/src/mc/RemotePtr.hpp
+++ b/src/mc/remote/RemotePtr.hpp
@@ -33,38 +33,29 @@ namespace mc {
  *  in the current process and in the target process: we don't handle
  *  cross-architecture (such as 32-bit/64-bit access).
  */
-template<class T>
-union Remote {
+template <class T> union Remote {
 private:
   T buffer;
+
 public:
   Remote() {}
   ~Remote() {}
-  Remote(T& p)
-  {
-    std::memcpy(&buffer, &p, sizeof(buffer));
-  }
-  Remote(Remote const& that)
-  {
-    std::memcpy(&buffer, &that.buffer, sizeof(buffer));
-  }
+  Remote(T& p) { std::memcpy(&buffer, &p, sizeof(buffer)); }
+  Remote(Remote const& that) { std::memcpy(&buffer, &that.buffer, sizeof(buffer)); }
   Remote& operator=(Remote const& that)
   {
     std::memcpy(&buffer, &that.buffer, sizeof(buffer));
     return *this;
   }
-  T*       getBuffer() { return &buffer; }
+  T* getBuffer() { return &buffer; }
   const T* getBuffer() const { return &buffer; }
   std::size_t getBufferSize() const { return sizeof(T); }
-  operator T() const {
+  operator T() const
+  {
     static_assert(std::is_trivial<T>::value, "Cannot convert non trivial type");
     return buffer;
   }
-  void clear()
-  {
-    std::memset(static_cast<void*>(&buffer), 0, sizeof(T));
-  }
-
+  void clear() { std::memset(static_cast<void*>(&buffer), 0, sizeof(T)); }
 };
 
 /** Pointer to a remote address-space (process, snapshot)
@@ -81,8 +72,9 @@ public:
  *  always detect it in context. This way `RemotePtr` is as efficient
  *  as a `uint64_t`.
  */
-template<class T> class RemotePtr {
+template <class T> class RemotePtr {
   std::uint64_t address_;
+
 public:
   RemotePtr() : address_(0) {}
   RemotePtr(std::uint64_t address) : address_(address) {}
@@ -93,28 +85,13 @@ public:
   /** Turn into a local pointer
    *
    (if the remote process is not, in fact, remote) */
-  T* local() const { return (T*) address_; }
+  T* local() const { return (T*)address_; }
 
-  operator bool() const
-  {
-    return address_;
-  }
-  bool operator!() const
-  {
-    return !address_;
-  }
-  operator RemotePtr<void>() const
-  {
-    return RemotePtr<void>(address_);
-  }
-  RemotePtr<T> operator+(std::uint64_t n) const
-  {
-    return RemotePtr<T>(address_ + n * sizeof(T));
-  }
-  RemotePtr<T> operator-(std::uint64_t n) const
-  {
-    return RemotePtr<T>(address_ - n * sizeof(T));
-  }
+  operator bool() const { return address_; }
+  bool operator!() const { return !address_; }
+  operator RemotePtr<void>() const { return RemotePtr<void>(address_); }
+  RemotePtr<T> operator+(std::uint64_t n) const { return RemotePtr<T>(address_ + n * sizeof(T)); }
+  RemotePtr<T> operator-(std::uint64_t n) const { return RemotePtr<T>(address_ - n * sizeof(T)); }
   RemotePtr<T>& operator+=(std::uint64_t n)
   {
     address_ += n * sizeof(T);
@@ -127,54 +104,45 @@ public:
   }
 };
 
-template<class X, class Y>
-bool operator<(RemotePtr<X> const& x, RemotePtr<Y> const& y)
+template <class X, class Y> bool operator<(RemotePtr<X> const& x, RemotePtr<Y> const& y)
 {
   return x.address() < y.address();
 }
 
-template<class X, class Y>
-bool operator>(RemotePtr<X> const& x, RemotePtr<Y> const& y)
+template <class X, class Y> bool operator>(RemotePtr<X> const& x, RemotePtr<Y> const& y)
 {
   return x.address() > y.address();
 }
 
-template<class X, class Y>
-bool operator>=(RemotePtr<X> const& x, RemotePtr<Y> const& y)
+template <class X, class Y> bool operator>=(RemotePtr<X> const& x, RemotePtr<Y> const& y)
 {
   return x.address() >= y.address();
 }
 
-template<class X, class Y>
-bool operator<=(RemotePtr<X> const& x, RemotePtr<Y> const& y)
+template <class X, class Y> bool operator<=(RemotePtr<X> const& x, RemotePtr<Y> const& y)
 {
   return x.address() <= y.address();
 }
 
-template<class X, class Y>
-bool operator==(RemotePtr<X> const& x, RemotePtr<Y> const& y)
+template <class X, class Y> bool operator==(RemotePtr<X> const& x, RemotePtr<Y> const& y)
 {
   return x.address() == y.address();
 }
 
-template<class X, class Y>
-bool operator!=(RemotePtr<X> const& x, RemotePtr<Y> const& y)
+template <class X, class Y> bool operator!=(RemotePtr<X> const& x, RemotePtr<Y> const& y)
 {
   return x.address() != y.address();
 }
 
-template<class T> inline
-RemotePtr<T> remote(T *p)
+template <class T> inline RemotePtr<T> remote(T* p)
 {
   return RemotePtr<T>(p);
 }
 
-template<class T=void> inline
-RemotePtr<T> remote(uint64_t p)
+template <class T = void> inline RemotePtr<T> remote(uint64_t p)
 {
   return RemotePtr<T>(p);
 }
-
 }
 }
 

diff --git a/src/mc/remote/mc_protocol.cpp b/src/mc/remote/mc_protocol.cpp
new file mode 100644 (file)
index 0000000..5baf1d5
--- /dev/null
+++ b/src/mc/remote/mc_protocol.cpp
@@ -0,0 +1,52 @@
+/* Copyright (c) 2015. The SimGrid Team.
+ * All rights reserved.                                                     */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#include <cstddef> // std::size_t
+#include <errno.h>
+#include <stdio.h> // perror
+#include <string.h>
+
+#include <sys/socket.h>
+#include <sys/types.h>
+
+#include <xbt/log.h>
+
+#include "src/mc/remote/Client.hpp"
+#include "src/mc/remote/mc_protocol.h"
+
+XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_protocol, mc, "Generic MC protocol logic");
+
+const char* MC_message_type_name(e_mc_message_type type)
+{
+  switch (type) {
+    case MC_MESSAGE_NONE:
+      return "NONE";
+    case MC_MESSAGE_CONTINUE:
+      return "CONTINUE";
+    case MC_MESSAGE_IGNORE_HEAP:
+      return "IGNORE_HEAP";
+    case MC_MESSAGE_UNIGNORE_HEAP:
+      return "UNIGNORE_HEAP";
+    case MC_MESSAGE_IGNORE_MEMORY:
+      return "IGNORE_MEMORY";
+    case MC_MESSAGE_STACK_REGION:
+      return "STACK_REGION";
+    case MC_MESSAGE_REGISTER_SYMBOL:
+      return "REGISTER_SYMBOL";
+    case MC_MESSAGE_DEADLOCK_CHECK:
+      return "DEADLOCK_CHECK";
+    case MC_MESSAGE_DEADLOCK_CHECK_REPLY:
+      return "DEADLOCK_CHECK_REPLY";
+    case MC_MESSAGE_WAITING:
+      return "WAITING";
+    case MC_MESSAGE_SIMCALL_HANDLE:
+      return "SIMCALL_HANDLE";
+    case MC_MESSAGE_ASSERTION_FAILED:
+      return "ASSERTION_FAILED";
+    default:
+      return "?";
+  }
+}

diff --git a/src/mc/mc_protocol.h b/src/mc/remote/mc_protocol.h
similarity index 86%
rename from src/mc/mc_protocol.h
rename to src/mc/remote/mc_protocol.h
index 3e1da82..189abf3 100644 (file)
--- a/src/mc/mc_protocol.h
+++ b/src/mc/remote/mc_protocol.h
@@ -61,7 +61,7 @@ typedef enum {
 struct s_mc_message {
   e_mc_message_type type;
 };
-typedef struct s_mc_message  s_mc_message_t;
+typedef struct s_mc_message s_mc_message_t;
 typedef struct s_mc_message* mc_message_t;
 
 struct s_mc_int_message {
@@ -75,10 +75,10 @@ struct s_mc_ignore_heap_message {
   e_mc_message_type type;
   int block;
   int fragment;
-  void *address;
+  void* address;
   size_t size;
 };
-typedef struct s_mc_ignore_heap_message  s_mc_ignore_heap_message_t;
+typedef struct s_mc_ignore_heap_message s_mc_ignore_heap_message_t;
 typedef struct s_mc_ignore_heap_message* mc_ignore_heap_message_t;
 
 struct s_mc_ignore_memory_message {
@@ -86,14 +86,14 @@ struct s_mc_ignore_memory_message {
   uint64_t addr;
   size_t size;
 };
-typedef struct s_mc_ignore_memory_message  s_mc_ignore_memory_message_t;
+typedef struct s_mc_ignore_memory_message s_mc_ignore_memory_message_t;
 typedef struct s_mc_ignore_memory_message* mc_ignore_memory_message_t;
 
 struct s_mc_stack_region_message {
   e_mc_message_type type;
   s_stack_region_t stack_region;
 };
-typedef struct s_mc_stack_region_message  s_mc_stack_region_message_t;
+typedef struct s_mc_stack_region_message s_mc_stack_region_message_t;
 typedef struct s_mc_stack_region_message* mc_stack_region_message_t;
 
 struct s_mc_simcall_handle_message {
@@ -101,7 +101,7 @@ struct s_mc_simcall_handle_message {
   unsigned long pid;
   int value;
 };
-typedef struct s_mc_simcall_handle_message  s_mc_simcall_handle_message_t;
+typedef struct s_mc_simcall_handle_message s_mc_simcall_handle_message_t;
 typedef struct s_mc_simcall_handle_message* mc_simcall_handle_message;
 
 struct s_mc_register_symbol_message {
@@ -110,14 +110,14 @@ struct s_mc_register_symbol_message {
   int (*callback)(void*);
   void* data;
 };
-typedef struct s_mc_register_symbol_message  s_mc_register_symbol_message_t;
+typedef struct s_mc_register_symbol_message s_mc_register_symbol_message_t;
 typedef struct s_mc_register_symbol_message* mc_register_symbol_message_t;
 
 struct s_mc_restore_message {
   e_mc_message_type type;
   int index;
 };
-typedef struct s_mc_restore_message  s_mc_restore_message_t;
+typedef struct s_mc_restore_message s_mc_restore_message_t;
 typedef struct s_mc_restore_message* mc_restore_message_t;
 
 XBT_PRIVATE const char* MC_message_type_name(e_mc_message_type type);

diff --git a/src/simix/ActorImpl.cpp b/src/simix/ActorImpl.cpp
index b66efd1..a0e300d 100644 (file)
--- a/src/simix/ActorImpl.cpp
+++ b/src/simix/ActorImpl.cpp
@@ -25,8 +25,8 @@
 #include "src/kernel/activity/SynchroIo.hpp"
 #include "src/kernel/activity/SynchroRaw.hpp"
 #include "src/kernel/activity/SynchroSleep.hpp"
-#include "src/mc/Client.hpp"
 #include "src/mc/mc_replay.h"
+#include "src/mc/remote/Client.hpp"
 #include "src/msg/msg_private.h"
 #include "src/surf/cpu_interface.hpp"
 #include "src/surf/surf_interface.hpp"

diff --git a/src/simix/smx_global.cpp b/src/simix/smx_global.cpp
index 598882c..8503d4c 100644 (file)
--- a/src/simix/smx_global.cpp
+++ b/src/simix/smx_global.cpp
@@ -33,11 +33,9 @@
 
 #if HAVE_MC
 #include "src/mc/mc_private.h"
-#include "src/mc/mc_protocol.h"
-#include "src/mc/Client.hpp"
-
+#include "src/mc/remote/Client.hpp"
+#include "src/mc/remote/mc_protocol.h"
 #include <stdlib.h>
-#include "src/mc/mc_protocol.h"
 #endif 
 
 #include "src/mc/mc_record.h"

diff --git a/src/xbt/mmalloc/mm_legacy.c b/src/xbt/mmalloc/mm_legacy.c
index 4fb087a..dafcbbd 100644 (file)
--- a/src/xbt/mmalloc/mm_legacy.c
+++ b/src/xbt/mmalloc/mm_legacy.c
@@ -11,12 +11,12 @@
 
 #include <dlfcn.h>
 
-#include "src/mc/mc_base.h"
 #include "mmprivate.h"
-#include "src/xbt_modinter.h"
 #include "src/internal_config.h"
+#include "src/mc/mc_base.h"
+#include "src/mc/remote/mc_protocol.h"
+#include "src/xbt_modinter.h"
 #include <math.h>
-#include "src/mc/mc_protocol.h"
 
 /* ***** Whether to use `mmalloc` of the underlying malloc ***** */
 

diff --git a/tools/cmake/DefinePackages.cmake b/tools/cmake/DefinePackages.cmake
index 769d19c..114ea20 100644 (file)
--- a/tools/cmake/DefinePackages.cmake
+++ b/tools/cmake/DefinePackages.cmake
@@ -556,13 +556,16 @@ set(MC_SRC
   src/mc/checker/SafetyChecker.hpp
   src/mc/checker/LivenessChecker.cpp
   src/mc/checker/LivenessChecker.hpp
-  src/mc/RemotePtr.hpp
+  src/mc/remote/Channel.cpp
+  src/mc/remote/Channel.hpp
+  src/mc/remote/Client.cpp
+  src/mc/remote/Client.hpp
+  src/mc/remote/RemotePtr.hpp
+  src/mc/remote/mc_protocol.h
+  src/mc/remote/mc_protocol.cpp
+  
   src/mc/AddressSpace.hpp
   src/mc/AddressSpace.cpp
-  src/mc/Channel.cpp
-  src/mc/Channel.hpp
-  src/mc/Client.cpp
-  src/mc/Client.hpp
   src/mc/Frame.hpp
   src/mc/Frame.cpp
   src/mc/ModelChecker.hpp
@@ -617,8 +620,6 @@ set(MC_SRC
   src/mc/VisitedState.cpp
   src/mc/VisitedState.hpp
   src/mc/mc_client_api.cpp
-  src/mc/mc_protocol.h
-  src/mc/mc_protocol.cpp
   src/mc/mc_smx.h
   src/mc/mc_smx.cpp
   src/mc/mc_xbt.hpp