alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

fixpool: propose alternative policy

Browse source 
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.
This commit is contained in:
Etienne Renault 2018-07-11 14:28:34 +00:00
parent fe1be20f09
commit 23edf52dd5
12 changed files with 169 additions and 169 deletions
Download patch file Download diff file Expand all files Collapse all files

12
spot/ltsmin/ltsmin.cc
View file

@ -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<pool_type::Safe>* p)
: pool(p), size(s), count(1)
{
}
@ -102,7 +102,7 @@ namespace spot
}
public:
fixed_size_pool* pool;
fixed_size_pool<pool_type::Safe>* 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<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 =
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<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);
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<pool_type::Safe> statepool_;
multiple_size_pool compstatepool_;
// This cache is used to speedup repeated calls to state_condition()

4
spot/ltsmin/spins_kripke.hh
View file

@ -94,7 +94,7 @@ namespace spot
unsigned int size() const;
private:
fixed_size_pool p_;
fixed_size_pool<pool_type::Unsafe> 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,