add a pool allocator for STL containers
* spot/priv/allocator.hh, spot/priv/Makefile.am: add a STL-compliant allocator based on spot::fixed_size_pool * spot/misc/fixpool.hh, spot/misc/fixpool.cc, spot/misc/Makefile.am: refactor the existing spot::fixed_size_pool * spot/ltsmin/ltsmin.cc, spot/twa/twaproduct.cc: reflect changes in the interface of spot::fixed_size_pool * tests/core/mempool.cc: test the new allocator
This commit is contained in:
parent
3fe74f1cb9
commit
c9131aee72
8 changed files with 258 additions and 21 deletions
|
|
@ -109,7 +109,7 @@ namespace spot
|
||||||
{
|
{
|
||||||
if (--count)
|
if (--count)
|
||||||
return;
|
return;
|
||||||
pool->deallocate(this);
|
pool->deallocate(const_cast<spins_state*>(this));
|
||||||
}
|
}
|
||||||
|
|
||||||
size_t hash() const override
|
size_t hash() const override
|
||||||
|
|
|
||||||
|
|
@ -1,5 +1,5 @@
|
||||||
## -*- coding: utf-8 -*-
|
## -*- coding: utf-8 -*-
|
||||||
## Copyright (C) 2011, 2012, 2013, 2014, 2016, 2018 Laboratoire de Recherche
|
## Copyright (C) 2011, 2012, 2013, 2014, 2016-2018 Laboratoire de Recherche
|
||||||
## et Développement de l'Epita (LRDE).
|
## et Développement de l'Epita (LRDE).
|
||||||
## Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de
|
## Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de
|
||||||
## Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
|
## Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
|
||||||
|
|
@ -64,6 +64,7 @@ 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 \
|
||||||
|
|
|
||||||
112
spot/misc/fixpool.cc
Normal file
112
spot/misc/fixpool.cc
Normal file
|
|
@ -0,0 +1,112 @@
|
||||||
|
// -*- 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)
|
||||||
|
{}
|
||||||
|
}
|
||||||
|
|
@ -1,5 +1,5 @@
|
||||||
// -*- coding: utf-8 -*-
|
// -*- coding: utf-8 -*-
|
||||||
// Copyright (C) 2011, 2015, 2016, 2018 Laboratoire de Recherche et
|
// Copyright (C) 2011, 2015-2018 Laboratoire de Recherche et
|
||||||
// Développement de l'Epita (LRDE)
|
// Développement de l'Epita (LRDE)
|
||||||
//
|
//
|
||||||
// This file is part of Spot, a model checking library.
|
// This file is part of Spot, a model checking library.
|
||||||
|
|
@ -27,20 +27,12 @@
|
||||||
|
|
||||||
namespace spot
|
namespace spot
|
||||||
{
|
{
|
||||||
|
|
||||||
/// A fixed-size memory pool implementation.
|
/// A fixed-size memory pool implementation.
|
||||||
class 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);
|
||||||
: freelist_(nullptr), free_start_(nullptr),
|
|
||||||
free_end_(nullptr), chunklist_(nullptr)
|
|
||||||
{
|
|
||||||
const size_t alignement = 2 * sizeof(size_t);
|
|
||||||
size_ = ((size >= sizeof(block_) ? size : sizeof(block_))
|
|
||||||
+ alignement - 1) & ~(alignement - 1);
|
|
||||||
}
|
|
||||||
|
|
||||||
/// Free any memory allocated by this pool.
|
/// Free any memory allocated by this pool.
|
||||||
~fixed_size_pool()
|
~fixed_size_pool()
|
||||||
|
|
@ -48,7 +40,7 @@ namespace spot
|
||||||
while (chunklist_)
|
while (chunklist_)
|
||||||
{
|
{
|
||||||
chunk_* prev = chunklist_->prev;
|
chunk_* prev = chunklist_->prev;
|
||||||
free(chunklist_);
|
::operator delete(chunklist_);
|
||||||
chunklist_ = prev;
|
chunklist_ = prev;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
@ -78,9 +70,7 @@ namespace spot
|
||||||
if (free_start_ + size_ > free_end_)
|
if (free_start_ + size_ > free_end_)
|
||||||
{
|
{
|
||||||
const size_t requested = (size_ > 128 ? size_ : 128) * 8192 - 64;
|
const size_t requested = (size_ > 128 ? size_ : 128) * 8192 - 64;
|
||||||
chunk_* c = reinterpret_cast<chunk_*>(malloc(requested));
|
chunk_* c = reinterpret_cast<chunk_*>(::operator new(requested));
|
||||||
if (!c)
|
|
||||||
throw std::bad_alloc();
|
|
||||||
c->prev = chunklist_;
|
c->prev = chunklist_;
|
||||||
chunklist_ = c;
|
chunklist_ = c;
|
||||||
|
|
||||||
|
|
@ -103,10 +93,10 @@ namespace spot
|
||||||
/// reused by allocate as soon as possible. The memory is only
|
/// reused by allocate as soon as possible. The memory is only
|
||||||
/// freed when the pool is destroyed.
|
/// freed when the pool is destroyed.
|
||||||
void
|
void
|
||||||
deallocate (const void* ptr)
|
deallocate(void* ptr)
|
||||||
{
|
{
|
||||||
SPOT_ASSERT(ptr);
|
SPOT_ASSERT(ptr);
|
||||||
block_* b = reinterpret_cast<block_*>(const_cast<void*>(ptr));
|
block_* b = reinterpret_cast<block_*>(ptr);
|
||||||
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)
|
||||||
|
|
@ -115,11 +105,12 @@ namespace spot
|
||||||
}
|
}
|
||||||
|
|
||||||
private:
|
private:
|
||||||
size_t size_;
|
const size_t size_;
|
||||||
struct block_ { block_* next; }* freelist_;
|
struct block_ { block_* next; }* freelist_;
|
||||||
char* free_start_;
|
char* free_start_;
|
||||||
char* free_end_;
|
char* free_end_;
|
||||||
// chunk = several agglomerated blocks
|
// chunk = several agglomerated blocks
|
||||||
union chunk_ { chunk_* prev; char data_[1]; }* chunklist_;
|
union chunk_ { chunk_* prev; char data_[1]; }* chunklist_;
|
||||||
};
|
};
|
||||||
|
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -24,6 +24,7 @@ AM_CXXFLAGS = $(WARNING_CXXFLAGS)
|
||||||
noinst_LTLIBRARIES = libpriv.la
|
noinst_LTLIBRARIES = libpriv.la
|
||||||
libpriv_la_SOURCES = \
|
libpriv_la_SOURCES = \
|
||||||
accmap.hh \
|
accmap.hh \
|
||||||
|
allocator.hh \
|
||||||
bddalloc.cc \
|
bddalloc.cc \
|
||||||
bddalloc.hh \
|
bddalloc.hh \
|
||||||
freelist.cc \
|
freelist.cc \
|
||||||
|
|
|
||||||
103
spot/priv/allocator.hh
Normal file
103
spot/priv/allocator.hh
Normal file
|
|
@ -0,0 +1,103 @@
|
||||||
|
// -*- coding: utf-8 -*-
|
||||||
|
// Copyright (C) 2011, 2015-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/>.
|
||||||
|
|
||||||
|
#pragma once
|
||||||
|
|
||||||
|
#include <spot/misc/fixpool.hh>
|
||||||
|
|
||||||
|
namespace spot
|
||||||
|
{
|
||||||
|
/// An allocator to be used with STL containers.
|
||||||
|
/// It uses a spot::fixed_size_pool to handle memory.
|
||||||
|
/// It is intended to improve performance and locality of node-based
|
||||||
|
/// containers (std::{unordered}{multi}{set,map}).
|
||||||
|
/// It is geared towards efficiently allocating memory for one object at a
|
||||||
|
/// time (the nodes of the node-based containers). Larger allocations are
|
||||||
|
/// served by calling the global memory allocation mechanism (::operator new).
|
||||||
|
/// Using it for contiguous containers (such as std::vector or std::deque)
|
||||||
|
/// will be less efficient than using the default std::allocator.
|
||||||
|
///
|
||||||
|
/// Short reminder on STL concept of Allocator:
|
||||||
|
/// allocate() may throw
|
||||||
|
/// deallocate() must not throw
|
||||||
|
/// equality testing (i.e. == and !=) must not throw
|
||||||
|
/// copying allocator (constructor and assignment) must not throw
|
||||||
|
/// moving allocator (constructor and assignment) must not throw
|
||||||
|
///
|
||||||
|
/// WARNING this class is NOT thread-safe: the allocator relies on a static
|
||||||
|
/// fixed_size_pool (which is not thread-safe either).
|
||||||
|
template<class T>
|
||||||
|
class pool_allocator
|
||||||
|
{
|
||||||
|
static
|
||||||
|
fixed_size_pool&
|
||||||
|
pool()
|
||||||
|
{
|
||||||
|
static fixed_size_pool p = fixed_size_pool(sizeof(T));
|
||||||
|
return p;
|
||||||
|
}
|
||||||
|
|
||||||
|
public:
|
||||||
|
using value_type = T;
|
||||||
|
using pointer = value_type*;
|
||||||
|
using const_pointer = const value_type*;
|
||||||
|
using size_type = size_t;
|
||||||
|
|
||||||
|
constexpr pool_allocator() noexcept
|
||||||
|
{}
|
||||||
|
template<class U>
|
||||||
|
constexpr pool_allocator(const pool_allocator<U>&) noexcept
|
||||||
|
{}
|
||||||
|
|
||||||
|
template<class U>
|
||||||
|
struct rebind
|
||||||
|
{
|
||||||
|
using other = pool_allocator<U>;
|
||||||
|
};
|
||||||
|
|
||||||
|
pointer
|
||||||
|
allocate(size_type n)
|
||||||
|
{
|
||||||
|
if (SPOT_LIKELY(n == 1))
|
||||||
|
return static_cast<pointer>(pool().allocate());
|
||||||
|
else
|
||||||
|
return static_cast<pointer>(::operator new(n*sizeof(T)));
|
||||||
|
}
|
||||||
|
|
||||||
|
void
|
||||||
|
deallocate(pointer ptr, size_type n) noexcept
|
||||||
|
{
|
||||||
|
if (SPOT_LIKELY(n == 1))
|
||||||
|
pool().deallocate(static_cast<void*>(ptr));
|
||||||
|
else
|
||||||
|
::operator delete(ptr);
|
||||||
|
}
|
||||||
|
|
||||||
|
bool
|
||||||
|
operator==(const pool_allocator&) const noexcept
|
||||||
|
{
|
||||||
|
return true;
|
||||||
|
}
|
||||||
|
bool
|
||||||
|
operator!=(const pool_allocator& o) const noexcept
|
||||||
|
{
|
||||||
|
return !(this->operator==(o));
|
||||||
|
}
|
||||||
|
};
|
||||||
|
}
|
||||||
|
|
@ -46,7 +46,7 @@ namespace spot
|
||||||
return;
|
return;
|
||||||
fixed_size_pool* p = pool_;
|
fixed_size_pool* p = pool_;
|
||||||
this->~state_product();
|
this->~state_product();
|
||||||
p->deallocate(this);
|
p->deallocate(const_cast<state_product*>(this));
|
||||||
}
|
}
|
||||||
|
|
||||||
int
|
int
|
||||||
|
|
|
||||||
|
|
@ -23,6 +23,9 @@
|
||||||
|
|
||||||
#include <spot/misc/fixpool.hh>
|
#include <spot/misc/fixpool.hh>
|
||||||
#include <spot/misc/mspool.hh>
|
#include <spot/misc/mspool.hh>
|
||||||
|
#include <spot/priv/allocator.hh>
|
||||||
|
|
||||||
|
#include <set>
|
||||||
|
|
||||||
namespace
|
namespace
|
||||||
{
|
{
|
||||||
|
|
@ -154,6 +157,32 @@ int main()
|
||||||
c->incr();
|
c->incr();
|
||||||
// no delete: valgrind should find a leak
|
// no delete: valgrind should find a leak
|
||||||
}
|
}
|
||||||
|
{
|
||||||
|
std::set<int, std::less<int>, spot::pool_allocator<int>> s;
|
||||||
|
s.insert(1);
|
||||||
|
s.insert(2);
|
||||||
|
s.insert(1);
|
||||||
|
s.erase(1);
|
||||||
|
s.insert(3);
|
||||||
|
s.insert(4);
|
||||||
|
|
||||||
|
s.clear();
|
||||||
|
|
||||||
|
auto t = s;
|
||||||
|
t.insert(5);
|
||||||
|
t.insert(6);
|
||||||
|
|
||||||
|
std::swap(s, t);
|
||||||
|
|
||||||
|
s.erase(5);
|
||||||
|
s.erase(6);
|
||||||
|
|
||||||
|
if (s != t)
|
||||||
|
return 1;
|
||||||
|
else
|
||||||
|
return 0;
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
return 0;
|
return 0;
|
||||||
}
|
}
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue