[mc] Make a std::vector of Process::checkpoint_ignore

diff --git a/src/mc/mc_checkpoint.cpp b/src/mc/mc_checkpoint.cpp
index e05a59e..aca9153 100644 (file)
--- a/src/mc/mc_checkpoint.cpp
+++ b/src/mc/mc_checkpoint.cpp
@@ -575,23 +575,21 @@ static void MC_snapshot_handle_ignore(mc_snapshot_t snapshot)
   snapshot->ignored_data = xbt_dynar_new(sizeof(s_mc_snapshot_ignored_data_t), mc_free_snapshot_ignored_data_pvoid);
 
   // Copy the memory:
   snapshot->ignored_data = xbt_dynar_new(sizeof(s_mc_snapshot_ignored_data_t), mc_free_snapshot_ignored_data_pvoid);
 
   // Copy the memory:

-  unsigned int cursor = 0;
-  mc_checkpoint_ignore_region_t region;
-  xbt_dynar_foreach (mc_model_checker->process().checkpoint_ignore, cursor, region) {
+  for (auto const& region : mc_model_checker->process().ignored_regions()) {

     s_mc_snapshot_ignored_data_t ignored_data;
     s_mc_snapshot_ignored_data_t ignored_data;

-    ignored_data.start = region->addr;
-    ignored_data.size = region->size;
-    ignored_data.data = malloc(region->size);
+    ignored_data.start = (void*)region.addr;
+    ignored_data.size = region.size;
+    ignored_data.data = malloc(region.size);

     // TODO, we should do this once per privatization segment:
     snapshot->process->read_bytes(
     // TODO, we should do this once per privatization segment:
     snapshot->process->read_bytes(

-      ignored_data.data, region->size, remote(region->addr),
+      ignored_data.data, region.size, remote(region.addr),

       simgrid::mc::ProcessIndexDisabled);
     xbt_dynar_push(snapshot->ignored_data, &ignored_data);
   }
 
   // Zero the memory:
       simgrid::mc::ProcessIndexDisabled);
     xbt_dynar_push(snapshot->ignored_data, &ignored_data);
   }
 
   // Zero the memory:

-  xbt_dynar_foreach (mc_model_checker->process().checkpoint_ignore, cursor, region) {
-    snapshot->process->clear_bytes(remote(region->addr), region->size);
+  for(auto const& region : mc_model_checker->process().ignored_regions()) {
+    snapshot->process->clear_bytes(remote(region.addr), region.size);

   }
 
 }
   }
 
 }

diff --git a/src/mc/mc_process.cpp b/src/mc/mc_process.cpp
index 66bb067..e80715b 100644 (file)
--- a/src/mc/mc_process.cpp
+++ b/src/mc/mc_process.cpp
@@ -225,8 +225,6 @@ Process::Process(pid_t pid, int sockfd)
   process->smx_process_infos = MC_smx_process_info_list_new();
   process->smx_old_process_infos = MC_smx_process_info_list_new();
 
   process->smx_process_infos = MC_smx_process_info_list_new();
   process->smx_old_process_infos = MC_smx_process_info_list_new();
 

-  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;


@@ -250,8 +248,6 @@ Process::~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);
-

   xbt_dynar_free(&process->smx_process_infos);
   xbt_dynar_free(&process->smx_old_process_infos);
 
   xbt_dynar_free(&process->smx_process_infos);
   xbt_dynar_free(&process->smx_old_process_infos);
 


@@ -591,5 +587,53 @@ void Process::clear_bytes(remote_ptr<void> address, size_t len)
   }
 }
 
   }
 }
 

