From 91c01af98e14d7aa23b1b95199d00aa684434fc6 Mon Sep 17 00:00:00 2001 From: Gabriel Corona Date: Fri, 9 Oct 2015 11:32:58 +0200 Subject: [PATCH] [mc] Move MC_important_snapshot() as a method of ModelChecker --- src/mc/ModelChecker.hpp | 5 +++++ src/mc/mc_checkpoint.cpp | 12 ------------ src/mc/mc_private.h | 2 -- src/mc/mc_visited.cpp | 5 +++-- 4 files changed, 8 insertions(+), 16 deletions(-) diff --git a/src/mc/ModelChecker.hpp b/src/mc/ModelChecker.hpp index 2e7295611c..f8b0982139 100644 --- a/src/mc/ModelChecker.hpp +++ b/src/mc/ModelChecker.hpp @@ -52,6 +52,11 @@ public: return page_store_; } const char* get_host_name(const char* name); + + bool is_important_snapshot(Snapshot const& snapshot) const + { + return &snapshot == mc_model_checker->parent_snapshot_; + } }; } diff --git a/src/mc/mc_checkpoint.cpp b/src/mc/mc_checkpoint.cpp index aadcea88d9..763e116109 100644 --- a/src/mc/mc_checkpoint.cpp +++ b/src/mc/mc_checkpoint.cpp @@ -50,18 +50,6 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_checkpoint, mc, /************************************ Free functions **************************************/ /*****************************************************************************************/ -int MC_important_snapshot(mc_snapshot_t snapshot) -{ - // We need this snapshot in order to know which - // pages needs to be stored in the next snapshot. - // This field is only non-NULL when using soft-dirty - // page tracking. - if (snapshot == mc_model_checker->parent_snapshot_) - return true; - - return false; -} - /** @brief Restore a region from a snapshot * * @param reg Target region diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h index f88c5c4414..bbd2a64823 100644 --- a/src/mc/mc_private.h +++ b/src/mc/mc_private.h @@ -118,8 +118,6 @@ XBT_PRIVATE void MC_report_assertion_error(void); XBT_PRIVATE void MC_invalidate_cache(void); -XBT_PRIVATE int MC_important_snapshot(mc_snapshot_t snapshot); - SG_END_DECL() #endif diff --git a/src/mc/mc_visited.cpp b/src/mc/mc_visited.cpp index e8e6922f25..40db5aad8a 100644 --- a/src/mc/mc_visited.cpp +++ b/src/mc/mc_visited.cpp @@ -355,7 +355,8 @@ mc_visited_state_t is_visited_state(mc_state_t graph_state) mc_visited_state_t state_test; xbt_dynar_foreach(visited_states, cursor2, state_test){ - if (!MC_important_snapshot(state_test->system_state) && state_test->num < min2) { + if (!mc_model_checker->is_important_snapshot(*state_test->system_state) + && state_test->num < min2) { index2 = cursor2; min2 = state_test->num; } @@ -472,7 +473,7 @@ int is_visited_pair(mc_visited_pair_t visited_pair, mc_pair_t pair) { unsigned int cursor2 = 0; unsigned int index2 = 0; xbt_dynar_foreach(visited_pairs, cursor2, pair_test) { - if (!MC_important_snapshot(pair_test->graph_state->system_state) + if (!mc_model_checker->is_important_snapshot(*pair_test->graph_state->system_state) && pair_test->num < min2) { index2 = cursor2; min2 = pair_test->num; -- 2.20.1