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

* iface/dve2/dve2.cc: Use a fixed-size memory pool for dve2_state

Browse source 
instances and their variables.
This commit is contained in:
Alexandre Duret-Lutz 2011-04-03 19:13:11 +02:00
parent 3396a03818
commit 5d12152449
2 changed files with 35 additions and 18 deletions
Download patch file Download diff file Expand all files Collapse all files

5
ChangeLog
View file

@ -1,3 +1,8 @@
2011-04-03 Alexandre Duret-Lutz <adl@lrde.epita.fr>
* iface/dve2/dve2.cc: Use a fixed-size memory pool for dve2_state
instances and their variables.
2011-04-03 Alexandre Duret-Lutz <adl@lrde.epita.fr> 2011-04-03 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Add a fixed-size memory pool implementation. Add a fixed-size memory pool implementation.

48
iface/dve2/dve2.cc
View file

@ -27,8 +27,10 @@
#include <unistd.h> #include <unistd.h>
#include "misc/hashfunc.hh" #include "misc/hashfunc.hh"
#include "misc/fixpool.hh"
#include "dve2.hh" #include "dve2.hh"
namespace spot namespace spot
{ {
namespace namespace
@ -68,13 +70,8 @@ namespace spot
struct dve2_state: public state struct dve2_state: public state
{ {
int* vars; dve2_state(int s, fixed_size_pool* p)
int size; : size(s), count(1), pool(p)
mutable int count;
size_t hash_value;
dve2_state(int s)
: vars(new int[s]), size(s), count(1)
{ {
} }
@ -95,7 +92,7 @@ namespace spot
{ {
if (--count) if (--count)
return; return;
delete this; pool->deallocate(this);
} }
size_t hash() const size_t hash() const
@ -120,9 +117,14 @@ namespace spot
~dve2_state() ~dve2_state()
{ {
delete[] vars;
} }
public:
int size;
mutable unsigned count;
size_t hash_value;
fixed_size_pool* pool;
int vars[0];
}; };
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
@ -130,9 +132,10 @@ namespace spot
struct callback_context struct callback_context
{ {
typedef std::vector<dve2_state*> transitions_t; typedef std::vector<dve2_state*> transitions_t; // FIXME: Vector->List
transitions_t transitions; transitions_t transitions;
int state_size; int state_size;
fixed_size_pool* pool;
~callback_context() ~callback_context()
{ {
@ -145,7 +148,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);
dve2_state* out = new dve2_state(ctx->state_size); dve2_state* out =
new(ctx->pool->allocate()) dve2_state(ctx->state_size, ctx->pool);
memcpy(out->vars, dst, ctx->state_size * sizeof(int)); memcpy(out->vars, dst, ctx->state_size * sizeof(int));
out->compute_hash(); out->compute_hash();
ctx->transitions.push_back(out); ctx->transitions.push_back(out);
@ -504,11 +508,12 @@ namespace spot
dve2_kripke(const dve2_interface* d, bdd_dict* dict, const prop_set* ps, dve2_kripke(const dve2_interface* d, bdd_dict* dict, const prop_set* ps,
const ltl::formula* dead) const ltl::formula* dead)
: d_(d), dict_(dict), ps_(ps), state_condition_last_state_(0), : d_(d),
state_condition_last_cc_(0) state_size_(d_->get_state_variable_count()),
dict_(dict), ps_(ps),
statepool_(sizeof(dve2_state) + state_size_ * sizeof(int)),
state_condition_last_state_(0), state_condition_last_cc_(0)
{ {
state_size_ = d_->get_state_variable_count();
vname_ = new const char*[state_size_]; vname_ = new const char*[state_size_];
for (int i = 0; i < state_size_; ++i) for (int i = 0; i < state_size_; ++i)
vname_[i] = d_->get_state_variable_name(i); vname_[i] = d_->get_state_variable_name(i);
@ -563,7 +568,8 @@ namespace spot
virtual virtual
state* get_init_state() const state* get_init_state() const
{ {
dve2_state* res = new dve2_state(state_size_); fixed_size_pool* p = const_cast<fixed_size_pool*>(&statepool_);
dve2_state* res = new(p->allocate()) dve2_state(state_size_, p);
d_->get_initial_state(res->vars); d_->get_initial_state(res->vars);
res->compute_hash(); res->compute_hash();
return res; return res;
@ -622,7 +628,9 @@ namespace spot
callback_context* cc = new callback_context; callback_context* cc = new callback_context;
cc->state_size = state_size_; cc->state_size = state_size_;
int t = d_->get_successors(0, s->vars, transition_callback, cc); cc->pool = const_cast<fixed_size_pool*>(&statepool_);
int t = d_->get_successors(0, const_cast<int*>(s->vars),
transition_callback, cc);
assert((unsigned)t == cc->transitions.size()); assert((unsigned)t == cc->transitions.size());
state_condition_last_cc_ = cc; state_condition_last_cc_ = cc;
@ -667,7 +675,9 @@ namespace spot
{ {
cc = new callback_context; cc = new callback_context;
cc->state_size = state_size_; cc->state_size = state_size_;
int t = d_->get_successors(0, s->vars, transition_callback, cc); cc->pool = const_cast<fixed_size_pool*>(&statepool_);
int t = d_->get_successors(0, const_cast<int*>(s->vars),
transition_callback, cc);
assert((unsigned)t == cc->transitions.size()); assert((unsigned)t == cc->transitions.size());
// Add a self-loop to dead-states if we care about these. // Add a self-loop to dead-states if we care about these.
@ -725,6 +735,8 @@ namespace spot
bdd alive_prop; bdd alive_prop;
bdd dead_prop; bdd dead_prop;
fixed_size_pool statepool_;
// This cache is used to speedup repeated calls to state_condition() // This cache is used to speedup repeated calls to state_condition()
// and get_succ(). // and get_succ().
// If state_condition_last_state_ != 0, then state_condition_last_cond_ // If state_condition_last_state_ != 0, then state_condition_last_cond_