From a2b07e1db97dbd4d8acb6c83de13d2e9449520e1 Mon Sep 17 00:00:00 2001 From: Martin Quinson Date: Sun, 7 Aug 2022 00:33:02 +0200 Subject: [PATCH] Convert simgrid::mc::snapshot_equal() into Snapshot::operator==() Also inline 2 more functions from mc::api --- src/mc/VisitedState.cpp | 2 +- src/mc/api.cpp | 12 ------- src/mc/api.hpp | 4 --- src/mc/api/State.cpp | 3 +- src/mc/compare.cpp | 59 ++++++++++++++++---------------- src/mc/explo/DFSExplorer.cpp | 2 +- src/mc/explo/LivenessChecker.cpp | 6 ++-- src/mc/sosp/Snapshot.hpp | 3 ++ 8 files changed, 38 insertions(+), 53 deletions(-) diff --git a/src/mc/VisitedState.cpp b/src/mc/VisitedState.cpp index fa2302adb3..790d90afb2 100644 --- a/src/mc/VisitedState.cpp +++ b/src/mc/VisitedState.cpp @@ -52,7 +52,7 @@ VisitedStates::addVisitedState(unsigned long state_number, simgrid::mc::State* g if (compare_snapshots) for (auto i = range_begin; i != range_end; ++i) { auto& visited_state = *i; - if (Api::get().snapshot_equal(visited_state->system_state.get(), new_state->system_state.get())) { + if (*visited_state->system_state.get() == *new_state->system_state.get()) { // The state has been visited: std::unique_ptr old_state = diff --git a/src/mc/api.cpp b/src/mc/api.cpp index 70f4c57cfd..d866d445e1 100644 --- a/src/mc/api.cpp +++ b/src/mc/api.cpp @@ -35,16 +35,4 @@ std::size_t Api::get_remote_heap_bytes() const auto heap_bytes_used = mmalloc_get_bytes_used_remote(process.get_heap()->heaplimit, process.get_malloc_info()); return heap_bytes_used; } - -bool Api::snapshot_equal(const Snapshot* s1, const Snapshot* s2) const -{ - return simgrid::mc::snapshot_equal(s1, s2); -} - -simgrid::mc::Snapshot* Api::take_snapshot(long num_state) const -{ - auto snapshot = new simgrid::mc::Snapshot(num_state); - return snapshot; -} - } // namespace simgrid::mc diff --git a/src/mc/api.hpp b/src/mc/api.hpp index 7c084d69cf..b5422c2469 100644 --- a/src/mc/api.hpp +++ b/src/mc/api.hpp @@ -54,10 +54,6 @@ public: // REMOTE APIs std::size_t get_remote_heap_bytes() const; - // SNAPSHOT APIs - bool snapshot_equal(const Snapshot* s1, const Snapshot* s2) const; - simgrid::mc::Snapshot* take_snapshot(long num_state) const; - // AUTOMATION APIs inline DerefAndCompareByActorsCountAndUsedHeap compare_pair() const { diff --git a/src/mc/api/State.cpp b/src/mc/api/State.cpp index 7467b6aa5a..c2b8af51ee 100644 --- a/src/mc/api/State.cpp +++ b/src/mc/api/State.cpp @@ -22,8 +22,7 @@ State::State(RemoteApp& remote_app) : num_(++expended_states_) transition_.reset(new Transition()); /* Stateful model checking */ if ((_sg_mc_checkpoint > 0 && (num_ % _sg_mc_checkpoint == 0)) || _sg_mc_termination) { - auto snapshot_ptr = Api::get().take_snapshot(num_); - system_state_ = std::shared_ptr(snapshot_ptr); + system_state_ = std::make_shared(num_); } } diff --git a/src/mc/compare.cpp b/src/mc/compare.cpp index a59f4c7fe2..8acb0dd135 100644 --- a/src/mc/compare.cpp +++ b/src/mc/compare.cpp @@ -1174,61 +1174,62 @@ static bool local_variables_differ(const simgrid::mc::RemoteProcess& process, si namespace simgrid::mc { -bool snapshot_equal(const Snapshot* s1, const Snapshot* s2) +bool Snapshot::operator==(const Snapshot& other) { // TODO, make this a field of ModelChecker or something similar static StateComparator state_comparator; const RemoteProcess& process = mc_model_checker->get_remote_process(); - if (s1->hash_ != s2->hash_) { - XBT_VERB("(%ld - %ld) Different hash: 0x%" PRIx64 "--0x%" PRIx64, s1->num_state_, s2->num_state_, s1->hash_, - s2->hash_); + if (hash_ != other.hash_) { + XBT_VERB("(%ld - %ld) Different hash: 0x%" PRIx64 "--0x%" PRIx64, this->num_state_, other.num_state_, this->hash_, + other.hash_); return false; } - XBT_VERB("(%ld - %ld) Same hash: 0x%" PRIx64, s1->num_state_, s2->num_state_, s1->hash_); + XBT_VERB("(%ld - %ld) Same hash: 0x%" PRIx64, this->num_state_, other.num_state_, this->hash_); /* TODO: re-enable the quick filter of counting enabled processes in each snapshots */ /* Compare size of stacks */ - 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 < this->stacks_.size(); i++) { + size_t size_used1 = this->stack_sizes_[i]; + size_t size_used2 = other.stack_sizes_[i]; if (size_used1 != size_used2) { - XBT_VERB("(%ld - %ld) Different size used in stacks: %zu - %zu", s1->num_state_, s2->num_state_, size_used1, + XBT_VERB("(%ld - %ld) Different size used in stacks: %zu - %zu", num_state_, other.num_state_, size_used1, size_used2); return false; } } /* Init heap information used in heap comparison algorithm */ - const s_xbt_mheap_t* heap1 = static_cast( - s1->read_bytes(alloca(sizeof(s_xbt_mheap_t)), sizeof(s_xbt_mheap_t), process.heap_address, ReadOptions::lazy())); - const s_xbt_mheap_t* heap2 = static_cast( - s2->read_bytes(alloca(sizeof(s_xbt_mheap_t)), sizeof(s_xbt_mheap_t), process.heap_address, ReadOptions::lazy())); - if (state_comparator.initHeapInformation(heap1, heap2, s1->to_ignore_, s2->to_ignore_) == -1) { - XBT_VERB("(%ld - %ld) Different heap information", s1->num_state_, s2->num_state_); + const s_xbt_mheap_t* heap1 = static_cast(this->read_bytes( + alloca(sizeof(s_xbt_mheap_t)), sizeof(s_xbt_mheap_t), process.heap_address, ReadOptions::lazy())); + const s_xbt_mheap_t* heap2 = static_cast(other.read_bytes( + alloca(sizeof(s_xbt_mheap_t)), sizeof(s_xbt_mheap_t), process.heap_address, ReadOptions::lazy())); + if (state_comparator.initHeapInformation(heap1, heap2, this->to_ignore_, other.to_ignore_) == -1) { + XBT_VERB("(%ld - %ld) Different heap information", this->num_state_, other.num_state_); return false; } /* Stacks comparison */ - for (unsigned int cursor = 0; cursor < s1->stacks_.size(); cursor++) { - const_mc_snapshot_stack_t stack1 = &s1->stacks_[cursor]; - const_mc_snapshot_stack_t stack2 = &s2->stacks_[cursor]; + for (unsigned int cursor = 0; cursor < this->stacks_.size(); cursor++) { + const_mc_snapshot_stack_t stack1 = &this->stacks_[cursor]; + const_mc_snapshot_stack_t stack2 = &other.stacks_[cursor]; - if (local_variables_differ(process, state_comparator, *s1, *s2, stack1, stack2)) { - XBT_VERB("(%ld - %ld) Different local variables between stacks %u", s1->num_state_, s2->num_state_, cursor + 1); + if (local_variables_differ(process, state_comparator, *this, other, stack1, stack2)) { + XBT_VERB("(%ld - %ld) Different local variables between stacks %u", this->num_state_, other.num_state_, + cursor + 1); return false; } } - size_t regions_count = s1->snapshot_regions_.size(); - if (regions_count != s2->snapshot_regions_.size()) + size_t regions_count = this->snapshot_regions_.size(); + if (regions_count != other.snapshot_regions_.size()) return false; for (size_t k = 0; k != regions_count; ++k) { - Region* region1 = s1->snapshot_regions_[k].get(); - Region* region2 = s2->snapshot_regions_[k].get(); + Region* region1 = this->snapshot_regions_[k].get(); + Region* region2 = other.snapshot_regions_[k].get(); // Preconditions: if (region1->region_type() != RegionType::Data) @@ -1239,20 +1240,20 @@ bool snapshot_equal(const Snapshot* s1, const Snapshot* s2) xbt_assert(region1->object_info()); /* Compare global variables */ - if (global_variables_differ(process, state_comparator, region1->object_info(), region1, region2, *s1, *s2)) { + if (global_variables_differ(process, state_comparator, region1->object_info(), region1, region2, *this, other)) { std::string const& name = region1->object_info()->file_name; - XBT_VERB("(%ld - %ld) Different global variables in %s", s1->num_state_, s2->num_state_, name.c_str()); + XBT_VERB("(%ld - %ld) Different global variables in %s", this->num_state_, other.num_state_, name.c_str()); return false; } } /* Compare heap */ - if (mmalloc_heap_differ(process, state_comparator, *s1, *s2)) { - XBT_VERB("(%ld - %ld) Different heap (mmalloc_compare)", s1->num_state_, s2->num_state_); + if (mmalloc_heap_differ(process, state_comparator, *this, other)) { + XBT_VERB("(%ld - %ld) Different heap (mmalloc_compare)", this->num_state_, other.num_state_); return false; } - XBT_VERB("(%ld - %ld) No difference found", s1->num_state_, s2->num_state_); + XBT_VERB("(%ld - %ld) No difference found", this->num_state_, other.num_state_); return true; } diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp index 1bd4125051..f2fb7abdad 100644 --- a/src/mc/explo/DFSExplorer.cpp +++ b/src/mc/explo/DFSExplorer.cpp @@ -41,7 +41,7 @@ xbt::signal DFSExplorer::on_log_state_signal; void DFSExplorer::check_non_termination(const State* current_state) { for (auto state = stack_.rbegin(); state != stack_.rend(); ++state) - if (Api::get().snapshot_equal((*state)->get_system_state(), current_state->get_system_state())) { + if (*(*state)->get_system_state() == *current_state->get_system_state()) { XBT_INFO("Non-progressive cycle: state %ld -> state %ld", (*state)->get_num(), current_state->get_num()); XBT_INFO("******************************************"); XBT_INFO("*** NON-PROGRESSIVE CYCLE DETECTED ***"); diff --git a/src/mc/explo/LivenessChecker.cpp b/src/mc/explo/LivenessChecker.cpp index 3d45e8db9f..fac533429a 100644 --- a/src/mc/explo/LivenessChecker.cpp +++ b/src/mc/explo/LivenessChecker.cpp @@ -69,8 +69,7 @@ std::shared_ptr LivenessChecker::insert_acceptance_pair(simgrid::mc std::shared_ptr const& pair_test = *i; if (xbt_automaton_state_compare(pair_test->prop_state_, new_pair->prop_state_) != 0 || *(pair_test->atomic_propositions) != *(new_pair->atomic_propositions) || - not Api::get().snapshot_equal(pair_test->app_state_->get_system_state(), - new_pair->app_state_->get_system_state())) + (*pair_test->app_state_->get_system_state() != *new_pair->app_state_->get_system_state())) continue; XBT_INFO("Pair %d already reached (equal to pair %d) !", new_pair->num, pair_test->num); exploration_stack_.pop_back(); @@ -146,8 +145,7 @@ int LivenessChecker::insert_visited_pair(std::shared_ptr visited_pa const VisitedPair* pair_test = i->get(); if (xbt_automaton_state_compare(pair_test->prop_state_, visited_pair->prop_state_) != 0 || *(pair_test->atomic_propositions) != *(visited_pair->atomic_propositions) || - not Api::get().snapshot_equal(pair_test->app_state_->get_system_state(), - visited_pair->app_state_->get_system_state())) + (*pair_test->app_state_->get_system_state() != *visited_pair->app_state_->get_system_state())) continue; if (pair_test->other_num == -1) visited_pair->other_num = pair_test->num; diff --git a/src/mc/sosp/Snapshot.hpp b/src/mc/sosp/Snapshot.hpp index dec7ffe7d7..2548423462 100644 --- a/src/mc/sosp/Snapshot.hpp +++ b/src/mc/sosp/Snapshot.hpp @@ -74,6 +74,9 @@ public: Region* get_region(const void* addr, Region* hinted_region) const; void restore(RemoteProcess* process) const; + bool operator==(const Snapshot& other); + bool operator!=(const Snapshot& other) { return not(*this == other); } + // To be private long num_state_; std::size_t heap_bytes_used_ = 0; -- 2.20.1