Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
[mc] Encapsulate model-checker/model-checker communications classes
authorGabriel Corona <gabriel.corona@loria.fr>
Thu, 10 Mar 2016 14:36:54 +0000 (15:36 +0100)
committerGabriel Corona <gabriel.corona@loria.fr>
Fri, 11 Mar 2016 13:59:31 +0000 (14:59 +0100)
- Channel, for low-lewel message send/receive (currently a wrapper around a socket);

- Client, for the client-side logic.

16 files changed:
src/mc/Channel.cpp [new file with mode: 0644]
src/mc/Channel.hpp [new file with mode: 0644]
src/mc/ModelChecker.cpp
src/mc/Process.cpp
src/mc/Process.hpp
src/mc/mc_checkpoint.cpp
src/mc/mc_client.cpp
src/mc/mc_client.h
src/mc/mc_client_api.cpp
src/mc/mc_comm_determinism.cpp
src/mc/mc_global.cpp
src/mc/mc_ignore.cpp
src/mc/mc_protocol.cpp
src/mc/mc_protocol.h
src/simix/smx_global.cpp
tools/cmake/DefinePackages.cmake

diff --git a/src/mc/Channel.cpp b/src/mc/Channel.cpp
new file mode 100644 (file)
index 0000000..b368eaf
--- /dev/null
@@ -0,0 +1,53 @@
+/* Copyright (c) 2015-2016. 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 <unistd.h>
+
+#include <sys/types.h>
+#include <sys/socket.h>
+
+#include <xbt/log.h>
+
+#include "src/mc/Channel.hpp"
+
+XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_Channel, mc, "MC interprocess communication");
+
+namespace simgrid {
+namespace mc {
+
+Channel::~Channel()
+{
+  if (this->socket_ >=0)
+    close(this->socket_);
+}
+
+int Channel::send(const void* message, size_t size) const
+{
+  XBT_DEBUG("Protocol [%s] send %s",
+    MC_mode_name(mc_mode),
+    MC_message_type_name(*(e_mc_message_type*) message));
+
+  while (::send(this->socket_, message, size, 0) == -1)
+    if (errno == EINTR)
+      continue;
+    else
+      return errno;
+  return 0;
+}
+
+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("Protocol [%s] received %s",
+      MC_mode_name(mc_mode),
+      MC_message_type_name(*(e_mc_message_type*) message));
+  return res;
+}
+
+}
+}
diff --git a/src/mc/Channel.hpp b/src/mc/Channel.hpp
new file mode 100644 (file)
index 0000000..61514ad
--- /dev/null
@@ -0,0 +1,81 @@
+/* Copyright (c) 2015-2016. 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. */
+
+#ifndef SIMGRID_MC_CHANNEL_HPP
+#define SIMGRID_MC_CHANNEL_HPP
+
+#include <unistd.h>
+
+#include <type_traits>
+
+#include "src/mc/mc_protocol.h"
+
+namespace simgrid {
+namespace mc {
+
+class Channel {
+  int socket_ = -1;
+  template<class M>
+  static constexpr bool messageType()
+  {
+    return std::is_class<M>::value && std::is_trivial<M>::value;
+  }
+public:
+
+  Channel() {}
+  Channel(int sock) : socket_(sock) {}
+  ~Channel();
+
+  // No copy:
+  Channel(Channel const&) = delete;
+  Channel& operator=(Channel const&) = delete;
+
+  // Move:
+  Channel(Channel&& that) : socket_(that.socket_)
+  {
+    that.socket_ = -1;
+  }
+  Channel& operator=(Channel&& that)
+  {
+    this->socket_ = that.socket_;
+    that.socket_ = -1;
+    return *this;
+  }
+
+  // Send
+  int send(const void* message, size_t size) const;
+  int send(e_mc_message_type type) const
+  {
+    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
+  {
+    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
+  {
+    return this->receive(&m, sizeof(M));
+  }
+
+  int getSocket() const
+  {
+    return socket_;
+  }
+
+};
+
+}
+}
+
+#endif
index a385dfc..bc69fbe 100644 (file)
@@ -88,7 +88,7 @@ void ModelChecker::start()
   // Prepare data for poll:
 
   struct pollfd* socket_pollfd = &fds_[SOCKET_FD_INDEX];
   // Prepare data for poll:
 
   struct pollfd* socket_pollfd = &fds_[SOCKET_FD_INDEX];
-  socket_pollfd->fd = process_->socket();;
+  socket_pollfd->fd = process_->getChannel().getSocket();
   socket_pollfd->events = POLLIN;
   socket_pollfd->revents = 0;
 
   socket_pollfd->events = POLLIN;
   socket_pollfd->revents = 0;
 
@@ -173,7 +173,7 @@ void ModelChecker::shutdown()
 
 void ModelChecker::resume(simgrid::mc::Process& process)
 {
 
 void ModelChecker::resume(simgrid::mc::Process& process)
 {
-  int res = process.send_message(MC_MESSAGE_CONTINUE);
+  int res = process.getChannel().send(MC_MESSAGE_CONTINUE);
   if (res)
     throw simgrid::xbt::errno_error(res);
   process.cache_flags = (mc_process_cache_flags_t) 0;
   if (res)
     throw simgrid::xbt::errno_error(res);
   process.cache_flags = (mc_process_cache_flags_t) 0;
@@ -310,7 +310,7 @@ bool ModelChecker::handle_events()
 
   if (socket_pollfd->revents) {
     if (socket_pollfd->revents & POLLIN) {
 
   if (socket_pollfd->revents) {
     if (socket_pollfd->revents & POLLIN) {
-      ssize_t size = MC_receive_message(socket_pollfd->fd, buffer, sizeof(buffer), MSG_DONTWAIT);
+      ssize_t size = process_->getChannel().receive(buffer, sizeof(buffer), false);
       if (size == -1 && errno != EAGAIN)
         throw simgrid::xbt::errno_error(errno);
       return handle_message(buffer, size);
       if (size == -1 && errno != EAGAIN)
         throw simgrid::xbt::errno_error(errno);
       return handle_message(buffer, size);
@@ -433,7 +433,7 @@ void ModelChecker::simcall_handle(simgrid::mc::Process& process, unsigned long p
   m.type  = MC_MESSAGE_SIMCALL_HANDLE;
   m.pid   = pid;
   m.value = value;
   m.type  = MC_MESSAGE_SIMCALL_HANDLE;
   m.pid   = pid;
   m.value = value;
-  process.send_message(m);
+  process.getChannel().send(m);
   process.cache_flags = (mc_process_cache_flags_t) 0;
   while (process.running())
     if (!this->handle_events())
   process.cache_flags = (mc_process_cache_flags_t) 0;
   while (process.running())
     if (!this->handle_events())
index f9099a2..3f06a40 100644 (file)
@@ -201,7 +201,7 @@ int open_vm(pid_t pid, int flags)
 // ***** Process
 
 Process::Process(pid_t pid, int sockfd) :
 // ***** Process
 
 Process::Process(pid_t pid, int sockfd) :
-   AddressSpace(this),pid_(pid), socket_(sockfd), running_(true)
+   AddressSpace(this), pid_(pid), channel_(sockfd), running_(true)
 {}
 
 void Process::init()
 {}
 
 void Process::init()
@@ -233,12 +233,6 @@ void Process::init()
 
 Process::~Process()
 {
 
 Process::~Process()
 {
-  if (this->socket_ >= 0 && close(this->socket_) < 0)
-    xbt_die("Could not close communication socket");
-
-  this->maestro_stack_start_ = nullptr;
-  this->maestro_stack_end_ = nullptr;
-
   if (this->memory_file >= 0)
     close(this->memory_file);
 
   if (this->memory_file >= 0)
     close(this->memory_file);
 
@@ -246,13 +240,8 @@ Process::~Process()
     unw_destroy_addr_space(this->unw_underlying_addr_space);
     _UPT_destroy(this->unw_underlying_context);
   }
     unw_destroy_addr_space(this->unw_underlying_addr_space);
     _UPT_destroy(this->unw_underlying_context);
   }
-  this->unw_underlying_context = nullptr;
-  this->unw_underlying_addr_space = nullptr;
 
   unw_destroy_addr_space(this->unw_addr_space);
 
   unw_destroy_addr_space(this->unw_addr_space);
-  this->unw_addr_space = nullptr;
-
-  this->cache_flags = MC_PROCESS_CACHE_FLAG_NONE;
 
   if (this->clear_refs_fd_ >= 0)
     close(this->clear_refs_fd_);
 
   if (this->clear_refs_fd_ >= 0)
     close(this->clear_refs_fd_);
index a2cef85..36ef994 100644 (file)
@@ -22,9 +22,8 @@
 #include <xbt/dynar.h>
 #include <xbt/mmalloc.h>
 
 #include <xbt/dynar.h>
 #include <xbt/mmalloc.h>
 
-#if HAVE_MC
 #include "src/xbt/mmalloc/mmprivate.h"
 #include "src/xbt/mmalloc/mmprivate.h"
-#endif
+#include "src/mc/Channel.hpp"
 
 #include <simgrid/simix.h>
 #include "src/simix/popping_private.h"
 
 #include <simgrid/simix.h>
 #include "src/simix/popping_private.h"
@@ -147,6 +146,9 @@ public:
     return this->heap_info.data();
   }
 
     return this->heap_info.data();
   }
 
+  Channel const& getChannel() const { return channel_; }
+  Channel& getChannel() { return channel_; }
+
   std::vector<IgnoredRegion> const& ignored_regions() const
   {
     return ignored_regions_;
   std::vector<IgnoredRegion> const& ignored_regions() const
   {
     return ignored_regions_;
@@ -170,25 +172,6 @@ public:
     running_ = false;
   }
 
     running_ = false;
   }
 
-  template<class M>
-  typename std::enable_if< std::is_class<M>::value && std::is_trivial<M>::value, int >::type
-  send_message(M const& m)
-  {
-    return MC_protocol_send(this->socket_, &m, sizeof(M));
-  }
-
-  int send_message(e_mc_message_type message_id)
-  {
-    return MC_protocol_send_simple_message(this->socket_, message_id);
-  }
-
-  template<class M>
-  typename std::enable_if< std::is_class<M>::value && std::is_trivial<M>::value, ssize_t >::type
-  receive_message(M& m)
-  {
-    return MC_receive_message(this->socket_, &m, sizeof(M), 0);
-  }
-
   void reset_soft_dirty();
   void read_pagemap(uint64_t* pagemap, size_t start_page, size_t page_count);
 
   void reset_soft_dirty();
   void read_pagemap(uint64_t* pagemap, size_t start_page, size_t page_count);
 
@@ -226,7 +209,6 @@ public:
   void unignore_heap(void *address, size_t size);
 
   void ignore_local_variable(const char *var_name, const char *frame_name);
   void unignore_heap(void *address, size_t size);
 
   void ignore_local_variable(const char *var_name, const char *frame_name);
-  int socket() { return socket_; }
   std::vector<simgrid::mc::SimixProcessInformation>& simix_processes();
   std::vector<simgrid::mc::SimixProcessInformation>& old_simix_processes();
 
   std::vector<simgrid::mc::SimixProcessInformation>& simix_processes();
   std::vector<simgrid::mc::SimixProcessInformation>& old_simix_processes();
 
@@ -238,7 +220,7 @@ private:
 
 private:
   pid_t pid_ = -1;
 
 private:
   pid_t pid_ = -1;
-  int socket_ = -1;
+  Channel channel_;
   bool running_ = false;
   std::vector<simgrid::xbt::VmMap> memory_map_;
   RemotePtr<void> maestro_stack_start_, maestro_stack_end_;
   bool running_ = false;
   std::vector<simgrid::xbt::VmMap> memory_map_;
   RemotePtr<void> maestro_stack_start_, maestro_stack_end_;
index 171db18..1c0c1ce 100644 (file)
@@ -603,7 +603,7 @@ void restore_snapshot_regions(mc_snapshot_t snapshot)
     s_mc_restore_message message;
     message.type = MC_MESSAGE_RESTORE;
     message.index = snapshot->privatization_index;
     s_mc_restore_message message;
     message.type = MC_MESSAGE_RESTORE;
     message.index = snapshot->privatization_index;
-    mc_model_checker->process().send_message(message);
+    mc_model_checker->process().getChannel().send(message);
   }
 #endif
 }
   }
 #endif
 }
index a173b8f..7598472 100644 (file)
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_client, mc, "MC client logic");
 
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_client, mc, "MC client logic");
 
-extern "C" {
+namespace simgrid {
+namespace mc {
 
 
-mc_client_t mc_client;
+std::unique_ptr<Client> Client::client_;
 
 
-void MC_client_init(void)
+Client* Client::initialize()
 {
 {
-  if (mc_mode != MC_MODE_NONE)
-    return;
+  // We are not in MC mode:
+  // TODO, handle this more gracefully.
   if (!getenv(MC_ENV_SOCKET_FD))
   if (!getenv(MC_ENV_SOCKET_FD))
-    return;
-  mc_mode = MC_MODE_CLIENT;
+    return nullptr;
 
 
-  if (mc_client) {
-    XBT_WARN("MC_client_init called more than once.");
-    return;
-  }
+  // Do not break if we are called multiple times:
+  if (client_)
+    return client_.get();
 
 
+  // Check and set the mode:
+  if (mc_mode != MC_MODE_NONE)
+    abort();
+  mc_mode = MC_MODE_CLIENT;
+
+  // Fetch socket from MC_ENV_SOCKET_FD:
   char* fd_env = std::getenv(MC_ENV_SOCKET_FD);
   if (!fd_env)
   char* fd_env = std::getenv(MC_ENV_SOCKET_FD);
   if (!fd_env)
-    xbt_die("MC socket not found");
-
-  int fd = xbt_str_parse_int(fd_env,bprintf("Variable %s should contain a number but contains '%%s'", MC_ENV_SOCKET_FD));
+    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));
   XBT_DEBUG("Model-checked application found socket FD %i", fd);
 
   XBT_DEBUG("Model-checked application found socket FD %i", fd);
 
+  // Check the socket type/validity:
   int type;
   socklen_t socklen = sizeof(type);
   if (getsockopt(fd, SOL_SOCKET, SO_TYPE, &type, &socklen) != 0)
   int type;
   socklen_t socklen = sizeof(type);
   if (getsockopt(fd, SOL_SOCKET, SO_TYPE, &type, &socklen) != 0)
@@ -57,36 +62,25 @@ void MC_client_init(void)
     xbt_die("Unexpected socket type %i", type);
   XBT_DEBUG("Model-checked application found expected socket type");
 
     xbt_die("Unexpected socket type %i", type);
   XBT_DEBUG("Model-checked application found expected socket type");
 
-  mc_client = xbt_new0(s_mc_client_t, 1);
-  mc_client->fd = fd;
-  mc_client->active = 1;
+  client_ = std::unique_ptr<Client>(new simgrid::mc::Client(fd));
 
 
-  // Waiting for the model-checker:
+  // Wait for the model-checker:
   if (ptrace(PTRACE_TRACEME, 0, nullptr, NULL) == -1 || raise(SIGSTOP) != 0)
     xbt_die("Could not wait for the model-checker");
   if (ptrace(PTRACE_TRACEME, 0, nullptr, NULL) == -1 || raise(SIGSTOP) != 0)
     xbt_die("Could not wait for the model-checker");
-  MC_client_handle_messages();
-}
 
 
-void MC_client_send_message(void* message, size_t size)
-{
-  if (MC_protocol_send(mc_client->fd, message, size))
-    xbt_die("Could not send message %i", (int) ((mc_message_t)message)->type);
+  client_->handleMessages();
+  return client_.get();
 }
 
 }
 
-void MC_client_send_simple_message(e_mc_message_type type)
-{
-  if (MC_protocol_send_simple_message(mc_client->fd, type))
-    xbt_die("Could not send message %i", type);
-}
-
-void MC_client_handle_messages(void)
+void Client::handleMessages()
 {
   while (1) {
     XBT_DEBUG("Waiting messages from model-checker");
 
     char message_buffer[MC_MESSAGE_LENGTH];
     ssize_t s;
 {
   while (1) {
     XBT_DEBUG("Waiting messages from model-checker");
 
     char message_buffer[MC_MESSAGE_LENGTH];
     ssize_t s;
-    if ((s = MC_receive_message(mc_client->fd, &message_buffer, sizeof(message_buffer), 0)) < 0)
+
+    if ((s = channel_.receive(&message_buffer, sizeof(message_buffer))) < 0)
       xbt_die("Could not receive commands from the model-checker");
 
     s_mc_message_t message;
       xbt_die("Could not receive commands from the model-checker");
 
     s_mc_message_t message;
@@ -101,7 +95,7 @@ void MC_client_handle_messages(void)
         s_mc_int_message_t answer;
         answer.type = MC_MESSAGE_DEADLOCK_CHECK_REPLY;
         answer.value = result;
         s_mc_int_message_t answer;
         answer.type = MC_MESSAGE_DEADLOCK_CHECK_REPLY;
         answer.value = result;
-        if (MC_protocol_send(mc_client->fd, &answer, sizeof(answer)))
+        if (channel_.send(answer))
           xbt_die("Could not send response");
       }
       break;
           xbt_die("Could not send response");
       }
       break;
@@ -119,7 +113,8 @@ void MC_client_handle_messages(void)
         if (!process)
           xbt_die("Invalid pid %lu", (unsigned long) message.pid);
         SIMIX_simcall_handle(&process->simcall, message.value);
         if (!process)
           xbt_die("Invalid pid %lu", (unsigned long) message.pid);
         SIMIX_simcall_handle(&process->simcall, message.value);
-        MC_protocol_send_simple_message(mc_client->fd, MC_MESSAGE_WAITING);
+        if (channel_.send(MC_MESSAGE_WAITING))
+          xbt_die("Could not send MESSAGE_WAITING to model-checker");
       }
       break;
 
       }
       break;
 
@@ -143,13 +138,15 @@ void MC_client_handle_messages(void)
   }
 }
 
   }
 }
 
