[mc] Implement remote support for MC_ignore

diff --git a/src/mc/mc_checkpoint.c b/src/mc/mc_checkpoint.c
index bce4bbd..fe602a4 100644 (file)
--- a/src/mc/mc_checkpoint.c
+++ b/src/mc/mc_checkpoint.c
@@ -599,7 +599,7 @@ static void MC_snapshot_handle_ignore(mc_snapshot_t snapshot)
   unsigned int cursor = 0;
   mc_checkpoint_ignore_region_t region;
   // FIXME, cross-process support (mc_checkpoint_ignore)
   unsigned int cursor = 0;
   mc_checkpoint_ignore_region_t region;
   // FIXME, cross-process support (mc_checkpoint_ignore)

-  xbt_dynar_foreach (mc_checkpoint_ignore, cursor, region) {
+  xbt_dynar_foreach (mc_model_checker->process.checkpoint_ignore, cursor, region) {

     s_mc_snapshot_ignored_data_t ignored_data;
     ignored_data.start = region->addr;
     ignored_data.size = region->size;
     s_mc_snapshot_ignored_data_t ignored_data;
     ignored_data.start = region->addr;
     ignored_data.size = region->size;


@@ -612,7 +612,7 @@ static void MC_snapshot_handle_ignore(mc_snapshot_t snapshot)
   }
 
   // Zero the memory:
   }
 
   // Zero the memory:

-  xbt_dynar_foreach (mc_checkpoint_ignore, cursor, region) {
+  xbt_dynar_foreach (mc_model_checker->process.checkpoint_ignore, cursor, region) {

     MC_process_clear_memory(snapshot->process, region->addr, region->size);
   }
 
     MC_process_clear_memory(snapshot->process, region->addr, region->size);
   }
 

diff --git a/src/mc/mc_client.c b/src/mc/mc_client.c
index 55cc2ca..c903246 100644 (file)
--- a/src/mc/mc_client.c
+++ b/src/mc/mc_client.c
@@ -13,10 +13,16 @@
 
 #include <xbt/log.h>
 #include <xbt/sysdep.h>
 
 #include <xbt/log.h>
 #include <xbt/sysdep.h>

+#include <xbt/mmalloc.h>

 
 #include "mc_protocol.h"
 #include "mc_client.h"
 
 
 #include "mc_protocol.h"
 #include "mc_client.h"
 

+// We won't need those once the separation MCer/MCed is complete:
+#include "mc_mmalloc.h"
+#include "mc_ignore.h"
+#include "mc_model_checker.h"
+

 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_client, mc, "MC client logic");
 
 mc_client_t mc_client;
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_client, mc, "MC client logic");
 
 mc_client_t mc_client;


@@ -56,6 +62,12 @@ void MC_client_hello(void)
   XBT_DEBUG("Greeted the MC server");
 }
 
   XBT_DEBUG("Greeted the MC server");
 }
 

+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);
+}
+

 void MC_client_handle_messages(void)
 {
   while (1) {
 void MC_client_handle_messages(void)
 {
   while (1) {


@@ -80,3 +92,21 @@ void MC_client_handle_messages(void)
     }
   }
 }
     }
   }
 }

+
+void MC_ignore(void* addr, size_t size)
+{
+  if (mc_mode == MC_MODE_CLIENT) {
+    s_mc_ignore_memory_message_t message;
+    message.type = MC_MESSAGE_IGNORE_MEMORY;
+    message.addr = addr;
+    message.size = size;
+    MC_client_send_message(&message, sizeof(message));
+  }
+
+  // TODO, remove this once the migration has been completed
+  int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
+  MC_SET_MC_HEAP;
+  MC_process_ignore_memory(&mc_model_checker->process, addr, size);
+  if (!raw_mem_set)
+    MC_SET_STD_HEAP;
+}

diff --git a/src/mc/mc_client.h b/src/mc/mc_client.h
index 12234ed..638a8ea 100644 (file)
--- a/src/mc/mc_client.h
+++ b/src/mc/mc_client.h
@@ -21,6 +21,10 @@ extern mc_client_t mc_client;
 void MC_client_init(void);
 void MC_client_hello(void);
 void MC_client_handle_messages(void);
 void MC_client_init(void);
 void MC_client_hello(void);
 void MC_client_handle_messages(void);

+void MC_client_send_message(void* message, size_t size);
+
+void MC_ignore(void* addr, size_t size);
+

 
 SG_END_DECL()
 
 
 SG_END_DECL()
 

diff --git a/src/mc/mc_ignore.c b/src/mc/mc_ignore.c
index 5f8ea90..d80a130 100644 (file)
--- a/src/mc/mc_ignore.c
+++ b/src/mc/mc_ignore.c
@@ -18,7 +18,7 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_ignore, mc,
 
 
 /**************************** Global variables ******************************/
 
 
 /**************************** Global variables ******************************/

-xbt_dynar_t mc_checkpoint_ignore;
+

 extern xbt_dynar_t mc_heap_comparison_ignore;
 extern xbt_dynar_t stacks_areas;
 
 extern xbt_dynar_t mc_heap_comparison_ignore;
 extern xbt_dynar_t stacks_areas;
 


@@ -62,19 +62,21 @@ static void checkpoint_ignore_region_free_voidp(void *r)
   checkpoint_ignore_region_free((mc_checkpoint_ignore_region_t) * (void **) r);
 }
 
   checkpoint_ignore_region_free((mc_checkpoint_ignore_region_t) * (void **) r);
 }
 

+xbt_dynar_t MC_checkpoint_ignore_new(void)
+{
+  return xbt_dynar_new(sizeof(mc_checkpoint_ignore_region_t),
+                        checkpoint_ignore_region_free_voidp);
+}
+

 /***********************************************************************/
 
 void MC_heap_region_ignore_insert(mc_heap_ignore_region_t region)
 {
 /***********************************************************************/
 
 void MC_heap_region_ignore_insert(mc_heap_ignore_region_t region)
 {

-  int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
-

   if (mc_heap_comparison_ignore == NULL) {
     mc_heap_comparison_ignore =
         xbt_dynar_new(sizeof(mc_heap_ignore_region_t),
                       heap_ignore_region_free_voidp);
     xbt_dynar_push(mc_heap_comparison_ignore, &region);
   if (mc_heap_comparison_ignore == NULL) {
     mc_heap_comparison_ignore =
         xbt_dynar_new(sizeof(mc_heap_ignore_region_t),
                       heap_ignore_region_free_voidp);
     xbt_dynar_push(mc_heap_comparison_ignore, &region);

-    if (!raw_mem_set)
-      MC_SET_STD_HEAP;

     return;
   }
 
     return;
   }
 


@@ -92,8 +94,6 @@ void MC_heap_region_ignore_insert(mc_heap_ignore_region_t region)
                                                    mc_heap_ignore_region_t);
     if (current_region->address == region->address) {
       heap_ignore_region_free(region);
                                                    mc_heap_ignore_region_t);
     if (current_region->address == region->address) {
       heap_ignore_region_free(region);

-      if (!raw_mem_set)
-        MC_SET_STD_HEAP;

       return;
     } else if (current_region->address < region->address) {
       start = cursor + 1;
       return;
     } else if (current_region->address < region->address) {
       start = cursor + 1;


@@ -107,9 +107,6 @@ void MC_heap_region_ignore_insert(mc_heap_ignore_region_t region)
     xbt_dynar_insert_at(mc_heap_comparison_ignore, cursor + 1, &region);
   else
     xbt_dynar_insert_at(mc_heap_comparison_ignore, cursor, &region);
     xbt_dynar_insert_at(mc_heap_comparison_ignore, cursor + 1, &region);
   else
     xbt_dynar_insert_at(mc_heap_comparison_ignore, cursor, &region);

-
-  if (!raw_mem_set)
-    MC_SET_STD_HEAP;

 }
 
 void MC_heap_region_ignore_send(mc_heap_ignore_region_t region)
 }
 
 void MC_heap_region_ignore_send(mc_heap_ignore_region_t region)


@@ -129,7 +126,6 @@ void MC_ignore_heap(void *address, size_t size)
     return;
 
   int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
     return;
 
   int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);

