// TODO, have a robust way to find it in O(1)
static inline RegionSnapshot* MC_get_heap_region(Snapshot* snapshot)
{
- for (auto const& region : snapshot->snapshot_regions)
+ for (auto const& region : snapshot->snapshot_regions_)
if (region->region_type() == simgrid::mc::RegionType::Heap)
return region.get();
xbt_die("No heap region");
for (simgrid::mc::Member& member : type->members) {
void* member1 = simgrid::dwarf::resolve_member(real_area1, type, &member, snapshot1, process_index);
void* member2 = simgrid::dwarf::resolve_member(real_area2, type, &member, snapshot2, process_index);
- simgrid::mc::RegionSnapshot* subregion1 = mc_get_region_hinted(member1, snapshot1, process_index, region1);
- simgrid::mc::RegionSnapshot* subregion2 = mc_get_region_hinted(member2, snapshot2, process_index, region2);
+ simgrid::mc::RegionSnapshot* subregion1 = snapshot1->get_region(member1, process_index, region1); // region1 is hinted
+ simgrid::mc::RegionSnapshot* subregion2 = snapshot2->get_region(member2, process_index, region2); // region2 is hinted
res = compare_areas_with_type(state, process_index, member1, snapshot1, subregion1, member2, snapshot2,
subregion2, member.type, pointer_level);
if (res == 1)
// TODO, fix current_varX->subprogram->name to include name if DW_TAG_inlined_subprogram
simgrid::mc::Type* subtype = current_var1->type;
- int res = compare_areas_with_type(
- state, process_index, current_var1->address, snapshot1,
- mc_get_snapshot_region(current_var1->address, snapshot1, process_index), current_var2->address, snapshot2,
- mc_get_snapshot_region(current_var2->address, snapshot2, process_index), subtype, 0);
+ int res =
+ compare_areas_with_type(state, process_index, current_var1->address, snapshot1,
+ snapshot1->get_region(current_var1->address, process_index), current_var2->address,
+ snapshot2, snapshot2->get_region(current_var2->address, process_index), subtype, 0);
if (res == 1) {
// TODO, fix current_varX->subprogram->name to include name if DW_TAG_inlined_subprogram
int hash_result = 0;
if (_sg_mc_hash) {
- hash_result = (s1->hash != s2->hash);
+ hash_result = (s1->hash_ != s2->hash_);
if (hash_result) {
- XBT_VERB("(%d - %d) Different hash: 0x%" PRIx64 "--0x%" PRIx64, s1->num_state, s2->num_state, s1->hash, s2->hash);
+ XBT_VERB("(%d - %d) Different hash: 0x%" PRIx64 "--0x%" PRIx64, s1->num_state_, s2->num_state_, s1->hash_,
+ s2->hash_);
#ifndef MC_DEBUG
return 1;
#endif
} else
- XBT_VERB("(%d - %d) Same hash: 0x%" PRIx64, s1->num_state, s2->num_state, s1->hash);
+ XBT_VERB("(%d - %d) Same hash: 0x%" PRIx64, s1->num_state_, s2->num_state_, s1->hash_);
}
/* Compare enabled processes */
- if (s1->enabled_processes != s2->enabled_processes) {
- XBT_VERB("(%d - %d) Different amount of enabled processes", s1->num_state, s2->num_state);
+ if (s1->enabled_processes_ != s2->enabled_processes_) {
+ XBT_VERB("(%d - %d) Different amount of enabled processes", s1->num_state_, s2->num_state_);
return 1;
}
/* Compare size of stacks */
int is_diff = 0;
- for (unsigned long i = 0; i < s1->stacks.size(); i++) {
- size_t size_used1 = s1->stack_sizes[i];
- size_t size_used2 = s2->stack_sizes[i];
+ for (unsigned long i = 0; i < s1->stacks_.size(); i++) {
+ size_t size_used1 = s1->stack_sizes_[i];
+ size_t size_used2 = s2->stack_sizes_[i];
if (size_used1 != size_used2) {
#ifdef MC_DEBUG
XBT_DEBUG("(%d - %d) Different size used in stacks: %zu - %zu", s1->num_state, s2->num_state, size_used1,
is_diff = 1;
#else
#ifdef MC_VERBOSE
- XBT_VERB("(%d - %d) Different size used in stacks: %zu - %zu", s1->num_state, s2->num_state, size_used1,
+ XBT_VERB("(%d - %d) Different size used in stacks: %zu - %zu", s1->num_state_, s2->num_state_, size_used1,
size_used2);
#endif
return 1;
alloca(sizeof(struct mdesc)), sizeof(struct mdesc),
remote(process->heap_address),
simgrid::mc::ProcessIndexMissing, simgrid::mc::ReadOptions::lazy());
- int res_init = state_comparator->initHeapInformation(heap1, heap2, &s1->to_ignore, &s2->to_ignore);
+ int res_init = state_comparator->initHeapInformation(heap1, heap2, &s1->to_ignore_, &s2->to_ignore_);
if (res_init == -1) {
#ifdef MC_DEBUG
errors++;
#else
#ifdef MC_VERBOSE
- XBT_VERB("(%d - %d) Different heap information", s1->num_state, s2->num_state);
+ XBT_VERB("(%d - %d) Different heap information", s1->num_state_, s2->num_state_);
#endif
return 1;
/* Stacks comparison */
int diff_local = 0;
- for (unsigned int cursor = 0; cursor < s1->stacks.size(); cursor++) {
- mc_snapshot_stack_t stack1 = &s1->stacks[cursor];
- mc_snapshot_stack_t stack2 = &s2->stacks[cursor];
+ for (unsigned int cursor = 0; cursor < s1->stacks_.size(); cursor++) {
+ mc_snapshot_stack_t stack1 = &s1->stacks_[cursor];
+ mc_snapshot_stack_t stack2 = &s2->stacks_[cursor];
if (stack1->process_index != stack2->process_index) {
diff_local = 1;
- XBT_DEBUG("(%d - %d) Stacks with different process index (%i vs %i)", s1->num_state, s2->num_state,
+ XBT_DEBUG("(%d - %d) Stacks with different process index (%i vs %i)", s1->num_state_, s2->num_state_,
stack1->process_index, stack2->process_index);
}
else diff_local = compare_local_variables(*state_comparator,
#else
#ifdef MC_VERBOSE
- XBT_VERB("(%d - %d) Different local variables between stacks %u", s1->num_state, s2->num_state, cursor + 1);
+ XBT_VERB("(%d - %d) Different local variables between stacks %u", s1->num_state_, s2->num_state_, cursor + 1);
#endif
return 1;
}
}
- size_t regions_count = s1->snapshot_regions.size();
+ size_t regions_count = s1->snapshot_regions_.size();
// TODO, raise a difference instead?
- xbt_assert(regions_count == s2->snapshot_regions.size());
+ xbt_assert(regions_count == s2->snapshot_regions_.size());
for (size_t k = 0; k != regions_count; ++k) {
- RegionSnapshot* region1 = s1->snapshot_regions[k].get();
- RegionSnapshot* region2 = s2->snapshot_regions[k].get();
+ RegionSnapshot* region1 = s1->snapshot_regions_[k].get();
+ RegionSnapshot* region2 = s2->snapshot_regions_[k].get();
// Preconditions:
if (region1->region_type() != RegionType::Data)
errors++;
#else
#ifdef MC_VERBOSE
- XBT_VERB("(%d - %d) Different global variables in %s", s1->num_state, s2->num_state, name.c_str());
+ XBT_VERB("(%d - %d) Different global variables in %s", s1->num_state_, s2->num_state_, name.c_str());
#endif
return 1;
#else
#ifdef MC_VERBOSE
- XBT_VERB("(%d - %d) Different heap (mmalloc_compare)", s1->num_state, s2->num_state);
+ XBT_VERB("(%d - %d) Different heap (mmalloc_compare)", s1->num_state_, s2->num_state_);
#endif
return 1;
#endif
#ifdef MC_VERBOSE
if (errors || hash_result)
- XBT_VERB("(%d - %d) Difference found", s1->num_state, s2->num_state);
+ XBT_VERB("(%d - %d) Difference found", s1->num_state_, s2->num_state_);
else
- XBT_VERB("(%d - %d) No difference found", s1->num_state, s2->num_state);
+ XBT_VERB("(%d - %d) No difference found", s1->num_state_, s2->num_state_);
#endif
#if defined(MC_DEBUG) && defined(MC_VERBOSE)
hash_type hash(Snapshot const& snapshot)
{
- XBT_DEBUG("START hash %i", snapshot.num_state);
+ XBT_DEBUG("START hash %i", snapshot.num_state_);
djb_hash hash;
// TODO:
// * nb_processes
// * root variables
// * basic stack frame information
// * stack frame local variables
- XBT_DEBUG("END hash %i", snapshot.num_state);
+ XBT_DEBUG("END hash %i", snapshot.num_state_);
return hash.value();
}
}
#endif
-static void add_region(simgrid::mc::Snapshot* snapshot, simgrid::mc::RegionType type,
- simgrid::mc::ObjectInformation* object_info, void* start_addr, void* permanent_addr,
- std::size_t size)
-{
- if (type == simgrid::mc::RegionType::Data)
- xbt_assert(object_info, "Missing object info for object.");
- else if (type == simgrid::mc::RegionType::Heap)
- xbt_assert(not object_info, "Unexpected object info for heap region.");
-
- simgrid::mc::RegionSnapshot region;
-#if HAVE_SMPI
- const bool privatization_aware = object_info && mc_model_checker->process().privatized(*object_info);
- if (privatization_aware && MC_smpi_process_count())
- region = simgrid::mc::privatized_region(type, start_addr, permanent_addr, size);
- else
-#endif
- region = simgrid::mc::region(type, start_addr, permanent_addr, size);
-
- region.object_info(object_info);
- snapshot->snapshot_regions.push_back(
- std::unique_ptr<simgrid::mc::RegionSnapshot>(new simgrid::mc::RegionSnapshot(std::move(region))));
-}
-
static void get_memory_regions(simgrid::mc::RemoteClient* process, simgrid::mc::Snapshot* snapshot)
{
- snapshot->snapshot_regions.clear();
+ snapshot->snapshot_regions_.clear();
for (auto const& object_info : process->object_infos)
- add_region(snapshot, simgrid::mc::RegionType::Data, object_info.get(), object_info->start_rw, object_info->start_rw,
- object_info->end_rw - object_info->start_rw);
+ snapshot->add_region(simgrid::mc::RegionType::Data, object_info.get(), object_info->start_rw, object_info->start_rw,
+ object_info->end_rw - object_info->start_rw);
xbt_mheap_t heap = process->get_heap();
void* start_heap = heap->base;
void* end_heap = heap->breakval;
- add_region(snapshot, simgrid::mc::RegionType::Heap, nullptr, start_heap, start_heap,
- (char*)end_heap - (char*)start_heap);
- snapshot->heap_bytes_used = mmalloc_get_bytes_used_remote(heap->heaplimit, process->get_malloc_info());
+ snapshot->add_region(simgrid::mc::RegionType::Heap, nullptr, start_heap, start_heap,
+ (char*)end_heap - (char*)start_heap);
+ snapshot->heap_bytes_used_ = mmalloc_get_bytes_used_remote(heap->heaplimit, process->get_malloc_info());
#if HAVE_SMPI
if (mc_model_checker->process().privatized() && MC_smpi_process_count())
// snapshot->privatization_index = smpi_loaded_page
- mc_model_checker->process().read_variable("smpi_loaded_page", &snapshot->privatization_index,
- sizeof(snapshot->privatization_index));
+ mc_model_checker->process().read_variable("smpi_loaded_page", &snapshot->privatization_index_,
+ sizeof(snapshot->privatization_index_));
else
#endif
- snapshot->privatization_index = simgrid::mc::ProcessIndexMissing;
+ snapshot->privatization_index_ = simgrid::mc::ProcessIndexMissing;
}
/** @brief Fills the position of the segments (executable, read-only, read/write).
xbt_die("Error while unwinding stack");
}
- if (result.empty()) {
- XBT_INFO("unw_init_local failed");
- xbt_abort();
- }
+ xbt_assert(not result.empty(), "unw_init_local failed");
return result;
}
-static std::vector<s_mc_snapshot_stack_t> take_snapshot_stacks(simgrid::mc::Snapshot* snapshot)
+static void take_snapshot_stacks(simgrid::mc::Snapshot* snapshot)
{
- std::vector<s_mc_snapshot_stack_t> res;
-
for (auto const& stack : mc_model_checker->process().stack_areas()) {
s_mc_snapshot_stack_t st;
unw_word_t sp = st.stack_frames[0].sp;
- res.push_back(std::move(st));
+ snapshot->stacks_.push_back(std::move(st));
size_t stack_size = (char*)stack.address + stack.size - (char*)sp;
- snapshot->stack_sizes.push_back(stack_size);
+ snapshot->stack_sizes_.push_back(stack_size);
}
-
- return res;
}
static void snapshot_handle_ignore(simgrid::mc::Snapshot* snapshot)
// TODO, we should do this once per privatization segment:
snapshot->process()->read_bytes(ignored_data.data.data(), region.size, remote(region.addr),
simgrid::mc::ProcessIndexDisabled);
- snapshot->ignored_data.push_back(std::move(ignored_data));
+ snapshot->ignored_data_.push_back(std::move(ignored_data));
}
// Zero the memory:
static void snapshot_ignore_restore(simgrid::mc::Snapshot* snapshot)
{
- for (auto const& ignored_data : snapshot->ignored_data)
+ for (auto const& ignored_data : snapshot->ignored_data_)
snapshot->process()->write_bytes(ignored_data.data.data(), ignored_data.data.size(), remote(ignored_data.start));
}
std::shared_ptr<simgrid::mc::Snapshot> snapshot = std::make_shared<simgrid::mc::Snapshot>(mc_process, num_state);
for (auto const& p : mc_model_checker->process().actors())
- snapshot->enabled_processes.insert(p.copy.getBuffer()->get_pid());
+ snapshot->enabled_processes_.insert(p.copy.getBuffer()->get_pid());
snapshot_handle_ignore(snapshot.get());
/* Save the std heap and the writable mapped pages of libsimgrid and binary */
get_memory_regions(mc_process, snapshot.get());
- snapshot->to_ignore = mc_model_checker->process().ignored_heap();
+ snapshot->to_ignore_ = mc_model_checker->process().ignored_heap();
if (_sg_mc_max_visited_states > 0 || not _sg_mc_property_file.get().empty()) {
- snapshot->stacks = take_snapshot_stacks(snapshot.get());
+ take_snapshot_stacks(snapshot.get());
if (_sg_mc_hash)
- snapshot->hash = simgrid::mc::hash(*snapshot);
+ snapshot->hash_ = simgrid::mc::hash(*snapshot);
}
snapshot_ignore_restore(snapshot.get());
static inline void restore_snapshot_regions(simgrid::mc::Snapshot* snapshot)
{
- for (std::unique_ptr<simgrid::mc::RegionSnapshot> const& region : snapshot->snapshot_regions) {
+ for (std::unique_ptr<simgrid::mc::RegionSnapshot> const& region : snapshot->snapshot_regions_) {
// For privatized, variables we decided it was not necessary to take the snapshot:
if (region)
restore(region.get());
}
#if HAVE_SMPI
- if (snapshot->privatization_index >= 0) {
+ if (snapshot->privatization_index_ >= 0) {
// Fix the privatization mmap:
- s_mc_message_restore_t message{MC_MESSAGE_RESTORE, snapshot->privatization_index};
+ s_mc_message_restore_t message{MC_MESSAGE_RESTORE, snapshot->privatization_index_};
mc_model_checker->process().getChannel().send(message);
}
#endif
void restore_snapshot(std::shared_ptr<simgrid::mc::Snapshot> snapshot)
{
- XBT_DEBUG("Restore snapshot %i", snapshot->num_state);
+ XBT_DEBUG("Restore snapshot %i", snapshot->num_state_);
restore_snapshot_regions(snapshot.get());
snapshot_ignore_restore(snapshot.get());
mc_model_checker->process().clear_cache();
#include "src/mc/mc_mmu.hpp"
#include "src/mc/mc_private.hpp"
+#include "src/mc/mc_smx.hpp"
#include "src/mc/sosp/PageStore.hpp"
#include "src/mc/sosp/mc_snapshot.hpp"
-/** @brief Find the snapshoted region from a pointer
- *
- * @param addr Pointer
- * @param snapshot Snapshot
- * @param process_index rank requesting the region
- * */
-simgrid::mc::RegionSnapshot* mc_get_snapshot_region(const void* addr, const simgrid::mc::Snapshot* snapshot,
- int process_index)
-{
- size_t n = snapshot->snapshot_regions.size();
- for (size_t i = 0; i != n; ++i) {
- simgrid::mc::RegionSnapshot* region = snapshot->snapshot_regions[i].get();
- if (not(region && region->contain(simgrid::mc::remote(addr))))
- continue;
-
- if (region->storage_type() == simgrid::mc::StorageType::Privatized) {
-#if HAVE_SMPI
- // Use the current process index of the snapshot:
- if (process_index == simgrid::mc::ProcessIndexDisabled)
- process_index = snapshot->privatization_index;
- if (process_index < 0)
- xbt_die("Missing process index");
- if (process_index >= (int)region->privatized_data().size())
- xbt_die("Invalid process index");
- simgrid::mc::RegionSnapshot& priv_region = region->privatized_data()[process_index];
- xbt_assert(priv_region.contain(simgrid::mc::remote(addr)));
- return &priv_region;
-#else
- xbt_die("Privatized region in a non SMPI build (this should not happen)");
-#endif
- }
-
- return region;
- }
-
- return nullptr;
-}
/** @brief Read memory from a snapshot region broken across fragmented pages
*
Snapshot::Snapshot(RemoteClient* process, int _num_state)
: AddressSpace(process)
- , num_state(_num_state)
- , heap_bytes_used(0)
- , enabled_processes()
- , privatization_index(0)
- , hash(0)
+ , num_state_(_num_state)
+ , heap_bytes_used_(0)
+ , enabled_processes_()
+ , privatization_index_(0)
+ , hash_(0)
{
}
+void Snapshot::add_region(RegionType type, ObjectInformation* object_info, void* start_addr, void* permanent_addr,
+ std::size_t size)
+{
+ if (type == simgrid::mc::RegionType::Data)
+ xbt_assert(object_info, "Missing object info for object.");
+ else if (type == simgrid::mc::RegionType::Heap)
+ xbt_assert(not object_info, "Unexpected object info for heap region.");
+
+ simgrid::mc::RegionSnapshot region;
+#if HAVE_SMPI
+ const bool privatization_aware = object_info && mc_model_checker->process().privatized(*object_info);
+ if (privatization_aware && MC_smpi_process_count())
+ region = simgrid::mc::privatized_region(type, start_addr, permanent_addr, size);
+ else
+#endif
+ region = simgrid::mc::region(type, start_addr, permanent_addr, size);
+
+ region.object_info(object_info);
+ snapshot_regions_.push_back(std::unique_ptr<simgrid::mc::RegionSnapshot>(new RegionSnapshot(std::move(region))));
+}
+
const void* Snapshot::read_bytes(void* buffer, std::size_t size, RemotePtr<void> address, int process_index,
ReadOptions options) const
{
- RegionSnapshot* region = mc_get_snapshot_region((void*)address.address(), this, process_index);
+ RegionSnapshot* region = this->get_region((void*)address.address(), process_index);
if (region) {
const void* res = MC_region_read(region, buffer, (void*)address.address(), size);
if (buffer == res || options & ReadOptions::lazy())
} else
return this->process()->read_bytes(buffer, size, address, process_index, options);
}
+/** @brief Find the snapshoted region from a pointer
+ *
+ * @param addr Pointer
+ * @param process_index rank requesting the region
+ * */
+RegionSnapshot* Snapshot::get_region(const void* addr, int process_index) const
+{
+ size_t n = snapshot_regions_.size();
+ for (size_t i = 0; i != n; ++i) {
+ RegionSnapshot* region = snapshot_regions_[i].get();
+ if (not(region && region->contain(simgrid::mc::remote(addr))))
+ continue;
+
+ if (region->storage_type() == simgrid::mc::StorageType::Privatized) {
+#if HAVE_SMPI
+ // Use the current process index of the snapshot:
+ if (process_index == simgrid::mc::ProcessIndexDisabled)
+ process_index = privatization_index_;
+ xbt_assert(process_index >= 0, "Missing process index");
+ xbt_assert(process_index < (int)region->privatized_data().size(), "Invalid process index");
+
+ RegionSnapshot& priv_region = region->privatized_data()[process_index];
+ xbt_assert(priv_region.contain(simgrid::mc::remote(addr)));
+ return &priv_region;
+#else
+ xbt_die("Privatized region in a non SMPI build (this should not happen)");
+#endif
+ }
+
+ return region;
+ }
+
+ return nullptr;
+}
+
+/** @brief Find the snapshoted region from a pointer, with a hinted_region */
+RegionSnapshot* Snapshot::get_region(const void* addr, int process_index, RegionSnapshot* hinted_region) const
+{
+ if (hinted_region->contain(simgrid::mc::remote(addr)))
+ return hinted_region;
+ else
+ return get_region(addr, process_index);
+}
} // namespace mc
} // namespace simgrid
}
}
-XBT_PRIVATE simgrid::mc::RegionSnapshot* mc_get_snapshot_region(const void* addr, const simgrid::mc::Snapshot* snapshot,
- int process_index);
-
// ***** MC Snapshot
/** Ignored data
public:
Snapshot(RemoteClient* process, int num_state);
~Snapshot() = default;
+
+ /* Initialization */
+ void add_region(RegionType type, ObjectInformation* object_info, void* start_addr, void* permanent_addr,
+ std::size_t size);
+
+ /* Regular use */
const void* read_bytes(void* buffer, std::size_t size, RemotePtr<void> address, int process_index = ProcessIndexAny,
ReadOptions options = ReadOptions::none()) const override;
+ RegionSnapshot* get_region(const void* addr, int process_index) const;
+ RegionSnapshot* get_region(const void* addr, int process_index, RegionSnapshot* hinted_region) const;
// To be private
- int num_state;
- std::size_t heap_bytes_used;
- std::vector<std::unique_ptr<RegionSnapshot>> snapshot_regions;
- std::set<pid_t> enabled_processes;
- int privatization_index;
- std::vector<std::size_t> stack_sizes;
- std::vector<s_mc_snapshot_stack_t> stacks;
- std::vector<simgrid::mc::IgnoredHeapRegion> to_ignore;
- std::uint64_t hash = 0;
- std::vector<s_mc_snapshot_ignored_data_t> ignored_data;
+ int num_state_;
+ std::size_t heap_bytes_used_;
+ std::vector<std::unique_ptr<RegionSnapshot>> snapshot_regions_;
+ std::set<pid_t> enabled_processes_;
+ int privatization_index_;
+ std::vector<std::size_t> stack_sizes_;
+ std::vector<s_mc_snapshot_stack_t> stacks_;
+ std::vector<simgrid::mc::IgnoredHeapRegion> to_ignore_;
+ std::uint64_t hash_ = 0;
+ std::vector<s_mc_snapshot_ignored_data_t> ignored_data_;
};
} // namespace mc
} // namespace simgrid
-static XBT_ALWAYS_INLINE simgrid::mc::RegionSnapshot* mc_get_region_hinted(void* addr, simgrid::mc::Snapshot* snapshot,
- int process_index,
- simgrid::mc::RegionSnapshot* region)
-{
- if (region->contain(simgrid::mc::remote(addr)))
- return region;
- else
- return mc_get_snapshot_region(addr, snapshot, process_index);
-}
-
static const void* mc_snapshot_get_heap_end(simgrid::mc::Snapshot* snapshot);
namespace simgrid {