-void MC_client_main_loop(void)
+void Client::mainLoop(void)
 {
   while (1) {
 {
   while (1) {
-    MC_protocol_send_simple_message(mc_client->fd, MC_MESSAGE_WAITING);
-    MC_client_handle_messages();
+    if (channel_.send(MC_MESSAGE_WAITING))
+      xbt_die("Could not send WAITING mesage to model-checker");
+    this->handleMessages();
     simgrid::mc::wait_for_requests();
   }
 }
 
 }
     simgrid::mc::wait_for_requests();
   }
 }
 
 }
+}
index 0f1fc22..8ed4907 100644 (file)
@@ -9,29 +9,47 @@
 
 #include <cstddef>
 
 
 #include <cstddef>
 
+#include <memory>
+
 #include <xbt/base.h>
 #include <xbt/base.h>
+
 #include "src/mc/mc_protocol.h"
 #include "src/mc/mc_protocol.h"
+#include "src/mc/Channel.hpp"
+
+namespace simgrid {
+namespace mc {
+
+class XBT_PUBLIC() Client {
+private:
+  bool active_ = false;
+  Channel channel_;
+  static std::unique_ptr<Client> client_;
+public:
+  Client();
+  Client(int fd) : active_(true), channel_(fd) {}
+  void handleMessages();
+  Channel const& getChannel() const { return channel_; }
+  Channel& getChannel() { return channel_; }
+  void mainLoop(void);
+
+  // Singleton :/
+  // TODO, remove the singleton antipattern.
+  static Client* initialize();
+  static Client* get()
+  {
+    return client_.get();
+  }
+};
+
+}
+}
 
 SG_BEGIN_DECL()
 
 
 SG_BEGIN_DECL()
 
