It generates a lot of page faults and is slow.
extern int _sg_do_model_check_record;
extern int _sg_mc_checkpoint;
extern int _sg_mc_sparse_checkpoint;
-extern int _sg_mc_soft_dirty;
extern char* _sg_mc_property_file;
extern int _sg_mc_timeout;
extern int _sg_mc_hash;
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_soft_dirty(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);
static mc_mem_region_t mc_region_new_dense(
mc_region_type_t region_type,
- void *start_addr, void* permanent_addr, size_t size, mc_mem_region_t ref_reg)
+ void *start_addr, void* permanent_addr, size_t size)
{
mc_mem_region_t region = xbt_new(s_mc_mem_region_t, 1);
region->region_type = region_type;
* @param start_addr Address of the region in the simulated process
* @param permanent_addr Permanent address of this data (for privatized variables, this is the virtual address of the privatized mapping)
* @param size Size of the data*
- * @param ref_reg Reference corresponding region
*/
-static mc_mem_region_t MC_region_new(mc_region_type_t type, void *start_addr, void* permanent_addr, size_t size, mc_mem_region_t ref_reg)
+static mc_mem_region_t MC_region_new(
+ mc_region_type_t type, void *start_addr, void* permanent_addr, size_t size)
{
if (_sg_mc_sparse_checkpoint) {
- return mc_region_new_sparse(type, start_addr, permanent_addr, size, ref_reg);
+ return mc_region_new_sparse(type, start_addr, permanent_addr, size);
} else {
- return mc_region_new_dense(type, start_addr, permanent_addr, size, ref_reg);
+ return mc_region_new_dense(type, start_addr, permanent_addr, size);
}
}
/** @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 region, mc_mem_region_t ref_region)
+static void MC_region_restore(mc_mem_region_t region)
{
switch(region->storage_type) {
case MC_REGION_STORAGE_TYPE_NONE:
break;
case MC_REGION_STORAGE_TYPE_CHUNKED:
- mc_region_restore_sparse(&mc_model_checker->process, region, ref_region);
+ mc_region_restore_sparse(&mc_model_checker->process, region);
break;
case MC_REGION_STORAGE_TYPE_PRIVATIZED:
{
- bool has_ref_regions = ref_region &&
- ref_region->storage_type == MC_REGION_STORAGE_TYPE_PRIVATIZED;
size_t process_count = region->privatized.regions_count;
for (size_t i = 0; i < process_count; i++) {
- MC_region_restore(region->privatized.regions[i],
- has_ref_regions ? ref_region->privatized.regions[i] : NULL);
+ MC_region_restore(region->privatized.regions[i]);
}
break;
}
}
static mc_mem_region_t MC_region_new_privatized(
- mc_region_type_t region_type, void *start_addr, void* permanent_addr, size_t size,
- mc_mem_region_t ref_reg)
+ mc_region_type_t region_type, void *start_addr, void* permanent_addr, size_t size
+ )
{
size_t process_count = MC_smpi_process_count();
mc_mem_region_t region = xbt_new(s_mc_mem_region_t, 1);
remote_smpi_privatisation_regions, sizeof(privatisation_regions));
for (size_t i = 0; i < process_count; i++) {
- mc_mem_region_t ref_subreg = NULL;
- if (ref_reg && ref_reg->storage_type == MC_REGION_STORAGE_TYPE_PRIVATIZED)
- ref_subreg = ref_reg->privatized.regions[i];
region->privatized.regions[i] =
MC_region_new(region_type, start_addr,
- privatisation_regions[i].address, size,
- ref_subreg);
+ privatisation_regions[i].address, size);
}
return region;
else if (type == MC_REGION_TYPE_HEAP)
xbt_assert(!object_info, "Unexpected object info for heap region.");
- mc_mem_region_t ref_reg = NULL;
- if (mc_model_checker->parent_snapshot)
- ref_reg = mc_model_checker->parent_snapshot->snapshot_regions[index];
-
mc_mem_region_t region;
const bool privatization_aware = MC_object_info_is_privatized(object_info);
if (privatization_aware && MC_smpi_process_count())
- region = MC_region_new_privatized(type, start_addr, permanent_addr, size, ref_reg);
+ region = MC_region_new_privatized(type, start_addr, permanent_addr, size);
else
- region = MC_region_new(type, start_addr, permanent_addr, size, ref_reg);
+ region = MC_region_new(type, start_addr, permanent_addr, size);
region->object_info = object_info;
snapshot->snapshot_regions[index] = region;
if (_sg_mc_snapshot_fds)
MC_get_current_fd(snapshot);
- const bool use_soft_dirty = _sg_mc_sparse_checkpoint
- && _sg_mc_soft_dirty
- && MC_process_is_self(mc_process);
-
/* Save the std heap and the writable mapped pages of libsimgrid and binary */
MC_get_memory_regions(mc_process, snapshot);
- if (use_soft_dirty)
- mc_softdirty_reset();
snapshot->to_ignore = MC_take_snapshot_ignore();
}
MC_snapshot_ignore_restore(snapshot);
- if (use_soft_dirty)
- mc_model_checker->parent_snapshot = snapshot;
return snapshot;
}
static inline
void MC_restore_snapshot_regions(mc_snapshot_t snapshot)
{
- mc_snapshot_t parent_snapshot = mc_model_checker->parent_snapshot;
-
const size_t n = snapshot->snapshot_regions_count;
for (size_t i = 0; i < n; i++) {
// For privatized, variables we decided it was not necessary to take the snapshot:
if (snapshot->snapshot_regions[i])
- MC_region_restore(snapshot->snapshot_regions[i],
- parent_snapshot ? parent_snapshot->snapshot_regions[i] : NULL);
+ MC_region_restore(snapshot->snapshot_regions[i]);
}
#ifdef HAVE_SMPI
void MC_restore_snapshot(mc_snapshot_t snapshot)
{
XBT_DEBUG("Restore snapshot %i", snapshot->num_state);
-
- const bool use_soft_dirty = _sg_mc_sparse_checkpoint
- && _sg_mc_soft_dirty
- && MC_process_is_self(&mc_model_checker->process);
-
MC_restore_snapshot_regions(snapshot);
if (_sg_mc_snapshot_fds)
MC_restore_snapshot_fds(snapshot);
- if (use_soft_dirty) {
- mc_softdirty_reset();
- }
MC_snapshot_ignore_restore(snapshot);
- if (use_soft_dirty) {
- mc_model_checker->parent_snapshot = snapshot;
- }
-
mc_model_checker->process.cache_flags = 0;
}
int _sg_do_model_check_record = 0;
int _sg_mc_checkpoint = 0;
int _sg_mc_sparse_checkpoint = 0;
-int _sg_mc_soft_dirty = 0;
char *_sg_mc_property_file = NULL;
int _sg_mc_hash = 0;
int _sg_mc_max_depth = 1000;
_sg_mc_sparse_checkpoint = xbt_cfg_get_boolean(_sg_cfg_set, name);
}
-void _mc_cfg_cb_soft_dirty(const char *name, int pos) {
- if (_sg_cfg_init_status && !_sg_do_model_check) {
- xbt_die("You are specifying a soft dirty 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_soft_dirty = xbt_cfg_get_boolean(_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 = xbt_new0(s_mc_model_checker_t, 1);
mc->pages = mc_pages_store_new();
mc->fd_clear_refs = -1;
- mc->fd_pagemap = -1;
MC_process_init(&mc->process, pid, socket);
mc->hosts = xbt_dict_new();
return mc;
mc_snapshot_t parent_snapshot;
mc_pages_store_t pages;
int fd_clear_refs;
- int fd_pagemap;
xbt_dynar_t record;
s_mc_process_t process;
/** String pool for host names */
#include <xbt/mmalloc.h>
-#define SOFT_DIRTY_BIT_NUMBER 55
-#define SOFT_DIRTY (((uint64_t)1) << SOFT_DIRTY_BIT_NUMBER)
-
extern "C" {
// ***** Region management:
*
* @param data The start of the region (must be at the beginning of a page)
* @param pag_count Number of pages of the region
- * @param pagemap Linux kernel pagemap values fot this region (or NULL)
- * @param reference_pages Snapshot page numbers of the previous soft_dirty_reset (or NULL)
* @return Snapshot page numbers of this new snapshot
*/
size_t* mc_take_page_snapshot_region(mc_process_t process,
- void* data, size_t page_count, uint64_t* pagemap, size_t* reference_pages)
+ void* data, size_t page_count)
{
size_t* pagenos = (size_t*) malloc(page_count * sizeof(size_t));
temp = malloc(xbt_pagesize);
for (size_t i=0; i!=page_count; ++i) {
- bool softclean = pagemap && !(pagemap[i] & SOFT_DIRTY);
- if (softclean && reference_pages) {
- // 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 way
// (by reading its content):
void* page = (char*) data + (i << xbt_pagebits);
temp, page, xbt_pagesize, MC_PROCESS_INDEX_DISABLED);
}
pagenos[i] = mc_model_checker->pages->store_page(page_data);
- }
+
}
free(temp);
* @param start_addr
* @param page_count Number of pages of the region
* @param pagenos
- * @param pagemap Linux kernel pagemap values fot this region (or NULL)
- * @param reference_pages Snapshot page numbers of the previous soft_dirty_reset (or NULL)
*/
void mc_restore_page_snapshot_region(mc_process_t process,
- void* start_addr, size_t page_count, size_t* pagenos, uint64_t* pagemap, size_t* reference_pagenos)
+ void* start_addr, size_t page_count, size_t* pagenos)
{
for (size_t i=0; i!=page_count; ++i) {
-
- bool softclean = pagemap && !(pagemap[i] & SOFT_DIRTY);
- if (softclean && reference_pagenos && pagenos[i] == reference_pagenos[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(start_addr, i);
const void* source_page = mc_model_checker->pages->get_page(pagenos[i]);
}
}
-// ***** 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 = 0;
-
- char* data = (char*) buf;
- while(count) {
- ssize_t n = pread(fd, buf, count, offset);
- // EOF
- if (n==0)
- return res;
-
- // Error (or EINTR):
- if (n==-1) {
- if (errno == EINTR)
- continue;
- else
- return -1;
- }
-
- // It might be a partial read:
- count -= n;
- data += n;
- offset += n;
- res += n;
- }
-
- return res;
-}
-
-static inline __attribute__ ((always_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 soft-dirty bits
- *
- * This is done after checkpointing and after checkpoint restoration
- * (if per page checkpoiting is used) in order to know which pages were
- * modified.
- *
- * See https://www.kernel.org/doc/Documentation/vm/soft-dirty.txt
- * */
-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 memory page informations
- *
- * For each virtual memory page of the process,
- * /proc/self/pagemap provides a 64 bit field of information.
- * 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.
- *
- * See https://www.kernel.org/doc/Documentation/vm/pagemap.txt
- *
- * @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("Could not read pagemap");
- }
-}
-
// ***** High level API
mc_mem_region_t mc_region_new_sparse(mc_region_type_t region_type,
- void *start_addr, void* permanent_addr, size_t size,
- mc_mem_region_t ref_reg)
+ void *start_addr, void* permanent_addr, size_t size)
{
mc_process_t process = &mc_model_checker->process;
"Not at the beginning of a page");
size_t page_count = mc_page_count(size);
- uint64_t* pagemap = NULL;
- if (_sg_mc_soft_dirty && mc_model_checker->parent_snapshot &&
- MC_process_is_self(process)) {
- pagemap = (uint64_t*) malloc_no_memset(sizeof(uint64_t) * page_count);
- mc_read_pagemap(pagemap, mc_page_number(NULL, permanent_addr), page_count);
- }
-
- size_t* reg_page_numbers = NULL;
- if (ref_reg!=NULL && ref_reg->storage_type == MC_REGION_STORAGE_TYPE_CHUNKED)
- reg_page_numbers = ref_reg->chunked.page_numbers;
-
// Take incremental snapshot:
region->chunked.page_numbers = mc_take_page_snapshot_region(process,
- permanent_addr, page_count, pagemap, reg_page_numbers);
+ permanent_addr, page_count);
- if(pagemap) {
- mfree(mc_heap, pagemap);
- }
return region;
}
-void mc_region_restore_sparse(mc_process_t process, mc_mem_region_t reg, mc_mem_region_t ref_reg)
+void mc_region_restore_sparse(mc_process_t process, mc_mem_region_t reg)
{
xbt_assert((((uintptr_t)reg->permanent_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 (_sg_mc_soft_dirty && mc_model_checker->parent_snapshot
- && MC_process_is_self(process)) {
- pagemap = (uint64_t*) malloc_no_memset(sizeof(uint64_t) * page_count);
- mc_read_pagemap(pagemap, mc_page_number(NULL, reg->permanent_addr), page_count);
- }
-
- // Incremental per-page snapshot restoration:s
- size_t* reg_page_numbers = NULL;
- if (ref_reg && ref_reg->storage_type == MC_REGION_STORAGE_TYPE_CHUNKED)
- reg_page_numbers = ref_reg->chunked.page_numbers;
-
mc_restore_page_snapshot_region(process,
- reg->permanent_addr, page_count, reg->chunked.page_numbers,
- pagemap, reg_page_numbers);
-
- if(pagemap) {
- free(pagemap);
- }
+ reg->permanent_addr, page_count, reg->chunked.page_numbers);
}
}
static void test_snapshot(bool sparse_checkpoint) {
xbt_test_add("Initialisation");
- _sg_mc_soft_dirty = 0;
_sg_mc_sparse_checkpoint = sparse_checkpoint;
xbt_assert(xbt_pagesize == getpagesize());
xbt_assert(1 << xbt_pagebits == xbt_pagesize);
// Init memory and take snapshots:
init_memory(source, byte_size);
- mc_mem_region_t region0 = mc_region_new_sparse(MC_REGION_TYPE_UNKNOWN, source, source, byte_size, NULL);
+ mc_mem_region_t region0 = mc_region_new_sparse(
+ MC_REGION_TYPE_UNKNOWN, source, source, byte_size);
for(int i=0; i<n; i+=2) {
init_memory((char*) source + i*xbt_pagesize, xbt_pagesize);
}
- mc_mem_region_t region = mc_region_new_sparse(MC_REGION_TYPE_UNKNOWN, source, source, byte_size, NULL);
+ mc_mem_region_t region = mc_region_new_sparse(
+ MC_REGION_TYPE_UNKNOWN, source, source, byte_size);
void* destination = mmap(NULL, byte_size, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0);
xbt_assert(source!=MAP_FAILED, "Could not allocate destination memory");
if (n==1) {
xbt_test_add("Read pointer for %i page(s)", n);
memcpy(source, &mc_model_checker, sizeof(void*));
- mc_mem_region_t region2 = mc_region_new_sparse(MC_REGION_TYPE_UNKNOWN, source, source, byte_size, NULL);
+ mc_mem_region_t region2 = mc_region_new_sparse(
+ MC_REGION_TYPE_UNKNOWN, source, source, byte_size);
xbt_test_assert(MC_region_read_pointer(region2, source) == mc_model_checker,
"Mismtach in MC_region_read_pointer()");
MC_region_destroy(region2);
SG_BEGIN_DECL()
-void mc_softdirty_reset(void);
-
// ***** Snapshot region
typedef enum e_mc_region_type_t {
};
-mc_mem_region_t mc_region_new_sparse(mc_region_type_t type, void *start_addr, void* data_addr, size_t size, mc_mem_region_t ref_reg);
+mc_mem_region_t mc_region_new_sparse(
+ mc_region_type_t type, void *start_addr, void* data_addr, size_t size);
void MC_region_destroy(mc_mem_region_t reg);
-void mc_region_restore_sparse(mc_process_t process, mc_mem_region_t reg, mc_mem_region_t ref_reg);
+void mc_region_restore_sparse(mc_process_t process, mc_mem_region_t reg);
static inline __attribute__ ((always_inline))
bool mc_region_contain(mc_mem_region_t region, const void* p)
int mc_important_snapshot(mc_snapshot_t snapshot);
size_t* mc_take_page_snapshot_region(mc_process_t process,
- void* data, size_t page_count, uint64_t* pagemap, size_t* reference_pages);
+ void* data, size_t page_count);
void mc_free_page_snapshot_region(size_t* pagenos, size_t page_count);
void mc_restore_page_snapshot_region(
mc_process_t process,
- void* start_addr, size_t page_count, size_t* pagenos,
- uint64_t* pagemap, size_t* reference_pagenos);
+ void* start_addr, size_t page_count, size_t* pagenos);
const void* MC_region_read_fragmented(mc_mem_region_t region, void* target, const void* addr, size_t size);
xbt_cfgelm_boolean, 1, 1, _mc_cfg_cb_sparse_checkpoint, NULL);
xbt_cfg_setdefault_boolean(_sg_cfg_set, "model-check/sparse-checkpoint", "no");
- /* do stateful model-checking */
- xbt_cfg_register(&_sg_cfg_set, "model-check/soft-dirty",
- "Use sparse per-page snapshots.",
- xbt_cfgelm_boolean, 1, 1, _mc_cfg_cb_soft_dirty, NULL);
- xbt_cfg_setdefault_boolean(_sg_cfg_set, "model-check/soft-dirty", "no");
-
/* do liveness model-checking */
xbt_cfg_register(&_sg_cfg_set, "model-check/property",
"Specify the name of the file containing the property. It must be the result of the ltl2ba program.",