X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/b40c2e9bf3cf6e8b2fad15594852ce186bf99574..a24865789e18ecc8625a9518db00c95607d541af:/src/mc/mc_checkpoint.c

diff --git a/src/mc/mc_checkpoint.c b/src/mc/mc_checkpoint.c
index 211d99dd31..202a2f10a0 100644
--- a/src/mc/mc_checkpoint.c
+++ b/src/mc/mc_checkpoint.c
@@ -13,6 +13,7 @@
 #include "xbt/module.h"
 #include <xbt/mmalloc.h>
 #include "../smpi/private.h"
+#include <alloca.h>
 
 #include "xbt/mmalloc/mmprivate.h"
 
@@ -22,6 +23,9 @@
 #include <libelf.h>
 
 #include "mc_private.h"
+#include <mc/mc.h>
+
+#include "mc_mmu.h"
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_checkpoint, mc,
                                 "Logging specific to mc_checkpoint");
@@ -60,6 +64,9 @@ static void MC_region_destroy(mc_mem_region_t reg)
 {
   //munmap(reg->data, reg->size);
   xbt_free(reg->data);
+  if (reg->page_numbers) {
+    mc_free_page_snapshot_region(reg->page_numbers, mc_page_count(reg->size));
+  }
   xbt_free(reg);
 }
 
@@ -72,9 +79,10 @@ void MC_free_snapshot(mc_snapshot_t snapshot)
   xbt_free(snapshot->stack_sizes);
   xbt_dynar_free(&(snapshot->stacks));
   xbt_dynar_free(&(snapshot->to_ignore));
+  xbt_dynar_free(&snapshot->ignored_data);
 
   if (snapshot->privatization_regions) {
-    size_t n = snapshot->nb_processes;
+    size_t n = xbt_dynar_length(snapshot->enabled_processes);
     for (i = 0; i != n; ++i) {
       MC_region_destroy(snapshot->privatization_regions[i]);
     }
@@ -84,41 +92,57 @@ void MC_free_snapshot(mc_snapshot_t snapshot)
   xbt_free(snapshot);
 }
 
-
 /*******************************  Snapshot regions ********************************/
 /*********************************************************************************/
 
-static mc_mem_region_t MC_region_new(int type, void *start_addr, size_t size)
+static mc_mem_region_t MC_region_new(int type, void *start_addr, size_t size, mc_mem_region_t ref_reg)
 {
+  if (_sg_mc_sparse_checkpoint) {
+    return mc_region_new_sparse(type, start_addr, size, ref_reg);
+  }
+
   mc_mem_region_t new_reg = xbt_new(s_mc_mem_region_t, 1);
   new_reg->start_addr = start_addr;
+  new_reg->data = NULL;
   new_reg->size = size;
-  //new_reg->data = mmap(NULL, size, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0);
-  //if(new_reg->data==MAP_FAILED)
-  //xbt_die("Could not mmap new memory for snapshot.");
+  new_reg->page_numbers = NULL;
   new_reg->data = xbt_malloc(size);
   memcpy(new_reg->data, start_addr, size);
-  //madvise(new_reg->data, size, MADV_MERGEABLE);
-
   XBT_DEBUG("New region : type : %d, data : %p (real addr %p), size : %zu",
             type, new_reg->data, start_addr, size);
-
   return new_reg;
+
 }
 
-static void MC_region_restore(mc_mem_region_t reg)
+/** @brief Restore a region from a snapshot
+ *
+ *  If we are using per page snapshots, it is possible to use the reference
+ *  region in order to do an incremental restoration of the region: the
+ *  softclean pages which are shared between the two snapshots do not need
+ *  to be restored.
+ *
+ *  @param reg     Target region
+ *  @param reg_reg Current region (if not NULL), used for lazy per page restoration
+ */
+static void MC_region_restore(mc_mem_region_t reg, mc_mem_region_t ref_reg)
 {
   /*FIXME: check if start_addr is still mapped, if it is not, then map it
-     before copying the data */
-
-  memcpy(reg->start_addr, reg->data, reg->size);
+    before copying the data */
+  if (!reg->page_numbers) {
+    memcpy(reg->start_addr, reg->data, reg->size);
+  } else {
+    mc_region_restore_sparse(reg, ref_reg);
+  }
   return;
 }
 
 static void MC_snapshot_add_region(mc_snapshot_t snapshot, int type,
                                    void *start_addr, size_t size)
