Commit 361b44e5 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

[buddy] use powers of two for the sizes of all hash tables

* src/bddop.c, src/bddx.h, src/cache.c, src/cache.h, src/kernel.c,
src/kernel.h, src/prime.c, src/prime.h, src/reorder.c: Use power of
two for the sizes of all hash tables, in order to reduce the amount of
divisions performed.  Also allow bddhash to be smaller than bddnodes.
parent 98e7e4e4
...@@ -261,13 +261,13 @@ static void bdd_operator_noderesize(void) ...@@ -261,13 +261,13 @@ static void bdd_operator_noderesize(void)
if (cacheratio > 0) if (cacheratio > 0)
{ {
int newcachesize = bddnodesize / cacheratio; int newcachesize = bddnodesize / cacheratio;
BddCache_resize(&applycache, newcachesize); BddCache_resize(&applycache, newcachesize);
BddCache_resize(&itecache, newcachesize); BddCache_resize(&itecache, newcachesize);
BddCache_resize(&quantcache, newcachesize); BddCache_resize(&quantcache, newcachesize);
BddCache_resize(&appexcache, newcachesize); BddCache_resize(&appexcache, newcachesize);
BddCache_resize(&replacecache, newcachesize); BddCache_resize(&replacecache, newcachesize);
BddCache_resize(&misccache, newcachesize); BddCache_resize(&misccache, newcachesize);
bddcachesize = misccache.tablesize;
} }
} }
......
...@@ -154,6 +154,7 @@ DESCR {* The fields are \\[\baselineskip] \begin{tabular}{lp{10cm}} ...@@ -154,6 +154,7 @@ DESCR {* The fields are \\[\baselineskip] \begin{tabular}{lp{10cm}}
garbage collection. \\ garbage collection. \\
{\tt varnum} & number of defined bdd variables \\ {\tt varnum} & number of defined bdd variables \\
{\tt cachesize} & number of entries in the internal caches \\ {\tt cachesize} & number of entries in the internal caches \\
{\tt hashsize} & number of entries in the node hash table \\
{\tt gbcnum} & number of garbage collections done until now {\tt gbcnum} & number of garbage collections done until now
\end{tabular} *} \end{tabular} *}
ALSO {* bdd\_stats *} ALSO {* bdd\_stats *}
...@@ -167,6 +168,7 @@ typedef struct s_bddStat ...@@ -167,6 +168,7 @@ typedef struct s_bddStat
int minfreenodes; int minfreenodes;
int varnum; int varnum;
int cachesize; int cachesize;
int hashsize;
int gbcnum; int gbcnum;
} bddStat; } bddStat;
......
...@@ -36,6 +36,7 @@ ...@@ -36,6 +36,7 @@
*************************************************************************/ *************************************************************************/
#include <stdlib.h> #include <stdlib.h>
#include <string.h> #include <string.h>
#include <limits.h>
#include "kernel.h" #include "kernel.h"
#include "cache.h" #include "cache.h"
#include "prime.h" #include "prime.h"
...@@ -50,9 +51,10 @@ void BddCache_reset(BddCache *cache) ...@@ -50,9 +51,10 @@ void BddCache_reset(BddCache *cache)
cache->table[n].i.a = -1; cache->table[n].i.a = -1;
} }
int BddCache_init(BddCache *cache, int size) int BddCache_init(BddCache *cache, int size)
{ {
size = bdd_prime_gte(size); size = bdd_nextpower(size);
if ((cache->table=NEW(BddCacheData,size)) == NULL) if ((cache->table=NEW(BddCacheData,size)) == NULL)
return bdd_error(BDD_MEMORY); return bdd_error(BDD_MEMORY);
......
...@@ -57,7 +57,7 @@ typedef union ...@@ -57,7 +57,7 @@ typedef union
typedef struct typedef struct
{ {
BddCacheData *table; BddCacheData *table;
int tablesize; int tablesize; /* a power of 2 */
} BddCache; } BddCache;
...@@ -66,7 +66,7 @@ extern void BddCache_done(BddCache *); ...@@ -66,7 +66,7 @@ extern void BddCache_done(BddCache *);
extern int BddCache_resize(BddCache *, int); extern int BddCache_resize(BddCache *, int);
extern void BddCache_reset(BddCache *); extern void BddCache_reset(BddCache *);
#define BddCache_lookup(cache, hash) (&(cache)->table[hash % (cache)->tablesize]) #define BddCache_lookup(cache, hash) (&(cache)->table[hash & ((cache)->tablesize - 1)])
#endif /* _CACHE_H */ #endif /* _CACHE_H */
......
...@@ -101,6 +101,8 @@ int* bddvar2level; /* Variable -> level table */ ...@@ -101,6 +101,8 @@ int* bddvar2level; /* Variable -> level table */
int* bddlevel2var; /* Level -> variable table */ int* bddlevel2var; /* Level -> variable table */
jmp_buf bddexception; /* Long-jump point for interrupting calc. */ jmp_buf bddexception; /* Long-jump point for interrupting calc. */
int bddresized; /* Flag indicating a resize of the nodetable */ int bddresized; /* Flag indicating a resize of the nodetable */
int bddcachesize; /* Size of the operator caches */
int bddhashsize; /* Size of the BDD node hash */
bddCacheStat bddcachestats; bddCacheStat bddcachestats;
...@@ -109,7 +111,6 @@ bddCacheStat bddcachestats; ...@@ -109,7 +111,6 @@ bddCacheStat bddcachestats;
static BDD* bddvarset; /* Set of defined BDD variables */ static BDD* bddvarset; /* Set of defined BDD variables */
static int gbcollectnum; /* Number of garbage collections */ static int gbcollectnum; /* Number of garbage collections */
static int cachesize; /* Size of the operator caches */
static long int gbcclock; /* Clock ticks used in GBC */ static long int gbcclock; /* Clock ticks used in GBC */
static int usednodes_nextreorder; /* When to do reorder next time */ static int usednodes_nextreorder; /* When to do reorder next time */
static bddinthandler err_handler; /* Error handler */ static bddinthandler err_handler; /* Error handler */
...@@ -140,7 +141,7 @@ static const char *errorstrings[BDD_ERRNUM] = ...@@ -140,7 +141,7 @@ static const char *errorstrings[BDD_ERRNUM] =
/*=== OTHER INTERNAL DEFINITIONS =======================================*/ /*=== OTHER INTERNAL DEFINITIONS =======================================*/
#define NODEHASH(lvl,l,h) (TRIPLE(lvl,l,h) % bddnodesize) #define NODEHASH(lvl,l,h) (TRIPLE(lvl,l,h) & (bddhashsize - 1))
/************************************************************************* /*************************************************************************
...@@ -179,12 +180,13 @@ int bdd_init(int initnodesize, int cs) ...@@ -179,12 +180,13 @@ int bdd_init(int initnodesize, int cs)
if (bddrunning) if (bddrunning)
return bdd_error(BDD_RUNNING); return bdd_error(BDD_RUNNING);
bddnodesize = bdd_prime_gte(initnodesize); bddnodesize = initnodesize;
if ((bddnodes=(BddNode*)malloc(sizeof(BddNode)*bddnodesize)) == NULL) if ((bddnodes=(BddNode*)malloc(sizeof(BddNode)*bddnodesize)) == NULL)
return bdd_error(BDD_MEMORY); return bdd_error(BDD_MEMORY);
if ((bddhash=(int*)calloc(bddnodesize, sizeof(*bddhash))) == NULL) bddhashsize = bdd_nextpower(bddnodesize);
if ((bddhash=(int*)calloc(bddhashsize, sizeof(*bddhash))) == NULL)
{ {
free(bddnodes); free(bddnodes);
return bdd_error(BDD_MEMORY); return bdd_error(BDD_MEMORY);
...@@ -225,7 +227,7 @@ int bdd_init(int initnodesize, int cs) ...@@ -225,7 +227,7 @@ int bdd_init(int initnodesize, int cs)
bddvarnum = 0; bddvarnum = 0;
gbcollectnum = 0; gbcollectnum = 0;
gbcclock = 0; gbcclock = 0;
cachesize = cs; bddcachesize = cs;
usednodes_nextreorder = bddnodesize; usednodes_nextreorder = bddnodesize;
bddmaxnodeincrease = DEFAULTMAXNODEINC; bddmaxnodeincrease = DEFAULTMAXNODEINC;
...@@ -736,7 +738,8 @@ void bdd_stats(bddStat *s) ...@@ -736,7 +738,8 @@ void bdd_stats(bddStat *s)
s->freenodes = bddfreenum; s->freenodes = bddfreenum;
s->minfreenodes = minfreenodes; s->minfreenodes = minfreenodes;
s->varnum = bddvarnum; s->varnum = bddvarnum;
s->cachesize = cachesize; s->cachesize = bddcachesize;
s->hashsize = bddhashsize;
s->gbcnum = gbcollectnum; s->gbcnum = gbcollectnum;
} }
...@@ -1080,7 +1083,7 @@ void bdd_gbc(void) ...@@ -1080,7 +1083,7 @@ void bdd_gbc(void)
bdd_mark(n); bdd_mark(n);
} }
memset(bddhash, 0, bddnodesize*sizeof(*bddhash)); memset(bddhash, 0, bddhashsize*sizeof(*bddhash));
bddfreepos = 0; bddfreepos = 0;
bddfreenum = 0; bddfreenum = 0;
...@@ -1361,7 +1364,7 @@ int bdd_makenode(unsigned int level, int low, int high) ...@@ -1361,7 +1364,7 @@ int bdd_makenode(unsigned int level, int low, int high)
#endif #endif
/* Any free nodes to use ? */ /* Any free nodes to use ? */
if (bddfreepos == 0) if (__unlikely(bddfreepos == 0))
{ {
if (bdderrorcond) if (bdderrorcond)
return 0; return 0;
...@@ -1413,12 +1416,13 @@ int bdd_noderesize(int doRehash) ...@@ -1413,12 +1416,13 @@ int bdd_noderesize(int doRehash)
{ {
BddNode *newnodes; BddNode *newnodes;
int oldsize = bddnodesize; int oldsize = bddnodesize;
int oldhashsize = bddhashsize;
int n; int n;
if (bddnodesize >= bddmaxnodesize && bddmaxnodesize > 0) if (bddnodesize >= bddmaxnodesize && bddmaxnodesize > 0)
return -1; return -1;
bddnodesize = bddnodesize << 1; bddnodesize <<= 1;
if (bddnodesize > oldsize + bddmaxnodeincrease) if (bddnodesize > oldsize + bddmaxnodeincrease)
bddnodesize = oldsize + bddmaxnodeincrease; bddnodesize = oldsize + bddmaxnodeincrease;
...@@ -1426,8 +1430,6 @@ int bdd_noderesize(int doRehash) ...@@ -1426,8 +1430,6 @@ int bdd_noderesize(int doRehash)
if (bddnodesize > bddmaxnodesize && bddmaxnodesize > 0) if (bddnodesize > bddmaxnodesize && bddmaxnodesize > 0)
bddnodesize = bddmaxnodesize; bddnodesize = bddmaxnodesize;
bddnodesize = bdd_prime_lte(bddnodesize);
if (resize_handler != NULL) if (resize_handler != NULL)
resize_handler(oldsize, bddnodesize); resize_handler(oldsize, bddnodesize);
...@@ -1436,21 +1438,22 @@ int bdd_noderesize(int doRehash) ...@@ -1436,21 +1438,22 @@ int bdd_noderesize(int doRehash)
return bdd_error(BDD_MEMORY); return bdd_error(BDD_MEMORY);
bddnodes = newnodes; bddnodes = newnodes;
/* An error while reallocating bddhash is very unlikely, because if (oldhashsize * 2 <= bddnodesize)
the new bddhash should fit easily in the area freed by the old bddhashsize <<= 1;
bddnode. */
if (doRehash) if (doRehash)
{ {
free(bddhash); free(bddhash);
if ((bddhash=(int*)calloc(bddnodesize, sizeof(*bddhash))) == NULL) if ((bddhash=(int*)calloc(bddhashsize, sizeof(*bddhash))) == NULL)
return bdd_error(BDD_MEMORY); return bdd_error(BDD_MEMORY);
} }
else else
{ {
bddhash = (int*)realloc(bddhash, sizeof(*bddhash)*bddnodesize); bddhash = (int*)realloc(bddhash, sizeof(*bddhash)*bddhashsize);
if (bddhash == NULL) if (bddhash == NULL)
return bdd_error(BDD_MEMORY); return bdd_error(BDD_MEMORY);
memset(bddhash + oldsize, 0, (bddnodesize-oldsize)*sizeof(*bddhash)); memset(bddhash + oldhashsize, 0,
(bddhashsize-oldhashsize)*sizeof(*bddhash));
} }
/* copy these global variables into local variables to help the /* copy these global variables into local variables to help the
......
...@@ -118,6 +118,7 @@ extern "C" { ...@@ -118,6 +118,7 @@ extern "C" {
extern int bddrunning; /* Flag - package initialized */ extern int bddrunning; /* Flag - package initialized */
extern int bdderrorcond; /* Some error condition was met */ extern int bdderrorcond; /* Some error condition was met */
extern int bddnodesize; /* Number of allocated nodes */ extern int bddnodesize; /* Number of allocated nodes */
extern int bddhashsize; /* Size of node hash tableq */
extern int bddmaxnodesize; /* Maximum allowed number of nodes */ extern int bddmaxnodesize; /* Maximum allowed number of nodes */
extern int bddmaxnodeincrease; /* Max. # of nodes used to inc. table */ extern int bddmaxnodeincrease; /* Max. # of nodes used to inc. table */
extern BddNode* bddnodes; /* All of the bdd nodes */ extern BddNode* bddnodes; /* All of the bdd nodes */
...@@ -130,6 +131,7 @@ extern int* bddlevel2var; ...@@ -130,6 +131,7 @@ extern int* bddlevel2var;
extern jmp_buf bddexception; extern jmp_buf bddexception;
extern int bddreorderdisabled; extern int bddreorderdisabled;
extern int bddresized; extern int bddresized;
extern int bddcachesize;
extern bddCacheStat bddcachestats; extern bddCacheStat bddcachestats;
/* from reorder.c */ /* from reorder.c */
......
...@@ -244,6 +244,19 @@ unsigned int bdd_prime_lte(unsigned int src) ...@@ -244,6 +244,19 @@ unsigned int bdd_prime_lte(unsigned int src)
return src; return src;
} }
unsigned int bdd_nextpower(unsigned int v)
{
v--;
v |= v >> 1;
v |= v >> 2;
v |= v >> 4;
v |= v >> 8;
v |= v >> 16;
#if INT_MAX > 0x7FFFFFFF
v |= v >> 32;
#endif
return v + 1;
}
/************************************************************************* /*************************************************************************
......
...@@ -40,6 +40,7 @@ ...@@ -40,6 +40,7 @@
unsigned int bdd_prime_gte(unsigned int src); unsigned int bdd_prime_gte(unsigned int src);
unsigned int bdd_prime_lte(unsigned int src); unsigned int bdd_prime_lte(unsigned int src);
unsigned int bdd_nextpower(unsigned int v);
#endif /* _PRIME_H */ #endif /* _PRIME_H */
......
...@@ -909,7 +909,7 @@ static int mark_roots(void) ...@@ -909,7 +909,7 @@ static int mark_roots(void)
/* Make sure the hash is empty. This saves a loop in the initial /* Make sure the hash is empty. This saves a loop in the initial
GBC */ GBC */
memset(bddhash, 0, bddnodesize*sizeof(*bddhash)); memset(bddhash, 0, bddhashsize*sizeof(*bddhash));
free(dep); free(dep);
return 0; return 0;
...@@ -960,11 +960,11 @@ static void reorder_setLevellookup(void) ...@@ -960,11 +960,11 @@ static void reorder_setLevellookup(void)
for (n=0 ; n<bddvarnum ; n++) for (n=0 ; n<bddvarnum ; n++)
{ {
#ifdef USERESIZE #ifdef USERESIZE
levels[n].maxsize = bddnodesize / bddvarnum; levels[n].maxsize = bddhashsize / bddvarnum;
levels[n].start = n * levels[n].maxsize; levels[n].start = n * levels[n].maxsize;
levels[n].size = MIN(levels[n].maxsize, (levels[n].nodenum*5)/4); levels[n].size = MIN(levels[n].maxsize, (levels[n].nodenum*5)/4);
#else #else
levels[n].maxsize = bddnodesize / bddvarnum; levels[n].maxsize = bddhashsize / bddvarnum;
levels[n].start = n * levels[n].maxsize; levels[n].start = n * levels[n].maxsize;
levels[n].size = levels[n].maxsize; levels[n].size = levels[n].maxsize;
#endif #endif
...@@ -987,7 +987,7 @@ static void reorder_rehashAll(void) ...@@ -987,7 +987,7 @@ static void reorder_rehashAll(void)
reorder_setLevellookup(); reorder_setLevellookup();
bddfreepos = 0; bddfreepos = 0;
memset(bddhash, 0, sizeof(*bddhash)*bddnodesize); memset(bddhash, 0, sizeof(*bddhash)*bddhashsize);
for (n=bddnodesize-1 ; n>=2 ; n--) for (n=bddnodesize-1 ; n>=2 ; n--)
{ {
......
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