+void Process::ignore_region(std::uint64_t addr, std::size_t size)
+{
+  IgnoredRegion region;
+  region.addr = addr;
+  region.size = size;
+
+  if (ignored_regions_.empty()) {
+    ignored_regions_.push_back(region);
+    return;
+  }
+
+  unsigned int cursor = 0;
+  IgnoredRegion* current_region = nullptr;
+
+  int start = 0;
+  int end = ignored_regions_.size() - 1;
+  while (start <= end) {
+    cursor = (start + end) / 2;
+    current_region = &ignored_regions_[cursor];
+    if (current_region->addr == addr) {
+      if (current_region->size == size)
+        return;
+      else if (current_region->size < size)
+        start = cursor + 1;
+      else
+        end = cursor - 1;
+    } else if (current_region->addr < addr)
+      start = cursor + 1;
+    else
+      end = cursor - 1;
+  }
+
+  std::size_t position;
+  if (current_region->addr == addr) {
+    if (current_region->size < size) {
+      position = cursor + 1;
+    } else {
+      position = cursor;
+    }
+  } else if (current_region->addr < addr) {
+    position = cursor + 1;
+  } else {
+    position = cursor;
+  }
+  ignored_regions_.insert(
+    ignored_regions_.begin() + position, region);
+}
+

 }
 }
 }
 }

diff --git a/src/mc/mc_process.h b/src/mc/mc_process.h
index 703dd55..b8408c1 100644 (file)
--- a/src/mc/mc_process.h
+++ b/src/mc/mc_process.h
@@ -10,6 +10,8 @@
 #include <stdbool.h>
 #include <sys/types.h>
 
 #include <stdbool.h>
 #include <sys/types.h>
 

+#include <vector>
+

 #include "simgrid_config.h"
 #include <sys/types.h>
 
 #include "simgrid_config.h"
 #include <sys/types.h>
 


