From 992bc1ec57d376cf14b124ea21b58b30f1e162f9 Mon Sep 17 00:00:00 2001 From: Martin Quinson Date: Sat, 30 Jul 2022 17:11:26 +0200 Subject: [PATCH] further reduce the amount of call sites for RemoteProcess::actors() --- src/mc/VisitedState.cpp | 6 +++--- src/mc/VisitedState.hpp | 6 +++--- src/mc/api.hpp | 2 +- src/mc/compare.cpp | 6 +----- src/mc/explo/DFSExplorer.cpp | 6 +++--- src/mc/explo/LivenessChecker.cpp | 2 +- src/mc/explo/LivenessChecker.hpp | 2 +- src/mc/sosp/Snapshot.cpp | 3 --- src/mc/sosp/Snapshot.hpp | 1 - 9 files changed, 13 insertions(+), 21 deletions(-) diff --git a/src/mc/VisitedState.cpp b/src/mc/VisitedState.cpp index 5ad4043429..5e45f7120b 100644 --- a/src/mc/VisitedState.cpp +++ b/src/mc/VisitedState.cpp @@ -17,10 +17,10 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_VisitedState, mc, "Logging specific to state namespace simgrid::mc { /** @brief Save the current state */ -VisitedState::VisitedState(unsigned long state_number) : num(state_number) +VisitedState::VisitedState(unsigned long state_number, unsigned int actor_count) + : actor_count_(actor_count), num(state_number) { this->heap_bytes_used = Api::get().get_remote_heap_bytes(); - this->actors_count = mc_model_checker->get_remote_process().actors().size(); this->system_state = std::make_shared(state_number); } @@ -42,7 +42,7 @@ void VisitedStates::prune() std::unique_ptr VisitedStates::addVisitedState(unsigned long state_number, simgrid::mc::State* graph_state, bool compare_snapshots) { - auto new_state = std::make_unique(state_number); + auto new_state = std::make_unique(state_number, graph_state->get_actor_count()); graph_state->set_system_state(new_state->system_state); XBT_DEBUG("Snapshot %p of visited state %ld (exploration stack state %ld)", new_state->system_state.get(), new_state->num, graph_state->get_num()); diff --git a/src/mc/VisitedState.hpp b/src/mc/VisitedState.hpp index 33f3d1ae94..50ef93f0b2 100644 --- a/src/mc/VisitedState.hpp +++ b/src/mc/VisitedState.hpp @@ -18,11 +18,11 @@ class XBT_PRIVATE VisitedState { public: std::shared_ptr system_state = nullptr; std::size_t heap_bytes_used = 0; - int actors_count = 0; - long num = 0; // unique id of that state in the storage of all stored IDs + int actor_count_; + long num; // unique id of that state in the storage of all stored IDs long original_num = -1; // num field of the VisitedState to which I was declared equal to (used for dot_output) - explicit VisitedState(unsigned long state_number); + explicit VisitedState(unsigned long state_number, unsigned int actor_count); }; class XBT_PRIVATE VisitedStates { diff --git a/src/mc/api.hpp b/src/mc/api.hpp index c30d9991f1..2a9d2500ce 100644 --- a/src/mc/api.hpp +++ b/src/mc/api.hpp @@ -36,7 +36,7 @@ private: struct DerefAndCompareByActorsCountAndUsedHeap { template bool operator()(X const& a, Y const& b) const { - return std::make_pair(a->actors_count, a->heap_bytes_used) < std::make_pair(b->actors_count, b->heap_bytes_used); + return std::make_pair(a->actor_count_, a->heap_bytes_used) < std::make_pair(b->actor_count_, b->heap_bytes_used); } }; diff --git a/src/mc/compare.cpp b/src/mc/compare.cpp index 6b7ffe1f45..a59f4c7fe2 100644 --- a/src/mc/compare.cpp +++ b/src/mc/compare.cpp @@ -1188,11 +1188,7 @@ bool snapshot_equal(const Snapshot* s1, const Snapshot* s2) } XBT_VERB("(%ld - %ld) Same hash: 0x%" PRIx64, s1->num_state_, s2->num_state_, s1->hash_); - /* Compare enabled processes */ - if (s1->enabled_processes_ != s2->enabled_processes_) { - XBT_VERB("(%ld - %ld) Different amount of enabled processes", s1->num_state_, s2->num_state_); - return false; - } + /* 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++) { diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp index 76825fa923..d7e0f1e7a9 100644 --- a/src/mc/explo/DFSExplorer.cpp +++ b/src/mc/explo/DFSExplorer.cpp @@ -126,10 +126,10 @@ void DFSExplorer::run() int next = state->next_transition(); if (next < 0) { // If there is no more transition in the current state, backtrack. - XBT_DEBUG("There remains %zu actors, but none to interleave (depth %zu).", - mc_model_checker->get_remote_process().actors().size(), stack_.size() + 1); + XBT_DEBUG("There remains %d actors, but none to interleave (depth %zu).", state->get_actor_count(), + stack_.size() + 1); - if (mc_model_checker->get_remote_process().actors().empty()) { + if (state->get_actor_count() == 0) { mc_model_checker->finalize_app(); XBT_VERB("Execution came to an end at %s (state: %ld, depth: %zu)", get_record_trace().to_string().c_str(), state->get_num(), stack_.size()); diff --git a/src/mc/explo/LivenessChecker.cpp b/src/mc/explo/LivenessChecker.cpp index 64d9f3635f..cc418c5704 100644 --- a/src/mc/explo/LivenessChecker.cpp +++ b/src/mc/explo/LivenessChecker.cpp @@ -27,7 +27,7 @@ VisitedPair::VisitedPair(int pair_num, xbt_automaton_state_t automaton_state, if (not this->graph_state->get_system_state()) this->graph_state->set_system_state(std::make_shared(pair_num)); this->heap_bytes_used = Api::get().get_remote_heap_bytes(); - this->actors_count = mc_model_checker->get_remote_process().actors().size(); + this->actor_count_ = mc_model_checker->get_remote_process().actors().size(); this->other_num = -1; this->atomic_propositions = std::move(atomic_propositions); } diff --git a/src/mc/explo/LivenessChecker.hpp b/src/mc/explo/LivenessChecker.hpp index 31aa65cca1..a783d46b62 100644 --- a/src/mc/explo/LivenessChecker.hpp +++ b/src/mc/explo/LivenessChecker.hpp @@ -42,7 +42,7 @@ public: xbt_automaton_state_t automaton_state; std::shared_ptr> atomic_propositions; std::size_t heap_bytes_used = 0; - int actors_count = 0; + int actor_count_; VisitedPair(int pair_num, xbt_automaton_state_t automaton_state, std::shared_ptr> atomic_propositions, std::shared_ptr graph_state); diff --git a/src/mc/sosp/Snapshot.cpp b/src/mc/sosp/Snapshot.cpp index 6b07c1f544..bf91e7c82e 100644 --- a/src/mc/sosp/Snapshot.cpp +++ b/src/mc/sosp/Snapshot.cpp @@ -203,9 +203,6 @@ Snapshot::Snapshot(long num_state, RemoteProcess* process) : AddressSpace(proces { XBT_DEBUG("Taking snapshot %ld", num_state); - for (auto const& p : process->actors()) - enabled_processes_.insert(p.copy.get_buffer()->get_pid()); - snapshot_handle_ignore(this); /* Save the std heap and the writable mapped pages of libsimgrid and binary */ diff --git a/src/mc/sosp/Snapshot.hpp b/src/mc/sosp/Snapshot.hpp index 412c7b998c..dec7ffe7d7 100644 --- a/src/mc/sosp/Snapshot.hpp +++ b/src/mc/sosp/Snapshot.hpp @@ -78,7 +78,6 @@ public: long num_state_; std::size_t heap_bytes_used_ = 0; std::vector> snapshot_regions_; - std::set enabled_processes_; std::vector stack_sizes_; std::vector stacks_; std::vector to_ignore_; -- 2.20.1