From 82bebb568ecbca2bcac029c94e62e7e332743a58 Mon Sep 17 00:00:00 2001 From: Gabriel Corona Date: Thu, 19 Jun 2014 15:49:21 +0200 Subject: [PATCH] [mc] Config to disable soft-dirty page tracking --cfg=model-check/soft-dirty:yes It is here mostly to test the effect on soft-dirty page tracking on the performance of the simulator. It might be removed in the future once we will be certain that soft-dirty page tracking does not have a significant negative impact on some workloads. --- src/include/mc/mc.h | 2 ++ src/mc/mc_checkpoint.c | 4 ++-- src/mc/mc_global.c | 8 ++++++++ src/mc/mc_page_snapshot.cpp | 4 ++-- src/simgrid/sg_config.c | 6 ++++++ 5 files changed, 20 insertions(+), 4 deletions(-) diff --git a/src/include/mc/mc.h b/src/include/mc/mc.h index a49184d90a..c8a24f49e7 100644 --- a/src/include/mc/mc.h +++ b/src/include/mc/mc.h @@ -39,6 +39,7 @@ SG_BEGIN_DECL() extern int _sg_do_model_check; 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; @@ -59,6 +60,7 @@ extern void *maestro_stack_end; 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); diff --git a/src/mc/mc_checkpoint.c b/src/mc/mc_checkpoint.c index 883f9002d5..722e3d5d74 100644 --- a/src/mc/mc_checkpoint.c +++ b/src/mc/mc_checkpoint.c @@ -585,7 +585,7 @@ 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) { + if (_sg_mc_sparse_checkpoint && _sg_mc_soft_dirty) { mc_softdirty_reset(); } @@ -631,7 +631,7 @@ void MC_restore_snapshot(mc_snapshot_t snapshot) } MC_snapshot_ignore_restore(snapshot); - if (_sg_mc_sparse_checkpoint) { + if (_sg_mc_sparse_checkpoint && _sg_mc_soft_dirty) { mc_softdirty_reset(); } mc_model_checker->parent_snapshot = snapshot; diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index b22364d7c5..1359cf3c3d 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -30,6 +30,7 @@ e_mc_reduce_t mc_reduce_kind = e_mc_reduce_unset; int _sg_do_model_check = 0; int _sg_mc_checkpoint = 0; int _sg_mc_sparse_checkpoint = 0; +int _sg_mc_soft_dirty = 1; char *_sg_mc_property_file = NULL; int _sg_mc_timeout = 0; int _sg_mc_hash = 0; @@ -76,6 +77,13 @@ void _mc_cfg_cb_sparse_checkpoint(const char *name, int pos) { _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) { diff --git a/src/mc/mc_page_snapshot.cpp b/src/mc/mc_page_snapshot.cpp index c049b7d326..4a964acab3 100644 --- a/src/mc/mc_page_snapshot.cpp +++ b/src/mc/mc_page_snapshot.cpp @@ -151,7 +151,7 @@ mc_mem_region_t mc_region_new_sparse(int type, void *start_addr, size_t size, mc size_t page_count = mc_page_count(size); uint64_t* pagemap = NULL; - if (mc_model_checker->parent_snapshot) { + if (_sg_mc_soft_dirty && mc_model_checker->parent_snapshot) { pagemap = (uint64_t*) mmalloc_no_memset((xbt_mheap_t) mc_heap, sizeof(uint64_t) * page_count); mc_read_pagemap(pagemap, mc_page_number(NULL, start_addr), page_count); } @@ -175,7 +175,7 @@ void mc_region_restore_sparse(mc_mem_region_t reg, mc_mem_region_t ref_reg) uint64_t* pagemap = NULL; // Read soft-dirty bits if necessary in order to know which pages have changed: - if (mc_model_checker->parent_snapshot) { + if (_sg_mc_soft_dirty && mc_model_checker->parent_snapshot) { pagemap = (uint64_t*) mmalloc_no_memset((xbt_mheap_t) mc_heap, sizeof(uint64_t) * page_count); mc_read_pagemap(pagemap, mc_page_number(NULL, reg->start_addr), page_count); } diff --git a/src/simgrid/sg_config.c b/src/simgrid/sg_config.c index d9dea55c65..65878a0af4 100644 --- a/src/simgrid/sg_config.c +++ b/src/simgrid/sg_config.c @@ -608,6 +608,12 @@ void sg_config_init(int *argc, char **argv) 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", "yes"); + /* 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.", -- 2.20.1