From c44b60f08fd339ae18ad4bbdda845715e2b4e3f0 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 3 Apr 2011 21:00:11 +0200 Subject: [PATCH] * src/tgba/tgbaproduct.hh, src/tgba/tgbaproduct.cc: Use a fixed-size memory pool for product_state instances. --- ChangeLog | 5 +++ src/tgba/tgbaproduct.cc | 71 ++++++++++++++++++++++++++++------------- src/tgba/tgbaproduct.hh | 19 +++++++---- 3 files changed, 66 insertions(+), 29 deletions(-) diff --git a/ChangeLog b/ChangeLog index a8f13cc02..274ec4e0f 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,8 @@ +2011-04-03 Alexandre Duret-Lutz + + * src/tgba/tgbaproduct.hh, src/tgba/tgbaproduct.cc: Use + a fixed-size memory pool for product_state instances. + 2011-04-03 Alexandre Duret-Lutz * iface/dve2/dve2.cc: Use a fixed-size memory pool for dve2_state diff --git a/src/tgba/tgbaproduct.cc b/src/tgba/tgbaproduct.cc index 92573ec60..8d1bad400 100644 --- a/src/tgba/tgbaproduct.cc +++ b/src/tgba/tgbaproduct.cc @@ -33,19 +33,22 @@ namespace spot //////////////////////////////////////////////////////////// // state_product - state_product::state_product(const state_product& o) - : state(), - left_(o.left()->clone()), - right_(o.right()->clone()) - { - } - state_product::~state_product() { left_->destroy(); right_->destroy(); } + void + state_product::destroy() const + { + if (--count_) + return; + fixed_size_pool* p = pool_; + this->~state_product(); + p->deallocate(this); + } + int state_product::compare(const state* other) const { @@ -67,7 +70,8 @@ namespace spot state_product* state_product::clone() const { - return new state_product(*this); + ++count_; + return const_cast(this); } //////////////////////////////////////////////////////////// @@ -80,8 +84,9 @@ namespace spot { public: tgba_succ_iterator_product_common(tgba_succ_iterator* left, - tgba_succ_iterator* right) - : left_(left), right_(right) + tgba_succ_iterator* right, + fixed_size_pool* pool) + : left_(left), right_(right), pool_(pool) { } @@ -120,13 +125,15 @@ namespace spot state_product* current_state() const { - return new state_product(left_->current_state(), - right_->current_state()); + return new(pool_->allocate()) state_product(left_->current_state(), + right_->current_state(), + pool_); } protected: tgba_succ_iterator* left_; tgba_succ_iterator* right_; + fixed_size_pool* pool_; friend class spot::tgba_product; }; @@ -138,8 +145,9 @@ namespace spot tgba_succ_iterator_product(tgba_succ_iterator* left, tgba_succ_iterator* right, bdd left_neg, bdd right_neg, - bddPair* right_common_acc) - : tgba_succ_iterator_product_common(left, right), + bddPair* right_common_acc, + fixed_size_pool* pool) + : tgba_succ_iterator_product_common(left, right, pool), left_neg_(left_neg), right_neg_(right_neg), right_common_acc_(right_common_acc) @@ -209,8 +217,9 @@ namespace spot { public: tgba_succ_iterator_product_kripke(tgba_succ_iterator* left, - tgba_succ_iterator* right) - : tgba_succ_iterator_product_common(left, right) + tgba_succ_iterator* right, + fixed_size_pool* pool) + : tgba_succ_iterator_product_common(left, right, pool) { } @@ -268,7 +277,8 @@ namespace spot // tgba_product tgba_product::tgba_product(const tgba* left, const tgba* right) - : dict_(left->get_dict()), left_(left), right_(right) + : dict_(left->get_dict()), left_(left), right_(right), + pool_(sizeof(state_product)) { assert(dict_ == right_->get_dict()); @@ -338,13 +348,26 @@ namespace spot if (!left_kripke_) bdd_freepair(right_common_acc_); dict_->unregister_all_my_variables(this); + // Prevent these states from being destroyed by ~tgba(): they + // will be destroyed before when the pool is destructed. + if (last_support_conditions_input_) + { + last_support_conditions_input_->destroy(); + last_support_conditions_input_ = 0; + } + if (last_support_variables_input_) + { + last_support_variables_input_->destroy(); + last_support_variables_input_ = 0; + } } state* tgba_product::get_init_state() const { - return new state_product(left_->get_init_state(), - right_->get_init_state()); + fixed_size_pool* p = const_cast(&pool_); + return new(p->allocate()) state_product(left_->get_init_state(), + right_->get_init_state(), p); } tgba_succ_iterator* @@ -369,13 +392,15 @@ namespace spot tgba_succ_iterator* ri = right_->succ_iter(s->right(), global_state, global_automaton); + fixed_size_pool* p = const_cast(&pool_); if (left_kripke_) - return new tgba_succ_iterator_product_kripke(li, ri); + return new tgba_succ_iterator_product_kripke(li, ri, p); else return new tgba_succ_iterator_product(li, ri, left_acc_complement_, right_acc_complement_, - right_common_acc_); + right_common_acc_, + p); } bdd @@ -470,7 +495,9 @@ namespace spot state* tgba_product_init::get_init_state() const { - return new state_product(left_init_->clone(), right_init_->clone()); + fixed_size_pool* p = const_cast(&pool_); + return new(p->allocate()) state_product(left_init_->clone(), + right_init_->clone(), p); } } diff --git a/src/tgba/tgbaproduct.hh b/src/tgba/tgbaproduct.hh index 4c857b77a..e351c50a6 100644 --- a/src/tgba/tgbaproduct.hh +++ b/src/tgba/tgbaproduct.hh @@ -25,6 +25,7 @@ # define SPOT_TGBA_TGBAPRODUCT_HH #include "tgba.hh" +#include "misc/fixpool.hh" namespace spot { @@ -40,18 +41,15 @@ namespace spot /// \brief Constructor /// \param left The state from the left automaton. /// \param right The state from the right automaton. + /// \param pool The pool from which the state was allocated. /// These states are acquired by spot::state_product, and will /// be destroyed on destruction. - state_product(state* left, state* right) - : left_(left), - right_(right) + state_product(state* left, state* right, fixed_size_pool* pool) + : left_(left), right_(right), count_(1), pool_(pool) { } - /// Copy constructor - state_product(const state_product& o); - - virtual ~state_product(); + virtual void destroy() const; state* left() const @@ -72,6 +70,11 @@ namespace spot private: state* left_; ///< State from the left automaton. state* right_; ///< State from the right automaton. + mutable unsigned count_; + fixed_size_pool* pool_; + + virtual ~state_product(); + state_product(const state_product& o); // No implementation. }; @@ -120,6 +123,8 @@ namespace spot bdd all_acceptance_conditions_; bdd neg_acceptance_conditions_; bddPair* right_common_acc_; + fixed_size_pool pool_; + private: // Disallow copy. tgba_product(const tgba_product&);