-

   MC_SET_MC_HEAP;
 
   mc_heap_ignore_region_t region = NULL;
   MC_SET_MC_HEAP;
 
   mc_heap_ignore_region_t region = NULL;


@@ -387,44 +383,32 @@ void MC_new_stack_area(void *stack, smx_process_t process, void *context, size_t
     MC_SET_STD_HEAP;
 }
 
     MC_SET_STD_HEAP;
 }
 

-void MC_ignore(void *addr, size_t size)
+void MC_process_ignore_memory(mc_process_t process, void *addr, size_t size)

 {
 {

-
-  int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
-
-  MC_SET_MC_HEAP;
-
-  // FIXME, cross-process support
-  if (mc_checkpoint_ignore == NULL)
-    mc_checkpoint_ignore =
-        xbt_dynar_new(sizeof(mc_checkpoint_ignore_region_t),
-                      checkpoint_ignore_region_free_voidp);
-
+  xbt_dynar_t checkpoint_ignore = process->checkpoint_ignore;

   mc_checkpoint_ignore_region_t region =
       xbt_new0(s_mc_checkpoint_ignore_region_t, 1);
   region->addr = addr;
   region->size = size;
 
   mc_checkpoint_ignore_region_t region =
       xbt_new0(s_mc_checkpoint_ignore_region_t, 1);
   region->addr = addr;
   region->size = size;
 

-  if (xbt_dynar_is_empty(mc_checkpoint_ignore)) {
-    xbt_dynar_push(mc_checkpoint_ignore, &region);
+  if (xbt_dynar_is_empty(checkpoint_ignore)) {
+    xbt_dynar_push(checkpoint_ignore, &region);

   } else {
 
     unsigned int cursor = 0;
     int start = 0;
   } else {
 
     unsigned int cursor = 0;
     int start = 0;

-    int end = xbt_dynar_length(mc_checkpoint_ignore) - 1;
+    int end = xbt_dynar_length(checkpoint_ignore) - 1;

     mc_checkpoint_ignore_region_t current_region = NULL;
 
     while (start <= end) {
       cursor = (start + end) / 2;
       current_region =
     mc_checkpoint_ignore_region_t current_region = NULL;
 
     while (start <= end) {
       cursor = (start + end) / 2;
       current_region =

-          (mc_checkpoint_ignore_region_t) xbt_dynar_get_as(mc_checkpoint_ignore,
+          (mc_checkpoint_ignore_region_t) xbt_dynar_get_as(checkpoint_ignore,

                                                            cursor,
                                                            mc_checkpoint_ignore_region_t);
       if (current_region->addr == addr) {
         if (current_region->size == size) {
           checkpoint_ignore_region_free(region);
                                                            cursor,
                                                            mc_checkpoint_ignore_region_t);
       if (current_region->addr == addr) {
         if (current_region->size == size) {
           checkpoint_ignore_region_free(region);

-          if (!raw_mem_set)
-            MC_SET_STD_HEAP;

           return;
         } else if (current_region->size < size) {
           start = cursor + 1;
           return;
         } else if (current_region->size < size) {
           start = cursor + 1;


@@ -440,17 +424,14 @@ void MC_ignore(void *addr, size_t size)
 
     if (current_region->addr == addr) {
       if (current_region->size < size) {
 
     if (current_region->addr == addr) {
       if (current_region->size < size) {

-        xbt_dynar_insert_at(mc_checkpoint_ignore, cursor + 1, &region);
+        xbt_dynar_insert_at(checkpoint_ignore, cursor + 1, &region);

       } else {
       } else {

-        xbt_dynar_insert_at(mc_checkpoint_ignore, cursor, &region);
+        xbt_dynar_insert_at(checkpoint_ignore, cursor, &region);

       }
     } else if (current_region->addr < addr) {
       }
     } else if (current_region->addr < addr) {

-      xbt_dynar_insert_at(mc_checkpoint_ignore, cursor + 1, &region);
+      xbt_dynar_insert_at(checkpoint_ignore, cursor + 1, &region);

     } else {
     } else {

-      xbt_dynar_insert_at(mc_checkpoint_ignore, cursor, &region);
+      xbt_dynar_insert_at(checkpoint_ignore, cursor, &region);

     }
   }
     }
   }

-
-  if (!raw_mem_set)
-    MC_SET_STD_HEAP;

 }
 }

diff --git a/src/mc/mc_ignore.h b/src/mc/mc_ignore.h
new file mode 100644 (file)
index 0000000..35572d4
--- /dev/null
+++ b/src/mc/mc_ignore.h
@@ -0,0 +1,21 @@
+/* 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 <xbt/dynar.h>
+
+#include "mc/datatypes.h"
+#include "mc_process.h"
+
+#include "xbt/misc.h"           /* SG_BEGIN_DECL */
+
+SG_BEGIN_DECL();
+
+void MC_heap_region_ignore_insert(mc_heap_ignore_region_t region);
+void MC_heap_region_ignore_send(mc_heap_ignore_region_t region);
+void MC_process_ignore_memory(mc_process_t process, void *addr, size_t size);
+
+xbt_dynar_t MC_checkpoint_ignore_new(void);
+
+SG_END_DECL();

diff --git a/src/mc/mc_model_checker.h b/src/mc/mc_model_checker.h
index e8e7c82..308cf12 100644 (file)
--- a/src/mc/mc_model_checker.h
+++ b/src/mc/mc_model_checker.h
@@ -17,15 +17,6 @@
 
 SG_BEGIN_DECL()
 
 
 SG_BEGIN_DECL()
 

-typedef enum {
-  MC_MODE_NONE = 0,
-  MC_MODE_STANDALONE,
-  MC_MODE_CLIENT,
-  MC_MODE_SERVER
-} e_mc_mode_t;
-
-extern e_mc_mode_t mc_mode;
-

 /** @brief State of the model-checker (global variables for the model checker)
  *
  *  Each part of the state of the model chercker represented as a global
 /** @brief State of the model-checker (global variables for the model checker)
  *
  *  Each part of the state of the model chercker represented as a global

diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h
index 7f092a5..f6087c6 100644 (file)
--- a/src/mc/mc_private.h
+++ b/src/mc/mc_private.h
@@ -41,10 +41,6 @@ SG_BEGIN_DECL()
 
 typedef struct s_mc_function_index_item s_mc_function_index_item_t, *mc_function_index_item_t;
 
 
 typedef struct s_mc_function_index_item s_mc_function_index_item_t, *mc_function_index_item_t;
 

-/****************************** Snapshots ***********************************/
-
-extern xbt_dynar_t mc_checkpoint_ignore;
-

 /********************************* MC Global **********************************/
 
 /** Initialisation of the model-checker
 /********************************* MC Global **********************************/
 
 /** Initialisation of the model-checker

diff --git a/src/mc/mc_process.c b/src/mc/mc_process.c
index fd39420..10d0a45 100644 (file)
--- a/src/mc/mc_process.c
+++ b/src/mc/mc_process.c
@@ -21,6 +21,8 @@
 #include "mc_object_info.h"
 #include "mc_address_space.h"
 #include "mc_unw.h"
 #include "mc_object_info.h"
 #include "mc_address_space.h"
 #include "mc_unw.h"

+#include "mc_snapshot.h"
+#include "mc_ignore.h"

 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_process, mc,
                                 "MC process information");
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_process, mc,
                                 "MC process information");


@@ -28,6 +30,10 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_process, mc,
 static void MC_process_init_memory_map_info(mc_process_t process);
 static void MC_process_open_memory_file(mc_process_t process);
 
 static void MC_process_init_memory_map_info(mc_process_t process);
 static void MC_process_open_memory_file(mc_process_t process);
 

+// ***** Destructor callbacks
+
+// ***** mc_address_space methods for mc_process
+

 static mc_process_t MC_process_get_process(mc_process_t p) {
   return p;
 }
 static mc_process_t MC_process_get_process(mc_process_t p) {
   return p;
 }


@@ -42,6 +48,8 @@ bool MC_is_process(mc_address_space_t p)
   return p->address_space_class == &mc_process_class;
 }
 
   return p->address_space_class == &mc_process_class;
 }
 

+// ***** mc_process
+

 void MC_process_init(mc_process_t process, pid_t pid, int sockfd)
 {
   process->address_space.address_space_class = &mc_process_class;
 void MC_process_init(mc_process_t process, pid_t pid, int sockfd)
 {
   process->address_space.address_space_class = &mc_process_class;


@@ -70,6 +78,8 @@ void MC_process_init(mc_process_t process, pid_t pid, int sockfd)
     &process->heap_address, std_heap_var->address, sizeof(struct mdesc*),
     MC_PROCESS_INDEX_DISABLED);
 
     &process->heap_address, std_heap_var->address, sizeof(struct mdesc*),
     MC_PROCESS_INDEX_DISABLED);
 

+  process->checkpoint_ignore = MC_checkpoint_ignore_new();
+

   process->unw_addr_space = unw_create_addr_space(&mc_unw_accessors  , __BYTE_ORDER);
   if (process->process_flags & MC_PROCESS_SELF_FLAG) {
     process->unw_underlying_addr_space = unw_local_addr_space;
   process->unw_addr_space = unw_create_addr_space(&mc_unw_accessors  , __BYTE_ORDER);
   if (process->process_flags & MC_PROCESS_SELF_FLAG) {
     process->unw_underlying_addr_space = unw_local_addr_space;


@@ -92,6 +102,8 @@ void MC_process_clear(mc_process_t process)
   process->maestro_stack_start = NULL;
   process->maestro_stack_end = NULL;
 
   process->maestro_stack_start = NULL;
   process->maestro_stack_end = NULL;
 

+  xbt_dynar_free(&process->checkpoint_ignore);
+

   size_t i;
   for (i=0; i!=process->object_infos_size; ++i) {
     MC_free_object_info(&process->object_infos[i]);
   size_t i;
   for (i=0; i!=process->object_infos_size; ++i) {
     MC_free_object_info(&process->object_infos[i]);

diff --git a/src/mc/mc_process.h b/src/mc/mc_process.h
index b8c5514..1e4384d 100644 (file)
--- a/src/mc/mc_process.h
+++ b/src/mc/mc_process.h
@@ -102,6 +102,8 @@ struct s_mc_process {
   /** The corresponding context
    */
   void* unw_underlying_context;
   /** The corresponding context
    */
   void* unw_underlying_context;

+
+  xbt_dynar_t checkpoint_ignore;

 };
 
 bool MC_is_process(mc_address_space_t p);
 };
 
 bool MC_is_process(mc_address_space_t p);

diff --git a/src/mc/mc_protocol.h b/src/mc/mc_protocol.h
index be17129..70fcbbf 100644 (file)
--- a/src/mc/mc_protocol.h
+++ b/src/mc/mc_protocol.h
@@ -23,6 +23,17 @@ SG_BEGIN_DECL()
 /** Environment variable name used to pass the communication socket */
 #define MC_ENV_SOCKET_FD "SIMGRID_MC_SOCKET_FD"
 
 /** Environment variable name used to pass the communication socket */
 #define MC_ENV_SOCKET_FD "SIMGRID_MC_SOCKET_FD"
 

+// ***** MC mode
+
+typedef enum {
+  MC_MODE_NONE = 0,
+  MC_MODE_STANDALONE,
+  MC_MODE_CLIENT,
+  MC_MODE_SERVER
+} e_mc_mode_t;
+
+extern e_mc_mode_t mc_mode;
+

 // ***** Messages
 
 typedef enum {
 // ***** Messages
 
 typedef enum {


@@ -30,6 +41,7 @@ typedef enum {
   MC_MESSAGE_HELLO = 1,
   MC_MESSAGE_CONTINUE = 2,
   MC_MESSAGE_IGNORE_REGION = 3,
   MC_MESSAGE_HELLO = 1,
   MC_MESSAGE_CONTINUE = 2,
   MC_MESSAGE_IGNORE_REGION = 3,

+  MC_MESSAGE_IGNORE_MEMORY = 4,

 } e_mc_message_type;
 
 #define MC_MESSAGE_LENGTH 512
 } e_mc_message_type;
 
 #define MC_MESSAGE_LENGTH 512


@@ -55,6 +67,12 @@ typedef struct s_mc_ignore_region_message {
   s_mc_heap_ignore_region_t region;
 } s_mc_ignore_region_message_t, *mc_ignore_region_message_t;
 
   s_mc_heap_ignore_region_t region;
 } s_mc_ignore_region_message_t, *mc_ignore_region_message_t;
 

+typedef struct s_mc_ignore_memory_message {
+  e_mc_message_type type;
+  void *addr;
+  size_t size;
+} s_mc_ignore_memory_message_t, *mc_ignore_memory_message_t;
+

 int MC_protocol_send(int socket, void* message, size_t size);
 int MC_protocol_send_simple_message(int socket, int type);
 int MC_protocol_hello(int socket);
 int MC_protocol_send(int socket, void* message, size_t size);
 int MC_protocol_send_simple_message(int socket, int type);
 int MC_protocol_hello(int socket);

diff --git a/src/mc/mc_server.cpp b/src/mc/mc_server.cpp
index 88f2bb0..2308a85 100644 (file)
--- a/src/mc/mc_server.cpp
+++ b/src/mc/mc_server.cpp
@@ -19,6 +19,7 @@
 #include "mc_protocol.h"
 #include "mc_server.h"
 #include "mc_private.h"
 #include "mc_protocol.h"
 #include "mc_server.h"
 #include "mc_private.h"

+#include "mc_ignore.h"

 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_server, mc, "MC server logic");
 
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_server, mc, "MC server logic");
 


@@ -124,7 +125,7 @@ void throw_socket_error(int fd)
 
 void s_mc_server::handle_events()
 {
 
 void s_mc_server::handle_events()
 {

-  s_mc_message_t message;
+  char buffer[MC_MESSAGE_LENGTH];

   struct pollfd* socket_pollfd = &fds[SOCKET_FD_INDEX];
   struct pollfd* signalfd_pollfd = &fds[SIGNAL_FD_INDEX];
 
   struct pollfd* socket_pollfd = &fds[SOCKET_FD_INDEX];
   struct pollfd* signalfd_pollfd = &fds[SIGNAL_FD_INDEX];
 


@@ -139,16 +140,40 @@ void s_mc_server::handle_events()
 
   if (socket_pollfd->revents) {
     if (socket_pollfd->revents & POLLIN) {
 
   if (socket_pollfd->revents) {
     if (socket_pollfd->revents & POLLIN) {

-      ssize_t size = recv(socket_pollfd->fd, &message, sizeof(message), MSG_DONTWAIT);
+
+      ssize_t size = recv(socket_pollfd->fd, buffer, sizeof(buffer), MSG_DONTWAIT);

       if (size == -1 && errno != EAGAIN)
         throw std::system_error(errno, std::system_category());
       if (size == -1 && errno != EAGAIN)
         throw std::system_error(errno, std::system_category());

-      else switch(message.type) {
+
+      s_mc_message_t base_message;
+      if (size < (ssize_t) sizeof(base_message))
+        xbt_die("Broken message");
+      memcpy(&base_message, buffer, sizeof(base_message));
+
+      switch(base_message.type) {
+

       case MC_MESSAGE_IGNORE_REGION:
         XBT_DEBUG("Received ignored region");
       case MC_MESSAGE_IGNORE_REGION:
         XBT_DEBUG("Received ignored region");

-        // Ignored for now
+        if (size != sizeof(s_mc_ignore_region_message_t))
+          xbt_die("Broken messsage");
+        // TODO, handle the message

         break;
         break;

+
+      case MC_MESSAGE_IGNORE_MEMORY:
+        {
+          XBT_DEBUG("Received ignored memory");
+          if (size != sizeof(s_mc_ignore_memory_message_t))
+            xbt_die("Broken messsage");
+          s_mc_ignore_memory_message_t message;
+          memcpy(&message, buffer, sizeof(message));
+          MC_process_ignore_memory(&mc_model_checker->process,
+            message.addr, message.size);
+        }
+        break;
+

       default:
         xbt_die("Unexpected message from model-checked application");
       default:
         xbt_die("Unexpected message from model-checked application");

+

       }
       return;
     }
       }
       return;
     }