+
 {
-  mc_mem_region_t new_reg = MC_region_new(type, start_addr, size);
+  mc_mem_region_t ref_reg =
+    mc_model_checker->parent_snapshot ? mc_model_checker->parent_snapshot->regions[type] : NULL;
+  mc_mem_region_t new_reg = MC_region_new(type, start_addr, size, ref_reg);
   snapshot->regions[type] = new_reg;
   return;
 }
@@ -145,8 +169,10 @@ static void MC_get_memory_regions(mc_snapshot_t snapshot)
     snapshot->privatization_regions =
         xbt_new(mc_mem_region_t, SIMIX_process_count());
     for (i = 0; i < SIMIX_process_count(); i++) {
+      mc_mem_region_t ref_reg =
+        mc_model_checker->parent_snapshot ? mc_model_checker->parent_snapshot->privatization_regions[i] : NULL;
       snapshot->privatization_regions[i] =
-          MC_region_new(-1, mappings[i], size_data_exe);
+        MC_region_new(-1, mappings[i], size_data_exe, ref_reg);
     }
     snapshot->privatization_index = loaded_page;
   }
@@ -440,7 +466,7 @@ static xbt_dynar_t MC_unwind_stack_frames(void *stack_context)
   return result;
 };
 
-static xbt_dynar_t MC_take_snapshot_stacks(mc_snapshot_t * snapshot, void *heap)
+static xbt_dynar_t MC_take_snapshot_stacks(mc_snapshot_t * snapshot)
 {
 
   xbt_dynar_t res =
@@ -456,18 +482,12 @@ static xbt_dynar_t MC_take_snapshot_stacks(mc_snapshot_t * snapshot, void *heap)
     st->local_variables = MC_get_local_variables_values(st->stack_frames);
 
     unw_word_t sp = xbt_dynar_get_as(st->stack_frames, 0, mc_stack_frame_t)->sp;
-    st->stack_pointer =
-        ((char *) heap + (size_t) (((char *) ((long) sp) - (char *) std_heap)));
 
-    st->real_address = current_stack->address;
     xbt_dynar_push(res, &st);
     (*snapshot)->stack_sizes =
         xbt_realloc((*snapshot)->stack_sizes, (cursor + 1) * sizeof(size_t));
     (*snapshot)->stack_sizes[cursor] =
-        current_stack->size - ((char *) st->stack_pointer -
-                               (char *) ((char *) heap +
-                                         ((char *) current_stack->address -
-                                          (char *) std_heap)));
+      (char*) current_stack->address + current_stack->size - (char*) sp;
   }
 
   return res;
@@ -501,53 +521,83 @@ static xbt_dynar_t MC_take_snapshot_ignore()
 
 }
 
-static void MC_dump_checkpoint_ignore(mc_snapshot_t snapshot)
+static void mc_free_snapshot_ignored_data_pvoid(void* data) {
+  mc_snapshot_ignored_data_t ignored_data = (mc_snapshot_ignored_data_t) data;
+  free(ignored_data->data);
+}
+
+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:
   unsigned int cursor = 0;
   mc_checkpoint_ignore_region_t region;