-typedef struct s_mc_client {
-  int active;
-  int fd;
-} s_mc_client_t, *mc_client_t;
-
-extern XBT_PRIVATE mc_client_t mc_client;
-
-XBT_PRIVATE void MC_client_init(void);
-XBT_PRIVATE void MC_client_handle_messages(void);
-XBT_PRIVATE void MC_client_send_message(void* message, std::size_t size);
-XBT_PRIVATE void MC_client_send_simple_message(e_mc_message_type type);
-
 #if HAVE_MC
 void MC_ignore(void* addr, std::size_t size);
 #endif
 
 #if HAVE_MC
 void MC_ignore(void* addr, std::size_t size);
 #endif
 
-void MC_client_main_loop(void);
-
 SG_END_DECL()
 
 #endif
 SG_END_DECL()
 
 #endif
index da2fece..f3b6538 100644 (file)
@@ -30,8 +30,9 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_client_api, mc,
 void MC_assert(int prop)
 {
   if (MC_is_active() && !prop) {
 void MC_assert(int prop)
 {
   if (MC_is_active() && !prop) {
-    MC_client_send_simple_message(MC_MESSAGE_ASSERTION_FAILED);
-    MC_client_handle_messages();
+    if (simgrid::mc::Client::get()->getChannel().send(MC_MESSAGE_ASSERTION_FAILED))
+      xbt_die("Could not send assertion to model-checker");
+    simgrid::mc::Client::get()->handleMessages();
   }
 }
 
   }
 }
 