@@ -47,6 +49,11 @@ typedef struct s_mc_smx_process_info s_mc_smx_process_info_t, *mc_smx_process_in
 namespace simgrid {
 namespace mc {
 
 namespace simgrid {
 namespace mc {
 

+struct IgnoredRegion {
+  std::uint64_t addr;
+  size_t size;
+};
+

 /** Representation of a process
  */
 class Process : public AddressSpace {
 /** Representation of a process
  */
 class Process : public AddressSpace {


@@ -91,6 +98,12 @@ public:
     return this->heap_info;
   }
 
     return this->heap_info;
   }
 

+  std::vector<IgnoredRegion> const& ignored_regions() const
+  {
+    return ignored_regions_;
+  }
+  void ignore_region(std::uint64_t address, std::size_t size);
+

 private:
   void init_memory_map_info();
   void refresh_heap();
 private:
   void init_memory_map_info();
   void refresh_heap();


@@ -164,7 +177,8 @@ public: // to be private
    */
   void* unw_underlying_context;
 
    */
   void* unw_underlying_context;
 

-  xbt_dynar_t checkpoint_ignore;
+private:
+  std::vector<IgnoredRegion> ignored_regions_;

 };
 
 /** Open a FD to a remote process memory (`/dev/$pid/mem`)
 };
 
 /** Open a FD to a remote process memory (`/dev/$pid/mem`)

diff --git a/src/mc/mc_server.cpp b/src/mc/mc_server.cpp
index ef4dae3..0e567b1 100644 (file)
--- a/src/mc/mc_server.cpp
+++ b/src/mc/mc_server.cpp
@@ -198,8 +198,8 @@ bool s_mc_server::handle_events()
           if (size != sizeof(message))
             xbt_die("Broken messsage");
           memcpy(&message, buffer, sizeof(message));
           if (size != sizeof(message))
             xbt_die("Broken messsage");
           memcpy(&message, buffer, sizeof(message));

-          MC_process_ignore_memory(&mc_model_checker->process(),
-            message.addr, message.size);
+          mc_model_checker->process().ignore_region(
+            (std::uint64_t)message.addr, message.size);

           break;
         }
 
           break;
         }
 

diff --git a/src/mc/mc_snapshot.h b/src/mc/mc_snapshot.h
index 135cf26..0764225 100644 (file)
--- a/src/mc/mc_snapshot.h
+++ b/src/mc/mc_snapshot.h
@@ -274,11 +274,6 @@ typedef struct s_mc_global_t {
   char *recv_diff;
 }s_mc_global_t, *mc_global_t;
 
   char *recv_diff;
 }s_mc_global_t, *mc_global_t;
 

-typedef struct s_mc_checkpoint_ignore_region{
-  void *addr;
-  size_t size;
-}s_mc_checkpoint_ignore_region_t, *mc_checkpoint_ignore_region_t;
-

 static const void* mc_snapshot_get_heap_end(mc_snapshot_t snapshot);
 
 XBT_INTERNAL mc_snapshot_t MC_take_snapshot(int num_state);
 static const void* mc_snapshot_get_heap_end(mc_snapshot_t snapshot);
 
 XBT_INTERNAL mc_snapshot_t MC_take_snapshot(int num_state);

diff --git a/src/mc/mcer_ignore.cpp b/src/mc/mcer_ignore.cpp
index 54d2da2..55b56d0 100644 (file)
--- a/src/mc/mcer_ignore.cpp
+++ b/src/mc/mcer_ignore.cpp
@@ -238,79 +238,6 @@ static void mc_ignore_local_variable_in_scope(const char *var_name,
   }
 }
 
   }
 }
 

-// ****** Checkpoint ignore:
-
-static void checkpoint_ignore_region_free(mc_checkpoint_ignore_region_t r)
-{
-  xbt_free(r);
-}
-
-static void checkpoint_ignore_region_free_voidp(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);
-}
-
-// ***** Generic memory ignore mechanism
-
-void MC_process_ignore_memory(mc_process_t process, void *addr, size_t size)
-{
-  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;
-
-  if (xbt_dynar_is_empty(checkpoint_ignore)) {
-    xbt_dynar_push(checkpoint_ignore, &region);
-  } else {
-
-    unsigned int cursor = 0;
-    int start = 0;
-    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) 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);
-          return;
-        } else if (current_region->size < size) {
-          start = cursor + 1;
-        } else {
-          end = cursor - 1;
-        }
-      } else if (current_region->addr < addr) {
-        start = cursor + 1;
-      } else {
-        end = cursor - 1;
-      }
-    }
-
-    if (current_region->addr == addr) {
-      if (current_region->size < size) {
-        xbt_dynar_insert_at(checkpoint_ignore, cursor + 1, &region);
-      } else {
-        xbt_dynar_insert_at(checkpoint_ignore, cursor, &region);
-      }
-    } else if (current_region->addr < addr) {
-      xbt_dynar_insert_at(checkpoint_ignore, cursor + 1, &region);
-    } else {
-      xbt_dynar_insert_at(checkpoint_ignore, cursor, &region);
-    }
-  }
-}
-

 extern xbt_dynar_t stacks_areas;
 
 void MC_stack_area_add(stack_region_t stack_area)
 extern xbt_dynar_t stacks_areas;
 
 void MC_stack_area_add(stack_region_t stack_area)

diff --git a/src/mc/mcer_ignore.h b/src/mc/mcer_ignore.h
index 1c56b62..aa740df 100644 (file)
--- a/src/mc/mcer_ignore.h
+++ b/src/mc/mcer_ignore.h
@@ -15,6 +15,5 @@ SG_BEGIN_DECL();
 XBT_INTERNAL void MCer_ignore_global_variable(const char *var_name);
 XBT_INTERNAL void MC_heap_region_ignore_insert(mc_heap_ignore_region_t region);
 XBT_INTERNAL void MC_heap_region_ignore_remove(void *address, size_t size);
 XBT_INTERNAL void MCer_ignore_global_variable(const char *var_name);
 XBT_INTERNAL void MC_heap_region_ignore_insert(mc_heap_ignore_region_t region);
 XBT_INTERNAL void MC_heap_region_ignore_remove(void *address, size_t size);

-XBT_INTERNAL void MC_process_ignore_memory(mc_process_t process, void *addr, size_t size);

 
 SG_END_DECL();
 
 SG_END_DECL();