### MC ###
IF(HAVE_MC)
+ ADD_TESH(page_store --setenv bindir=${CMAKE_BINARY_DIR}/teshsuite/mc --cd ${CMAKE_HOME_DIRECTORY}/teshsuite/mc page_store.tesh)
ADD_TESH(tesh-mc-dwarf --setenv bindir=${CMAKE_BINARY_DIR}/teshsuite/mc/dwarf --cd ${CMAKE_HOME_DIRECTORY}/teshsuite/mc/dwarf dwarf.tesh)
ADD_TESH(tesh-mc-dwarf-expression --setenv bindir=${CMAKE_BINARY_DIR}/teshsuite/mc/dwarf_expression --cd ${CMAKE_HOME_DIRECTORY}/teshsuite/mc/dwarf_expression dwarf_expression.tesh)
set(MC_SRC
src/mc/mc_checkpoint.c
+ src/mc/mc_page_store.cpp
+ src/mc/mc_page_snapshot.cpp
src/mc/mc_comm_determinism.c
src/mc/mc_compare.c
src/mc/mc_diff.c
add_subdirectory(${CMAKE_HOME_DIRECTORY}/examples/xbt)
+add_subdirectory(${CMAKE_HOME_DIRECTORY}/teshsuite/mc)
add_subdirectory(${CMAKE_HOME_DIRECTORY}/teshsuite/mc/dwarf)
add_subdirectory(${CMAKE_HOME_DIRECTORY}/teshsuite/mc/dwarf_expression)
/** Cache the size of a memory page for the current system. */
XBT_PUBLIC_DATA(int) xbt_pagesize;
+/** Cache the number of bits of addresses inside a given page, log2(xbt_pagesize). */
+ XBT_PUBLIC_DATA(int) xbt_pagebits;
+
XBT_PUBLIC(const char *) xbt_procname(void);
#define XBT_BACKTRACE_SIZE 10 /* FIXME: better place? Do document */
*/
#define xbt_die(...) \
do { \
- XBT_LOG_EXTERNAL_CATEGORY(xbt); \
XBT_CCRITICAL(xbt, __VA_ARGS__); \
xbt_abort(); \
} while (0)
/** @} */
+XBT_LOG_EXTERNAL_CATEGORY(xbt);
+
/* these ones live in str.h, but redeclare them here so that we do
not need to load the whole str.h and its heavy dependencies */
#ifndef __USE_GNU /* do not redeclare existing headers */
/********************************** Configuration of MC **************************************/
extern int _sg_do_model_check;
extern int _sg_mc_checkpoint;
+extern int _sg_mc_sparse_checkpoint;
extern char* _sg_mc_property_file;
extern int _sg_mc_timeout;
extern int _sg_mc_hash;
/********************************* Global *************************************/
void _mc_cfg_cb_reduce(const char *name, int pos);
void _mc_cfg_cb_checkpoint(const char *name, int pos);
+void _mc_cfg_cb_sparse_checkpoint(const char *name, int pos);
void _mc_cfg_cb_property(const char *name, int pos);
void _mc_cfg_cb_timeout(const char *name, int pos);
void _mc_cfg_cb_hash(const char *name, int pos);
#include "xbt/module.h"
#include <xbt/mmalloc.h>
#include "../smpi/private.h"
+#include <alloca.h>
#include "xbt/mmalloc/mmprivate.h"
#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");
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;
}
snapshot->privatization_regions =
xbt_new(mc_mem_region_t, SIMIX_process_count());
for (i = 0; i < SIMIX_process_count(); i++) {
+ // TODO, add support for sparse snapshot
snapshot->privatization_regions[i] =
- MC_region_new(-1, mappings[i], size_data_exe);
+ MC_region_new(-1, mappings[i], size_data_exe, NULL);
}
snapshot->privatization_index = loaded_page;
}
}
}
+/** @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)
{
/* Save the std heap and the writable mapped pages of libsimgrid and binary */
MC_get_memory_regions(snapshot);
+ if (_sg_mc_sparse_checkpoint) {
+ mc_softdirty_reset();
+ }
snapshot->to_ignore = MC_take_snapshot_ignore();
snapshot->hash = 0;
}
- // 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);
}
MC_snapshot_ignore_restore(snapshot);
+ if (_sg_mc_sparse_checkpoint) {
+ mc_softdirty_reset();
+ }
+ mc_model_checker->parent_snapshot = snapshot;
}
void *mc_translate_address(uintptr_t addr, mc_snapshot_t snapshot)
int _sg_do_model_check = 0;
int _sg_mc_checkpoint = 0;
+int _sg_mc_sparse_checkpoint = 0;
char *_sg_mc_property_file = NULL;
int _sg_mc_timeout = 0;
int _sg_mc_hash = 0;
_sg_mc_checkpoint = xbt_cfg_get_int(_sg_cfg_set, name);
}
+void _mc_cfg_cb_sparse_checkpoint(const char *name, int pos) {
+ if (_sg_cfg_init_status && !_sg_do_model_check) {
+ xbt_die("You are specifying a checkpointing value after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
+ }
+ _sg_mc_sparse_checkpoint = xbt_cfg_get_int(_sg_cfg_set, name);
+}
+
void _mc_cfg_cb_property(const char *name, int pos)
{
if (_sg_cfg_init_status && !_sg_do_model_check) {
}
+mc_model_checker_t mc_model_checker = NULL;
+
void MC_init()
{
-
int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
mc_time = xbt_new0(double, simix_process_maxpid);
MC_SET_MC_HEAP;
+ mc_model_checker = xbt_new0(s_mc_model_checker_t, 1);
+ mc_model_checker->pages = mc_pages_store_new();
+ mc_model_checker->fd_clear_refs = -1;
+ mc_model_checker->fd_pagemap = -1;
+
mc_comp_times = xbt_new0(s_mc_comparison_times_t, 1);
/* Initialize statistics */
MC_ignore_local_variable("ctx", "*");
MC_ignore_local_variable("self", "simcall_BODY_mc_snapshot");
- MC_ignore_local_variable("next_context", "smx_ctx_sysv_suspend_serial");
+ MC_ignore_local_variable("next_cont"
+ "ext", "smx_ctx_sysv_suspend_serial");
MC_ignore_local_variable("i", "smx_ctx_sysv_suspend_serial");
/* Ignore local variable about time used for tracing */
MC_ignore_local_variable("start_time", "*");
+ MC_ignore_global_variable("mc_model_checker");
+
+ // Mot of those things could be moved into mc_model_checker:
MC_ignore_global_variable("compared_pointers");
MC_ignore_global_variable("mc_comp_times");
MC_ignore_global_variable("mc_snapshot_comparison_time");
MC_ignore_global_variable("maestro_stack_end");
MC_ignore_global_variable("smx_total_comms");
+
MC_ignore_heap(mc_time, simix_process_maxpid * sizeof(double));
smx_process_t process;
--- /dev/null
+/* 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. */
+
+#ifndef MC_MMU_H
+#define MC_MMU_H
+
+#include <stdint.h>
+
+#include "mc_private.h"
+
+/** @brief How many memory pages are necessary to store size bytes?
+ *
+ * @param size Byte size
+ * @return Number of memory pages
+ */
+static inline size_t mc_page_count(size_t size)
+{
+ size_t page_count = size >> xbt_pagebits;
+ if (size & (xbt_pagesize-1)) {
+ page_count ++;
+ }
+ return page_count;
+}
+
+/** @brief Get the virtual memory page number of a given address
+ *
+ * @param address Address
+ * @return Virtual memory page number of the given address
+ */
+static inline size_t mc_page_number(void* address)
+{
+ return ((uintptr_t) address) >> xbt_pagebits;
+}
+
+/** @brief Get the offset of an address within a memory page
+ *
+ * @param address Address
+ * @return Offset within the memory page
+ */
+static inline size_t mc_page_offset(void* address)
+{
+ return ((uintptr_t) address) & (xbt_pagesize-1);
+}
+
+/** @brief Get the virtual address of a virtual memory page
+ *
+ * @param base Address of the first page
+ * @param page Index of the page
+ */
+static inline void* mc_page_from_number(void* base, size_t page)
+{
+ return (void*) ((char*)base + (page << xbt_pagebits));
+}
+
+#endif
--- /dev/null
+#include "mc_page_store.h"
+#include "mc_mmu.h"
+
+#define SOFT_DIRTY_BIT_NUMBER 55
+#define SOFT_DIRTY (((uint64_t)1) << SOFT_DIRTY_BIT_NUMBER)
+
+extern "C" {
+
+// ***** Region management:
+
+size_t* mc_take_page_snapshot_region(void* data, size_t page_count, uint64_t* pagemap, size_t* reference_pages)
+{
+ size_t* pagenos = (size_t*) malloc(page_count * sizeof(size_t));
+
+ for (size_t i=0; i!=page_count; ++i) {
+ if (pagemap && (pagemap[i] & SOFT_DIRTY)) {
+ // The page is softclean, it is the same page as the reference page:
+ pagenos[i] = reference_pages[i];
+ mc_model_checker->pages->ref_page(reference_pages[i]);
+ } else {
+ // Otherwise, we need to store the page the hard hard
+ // (by reading its content):
+ void* page = (char*) data + (i << xbt_pagebits);
+ pagenos[i] = mc_model_checker->pages->store_page(page);
+ }
+ }
+
+ return pagenos;
+}
+
+void mc_free_page_snapshot_region(size_t* pagenos, size_t page_count)
+{
+ for (size_t i=0; i!=page_count; ++i) {
+ mc_model_checker->pages->unref_page(pagenos[i]);
+ }
+}
+
+void mc_restore_page_snapshot_region(mc_mem_region_t region, size_t page_count, uint64_t* pagemap, mc_mem_region_t reference_region)
+{
+ for (size_t i=0; i!=page_count; ++i) {
+
+ bool softclean = pagemap && !(pagemap[i] & SOFT_DIRTY);
+ if (softclean && reference_region && reference_region->page_numbers[i] == region->page_numbers[i]) {
+ // The page is softclean and is the same as the reference one:
+ // the page is already in the target state.
+ continue;
+ }
+
+ // Otherwise, copy the page:
+ void* target_page = mc_page_from_number(region->start_addr, i);
+ const void* source_page = mc_model_checker->pages->get_page(region->page_numbers[i]);
+ memcpy(target_page, source_page, xbt_pagesize);
+ }
+}
+
+// ***** Soft dirty tracking
+
+/** @brief Like pread() but without partial reads */
+static size_t pread_whole(int fd, void* buf, size_t count, off_t offset) {
+ size_t res;
+
+ char* data = (char*) buf;
+ while(count) {
+ ssize_t n = pread(fd, buf, count, offset);
+ // EOF
+ if (n==0)
+ return res;
+
+ // Error (or EAGAIN):
+ if (n==-1) {
+ if (errno == EAGAIN)
+ continue;
+ else
+ return -1;
+ }
+
+ count -= n;
+ data += n;
+ offset += n;
+ res += n;
+ }
+
+ return res;
+}
+
+static inline void mc_ensure_fd(int* fd, const char* path, int flags) {
+ if (*fd != -1)
+ return;
+ *fd = open(path, flags);
+ if (*fd == -1) {
+ xbt_die("Could not open file %s", path);
+ }
+}
+
+/** @brief Reset the softdirty bits
+ *
+ * This is done after checkpointing and after checkpoint restoration
+ * (if per page checkpoiting is used) in order to know which pages were
+ * modified.
+ * */
+void mc_softdirty_reset() {
+ mc_ensure_fd(&mc_model_checker->fd_clear_refs, "/proc/self/clear_refs", O_WRONLY|O_CLOEXEC);
+ if( ::write(mc_model_checker->fd_clear_refs, "4\n", 2) != 2) {
+ xbt_die("Could not reset softdirty bits");
+ }
+}
+
+/** @brief Read /proc/self/pagemap informations in order to find properties on the pages
+ *
+ * For each virtual memory page, this file provides informations.
+ * We are interested in the soft-dirty bit: with this we can track which
+ * pages were modified between snapshots/restorations and avoid
+ * copying data which was not modified.
+ *
+ * @param pagemap Output buffer for pagemap informations
+ * @param start_addr Address of the first page
+ * @param page_count Number of pages
+ */
+static void mc_read_pagemap(uint64_t* pagemap, size_t page_start, size_t page_count)
+{
+ mc_ensure_fd(&mc_model_checker->fd_pagemap, "/proc/self/pagemap", O_RDONLY|O_CLOEXEC);
+ size_t bytesize = sizeof(uint64_t) * page_count;
+ off_t offset = sizeof(uint64_t) * page_start;
+ if (pread_whole(mc_model_checker->fd_pagemap, pagemap, bytesize, offset) != bytesize) {
+ xbt_die("Coult not read pagemap");
+ }
+}
+
+// ***** High level API
+
+mc_mem_region_t mc_region_new_sparse(int type, void *start_addr, size_t size, mc_mem_region_t 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->page_numbers = NULL;
+
+ xbt_assert((((uintptr_t)start_addr) & (xbt_pagesize-1)) == 0,
+ "Not at the beginning of a page");
+ size_t page_count = mc_page_count(size);
+
+ 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);
+ }
+
+ // Take incremental snapshot:
+ new_reg->page_numbers = mc_take_page_snapshot_region(start_addr, page_count, pagemap, ref_reg->page_numbers);
+
+ return new_reg;
+}
+
+void mc_region_restore_sparse(mc_mem_region_t reg, mc_mem_region_t ref_reg)
+{
+ xbt_assert((((uintptr_t)reg->start_addr) & (xbt_pagesize-1)) == 0,
+ "Not at the beginning of a page");
+ size_t page_count = mc_page_count(reg->size);
+
+ uint64_t* pagemap = NULL;
+
+ // 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);
+ }
+
+ // Incremental per-page snapshot restoration:
+ mc_restore_page_snapshot_region(reg, page_count, pagemap, ref_reg);
+}
+
+}
--- /dev/null
+/* 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 <unistd.h>
+#include <string.h> // memcpy, memcp
+
+#include <boost/foreach.hpp>
+
+#include <xbt.h>
+
+#include "mc_page_store.h"
+
+#include "mc_mmu.h"
+
+XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_page_snapshot, mc,
+ "Logging specific to mc_page_snapshot");
+
+extern "C" {
+
+static void mc_read_pagemap(uint64_t* pagemap, size_t page_start, size_t page_count);
+
+}
+
+// ***** Utility:
+
+/** @brief Compte a hash for the given memory page
+ *
+ * The page is used before inserting the page in the page store
+ * in order to find duplicate of this pae in the page store.
+ *
+ * @param data Memory page
+ * @return hash off the page
+ */
+static inline uint64_t mc_hash_page(const void* data)
+{
+ const uint64_t* values = (const uint64_t*) data;
+ size_t n = xbt_pagesize / sizeof(uint64_t);
+
+ // This djb2:
+ uint64_t hash = 5381;
+ for (size_t i=0; i!=n; ++i) {
+ hash = ((hash << 5) + hash) + values[i];
+ }
+ return hash;
+}
+
+// ***** snapshot_page_manager
+
+s_mc_pages_store::s_mc_pages_store(size_t size) :
+ memory_(NULL), capacity_(0), top_index_(0)
+{
+ // Using mmap in order to be able to expand the region
+ // by relocating it somewhere else in the virtual memory
+ // space:
+ void * memory = ::mmap(NULL, size << xbt_pagebits, PROT_READ|PROT_WRITE, MAP_SHARED|MAP_ANONYMOUS|MAP_POPULATE, -1, 0);
+ if (memory==MAP_FAILED) {
+ xbt_die("Could not mmap initial snapshot pages.");
+ }
+
+ this->top_index_ = 0;
+ this->capacity_ = size;
+ this->memory_ = memory;
+ this->page_counts_.resize(size);
+}
+
+s_mc_pages_store::~s_mc_pages_store()
+{
+ ::munmap(this->memory_, this->capacity_ << xbt_pagebits);
+}
+
+void s_mc_pages_store::resize(size_t size)
+{
+ size_t new_bytesize = size << xbt_pagebits;
+
+ // Expand the memory region by moving it into another
+ // virtual memory address if necessary:
+ void* new_memory = mremap(this->memory_, this->capacity_ << xbt_pagesize, new_bytesize, MREMAP_MAYMOVE);
+ if (new_memory == MAP_FAILED) {
+ xbt_die("Could not mremap snapshot pages.");
+ }
+
+ this->capacity_ = size;
+ this->memory_ = new_memory;
+ this->page_counts_.resize(size);
+}
+
+/** Allocate a free page
+ *
+ * @return index of the free page
+ */
+size_t s_mc_pages_store::alloc_page()
+{
+ if (this->free_pages_.empty()) {
+
+ // Expand the region:
+ if (top_index_ == this->capacity_) {
+ // All the pages are allocated, we need add more pages:
+ this->resize(2 * this->capacity_);
+ }
+
+ // Use a page from the top:
+ return this->top_index_++;
+
+ } else {
+
+ // Use a page from free_pages_ (inside of the region):
+ size_t res = this->free_pages_[this->free_pages_.size() - 1];
+ this->free_pages_.pop_back();
+ return res;
+
+ }
+}
+
+void s_mc_pages_store::remove_page(size_t pageno)
+{
+ this->free_pages_.push_back(pageno);
+ void* page = mc_page_from_number(this->memory_, pageno);
+ uint64_t hash = mc_hash_page(page);
+ this->hash_index_[hash].erase(pageno);
+}
+
+/** Store a page in memory */
+size_t s_mc_pages_store::store_page(void* page)
+{
+ xbt_assert(mc_page_offset(page)==0, "Not at the beginning of a page");
+ xbt_assert(top_index_ <= this->capacity_, "top_index is not consistent");
+
+ // Search the page in the snapshot pages:
+ uint64_t hash = mc_hash_page(page);
+ page_set_type& page_set = this->hash_index_[hash];
+ BOOST_FOREACH (size_t pageno, page_set) {
+ const void* snapshot_page = this->get_page(pageno);
+ if (memcmp(page, snapshot_page, xbt_pagesize) == 0) {
+ // Page found, reuse it:
+ page_counts_[pageno]++;
+ return pageno;
+ }
+ }
+
+ // Allocate a new page for this page:
+ size_t pageno = alloc_page();
+ void* snapshot_page = (void*) this->get_page(pageno);
+ memcpy(snapshot_page, page, xbt_pagesize);
+ page_set.insert(pageno);
+ page_counts_[pageno]++;
+ return pageno;
+}
+
+// ***** Main C API
+
+extern "C" {
+
+mc_pages_store_t mc_pages_store_new()
+{
+ return new s_mc_pages_store_t(500);
+}
+
+}
--- /dev/null
+/* 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 <stdint.h>
+
+#include <vector>
+
+#include <boost/utility.hpp>
+#include <boost/unordered_map.hpp>
+#include <boost/unordered_set.hpp>
+
+#include <xbt.h>
+
+#include "mc_private.h"
+#include "mc_mmu.h"
+
+#ifndef MC_PAGE_SNAPSHOT_H
+#define MC_PAGE_SNAPSHOT_H
+
+/** @brief Manager for snapshot pages
+ *
+ * Page management: the free pages are stored as a simple linked-list.
+ * The number of the first page if stored in `free_pages`.
+ * Each free page store the number of the next free page.
+ */
+struct s_mc_pages_store {
+private: // Types
+ typedef uint64_t hash_type;
+ typedef boost ::unordered_set<size_t> page_set_type;
+ typedef boost::unordered_map<hash_type, page_set_type> pages_map_type;
+
+private: // Fields:
+ /** First page */
+ void* memory_;
+ /** Number of available pages in virtual memory */
+ size_t capacity_;
+ /** Top of the used pages (index of the next available page) */
+ size_t top_index_;
+ /** Page reference count */
+ std::vector<uint64_t> page_counts_;
+ /** Index of available pages before the top */
+ std::vector<size_t> free_pages_;
+ /** Index from page hash to page index */
+ pages_map_type hash_index_;
+
+private: // Methods
+ void resize(size_t size);
+ size_t alloc_page();
+ void remove_page(size_t pageno);
+
+public: // Constructors
+ explicit s_mc_pages_store(size_t size);
+ ~s_mc_pages_store();
+
+public: // Methods
+
+ /** @brief Decrement the refcount for a given page */
+ void unref_page(size_t pageno) {
+ if ((--this->page_counts_[pageno]) == 0) {
+ this->remove_page(pageno);
+ }
+ }
+
+ /** @brief Increment the refcount for a given page */
+ void ref_page(size_t pageno) {
+ ++this->page_counts_[pageno];
+ }
+
+ /** @brief Store a page
+ *
+ * Either allocate a new page in the store or reuse
+ * a shared page if is is already in the page store.
+ */
+ size_t store_page(void* page);
+
+ /** @brief Get a page from its page number
+ *
+ * @param Number of the memory page in the store
+ * @return Start of the page
+ */
+ const void* get_page(size_t pageno) const {
+ return mc_page_from_number(this->memory_, pageno);
+ }
+
+public: // Debug/test methods
+
+ /** @brief Get the number of references for a page */
+ size_t get_ref(size_t pageno) {
+ return this->page_counts_[pageno];
+ }
+
+ /** @brief Get the number of used pages */
+ size_t size() {
+ return this->top_index_ - this->free_pages_.size();
+ }
+
+ /** @brief Get the capacity of the page store
+ *
+ * The capacity is expanded by a system call (mremap).
+ * */
+ size_t capacity() {
+ return this->capacity_;
+ }
+
+};
+
+#endif
+
void *data;
// Size of the data region:
size_t size;
+ // For per-page snapshots, this is an array to the number of
+ size_t* page_numbers;
} s_mc_mem_region_t, *mc_mem_region_t;
/** Ignored data
size_t size;
}s_mc_checkpoint_ignore_region_t, *mc_checkpoint_ignore_region_t;
+SG_BEGIN_DECL()
+
inline static void* mc_snapshot_get_heap_end(mc_snapshot_t snapshot) {
if(snapshot==NULL)
xbt_die("snapshot is NULL");
void MC_restore_snapshot(mc_snapshot_t);
void MC_free_snapshot(mc_snapshot_t);
+int mc_important_snapshot(mc_snapshot_t snapshot);
+
+size_t* mc_take_page_snapshot_region(void* data, size_t page_count, uint64_t* pagemap, size_t* reference_pages);
+void mc_free_page_snapshot_region(size_t* pagenos, size_t page_count);
+void mc_restore_page_snapshot_region(mc_mem_region_t region, size_t page_count, uint64_t* pagemap, mc_mem_region_t reference_region);
+
+mc_mem_region_t mc_region_new_sparse(int type, void *start_addr, size_t size, mc_mem_region_t ref_reg);
+void mc_region_restore_sparse(mc_mem_region_t reg, mc_mem_region_t ref_reg);
+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();
+
+/** @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
+ * variable prevents some sharing between snapshots and must be ignored.
+ * By moving as much state as possible in this structure allocated
+ * on the model-chercker heap, we avoid those issues.
+ */
+typedef struct s_mc_model_checker {
+ // This is the parent snapshot of the current state:
+ mc_snapshot_t parent_snapshot;
+ mc_pages_store_t pages;
+ int fd_clear_refs;
+ int fd_pagemap;
+} s_mc_model_checker_t, *mc_model_checker_t;
+
+extern mc_model_checker_t mc_model_checker;
+
/** \brief Translate a pointer from process address space to snapshot address space
*
* The address space contains snapshot of the main/application memory:
* */
uint64_t mc_hash_processes_state(int num_state, xbt_dynar_t stacks);
+SG_END_DECL()
+
#endif
int min2 = mc_stats->expanded_states;
unsigned int cursor2 = 0;
unsigned int index2 = 0;
- xbt_dynar_foreach(visited_states, cursor2, state_test) {
- if (state_test->num < min2) {
+ xbt_dynar_foreach(visited_states, cursor2, state_test){
+ if (!mc_important_snapshot(state_test->system_state) && state_test->num < min2) {
index2 = cursor2;
min2 = state_test->num;
}
unsigned int cursor2 = 0;
unsigned int index2 = 0;
xbt_dynar_foreach(visited_pairs, cursor2, pair_test) {
- if (pair_test->num < min2) {
+ if (!mc_important_snapshot(pair_test->graph_state->system_state) && pair_test->num < min2) {
index2 = cursor2;
min2 = pair_test->num;
}
int _sg_do_clean_atexit = 1;
int xbt_pagesize;
+int xbt_pagebits = 0;
/* Declare xbt_preinit and xbt_postexit as constructor/destructor of the library.
* This is crude and rather compiler-specific, unfortunately.
GetSystemInfo(&si);
xbt_pagesize = si.dwPageSize;
#endif
+
+ xbt_pagebits = 0;
+ int x = xbt_pagesize;
+ while(x >>= 1) {
+ ++xbt_pagebits;
+ }
+
#ifdef MMALLOC_WANT_OVERRIDE_LEGACY
mmalloc_preinit();
#endif
#ifndef _WIN32
srand48(seed);
#endif
-
atexit(xbt_postexit);
}
--- /dev/null
+cmake_minimum_required(VERSION 2.6)
+
+if(HAVE_MC)
+ set(EXECUTABLE_OUTPUT_PATH "${CMAKE_CURRENT_BINARY_DIR}")
+
+ add_executable(page_store page_store.cpp)
+ target_link_libraries(page_store simgrid)
+endif()
+
+set(tesh_files
+ ${tesh_files}
+ ${CMAKE_CURRENT_SOURCE_DIR}/page_store.tesh
+ PARENT_SCOPE
+ )
+set(testsuite_src
+ ${testsuite_src}
+ ${CMAKE_CURRENT_SOURCE_DIR}/page_store.cpp
+ PARENT_SCOPE
+ )
--- /dev/null
+#include <string.h>
+#include <stdlib.h>
+#include <stdint.h>
+#include <unistd.h>
+#include <sys/mman.h>
+
+#include "mc/mc_page_store.h"
+
+static int value = 0;
+
+static void new_content(void* data, size_t size)
+{
+ memset(data, ++value, size);
+}
+
+static void* getpage()
+{
+ return mmap(NULL, getpagesize(), PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0);
+}
+
+int main(int argc, char** argv)
+{
+ // Init
+ size_t pagesize = (size_t) getpagesize();
+ mc_pages_store_t store = new s_mc_pages_store(500);
+ void* data = getpage();
+
+ // Init:
+ xbt_assert(store->size()==0, "Bad size");
+
+ // Store the page once:
+ new_content(data, pagesize);
+ size_t pageno1 = store->store_page(data);
+ xbt_assert(store->get_ref(pageno1)==1, "Bad refcount");
+ const void* copy = store->get_page(pageno1);
+ xbt_assert(memcmp(data, copy, pagesize)==0, "Page data should be the same");
+ xbt_assert(store->size()==1, "Bad size");
+
+ // Store the same page again:
+ size_t pageno2 = store->store_page(data);
+ xbt_assert(pageno1==pageno2, "Page should be the same");
+ xbt_assert(store->get_ref(pageno1)==2, "Bad refcount");
+ xbt_assert(store->size()==1, "Bad size");
+
+ // Store a new page:
+ new_content(data, pagesize);
+ size_t pageno3 = store->store_page(data);
+ xbt_assert(pageno1 != pageno3, "New page should be different");
+ xbt_assert(store->size()==2, "Bad size");
+
+ // Unref pages:
+ store->unref_page(pageno1);
+ xbt_assert(store->get_ref(pageno1)==1, "Bad refcount");
+ xbt_assert(store->size()==2, "Bad size");
+ store->unref_page(pageno2);
+ xbt_assert(store->size()==1, "Bad size");
+
+ // Reallocate page:
+ new_content(data, pagesize);
+ size_t pageno4 = store->store_page(data);
+ xbt_assert(pageno1 == pageno4, "Page was not reused");
+ xbt_assert(store->get_ref(pageno4)==1, "Bad refcount");
+ xbt_assert(store->size()==2, "Bad size");
+
+ return 0;
+}
--- /dev/null
+#! ./tesh
+
+$ $SG_TEST_EXENV ${bindir:=.}/page_store
