[mc] Communicate MC_remove_ignore_heap to the remote model-checker

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index 52848e6..22b7535 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -178,18 +178,13 @@ void MC_init_pid(pid_t pid, int socket)
     /* SIMIX */
     MC_ignore_global_variable("smx_total_comms");
 
-    MC_ignore_heap(mc_time, simix_process_maxpid * sizeof(double));
-
-    smx_process_t process;
-    // FIXME, cross-process support (simix_global->process_list)
-
     if (mc_mode == MC_MODE_STANDALONE || mc_mode == MC_MODE_CLIENT) {
+      MC_ignore_heap(mc_time, simix_process_maxpid * sizeof(double));
+      smx_process_t process;
       xbt_swag_foreach(process, simix_global->process_list) {
         MC_ignore_heap(&(process->process_hookup),
                        sizeof(process->process_hookup));
                        }
-    } else {
-      // TODO
     }
   }
 

diff --git a/src/mc/mc_ignore.c b/src/mc/mc_ignore.c
index d80a130..1657fc1 100644 (file)
--- a/src/mc/mc_ignore.c
+++ b/src/mc/mc_ignore.c
@@ -111,8 +111,8 @@ void MC_heap_region_ignore_insert(mc_heap_ignore_region_t region)
 
 void MC_heap_region_ignore_send(mc_heap_ignore_region_t region)
 {
-  s_mc_ignore_region_message_t message;
-  message.type = MC_MESSAGE_IGNORE_REGION;
+  s_mc_ignore_heap_message_t message;
+  message.type = MC_MESSAGE_IGNORE_HEAP;
   message.region = *region;
   if (MC_protocol_send(mc_client->fd, &message, sizeof(message)))
     xbt_die("Could not send ignored region to MCer");
@@ -122,14 +122,10 @@ void MC_heap_region_ignore_send(mc_heap_ignore_region_t region)
 // FIXME, cross-process support? (or make this it is used on the app-side)
 void MC_ignore_heap(void *address, size_t size)
 {
-  if(!std_heap)
-    return;
-
   int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
   MC_SET_MC_HEAP;
 
-  mc_heap_ignore_region_t region = NULL;
-  region = xbt_new0(s_mc_heap_ignore_region_t, 1);
+  mc_heap_ignore_region_t region = xbt_new0(s_mc_heap_ignore_region_t, 1);
   region->address = address;
   region->size = size;
 
@@ -160,6 +156,13 @@ void MC_ignore_heap(void *address, size_t size)
 
 void MC_remove_ignore_heap(void *address, size_t size)
 {
+  if (mc_mode == MC_MODE_CLIENT) {
+    s_mc_ignore_memory_message_t message;
+    message.type = MC_MESSAGE_UNIGNORE_HEAP;
+    message.addr = address;
+    message.size = size;
+    MC_client_send_message(&message, sizeof(message));
+  }
 
   int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
 

diff --git a/src/mc/mc_protocol.h b/src/mc/mc_protocol.h
index 70fcbbf..9623ec0 100644 (file)
--- a/src/mc/mc_protocol.h
+++ b/src/mc/mc_protocol.h
@@ -37,11 +37,12 @@ extern e_mc_mode_t mc_mode;
 // ***** Messages
 
 typedef enum {
-  MC_MESSAGE_NONE = 0,
-  MC_MESSAGE_HELLO = 1,
-  MC_MESSAGE_CONTINUE = 2,
-  MC_MESSAGE_IGNORE_REGION = 3,
-  MC_MESSAGE_IGNORE_MEMORY = 4,
+  MC_MESSAGE_NONE,
+  MC_MESSAGE_HELLO,
+  MC_MESSAGE_CONTINUE,
+  MC_MESSAGE_IGNORE_HEAP,
+  MC_MESSAGE_UNIGNORE_HEAP,
+  MC_MESSAGE_IGNORE_MEMORY,
 } e_mc_message_type;
 
 #define MC_MESSAGE_LENGTH 512
@@ -62,10 +63,10 @@ typedef struct s_mc_message {
   e_mc_message_type type;
 } s_mc_message_t, *mc_message_t;
 
-typedef struct s_mc_ignore_region_message {
+typedef struct s_mc_ignore_heap_message {
   e_mc_message_type type;
   s_mc_heap_ignore_region_t region;
-} s_mc_ignore_region_message_t, *mc_ignore_region_message_t;
+} s_mc_ignore_heap_message_t, *mc_ignore_heap_message_t;
 
 typedef struct s_mc_ignore_memory_message {
   e_mc_message_type type;

diff --git a/src/mc/mc_server.cpp b/src/mc/mc_server.cpp
index 2308a85..fb123fa 100644 (file)
--- a/src/mc/mc_server.cpp
+++ b/src/mc/mc_server.cpp
@@ -152,9 +152,16 @@ void s_mc_server::handle_events()
 
       switch(base_message.type) {
 
-      case MC_MESSAGE_IGNORE_REGION:
+      case MC_MESSAGE_IGNORE_HEAP:
         XBT_DEBUG("Received ignored region");
-        if (size != sizeof(s_mc_ignore_region_message_t))
+        if (size != sizeof(s_mc_ignore_heap_message_t))
+          xbt_die("Broken messsage");
+        // TODO, handle the message
+        break;
+
+      case MC_MESSAGE_UNIGNORE_HEAP:
+        XBT_DEBUG("Received unignored region");
+        if (size != sizeof(s_mc_ignore_memory_message_t))
           xbt_die("Broken messsage");
         // TODO, handle the message
         break;