Commit 2e0f4ac7 authored by Thibault Allançon's avatar Thibault Allançon Committed by Thibault Allançon

WIP: strategy 1 (remove custom inner allocator)

parent f1d55251
Pipeline #18980 failed with stage
in 29 minutes and 33 seconds
......@@ -93,8 +93,11 @@ namespace spot
unsigned int size() const;
private:
// WARNING: remove memory pool for testing purposes
#if 0
fixed_size_pool<pool_type::Unsafe> p_;
multiple_size_pool msp_;
#endif
bool compress_;
const unsigned int state_size_;
void (*fn_compress_)(const int*, size_t, int*, size_t&);
......
......@@ -34,7 +34,7 @@ namespace spot
{
cspins_state_manager::cspins_state_manager(unsigned int state_size,
int compress)
: p_((state_size+2)*sizeof(int)), compress_(compress),
: /*p_((state_size+2)*sizeof(int)),*/ compress_(compress),
/* reserve one integer for the hash value and size */
state_size_(state_size),
fn_compress_(compress == 0 ? nullptr
......@@ -57,6 +57,10 @@ namespace spot
cspins_state out = nullptr;
size_t size = state_size_;
int* ref = dst;
(void)(cmp);
(void)(cmpsize);
// WARNING: disable the compress version for tests purposes only
#if 0
if (compress_)
{
size_t csize = cmpsize;
......@@ -66,7 +70,8 @@ namespace spot
out = (cspins_state) msp_.allocate((size+2)*sizeof(int));
}
else
out = (cspins_state) p_.allocate();
#endif
out = new int[size + 2];
int hash_value = 0;
memcpy(unbox_state(out), ref, size * sizeof(int));
for (unsigned int i = 0; i < state_size_; ++i)
......@@ -84,10 +89,13 @@ namespace spot
void cspins_state_manager::dealloc(cspins_state s)
{
// WARNING: disable the compress version for tests purposes only
#if 0
if (compress_)
msp_.deallocate(s, (s[1]+2)*sizeof(int));
else
p_.deallocate(s);
#endif
delete[] s;
}
unsigned int cspins_state_manager::size() const
......@@ -156,8 +164,8 @@ namespace spot
cspins_iterator::~cspins_iterator()
{
// Do not release successors states, the manager
// will do it on time.
delete[] cond_;
successors_.clear();
}
void cspins_iterator::next()
......@@ -279,7 +287,7 @@ namespace spot
cubeset_, dead_idx_, tid
};
if (SPOT_LIKELY(!recycle_[tid].empty()))
/*if (SPOT_LIKELY(!recycle_[tid].empty()))
{
auto tmp = recycle_[tid].back();
recycle_[tid].pop_back();
......@@ -287,7 +295,7 @@ namespace spot
compute_condition(p.cond, s, tid);
tmp->recycle(p);
return tmp;
}
}*/
cube cond = cubeset_.alloc();
p.cond = cond;
compute_condition(cond, s, tid);
......
......@@ -93,15 +93,6 @@ namespace spot
"error: does not match the kripkecube requirements");
}
virtual ~swarmed_deadlock_bitstate()
{
while (!todo_.empty())
{
sys_.recycle(todo_.back().it, tid_);
todo_.pop_back();
}
}
void setup()
{
tm_.start("DFS thread " + std::to_string(tid_));
......@@ -129,10 +120,11 @@ namespace spot
if (SPOT_UNLIKELY(deadlock_))
return;
todo_.pop_back();
sys_.recycle(elem.it, tid_);
map_.erase(elem.st, brick_state_hasher());
bloom_filter_.insert(state_hash_(elem.st.st));
//sys_.recycle(elem.it, tid_);
//delete elem.it;
todo_.pop_back();
}
void finalize()
......@@ -141,6 +133,15 @@ namespace spot
tm_.stop("DFS thread " + std::to_string(tid_));
}
void dealloc()
{
while (!todo_.empty())
{
delete todo_.back().it;
todo_.pop_back();
}
}
unsigned states()
{
return states_;
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment