Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
[mc] Partial integration of per-page snapshot address translation (wip)
authorGabriel Corona <gabriel.corona@loria.fr>
Fri, 13 Jun 2014 14:03:58 +0000 (16:03 +0200)
committerGabriel Corona <gabriel.corona@loria.fr>
Mon, 16 Jun 2014 11:26:08 +0000 (13:26 +0200)
buildtools/Cmake/DefinePackages.cmake
src/mc/mc_checkpoint.c
src/mc/mc_mmu.h
src/mc/mc_page_snapshot.cpp
src/mc/mc_private.h
src/mc/mc_snapshot.c [new file with mode: 0644]

index c12c3e2..57289cf 100644 (file)
@@ -584,6 +584,7 @@ set(JEDULE_SRC
 
 set(MC_SRC
   src/mc/mc_checkpoint.c
+  src/mc/mc_snapshot.c
   src/mc/mc_page_store.cpp
   src/mc/mc_page_snapshot.cpp
   src/mc/mc_comm_determinism.c
index 9d575f2..17cc3d5 100644 (file)
@@ -637,49 +637,6 @@ void MC_restore_snapshot(mc_snapshot_t snapshot)
   mc_model_checker->parent_snapshot = snapshot;
 }
 
-void *mc_translate_address(uintptr_t addr, mc_snapshot_t snapshot)
-{
-
-  // If not in a process state/clone:
-  if (!snapshot) {
-    return (uintptr_t *) addr;
-  }
-  // If it is in a snapshot:
-  for (size_t i = 0; i != NB_REGIONS; ++i) {
-    mc_mem_region_t region = snapshot->regions[i];
-    uintptr_t start = (uintptr_t) region->start_addr;
-    uintptr_t end = start + region->size;
-
-    // The address is in this region:
-    if (addr >= start && addr < end) {
-      uintptr_t offset = addr - start;
-      return (void *) ((uintptr_t) region->data + offset);
-    }
-
-  }
-
-  // It is not in a snapshot:
-  return (void *) addr;
-}
-
-uintptr_t mc_untranslate_address(void *addr, mc_snapshot_t snapshot)
-{
-  if (!snapshot) {
-    return (uintptr_t) addr;
-  }
-
-  for (size_t i = 0; i != NB_REGIONS; ++i) {
-    mc_mem_region_t region = snapshot->regions[i];
-    if (addr >= region->data
-        && addr <= (void *) (((char *) region->data) + region->size)) {
-      size_t offset = (size_t) ((char *) addr - (char *) region->data);
-      return ((uintptr_t) region->start_addr) + offset;
-    }
-  }
-
-  return (uintptr_t) addr;
-}
-
 mc_snapshot_t SIMIX_pre_mc_snapshot(smx_simcall_t simcall)
 {
   return MC_take_snapshot(1);
index 8df82fa..dd6f2da 100644 (file)
@@ -8,6 +8,7 @@
 #define MC_MMU_H
 
 #include <stdint.h>
+#include <stdbool.h>
 
 #include "mc_private.h"
 
@@ -30,9 +31,9 @@ static inline size_t mc_page_count(size_t size)
  *  @param address Address
  *  @return Virtual memory page number of the given address
  */
-static inline size_t mc_page_number(void* address)
+static inline size_t mc_page_number(void* base, void* address)
 {
-  return ((uintptr_t) address) >> xbt_pagebits;
+  return ((uintptr_t) address - (uintptr_t) base) >> xbt_pagebits;
 }
 
 /** @brief Get the offset of an address within a memory page
@@ -55,4 +56,9 @@ static inline void* mc_page_from_number(void* base, size_t page)
   return (void*) ((char*)base + (page << xbt_pagebits));
 }
 
+static inline bool mc_same_page(void* a, void* b)
+{
+  return mc_page_number(NULL, a) == mc_page_number(NULL, b);
+}
+
 #endif
index 245fc13..92959ad 100644 (file)
@@ -144,7 +144,7 @@ mc_mem_region_t mc_region_new_sparse(int type, void *start_addr, size_t size, mc
   uint64_t* pagemap = NULL;
   if (mc_model_checker->parent_snapshot) {
       pagemap = (uint64_t*) alloca(sizeof(uint64_t) * page_count);
-      mc_read_pagemap(pagemap, mc_page_number(start_addr), page_count);
+      mc_read_pagemap(pagemap, mc_page_number(NULL, start_addr), page_count);
   }
 
   // Take incremental snapshot:
@@ -164,7 +164,7 @@ void mc_region_restore_sparse(mc_mem_region_t reg, mc_mem_region_t ref_reg)
   // Read soft-dirty bits if necessary in order to know which pages have changed:
   if (mc_model_checker->parent_snapshot) {
     pagemap = (uint64_t*) alloca(sizeof(uint64_t) * page_count);
-    mc_read_pagemap(pagemap, mc_page_number(reg->start_addr), page_count);
+    mc_read_pagemap(pagemap, mc_page_number(NULL, reg->start_addr), page_count);
   }
 
   // Incremental per-page snapshot restoration:
index c8fa6bd..96fe0a0 100644 (file)
@@ -132,6 +132,9 @@ void mc_softdirty_reset();
 typedef struct s_mc_pages_store s_mc_pages_store_t, * mc_pages_store_t;
 mc_pages_store_t mc_pages_store_new();
 
+void* mc_snapshot_read_region(void* addr, mc_mem_region_t region, void* target, size_t size);
+void* mc_snapshot_read(void* addr, mc_snapshot_t snapshot, void* target, size_t size);
+
 /** @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
@@ -149,6 +152,8 @@ typedef struct s_mc_model_checker {
 
 extern mc_model_checker_t mc_model_checker;
 
+void* mc_translate_address_region(uintptr_t addr, mc_mem_region_t region);
+
 /** \brief Translate a pointer from process address space to snapshot address space
  *
  *  The address space contains snapshot of the main/application memory:
@@ -168,6 +173,8 @@ void* mc_translate_address(uintptr_t addr, mc_snapshot_t snapshot);
  *
  *  This is the inverse of mc_translate_address.
  *
+ *  Does not work for per-page snapshot, we change the logic to handle this.
+ *
  * \param addr    Address in the snapshot address space
  * \param snapsot Snapshot of interest (if NULL no translation is done)
  * \return        Translated address in the application address space
diff --git a/src/mc/mc_snapshot.c b/src/mc/mc_snapshot.c
new file mode 100644 (file)
index 0000000..2d59319
--- /dev/null
@@ -0,0 +1,166 @@
+/* Copyright (c) 2014. 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 "mc_private.h"
+#include "mc_mmu.h"
+
+static mc_mem_region_t mc_get_snapshot_region(void* addr, mc_snapshot_t snapshot)
+{
+  for (size_t i = 0; i != NB_REGIONS; ++i) {
+    mc_mem_region_t region = snapshot->regions[i];
+    void* start = region->start_addr;
+    void* end = (char*) start + region->size;
+
+    if (addr >= start && addr < end) {
+      return region;
+    }
+  }
+
+  return NULL;
+}
+
+void* mc_translate_address_region(uintptr_t addr, mc_mem_region_t region)
+{
+  if (!region) {
+    return (void *) addr;
+  }
+
+  // Flat snapshot:
+  else if (region->data) {
+    uintptr_t offset = addr - (uintptr_t) region->start_addr;
+    return (void *) ((uintptr_t) region->data + offset);
+  }
+
+  // Per-page snapshot:
+  else if (region->page_numbers) {
+    size_t pageno = mc_page_number(region->data, (void*) addr);
+    return (char*) region->page_numbers[pageno] + mc_page_offset((void*) addr);
+  }
+
+  else {
+    xbt_die("No data for this memory region");
+  }
+}
+
+void* mc_translate_address(uintptr_t addr, mc_snapshot_t snapshot)
+{
+
+  // If not in a process state/clone:
+  if (!snapshot) {
+    return (uintptr_t *) addr;
+  }
+
+  mc_mem_region_t region = mc_get_snapshot_region((void*) addr, snapshot);
+  return mc_translate_address_region(addr, region);
+
+}
+
+uintptr_t mc_untranslate_address(void *addr, mc_snapshot_t snapshot)
+{
+  if (!snapshot) {
+    return (uintptr_t) addr;
+  }
+
+  for (size_t i = 0; i != NB_REGIONS; ++i) {
+    mc_mem_region_t region = snapshot->regions[i];
+    if (region->page_numbers) {
+      xbt_die("Does not work for per-page snapshot.");
+    }
+    if (addr >= region->data
+        && addr <= (void *) (((char *) region->data) + region->size)) {
+      size_t offset = (size_t) ((char *) addr - (char *) region->data);
+      return ((uintptr_t) region->start_addr) + offset;
+    }
+  }
+
+  return (uintptr_t) addr;
+}
+
+/** @brief Read memory from a snapshot region broken across fragmented pages
+ *
+ *  @param addr    Process (non-snapshot) address of the data
+ *  @param region  Snapshot memory region where the data is located
+ *  @param target  Buffer to store the value
+ *  @param size    Size of the data to read in bytes
+ *  @return Pointer where the data is located (target buffer of original location)
+ */
+static void* mc_snapshot_read_fragmented(void* addr, mc_mem_region_t region, void* target, size_t size)
+{
+  void* end = (char*) addr + size - 1;
+  size_t page_end = mc_page_number(NULL, end);
+
+  // Read each page:
+  while (mc_page_number(NULL, addr) != page_end) {
+    void* snapshot_addr = mc_translate_address_region((uintptr_t) addr, region);
+    void* next_page = mc_page_from_number(NULL, mc_page_number(NULL, addr) + 1);
+    size_t readable = (char*) next_page - (char*) addr;
+    memcpy(target, snapshot_addr, readable);
+    target = (char*) target + readable;
+    size -= readable;
+  }
+
+  // Read the end:
+  void* snapshot_addr = mc_translate_address_region((uintptr_t)addr, region);
+  memcpy(target, snapshot_addr, size);
+
+  return target;
+}
+
+/** @brief Read memory from a snapshot region
+ *
+ *  @param addr    Process (non-snapshot) address of the data
+ *  @param region  Snapshot memory region where the data is located
+ *  @param target  Buffer to store the value
+ *  @param size    Size of the data to read in bytes
+ *  @return Pointer where the data is located (target buffer of original location)
+ */
+void* mc_snapshot_read_region(void* addr, mc_mem_region_t region, void* target, size_t size)
+{
+  uintptr_t offset = (uintptr_t) addr - (uintptr_t) region->start_addr;
+
+  if (addr < region->start_addr || offset+size > region->size) {
+    xbt_die("Trying to read out of the region boundary.");
+  }
+
+  // Linear memory region:
+  if (region->data) {
+    return (void*) ((uintptr_t) region->data + offset);
+  }
+
+  // Fragmented memory region:
+  else if (region->page_numbers) {
+    void* end = (char*) addr + size - 1;
+    if( mc_same_page(addr, end) ) {
+      // The memory is contained in a single page:
+      return mc_translate_address_region((uintptr_t) addr, region);
+    } else {
+      // The memory spans several pages:
+      return mc_snapshot_read_fragmented(addr, region, target, size);
+    }
+  }
+
+  else {
+    xbt_die("No data available for this region");
+  }
+}
+
+/** @brief Read memory from a snapshot
+ *
+ *  @param addr     Process (non-snapshot) address of the data
+ *  @param snapshot Snapshot (or NULL is no snapshot)
+ *  @param target   Buffer to store the value
+ *  @param size     Size of the data to read in bytes
+ *  @return Pointer where the data is located (target buffer of original location)
+ */
+void* mc_snapshot_read(void* addr, mc_snapshot_t snapshot, void* target, size_t size)
+{
+  if (snapshot) {
+    mc_mem_region_t region = mc_get_snapshot_region(addr, snapshot);
+    return mc_snapshot_read_region(addr, region, target, size);
+  } else {
+    return target;
+  }
+}