@@ -50,7 +51,8 @@ void MC_ignore(void* addr, size_t size)
   message.type = MC_MESSAGE_IGNORE_MEMORY;
   message.addr = (std::uintptr_t) addr;
   message.size = size;
   message.type = MC_MESSAGE_IGNORE_MEMORY;
   message.addr = (std::uintptr_t) addr;
   message.size = size;
-  MC_client_send_message(&message, sizeof(message));
+  if (simgrid::mc::Client::get()->getChannel().send(message))
+    xbt_die("Could not send IGNORE_MEMORY mesage to model-checker");
 }
 
 void MC_automaton_new_propositional_symbol(const char *id, int(*fct)(void))
 }
 
 void MC_automaton_new_propositional_symbol(const char *id, int(*fct)(void))
@@ -77,5 +79,6 @@ void MC_automaton_new_propositional_symbol_pointer(const char *name, int* value)
   strncpy(message.name, name, sizeof(message.name));
   message.callback = nullptr;
   message.data = value;
   strncpy(message.name, name, sizeof(message.name));
   message.callback = nullptr;
   message.data = value;
-  MC_client_send_message(&message, sizeof(message));
+  if (simgrid::mc::Client::get()->getChannel().send(message))
+    xbt_die("Could send REGISTER_SYMBOL message to model-checker");
 }
 }
