From 361b44e571ab540bbb0f66779f8cb367c040e7cb Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 24 Jul 2017 12:01:48 +0200 Subject: [PATCH] [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. --- buddy/src/bddop.c | 2 +- buddy/src/bddx.h | 2 ++ buddy/src/cache.c | 4 +++- buddy/src/cache.h | 4 ++-- buddy/src/kernel.c | 37 ++++++++++++++++++++----------------- buddy/src/kernel.h | 2 ++ buddy/src/prime.c | 13 +++++++++++++ buddy/src/prime.h | 1 + buddy/src/reorder.c | 8 ++++---- 9 files changed, 48 insertions(+), 25 deletions(-) diff --git a/buddy/src/bddop.c b/buddy/src/bddop.c index 5bd5821ee..5592ee232 100644 --- a/buddy/src/bddop.c +++ b/buddy/src/bddop.c @@ -261,13 +261,13 @@ static void bdd_operator_noderesize(void) if (cacheratio > 0) { int newcachesize = bddnodesize / cacheratio; - BddCache_resize(&applycache, newcachesize); BddCache_resize(&itecache, newcachesize); BddCache_resize(&quantcache, newcachesize); BddCache_resize(&appexcache, newcachesize); BddCache_resize(&replacecache, newcachesize); BddCache_resize(&misccache, newcachesize); + bddcachesize = misccache.tablesize; } } diff --git a/buddy/src/bddx.h b/buddy/src/bddx.h index a1d80f61c..957385b4f 100644 --- a/buddy/src/bddx.h +++ b/buddy/src/bddx.h @@ -154,6 +154,7 @@ DESCR {* The fields are \\[\baselineskip] \begin{tabular}{lp{10cm}} garbage collection. \\ {\tt varnum} & number of defined bdd variables \\ {\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 \end{tabular} *} ALSO {* bdd\_stats *} @@ -167,6 +168,7 @@ typedef struct s_bddStat int minfreenodes; int varnum; int cachesize; + int hashsize; int gbcnum; } bddStat; diff --git a/buddy/src/cache.c b/buddy/src/cache.c index 533cadd93..587c746d6 100644 --- a/buddy/src/cache.c +++ b/buddy/src/cache.c @@ -36,6 +36,7 @@ *************************************************************************/ #include #include +#include #include "kernel.h" #include "cache.h" #include "prime.h" @@ -50,9 +51,10 @@ void BddCache_reset(BddCache *cache) cache->table[n].i.a = -1; } + int BddCache_init(BddCache *cache, int size) { - size = bdd_prime_gte(size); + size = bdd_nextpower(size); if ((cache->table=NEW(BddCacheData,size)) == NULL) return bdd_error(BDD_MEMORY); diff --git a/buddy/src/cache.h b/buddy/src/cache.h index 6e17fff14..ea6c9e5f2 100644 --- a/buddy/src/cache.h +++ b/buddy/src/cache.h @@ -57,7 +57,7 @@ typedef union typedef struct { BddCacheData *table; - int tablesize; + int tablesize; /* a power of 2 */ } BddCache; @@ -66,7 +66,7 @@ extern void BddCache_done(BddCache *); extern int BddCache_resize(BddCache *, int); 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 */ diff --git a/buddy/src/kernel.c b/buddy/src/kernel.c index 5422c2d76..900ba2601 100644 --- a/buddy/src/kernel.c +++ b/buddy/src/kernel.c @@ -101,6 +101,8 @@ int* bddvar2level; /* Variable -> level table */ int* bddlevel2var; /* Level -> variable table */ jmp_buf bddexception; /* Long-jump point for interrupting calc. */ 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; @@ -109,7 +111,6 @@ bddCacheStat bddcachestats; static BDD* bddvarset; /* Set of defined BDD variables */ 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 int usednodes_nextreorder; /* When to do reorder next time */ static bddinthandler err_handler; /* Error handler */ @@ -140,7 +141,7 @@ static const char *errorstrings[BDD_ERRNUM] = /*=== 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) if (bddrunning) return bdd_error(BDD_RUNNING); - bddnodesize = bdd_prime_gte(initnodesize); + bddnodesize = initnodesize; if ((bddnodes=(BddNode*)malloc(sizeof(BddNode)*bddnodesize)) == NULL) 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); return bdd_error(BDD_MEMORY); @@ -225,7 +227,7 @@ int bdd_init(int initnodesize, int cs) bddvarnum = 0; gbcollectnum = 0; gbcclock = 0; - cachesize = cs; + bddcachesize = cs; usednodes_nextreorder = bddnodesize; bddmaxnodeincrease = DEFAULTMAXNODEINC; @@ -736,7 +738,8 @@ void bdd_stats(bddStat *s) s->freenodes = bddfreenum; s->minfreenodes = minfreenodes; s->varnum = bddvarnum; - s->cachesize = cachesize; + s->cachesize = bddcachesize; + s->hashsize = bddhashsize; s->gbcnum = gbcollectnum; } @@ -1080,7 +1083,7 @@ void bdd_gbc(void) bdd_mark(n); } - memset(bddhash, 0, bddnodesize*sizeof(*bddhash)); + memset(bddhash, 0, bddhashsize*sizeof(*bddhash)); bddfreepos = 0; bddfreenum = 0; @@ -1361,7 +1364,7 @@ int bdd_makenode(unsigned int level, int low, int high) #endif /* Any free nodes to use ? */ - if (bddfreepos == 0) + if (__unlikely(bddfreepos == 0)) { if (bdderrorcond) return 0; @@ -1413,12 +1416,13 @@ int bdd_noderesize(int doRehash) { BddNode *newnodes; int oldsize = bddnodesize; + int oldhashsize = bddhashsize; int n; if (bddnodesize >= bddmaxnodesize && bddmaxnodesize > 0) return -1; - bddnodesize = bddnodesize << 1; + bddnodesize <<= 1; if (bddnodesize > oldsize + bddmaxnodeincrease) bddnodesize = oldsize + bddmaxnodeincrease; @@ -1426,8 +1430,6 @@ int bdd_noderesize(int doRehash) if (bddnodesize > bddmaxnodesize && bddmaxnodesize > 0) bddnodesize = bddmaxnodesize; - bddnodesize = bdd_prime_lte(bddnodesize); - if (resize_handler != NULL) resize_handler(oldsize, bddnodesize); @@ -1436,21 +1438,22 @@ int bdd_noderesize(int doRehash) return bdd_error(BDD_MEMORY); bddnodes = newnodes; - /* An error while reallocating bddhash is very unlikely, because - the new bddhash should fit easily in the area freed by the old - bddnode. */ + if (oldhashsize * 2 <= bddnodesize) + bddhashsize <<= 1; + if (doRehash) { free(bddhash); - if ((bddhash=(int*)calloc(bddnodesize, sizeof(*bddhash))) == NULL) + if ((bddhash=(int*)calloc(bddhashsize, sizeof(*bddhash))) == NULL) return bdd_error(BDD_MEMORY); } else { - bddhash = (int*)realloc(bddhash, sizeof(*bddhash)*bddnodesize); + bddhash = (int*)realloc(bddhash, sizeof(*bddhash)*bddhashsize); if (bddhash == NULL) 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 diff --git a/buddy/src/kernel.h b/buddy/src/kernel.h index 5ed3d412e..e5525c7e5 100644 --- a/buddy/src/kernel.h +++ b/buddy/src/kernel.h @@ -118,6 +118,7 @@ extern "C" { extern int bddrunning; /* Flag - package initialized */ extern int bdderrorcond; /* Some error condition was met */ 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 bddmaxnodeincrease; /* Max. # of nodes used to inc. table */ extern BddNode* bddnodes; /* All of the bdd nodes */ @@ -130,6 +131,7 @@ extern int* bddlevel2var; extern jmp_buf bddexception; extern int bddreorderdisabled; extern int bddresized; +extern int bddcachesize; extern bddCacheStat bddcachestats; /* from reorder.c */ diff --git a/buddy/src/prime.c b/buddy/src/prime.c index 90351d67d..89f220eb3 100644 --- a/buddy/src/prime.c +++ b/buddy/src/prime.c @@ -244,6 +244,19 @@ unsigned int bdd_prime_lte(unsigned int 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; +} /************************************************************************* diff --git a/buddy/src/prime.h b/buddy/src/prime.h index 0d7693077..b70471174 100644 --- a/buddy/src/prime.h +++ b/buddy/src/prime.h @@ -40,6 +40,7 @@ unsigned int bdd_prime_gte(unsigned int src); unsigned int bdd_prime_lte(unsigned int src); +unsigned int bdd_nextpower(unsigned int v); #endif /* _PRIME_H */ diff --git a/buddy/src/reorder.c b/buddy/src/reorder.c index 139736f43..d61630801 100644 --- a/buddy/src/reorder.c +++ b/buddy/src/reorder.c @@ -909,7 +909,7 @@ static int mark_roots(void) /* Make sure the hash is empty. This saves a loop in the initial GBC */ - memset(bddhash, 0, bddnodesize*sizeof(*bddhash)); + memset(bddhash, 0, bddhashsize*sizeof(*bddhash)); free(dep); return 0; @@ -960,11 +960,11 @@ static void reorder_setLevellookup(void) for (n=0 ; n=2 ; n--) {