diff --git a/spot/ltsmin/ltsmin.cc b/spot/ltsmin/ltsmin.cc index 2f0d736fc..c0b2eec82 100644 --- a/spot/ltsmin/ltsmin.cc +++ b/spot/ltsmin/ltsmin.cc @@ -53,7 +53,7 @@ namespace spot struct spins_state final: public state { - spins_state(int s, fixed_size_pool* p) + spins_state(int s, fixed_size_pool* p) : pool(p), size(s), count(1) { } @@ -102,7 +102,7 @@ namespace spot } public: - fixed_size_pool* pool; + fixed_size_pool* pool; size_t hash_value: 32; int size: 16; mutable unsigned count: 16; @@ -197,7 +197,8 @@ namespace spot void transition_callback(void* arg, transition_info_t*, int *dst) { callback_context* ctx = static_cast(arg); - fixed_size_pool* p = static_cast(ctx->pool); + fixed_size_pool* p = + static_cast*>(ctx->pool); spins_state* out = new(p->allocate()) spins_state(ctx->state_size, p); SPOT_ASSUME(out != nullptr); @@ -686,7 +687,8 @@ namespace spot } else { - fixed_size_pool* p = const_cast(&statepool_); + fixed_size_pool* p = + const_cast*>(&statepool_); spins_state* res = new(p->allocate()) spins_state(state_size_, p); SPOT_ASSUME(res != nullptr); d_->get_initial_state(res->vars); @@ -895,7 +897,7 @@ namespace spot void (*decompress_)(const int*, size_t, int*, size_t); int* uncompressed_; int* compressed_; - fixed_size_pool statepool_; + fixed_size_pool statepool_; multiple_size_pool compstatepool_; // This cache is used to speedup repeated calls to state_condition() diff --git a/spot/ltsmin/spins_kripke.hh b/spot/ltsmin/spins_kripke.hh index 5cd7cfc03..42159cbb8 100644 --- a/spot/ltsmin/spins_kripke.hh +++ b/spot/ltsmin/spins_kripke.hh @@ -94,7 +94,7 @@ namespace spot unsigned int size() const; private: - fixed_size_pool p_; + fixed_size_pool p_; multiple_size_pool msp_; bool compress_; const unsigned int state_size_; @@ -121,6 +121,8 @@ namespace spot class cspins_iterator final { public: + cspins_iterator(const cspins_iterator&) = delete; + cspins_iterator(cspins_iterator&) = delete; cspins_iterator(cspins_state s, const spot::spins_interface* d, cspins_state_manager& manager, diff --git a/spot/mc/deadlock.hh b/spot/mc/deadlock.hh index 0c951fa4b..f51341b3d 100644 --- a/spot/mc/deadlock.hh +++ b/spot/mc/deadlock.hh @@ -247,7 +247,7 @@ namespace spot unsigned dfs_ = 0; ///< \brief Maximum DFS stack size /// \brief Maximum number of threads that can be handled by this algorithm unsigned nb_th_ = 0; - fixed_size_pool p_; ///< \brief State Allocator + fixed_size_pool p_; ///< \brief State Allocator bool deadlock_ = false; ///< \brief Deadlock detected? std::atomic& stop_; ///< \brief Stop-the-world boolean /// \brief Stack that grows according to the todo stack. It avoid multiple diff --git a/spot/misc/Makefile.am b/spot/misc/Makefile.am index f6a4a9cfd..ab1085cfa 100644 --- a/spot/misc/Makefile.am +++ b/spot/misc/Makefile.am @@ -64,7 +64,6 @@ libmisc_la_SOURCES = \ bitset.cc \ bitvect.cc \ escape.cc \ - fixpool.cc \ formater.cc \ game.cc \ intvcomp.cc \ diff --git a/spot/misc/fixpool.cc b/spot/misc/fixpool.cc deleted file mode 100644 index 06dbd55d8..000000000 --- a/spot/misc/fixpool.cc +++ /dev/null @@ -1,125 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2017-2018, 2020 Laboratoire de Recherche et -// Développement de l'Epita (LRDE) -// -// This file is part of Spot, a model checking library. -// -// Spot is free software; you can redistribute it and/or modify it -// under the terms of the GNU General Public License as published by -// the Free Software Foundation; either version 3 of the License, or -// (at your option) any later version. -// -// Spot is distributed in the hope that it will be useful, but WITHOUT -// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -// License for more details. -// -// You should have received a copy of the GNU General Public License -// along with this program. If not, see . - -#include "config.h" -#include - -#include -#include - -namespace spot -{ - - namespace - { -// use gcc and clang built-in functions -// both compilers use the same function names, and define __GNUC__ -#if __GNUC__ - template - struct _clz; - - template<> - struct _clz - { - unsigned - operator()(unsigned n) const noexcept - { - return __builtin_clz(n); - } - }; - - template<> - struct _clz - { - unsigned long - operator()(unsigned long n) const noexcept - { - return __builtin_clzl(n); - } - }; - - template<> - struct _clz - { - unsigned long long - operator()(unsigned long long n) const noexcept - { - return __builtin_clzll(n); - } - }; - - static - size_t - clz(size_t n) - { - return _clz()(n); - } - -#else - size_t - clz(size_t n) - { - size_t res = CHAR_BIT*sizeof(size_t); - while (n) - { - --res; - n >>= 1; - } - return res; - } -#endif - } - - fixed_size_pool::fixed_size_pool(size_t size) - : size_( - [](size_t size) - { - // to properly store chunks and freelist, we need size to be at - // least the size of a block_ - if (size < sizeof(block_)) - size = sizeof(block_); - // powers of 2 are a good alignment - if (!(size & (size-1))) - return size; - // small numbers are best aligned to the next power of 2 - else if (size < alignof(std::max_align_t)) - return size_t{1} << (CHAR_BIT*sizeof(size_t) - clz(size)); - else - { - size_t mask = alignof(std::max_align_t)-1; - return (size + mask) & ~mask; - } - }(size)), - freelist_(nullptr), - chunklist_(nullptr) - { - new_chunk_(); - } - - void fixed_size_pool::new_chunk_() - { - const size_t requested = (size_ > 128 ? size_ : 128) * 8192 - 64; - chunk_* c = reinterpret_cast(::operator new(requested)); - c->prev = chunklist_; - chunklist_ = c; - - free_start_ = c->data_ + size_; - free_end_ = c->data_ + requested; - } -} diff --git a/spot/misc/fixpool.hh b/spot/misc/fixpool.hh index 4d2068205..a99d22d39 100644 --- a/spot/misc/fixpool.hh +++ b/spot/misc/fixpool.hh @@ -20,6 +20,8 @@ #pragma once #include +#include +#include #if SPOT_DEBUG && defined(HAVE_VALGRIND_MEMCHECK_H) #include @@ -27,12 +29,108 @@ namespace spot { + namespace + { +// use gcc and clang built-in functions +// both compilers use the same function names, and define __GNUC__ +#if __GNUC__ + template + struct _clz; + + template<> + struct _clz + { + unsigned + operator()(unsigned n) const noexcept + { + return __builtin_clz(n); + } + }; + + template<> + struct _clz + { + unsigned long + operator()(unsigned long n) const noexcept + { + return __builtin_clzl(n); + } + }; + + template<> + struct _clz + { + unsigned long long + operator()(unsigned long long n) const noexcept + { + return __builtin_clzll(n); + } + }; + + static + size_t + clz(size_t n) + { + return _clz()(n); + } + +#else + size_t + clz(size_t n) + { + size_t res = CHAR_BIT*sizeof(size_t); + while (n) + { + --res; + n >>= 1; + } + return res; + } +#endif + } + + /// A enum class to define the policy of the fixed_sized_pool. + /// We propose 2 policies for the pool: + /// - Safe: ensure (when used with memcheck) that each allocation + /// is deallocated one at a time + /// - Unsafe: rely on the fact that deallocating the pool also release + /// all elements it contains. This case is usefull in a multithreaded + /// environnement with multiple fixed_sized_pool allocating the same + /// ressource. In this case it's hard to detect wich pool has allocated + /// some ressource. + enum class pool_type { Safe , Unsafe }; + /// A fixed-size memory pool implementation. + template class SPOT_API fixed_size_pool { public: /// Create a pool allocating objects of \a size bytes. - fixed_size_pool(size_t size); + fixed_size_pool(size_t size) + : size_( + [](size_t size) + { + // to properly store chunks and freelist, we need size to be at + // least the size of a block_ + if (size < sizeof(block_)) + size = sizeof(block_); + // powers of 2 are a good alignment + if (!(size & (size-1))) + return size; + // small numbers are best aligned to the next power of 2 + else if (size < alignof(std::max_align_t)) + return size_t{1} << (CHAR_BIT*sizeof(size_t) - clz(size)); + else + { + size_t mask = alignof(std::max_align_t)-1; + return (size + mask) & ~mask; + } + }(size)), + freelist_(nullptr), + chunklist_(nullptr) + { + new_chunk_(); + } /// Free any memory allocated by this pool. ~fixed_size_pool() @@ -54,10 +152,13 @@ namespace spot if (f) { #if SPOT_DEBUG && defined(HAVE_VALGRIND_MEMCHECK_H) - VALGRIND_MALLOCLIKE_BLOCK(f, size_, 0, false); - // field f->next is initialized: prevents valgrind from complaining - // about jumps depending on uninitialized memory - VALGRIND_MAKE_MEM_DEFINED(f, sizeof(block_*)); + if (Kind == pool_type::Safe) + { + VALGRIND_MALLOCLIKE_BLOCK(f, size_, 0, false); + // field f->next is initialized: prevents valgrind from + // complaining about jumps depending on uninitialized memory + VALGRIND_MAKE_MEM_DEFINED(f, sizeof(block_*)); + } #endif freelist_ = f->next; return f; @@ -73,7 +174,10 @@ namespace spot void* res = free_start_; free_start_ += size_; #if SPOT_DEBUG && defined(HAVE_VALGRIND_MEMCHECK_H) - VALGRIND_MALLOCLIKE_BLOCK(res, size_, 0, false); + if (Kind == pool_type::Safe) + { + VALGRIND_MALLOCLIKE_BLOCK(res, size_, 0, false); + } #endif return res; } @@ -92,12 +196,25 @@ namespace spot b->next = freelist_; freelist_ = b; #if SPOT_DEBUG && defined(HAVE_VALGRIND_MEMCHECK_H) - VALGRIND_FREELIKE_BLOCK(ptr, 0); + if (Kind == pool_type::Safe) + { + VALGRIND_FREELIKE_BLOCK(ptr, 0); + } #endif } private: - void new_chunk_(); + void new_chunk_() + { + const size_t requested = (size_ > 128 ? size_ : 128) * 8192 - 64; + chunk_* c = reinterpret_cast(::operator new(requested)); + c->prev = chunklist_; + chunklist_ = c; + + free_start_ = c->data_ + size_; + free_end_ = c->data_ + requested; + } + const size_t size_; struct block_ { block_* next; }* freelist_; @@ -106,5 +223,4 @@ namespace spot // chunk = several agglomerated blocks union chunk_ { chunk_* prev; char data_[1]; }* chunklist_; }; - } diff --git a/spot/priv/allocator.hh b/spot/priv/allocator.hh index c3fc7ba2b..9c3d50268 100644 --- a/spot/priv/allocator.hh +++ b/spot/priv/allocator.hh @@ -46,10 +46,11 @@ namespace spot class pool_allocator { static - fixed_size_pool& + fixed_size_pool& pool() { - static fixed_size_pool p = fixed_size_pool(sizeof(T)); + static fixed_size_pool p = + fixed_size_pool(sizeof(T)); return p; } diff --git a/spot/ta/tgtaproduct.cc b/spot/ta/tgtaproduct.cc index f073fbdbd..17b240bc6 100644 --- a/spot/ta/tgtaproduct.cc +++ b/spot/ta/tgtaproduct.cc @@ -53,7 +53,8 @@ namespace spot const state* tgta_product::get_init_state() const { - fixed_size_pool* p = const_cast (&pool_); + fixed_size_pool* p = + const_cast*> (&pool_); return new (p->allocate()) state_product(left_->get_init_state(), right_->get_init_state(), p); } @@ -63,7 +64,8 @@ namespace spot { const state_product* s = down_cast (state); - fixed_size_pool* p = const_cast (&pool_); + fixed_size_pool* p = + const_cast*> (&pool_); auto l = std::static_pointer_cast(left_); auto r = std::static_pointer_cast(right_); @@ -75,7 +77,7 @@ namespace spot tgta_succ_iterator_product::tgta_succ_iterator_product( const state_product* s, const const_kripke_ptr& k, const const_tgta_ptr& t, - fixed_size_pool* pool) + fixed_size_pool* pool) : source_(s), tgta_(t), kripke_(k), pool_(pool) { diff --git a/spot/ta/tgtaproduct.hh b/spot/ta/tgtaproduct.hh index d6adea188..46c201476 100644 --- a/spot/ta/tgtaproduct.hh +++ b/spot/ta/tgtaproduct.hh @@ -54,7 +54,7 @@ namespace spot tgta_succ_iterator_product(const state_product* s, const const_kripke_ptr& k, const const_tgta_ptr& tgta, - fixed_size_pool* pool); + fixed_size_pool* pool); virtual ~tgta_succ_iterator_product(); @@ -85,7 +85,7 @@ namespace spot const state_product* source_; const_tgta_ptr tgta_; const_kripke_ptr kripke_; - fixed_size_pool* pool_; + fixed_size_pool* pool_; twa_succ_iterator* tgta_succ_it_; twa_succ_iterator* kripke_succ_it_; state_product* current_state_; diff --git a/spot/twa/twaproduct.cc b/spot/twa/twaproduct.cc index a54621c8e..caa0ad3ef 100644 --- a/spot/twa/twaproduct.cc +++ b/spot/twa/twaproduct.cc @@ -44,7 +44,7 @@ namespace spot { if (--count_) return; - fixed_size_pool* p = pool_; + fixed_size_pool* p = pool_; this->~state_product(); p->deallocate(const_cast(this)); } @@ -83,9 +83,9 @@ namespace spot { public: twa_succ_iterator_product_common(twa_succ_iterator* left, - twa_succ_iterator* right, - const twa_product* prod, - fixed_size_pool* pool) + twa_succ_iterator* right, + const twa_product* prod, + fixed_size_pool* pool) : left_(left), right_(right), prod_(prod), pool_(pool) { } @@ -141,7 +141,7 @@ namespace spot twa_succ_iterator* left_; twa_succ_iterator* right_; const twa_product* prod_; - fixed_size_pool* pool_; + fixed_size_pool* pool_; friend class spot::twa_product; }; @@ -152,9 +152,9 @@ namespace spot { public: twa_succ_iterator_product(twa_succ_iterator* left, - twa_succ_iterator* right, - const twa_product* prod, - fixed_size_pool* pool) + twa_succ_iterator* right, + const twa_product* prod, + fixed_size_pool* pool) : twa_succ_iterator_product_common(left, right, prod, pool) { } @@ -218,9 +218,9 @@ namespace spot { public: twa_succ_iterator_product_kripke(twa_succ_iterator* left, - twa_succ_iterator* right, - const twa_product* prod, - fixed_size_pool* pool) + twa_succ_iterator* right, + const twa_product* prod, + fixed_size_pool* pool) : twa_succ_iterator_product_common(left, right, prod, pool) { } @@ -327,7 +327,8 @@ namespace spot const state* twa_product::get_init_state() const { - fixed_size_pool* p = const_cast(&pool_); + fixed_size_pool* p = + const_cast*>(&pool_); return new(p->allocate()) state_product(left_->get_init_state(), right_->get_init_state(), p); } @@ -348,7 +349,8 @@ namespace spot return it; } - fixed_size_pool* p = const_cast(&pool_); + fixed_size_pool* p = + const_cast*>(&pool_); if (left_kripke_) return new twa_succ_iterator_product_kripke(li, ri, this, p); else @@ -403,7 +405,8 @@ namespace spot const state* twa_product_init::get_init_state() const { - fixed_size_pool* p = const_cast(&pool_); + fixed_size_pool* p = + const_cast*>(&pool_); return new(p->allocate()) state_product(left_init_->clone(), right_init_->clone(), p); } diff --git a/spot/twa/twaproduct.hh b/spot/twa/twaproduct.hh index e16cc9cab..ec998122a 100644 --- a/spot/twa/twaproduct.hh +++ b/spot/twa/twaproduct.hh @@ -44,7 +44,7 @@ namespace spot /// be destroyed on destruction. state_product(const state* left, const state* right, - fixed_size_pool* pool) + fixed_size_pool* pool) : left_(left), right_(right), count_(1), pool_(pool) { } @@ -71,7 +71,7 @@ namespace spot const state* left_; ///< State from the left automaton. const state* right_; ///< State from the right automaton. mutable unsigned count_; - fixed_size_pool* pool_; + fixed_size_pool* pool_; virtual ~state_product(); state_product(const state_product& o) = delete; @@ -107,7 +107,7 @@ namespace spot const_twa_ptr left_; const_twa_ptr right_; bool left_kripke_; - fixed_size_pool pool_; + fixed_size_pool pool_; private: // Disallow copy. diff --git a/tests/core/mempool.cc b/tests/core/mempool.cc index 49480a9ea..0dae6ce0e 100644 --- a/tests/core/mempool.cc +++ b/tests/core/mempool.cc @@ -49,9 +49,9 @@ namespace { int i; - static spot::fixed_size_pool& pool() + static spot::fixed_size_pool& pool() { - static spot::fixed_size_pool p{sizeof(bar)}; + static spot::fixed_size_pool p{sizeof(bar)}; return p; } @@ -108,7 +108,7 @@ int main() #endif { - spot::fixed_size_pool p(sizeof(foo)); + spot::fixed_size_pool p(sizeof(foo)); foo* a = new (p.allocate()) foo(1); a->incr();