index 0836626..7745aa5 100644 (file)
@@ -468,7 +468,7 @@ int MC_modelcheck_comm_determinism(void)
 
   if (mc_mode == MC_MODE_CLIENT)
     // This will move somehwere else:
 
   if (mc_mode == MC_MODE_CLIENT)
     // This will move somehwere else:
-    MC_client_handle_messages();
+    simgrid::mc::Client::get()->handleMessages();
 
   /* Create exploration stack */
   mc_stack = xbt_fifo_new();
 
   /* Create exploration stack */
   mc_stack = xbt_fifo_new();
index 128e877..7c33396 100644 (file)
@@ -140,7 +140,7 @@ void MC_run()
 {
   mc_mode = MC_MODE_CLIENT;
   MC_init();
 {
   mc_mode = MC_MODE_CLIENT;
   MC_init();
-  MC_client_main_loop();
+  simgrid::mc::Client::get()->mainLoop();
 }
 
 void MC_exit(void)
 }
 
 void MC_exit(void)
@@ -155,10 +155,10 @@ int MC_deadlock_check()
 {
   if (mc_mode == MC_MODE_SERVER) {
     int res;
 {
   if (mc_mode == MC_MODE_SERVER) {
     int res;
-    if ((res = mc_model_checker->process().send_message(MC_MESSAGE_DEADLOCK_CHECK)))
+    if ((res = mc_model_checker->process().getChannel().send(MC_MESSAGE_DEADLOCK_CHECK)))
       xbt_die("Could not check deadlock state");
     s_mc_int_message_t message;
       xbt_die("Could not check deadlock state");
     s_mc_int_message_t message;
-    ssize_t s = mc_model_checker->process().receive_message(message);
+    ssize_t s = mc_model_checker->process().getChannel().receive(message);
     if (s == -1)
       xbt_die("Could not receive message");
     if (s != sizeof(message) || message.type != MC_MESSAGE_DEADLOCK_CHECK_REPLY)
     if (s == -1)
       xbt_die("Could not receive message");
     if (s != sizeof(message) || message.type != MC_MESSAGE_DEADLOCK_CHECK_REPLY)
index 51d781c..4ff5d5f 100644 (file)
@@ -43,7 +43,7 @@ void MC_ignore_heap(void *address, size_t size)
     heap->heapinfo[message.block].busy_frag.ignore[message.fragment]++;
   }
 
     heap->heapinfo[message.block].busy_frag.ignore[message.fragment]++;
   }
 
-  if (MC_protocol_send(mc_client->fd, &message, sizeof(message)))
+  if (simgrid::mc::Client::get()->getChannel().send(message))
     xbt_die("Could not send ignored region to MCer");
 }
 
     xbt_die("Could not send ignored region to MCer");
 }
 
@@ -56,7 +56,8 @@ void MC_remove_ignore_heap(void *address, size_t size)
   message.type = MC_MESSAGE_UNIGNORE_HEAP;
   message.addr = (std::uintptr_t) address;
   message.size = size;
   message.type = MC_MESSAGE_UNIGNORE_HEAP;
   message.addr = (std::uintptr_t) address;
   message.size = size;
-  MC_client_send_message(&message, sizeof(message));
+  if (simgrid::mc::Client::get()->getChannel().send(message))
+    xbt_die("Could not send UNIGNORE_HEAP mesasge to model-checker");
 }
 
 void MC_ignore_global_variable(const char *name)
 }
 
 void MC_ignore_global_variable(const char *name)
@@ -101,7 +102,8 @@ void MC_register_stack_area(void *stack, smx_process_t process, ucontext_t* cont
   s_mc_stack_region_message_t message;
   message.type = MC_MESSAGE_STACK_REGION;
   message.stack_region = region;
   s_mc_stack_region_message_t message;
   message.type = MC_MESSAGE_STACK_REGION;
   message.stack_region = region;
-  MC_client_send_message(&message, sizeof(message));
+  if (simgrid::mc::Client::get()->getChannel().send(message))
+    xbt_die("Coule not send STACK_REGION to model-checker");
 }
 
 }
 }
 
 }