-  size_t offset;
-
-  xbt_dynar_foreach(mc_checkpoint_ignore, cursor, region) {
-    if (region->addr > snapshot->regions[0]->start_addr
-        && (char *) (region->addr) <
-        (char *) snapshot->regions[0]->start_addr + STD_HEAP_SIZE) {
-      offset =
-          (char *) region->addr - (char *) snapshot->regions[0]->start_addr;
-      memset((char *) snapshot->regions[0]->data + offset, 0, region->size);
-    } else if (region->addr > snapshot->regions[2]->start_addr
-               && (char *) (region->addr) <
-               (char *) snapshot->regions[2]->start_addr +
-               snapshot->regions[2]->size) {
-      offset =
-          (char *) region->addr - (char *) snapshot->regions[2]->start_addr;
-      memset((char *) snapshot->regions[2]->data + offset, 0, region->size);
-    } else if (region->addr > snapshot->regions[1]->start_addr
-               && (char *) (region->addr) <
-               (char *) snapshot->regions[1]->start_addr +
-               snapshot->regions[1]->size) {
-      offset =
-          (char *) region->addr - (char *) snapshot->regions[1]->start_addr;
-      memset((char *) snapshot->regions[1]->data + offset, 0, region->size);
-    }
+  xbt_dynar_foreach (mc_checkpoint_ignore, cursor, region) {
+    s_mc_snapshot_ignored_data_t ignored_data;
+    ignored_data.start = region->addr;
+    ignored_data.size = region->size;
+    ignored_data.data = malloc(region->size);
+    memcpy(ignored_data.data, region->addr, region->size);
+    xbt_dynar_push(snapshot->ignored_data, &ignored_data);
   }
 
+  // Zero the memory:
+  xbt_dynar_foreach (mc_checkpoint_ignore, cursor, region) {
+    memset(region->addr, 0, region->size);
+  }
+
+}
+
+static void MC_snapshot_ignore_restore(mc_snapshot_t snapshot)
+{
+  unsigned int cursor = 0;
+  s_mc_snapshot_ignored_data_t ignored_data;
+  xbt_dynar_foreach (snapshot->ignored_data, cursor, ignored_data) {
+    memcpy(ignored_data.start, ignored_data.data, ignored_data.size);
+  }
+}
+
+/** @brief Can we remove this snapshot?
+ *
+ * Some snapshots cannot be removed (yet) because we need them
+ * at this point.
+ *
+ * @param snapshot
+ */
+int mc_important_snapshot(mc_snapshot_t snapshot)
+{
+  // We need this snapshot in order to know which
+  // pages needs to be stored in the next snapshot:
+  if (_sg_mc_sparse_checkpoint && snapshot == mc_model_checker->parent_snapshot)
+    return true;
+
+  return false;
 }
 
 mc_snapshot_t MC_take_snapshot(int num_state)
 {
 
   mc_snapshot_t snapshot = xbt_new0(s_mc_snapshot_t, 1);
-  snapshot->nb_processes = xbt_swag_size(simix_global->process_list);
+  snapshot->enabled_processes = xbt_dynar_new(sizeof(int), NULL);
+  smx_process_t process;
+  xbt_swag_foreach(process, simix_global->process_list) {
+    xbt_dynar_push_as(snapshot->enabled_processes, int, (int)process->pid);
+  }
+
+  MC_snapshot_handle_ignore(snapshot);
 
   /* Save the std heap and the writable mapped pages of libsimgrid and binary */
   MC_get_memory_regions(snapshot);
+  if (_sg_mc_sparse_checkpoint && _sg_mc_soft_dirty) {
+    mc_softdirty_reset();
+  }
 
   snapshot->to_ignore = MC_take_snapshot_ignore();
 
   if (_sg_mc_visited > 0 || strcmp(_sg_mc_property_file, "")) {
     snapshot->stacks =
-        MC_take_snapshot_stacks(&snapshot, snapshot->regions[0]->data);
+        MC_take_snapshot_stacks(&snapshot);
     if (_sg_mc_hash && snapshot->stacks != NULL) {
       snapshot->hash = mc_hash_processes_state(num_state, snapshot->stacks);
     } else {
@@ -557,80 +607,39 @@ mc_snapshot_t MC_take_snapshot(int num_state)
     snapshot->hash = 0;
   }
 
-  if (num_state > 0)
-    MC_dump_checkpoint_ignore(snapshot);
-
-  // mprotect the region after zero-ing ignored parts:
-  /*size_t i;
-     for(i=0; i!=NB_REGIONS; ++i) {
-     mc_mem_region_t region = snapshot->regions[i];
-     mprotect(region->data, region->size, PROT_READ);
-     } */
-
+  MC_snapshot_ignore_restore(snapshot);
+  mc_model_checker->parent_snapshot = snapshot;
   return snapshot;
-
 }
 
 void MC_restore_snapshot(mc_snapshot_t snapshot)
 {
+  mc_snapshot_t parent_snapshot = mc_model_checker->parent_snapshot;
+
   unsigned int i;
   for (i = 0; i < NB_REGIONS; i++) {
     // For privatized, variables we decided it was not necessary to take the snapshot:
     if (snapshot->regions[i])
-      MC_region_restore(snapshot->regions[i]);
+      MC_region_restore(snapshot->regions[i],
+        parent_snapshot ? parent_snapshot->regions[i] : NULL);
   }
 
   if (snapshot->privatization_regions) {
     for (i = 0; i < SIMIX_process_count(); i++) {
       if (snapshot->privatization_regions[i]) {
-        MC_region_restore(snapshot->privatization_regions[i]);
+        MC_region_restore(snapshot->privatization_regions[i],
+          parent_snapshot ? parent_snapshot->privatization_regions[i] : NULL);
       }
     }
     switch_data_segment(snapshot->privatization_index);
   }
-}
 
-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;
-    }
+  if (_sg_mc_sparse_checkpoint && _sg_mc_soft_dirty) {
+    mc_softdirty_reset();
   }
 
-  return (uintptr_t) addr;
+  MC_snapshot_ignore_restore(snapshot);
+  mc_model_checker->parent_snapshot = snapshot;
 }
 
 mc_snapshot_t SIMIX_pre_mc_snapshot(smx_simcall_t simcall)