Commit d998f613 authored by Etienne Renault's avatar Etienne Renault

fixpool: propose alternative policy

In 3fe74f1c, fixed_size_pool was changed in order to
help memcheck to detect "potential" memory leaks. In a
multithreaded context, this could raise false alarm. To
solve this, we proprose 2 policies for the pool, one with
the check and one without.

* spot/misc/fixpool.cc: deleted ...
* spot/ltsmin/ltsmin.cc, spot/ltsmin/spins_kripke.hh,
spot/mc/deadlock.hh, spot/misc/Makefile.am,
spot/misc/fixpool.cc, spot/misc/fixpool.hh,
spot/priv/allocator.hh, spot/ta/tgtaproduct.cc,
spot/ta/tgtaproduct.hh, spot/twa/twaproduct.cc,
spot/twa/twaproduct.hh, tests/core/mempool.cc: Here.
parent 45de5258
...@@ -53,7 +53,7 @@ namespace spot ...@@ -53,7 +53,7 @@ namespace spot
struct spins_state final: public state struct spins_state final: public state
{ {
spins_state(int s, fixed_size_pool* p) spins_state(int s, fixed_size_pool<pool_type::Safe>* p)
: pool(p), size(s), count(1) : pool(p), size(s), count(1)
{ {
} }
...@@ -102,7 +102,7 @@ namespace spot ...@@ -102,7 +102,7 @@ namespace spot
} }
public: public:
fixed_size_pool* pool; fixed_size_pool<pool_type::Safe>* pool;
size_t hash_value: 32; size_t hash_value: 32;
int size: 16; int size: 16;
mutable unsigned count: 16; mutable unsigned count: 16;
...@@ -197,7 +197,8 @@ namespace spot ...@@ -197,7 +197,8 @@ namespace spot
void transition_callback(void* arg, transition_info_t*, int *dst) void transition_callback(void* arg, transition_info_t*, int *dst)
{ {
callback_context* ctx = static_cast<callback_context*>(arg); callback_context* ctx = static_cast<callback_context*>(arg);
fixed_size_pool* p = static_cast<fixed_size_pool*>(ctx->pool); fixed_size_pool<pool_type::Safe>* p =
static_cast<fixed_size_pool<pool_type::Safe>*>(ctx->pool);
spins_state* out = spins_state* out =
new(p->allocate()) spins_state(ctx->state_size, p); new(p->allocate()) spins_state(ctx->state_size, p);
SPOT_ASSUME(out != nullptr); SPOT_ASSUME(out != nullptr);
...@@ -686,7 +687,8 @@ namespace spot ...@@ -686,7 +687,8 @@ namespace spot
} }
else else
{ {
fixed_size_pool* p = const_cast<fixed_size_pool*>(&statepool_); fixed_size_pool<pool_type::Safe>* p =
const_cast<fixed_size_pool<pool_type::Safe>*>(&statepool_);
spins_state* res = new(p->allocate()) spins_state(state_size_, p); spins_state* res = new(p->allocate()) spins_state(state_size_, p);
SPOT_ASSUME(res != nullptr); SPOT_ASSUME(res != nullptr);
d_->get_initial_state(res->vars); d_->get_initial_state(res->vars);
...@@ -895,7 +897,7 @@ namespace spot ...@@ -895,7 +897,7 @@ namespace spot
void (*decompress_)(const int*, size_t, int*, size_t); void (*decompress_)(const int*, size_t, int*, size_t);
int* uncompressed_; int* uncompressed_;
int* compressed_; int* compressed_;
fixed_size_pool statepool_; fixed_size_pool<pool_type::Safe> statepool_;
multiple_size_pool compstatepool_; multiple_size_pool compstatepool_;
// This cache is used to speedup repeated calls to state_condition() // This cache is used to speedup repeated calls to state_condition()
......
...@@ -94,7 +94,7 @@ namespace spot ...@@ -94,7 +94,7 @@ namespace spot
unsigned int size() const; unsigned int size() const;
private: private:
fixed_size_pool p_; fixed_size_pool<pool_type::Unsafe> p_;
multiple_size_pool msp_; multiple_size_pool msp_;
bool compress_; bool compress_;
const unsigned int state_size_; const unsigned int state_size_;
...@@ -121,6 +121,8 @@ namespace spot ...@@ -121,6 +121,8 @@ namespace spot
class cspins_iterator final class cspins_iterator final
{ {
public: public:
cspins_iterator(const cspins_iterator&) = delete;
cspins_iterator(cspins_iterator&) = delete;
cspins_iterator(cspins_state s, cspins_iterator(cspins_state s,
const spot::spins_interface* d, const spot::spins_interface* d,
cspins_state_manager& manager, cspins_state_manager& manager,
......
...@@ -247,7 +247,7 @@ namespace spot ...@@ -247,7 +247,7 @@ namespace spot
unsigned dfs_ = 0; ///< \brief Maximum DFS stack size unsigned dfs_ = 0; ///< \brief Maximum DFS stack size
/// \brief Maximum number of threads that can be handled by this algorithm /// \brief Maximum number of threads that can be handled by this algorithm
unsigned nb_th_ = 0; unsigned nb_th_ = 0;
fixed_size_pool p_; ///< \brief State Allocator fixed_size_pool<pool_type::Unsafe> p_; ///< \brief State Allocator
bool deadlock_ = false; ///< \brief Deadlock detected? bool deadlock_ = false; ///< \brief Deadlock detected?
std::atomic<bool>& stop_; ///< \brief Stop-the-world boolean std::atomic<bool>& stop_; ///< \brief Stop-the-world boolean
/// \brief Stack that grows according to the todo stack. It avoid multiple /// \brief Stack that grows according to the todo stack. It avoid multiple
......
...@@ -64,7 +64,6 @@ libmisc_la_SOURCES = \ ...@@ -64,7 +64,6 @@ libmisc_la_SOURCES = \
bitset.cc \ bitset.cc \
bitvect.cc \ bitvect.cc \
escape.cc \ escape.cc \
fixpool.cc \
formater.cc \ formater.cc \
game.cc \ game.cc \
intvcomp.cc \ intvcomp.cc \
......
// -*- coding: utf-8 -*-
// Copyright (C) 2017-2018 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 <http://www.gnu.org/licenses/>.
#include "config.h"
#include <spot/misc/fixpool.hh>
#include <climits>
#include <cstddef>
namespace spot
{
namespace
{
// use gcc and clang built-in functions
// both compilers use the same function names, and define __GNUC__
#if __GNUC__
template<class T>
struct _clz;
template<>
struct _clz<unsigned>
{
unsigned
operator()(unsigned n) const noexcept
{
return __builtin_clz(n);
}
};
template<>
struct _clz<unsigned long>
{
unsigned long
operator()(unsigned long n) const noexcept
{
return __builtin_clzl(n);
}
};
template<>
struct _clz<unsigned long long>
{
unsigned long long
operator()(unsigned long long n) const noexcept
{
return __builtin_clzll(n);
}
};
static
size_t
clz(size_t n)
{
return _clz<size_t>()(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), free_start_(nullptr),
free_end_(nullptr), chunklist_(nullptr)
{}
}
...@@ -20,6 +20,8 @@ ...@@ -20,6 +20,8 @@
#pragma once #pragma once
#include <spot/misc/common.hh> #include <spot/misc/common.hh>
#include <climits>
#include <cstddef>
#if SPOT_DEBUG && defined(HAVE_VALGRIND_MEMCHECK_H) #if SPOT_DEBUG && defined(HAVE_VALGRIND_MEMCHECK_H)
#include <valgrind/memcheck.h> #include <valgrind/memcheck.h>
...@@ -27,12 +29,106 @@ ...@@ -27,12 +29,106 @@
namespace spot namespace spot
{ {
namespace
{
// use gcc and clang built-in functions
// both compilers use the same function names, and define __GNUC__
#if __GNUC__
template<class T>
struct _clz;
template<>
struct _clz<unsigned>
{
unsigned
operator()(unsigned n) const noexcept
{
return __builtin_clz(n);
}
};
template<>
struct _clz<unsigned long>
{
unsigned long
operator()(unsigned long n) const noexcept
{
return __builtin_clzl(n);
}
};
template<>
struct _clz<unsigned long long>
{
unsigned long long
operator()(unsigned long long n) const noexcept
{
return __builtin_clzll(n);
}
};
static
size_t
clz(size_t n)
{
return _clz<size_t>()(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. /// A fixed-size memory pool implementation.
template<pool_type Kind>
class SPOT_API fixed_size_pool class SPOT_API fixed_size_pool
{ {
public: public:
/// Create a pool allocating objects of \a size bytes. /// 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), free_start_(nullptr),
free_end_(nullptr), chunklist_(nullptr)
{}
/// Free any memory allocated by this pool. /// Free any memory allocated by this pool.
~fixed_size_pool() ~fixed_size_pool()
...@@ -54,10 +150,13 @@ namespace spot ...@@ -54,10 +150,13 @@ namespace spot
if (f) if (f)
{ {
#if SPOT_DEBUG && defined(HAVE_VALGRIND_MEMCHECK_H) #if SPOT_DEBUG && defined(HAVE_VALGRIND_MEMCHECK_H)
if (Kind == pool_type::Safe)
{
VALGRIND_MALLOCLIKE_BLOCK(f, size_, 0, false); VALGRIND_MALLOCLIKE_BLOCK(f, size_, 0, false);
// field f->next is initialized: prevents valgrind from complaining // field f->next is initialized: prevents valgrind from
// about jumps depending on uninitialized memory // complaining about jumps depending on uninitialized memory
VALGRIND_MAKE_MEM_DEFINED(f, sizeof(block_*)); VALGRIND_MAKE_MEM_DEFINED(f, sizeof(block_*));
}
#endif #endif
freelist_ = f->next; freelist_ = f->next;
return f; return f;
...@@ -81,7 +180,10 @@ namespace spot ...@@ -81,7 +180,10 @@ namespace spot
void* res = free_start_; void* res = free_start_;
free_start_ += size_; free_start_ += size_;
#if SPOT_DEBUG && defined(HAVE_VALGRIND_MEMCHECK_H) #if SPOT_DEBUG && defined(HAVE_VALGRIND_MEMCHECK_H)
if (Kind == pool_type::Safe)
{
VALGRIND_MALLOCLIKE_BLOCK(res, size_, 0, false); VALGRIND_MALLOCLIKE_BLOCK(res, size_, 0, false);
}
#endif #endif
return res; return res;
} }
...@@ -100,7 +202,10 @@ namespace spot ...@@ -100,7 +202,10 @@ namespace spot
b->next = freelist_; b->next = freelist_;
freelist_ = b; freelist_ = b;
#if SPOT_DEBUG && defined(HAVE_VALGRIND_MEMCHECK_H) #if SPOT_DEBUG && defined(HAVE_VALGRIND_MEMCHECK_H)
if (Kind == pool_type::Safe)
{
VALGRIND_FREELIKE_BLOCK(ptr, 0); VALGRIND_FREELIKE_BLOCK(ptr, 0);
}
#endif #endif
} }
...@@ -112,5 +217,4 @@ namespace spot ...@@ -112,5 +217,4 @@ namespace spot
// chunk = several agglomerated blocks // chunk = several agglomerated blocks
union chunk_ { chunk_* prev; char data_[1]; }* chunklist_; union chunk_ { chunk_* prev; char data_[1]; }* chunklist_;
}; };
} }
...@@ -46,10 +46,11 @@ namespace spot ...@@ -46,10 +46,11 @@ namespace spot
class pool_allocator class pool_allocator
{ {
static static
fixed_size_pool& fixed_size_pool<pool_type::Safe>&
pool() pool()
{ {
static fixed_size_pool p = fixed_size_pool(sizeof(T)); static fixed_size_pool<pool_type::Safe> p =
fixed_size_pool<pool_type::Safe>(sizeof(T));
return p; return p;
} }
......
...@@ -53,7 +53,8 @@ namespace spot ...@@ -53,7 +53,8 @@ namespace spot
const state* const state*
tgta_product::get_init_state() const tgta_product::get_init_state() const
{ {
fixed_size_pool* p = const_cast<fixed_size_pool*> (&pool_); fixed_size_pool<pool_type::Safe>* p =
const_cast<fixed_size_pool<pool_type::Safe>*> (&pool_);
return new (p->allocate()) state_product(left_->get_init_state(), return new (p->allocate()) state_product(left_->get_init_state(),
right_->get_init_state(), p); right_->get_init_state(), p);
} }
...@@ -63,7 +64,8 @@ namespace spot ...@@ -63,7 +64,8 @@ namespace spot
{ {
const state_product* s = down_cast<const state_product*> (state); const state_product* s = down_cast<const state_product*> (state);
fixed_size_pool* p = const_cast<fixed_size_pool*> (&pool_); fixed_size_pool<pool_type::Safe>* p =
const_cast<fixed_size_pool<pool_type::Safe>*> (&pool_);
auto l = std::static_pointer_cast<const kripke>(left_); auto l = std::static_pointer_cast<const kripke>(left_);
auto r = std::static_pointer_cast<const tgta>(right_); auto r = std::static_pointer_cast<const tgta>(right_);
...@@ -75,7 +77,7 @@ namespace spot ...@@ -75,7 +77,7 @@ namespace spot
tgta_succ_iterator_product::tgta_succ_iterator_product( tgta_succ_iterator_product::tgta_succ_iterator_product(
const state_product* s, const state_product* s,
const const_kripke_ptr& k, const const_tgta_ptr& t, const const_kripke_ptr& k, const const_tgta_ptr& t,
fixed_size_pool* pool) fixed_size_pool<pool_type::Safe>* pool)
: source_(s), tgta_(t), kripke_(k), pool_(pool) : source_(s), tgta_(t), kripke_(k), pool_(pool)
{ {
......
...@@ -54,7 +54,7 @@ namespace spot ...@@ -54,7 +54,7 @@ namespace spot
tgta_succ_iterator_product(const state_product* s, tgta_succ_iterator_product(const state_product* s,
const const_kripke_ptr& k, const const_kripke_ptr& k,
const const_tgta_ptr& tgta, const const_tgta_ptr& tgta,
fixed_size_pool* pool); fixed_size_pool<pool_type::Safe>* pool);
virtual virtual
~tgta_succ_iterator_product(); ~tgta_succ_iterator_product();
...@@ -85,7 +85,7 @@ namespace spot ...@@ -85,7 +85,7 @@ namespace spot
const state_product* source_; const state_product* source_;
const_tgta_ptr tgta_; const_tgta_ptr tgta_;
const_kripke_ptr kripke_; const_kripke_ptr kripke_;
fixed_size_pool* pool_; fixed_size_pool<pool_type::Safe>* pool_;
twa_succ_iterator* tgta_succ_it_; twa_succ_iterator* tgta_succ_it_;
twa_succ_iterator* kripke_succ_it_; twa_succ_iterator* kripke_succ_it_;
state_product* current_state_; state_product* current_state_;
......
...@@ -44,7 +44,7 @@ namespace spot ...@@ -44,7 +44,7 @@ namespace spot
{ {
if (--count_) if (--count_)
return; return;
fixed_size_pool* p = pool_; fixed_size_pool<pool_type::Safe>* p = pool_;
this->~state_product(); this->~state_product();
p->deallocate(const_cast<state_product*>(this)); p->deallocate(const_cast<state_product*>(this));
} }
...@@ -85,7 +85,7 @@ namespace spot ...@@ -85,7 +85,7 @@ namespace spot
twa_succ_iterator_product_common(twa_succ_iterator* left, twa_succ_iterator_product_common(twa_succ_iterator* left,
twa_succ_iterator* right, twa_succ_iterator* right,
const twa_product* prod, const twa_product* prod,
fixed_size_pool* pool) fixed_size_pool<pool_type::Safe>* pool)
: left_(left), right_(right), prod_(prod), pool_(pool) : left_(left), right_(right), prod_(prod), pool_(pool)
{ {
} }
...@@ -141,7 +141,7 @@ namespace spot ...@@ -141,7 +141,7 @@ namespace spot
twa_succ_iterator* left_; twa_succ_iterator* left_;
twa_succ_iterator* right_; twa_succ_iterator* right_;
const twa_product* prod_; const twa_product* prod_;
fixed_size_pool* pool_; fixed_size_pool<pool_type::Safe>* pool_;
friend class spot::twa_product; friend class spot::twa_product;
}; };
...@@ -154,7 +154,7 @@ namespace spot ...@@ -154,7 +154,7 @@ namespace spot
twa_succ_iterator_product(twa_succ_iterator* left, twa_succ_iterator_product(twa_succ_iterator* left,
twa_succ_iterator* right, twa_succ_iterator* right,
const twa_product* prod, const twa_product* prod,
fixed_size_pool* pool) fixed_size_pool<pool_type::Safe>* pool)
: twa_succ_iterator_product_common(left, right, prod, pool) : twa_succ_iterator_product_common(left, right, prod, pool)
{ {
} }
...@@ -220,7 +220,7 @@ namespace spot ...@@ -220,7 +220,7 @@ namespace spot
twa_succ_iterator_product_kripke(twa_succ_iterator* left, twa_succ_iterator_product_kripke(twa_succ_iterator* left,
twa_succ_iterator* right, twa_succ_iterator* right,
const twa_product* prod, const twa_product* prod,
fixed_size_pool* pool) fixed_size_pool<pool_type::Safe>* pool)
: twa_succ_iterator_product_common(left, right, prod, pool) : twa_succ_iterator_product_common(left, right, prod, pool)
{ {
} }
...@@ -327,7 +327,8 @@ namespace spot ...@@ -327,7 +327,8 @@ namespace spot
const state* const state*
twa_product::get_init_state() const twa_product::get_init_state() const
{ {
fixed_size_pool* p = const_cast<fixed_size_pool*>(&pool_); fixed_size_pool<pool_type::Safe>* p =
const_cast<fixed_size_pool<pool_type::Safe>*>(&pool_);
return new(p->allocate()) state_product(left_->get_init_state(), return new(p->allocate()) state_product(left_->get_init_state(),
right_->get_init_state(), p); right_->get_init_state(), p);
} }
...@@ -348,7 +349,8 @@ namespace spot ...@@ -348,7 +349,8 @@ namespace spot
return it; return it;
} }
fixed_size_pool* p = const_cast<fixed_size_pool*>(&pool_); fixed_size_pool<pool_type::Safe>* p =
const_cast<fixed_size_pool<pool_type::Safe>*>(&pool_);
if (left_kripke_) if (left_kripke_)
return new twa_succ_iterator_product_kripke(li, ri, this, p); return new twa_succ_iterator_product_kripke(li, ri, this, p);
else else
...@@ -403,7 +405,8 @@ namespace spot ...@@ -403,7 +405,8 @@ namespace spot
const state* const state*
twa_product_init::get_init_state() const twa_product_init::get_init_state() const
{ {
fixed_size_pool* p = const_cast<fixed_size_pool*>(&pool_); fixed_size_pool<pool_type::Safe>* p =
const_cast<fixed_size_pool<pool_type::Safe>*>(&pool_);
return new(p->allocate()) state_product(left_init_->clone(), return new(p->allocate()) state_product(left_init_->clone(),
right_init_->clone(), p); right_init_->clone(), p);
} }
......
...@@ -44,7 +44,7 @@ namespace spot ...@@ -44,7 +44,7 @@ namespace spot
/// be destroyed on destruction. /// be destroyed on destruction.
state_product(const state* left, state_product(const state* left,
const state* right, const state* right,
fixed_size_pool* pool) fixed_size_pool<pool_type::Safe>* pool)
: left_(left), right_(right), count_(1), pool_(pool) : left_(left), right_(right), count_(1), pool_(pool)
{ {
} }
...@@ -71,7 +71,7 @@ namespace spot ...@@ -71,7 +71,7 @@ namespace spot
const state* left_; ///< State from the left automaton. const state* left_; ///< State from the left automaton.
const state* right_; ///< State from the right automaton. const state* right_; ///< State from the right automaton.
mutable unsigned count_; mutable unsigned count_;
fixed_size_pool* pool_;