index 55ab295..3815d39 100644 (file)
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_protocol, mc, "Generic MC protocol logic");
 
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_protocol, mc, "Generic MC protocol logic");
 
-extern "C" {
-
-int MC_protocol_send(int socket, const void* message, std::size_t size)
-{
-  XBT_DEBUG("Protocol [%s] send %s",
-    MC_mode_name(mc_mode),
-    MC_message_type_name(*(e_mc_message_type*) message));
-
-  while (send(socket, message, size, 0) == -1)
-    if (errno == EINTR)
-      continue;
-    else
-      return errno;
-  return 0;
-}
-
-int MC_protocol_send_simple_message(int socket, e_mc_message_type type)
-{
-  s_mc_message_t message;
-  message.type = type;
-  return MC_protocol_send(socket, &message, sizeof(message));
-}
-
-ssize_t MC_receive_message(int socket, void* message, size_t size, int options)
-{
-  int res = recv(socket, message, size, options);
-  if (res != -1)
-    XBT_DEBUG("Protocol [%s] received %s",
-      MC_mode_name(mc_mode),
-      MC_message_type_name(*(e_mc_message_type*) message));
-  return res;
-}
-
 const char* MC_message_type_name(e_mc_message_type type)
 {
   switch(type) {
 const char* MC_message_type_name(e_mc_message_type type)
 {
   switch(type) {
@@ -97,5 +64,3 @@ const char* MC_mode_name(e_mc_mode_t mode)
     return "?";
   }
 }
     return "?";
   }
 }
-
-}
index bd6fd13..b48902b 100644 (file)
@@ -114,10 +114,6 @@ typedef struct s_mc_restore_message {
   int index;
 } s_mc_restore_message_t, *mc_restore_message_t;
 
   int index;
 } s_mc_restore_message_t, *mc_restore_message_t;
 
-XBT_PRIVATE int MC_protocol_send(int socket, const void* message, size_t size);
-XBT_PRIVATE int MC_protocol_send_simple_message(int socket, e_mc_message_type type);
-XBT_PRIVATE ssize_t MC_receive_message(int socket, void* message, size_t size, int options);
-
 XBT_PRIVATE const char* MC_message_type_name(e_mc_message_type type);
 XBT_PRIVATE const char* MC_mode_name(e_mc_mode_t mode);
 
 XBT_PRIVATE const char* MC_message_type_name(e_mc_message_type type);
 XBT_PRIVATE const char* MC_mode_name(e_mc_mode_t mode);
 
index b48faf5..8a92857 100644 (file)
@@ -266,7 +266,7 @@ void SIMIX_global_init(int *argc, char **argv)
 #if HAVE_MC
   // The communication initialization is done ASAP.
   // We need to communicate  initialization of the different layers to the model-checker.
 #if HAVE_MC
   // The communication initialization is done ASAP.
   // We need to communicate  initialization of the different layers to the model-checker.
-  MC_client_init();
+  simgrid::mc::Client::initialize();
 #endif
 
   if (_sg_cfg_exit_asap)
 #endif
 
   if (_sg_cfg_exit_asap)
index ef11ae1..99b5aa5 100644 (file)
@@ -549,6 +549,8 @@ set(MC_SRC
   src/mc/RemotePtr.hpp
   src/mc/AddressSpace.hpp
   src/mc/AddressSpace.cpp
   src/mc/RemotePtr.hpp
   src/mc/AddressSpace.hpp
   src/mc/AddressSpace.cpp
+  src/mc/Channel.cpp
+  src/mc/Channel.hpp
   src/mc/Frame.hpp
   src/mc/Frame.cpp
   src/mc/ModelChecker.hpp
   src/mc/Frame.hpp
   src/mc/Frame.cpp
   src/mc/ModelChecker.hpp