[buddy] Reduce the size of bddNode to improve cache efficiency.
The unicity table was mixed with the bddNode table for now apparent reason. After the hash of some node is computed, bddnodes[hash] did only contain some random node (not the one looked for) whose .hash member would point to the actual node with this hash. So that's a two step lookup. With this patch, we sill have a two step lookup, but the .hash member have been moved to a separate array. A consequence is that bddNode is now 16-byte long (instead of 20) so it will never span across two cache lines. * src/kernel.h (bddNode): Remove the hash member, and move it... (bddhash): ... as this new separate table. * src/kernel.c, src/reorder.c: Adjust all code.
This commit is contained in:
parent
96c436e0e2
commit
e7a46e10e2
4 changed files with 75 additions and 43 deletions
|
|
@ -1,3 +1,20 @@
|
||||||
|
2012-06-08 Alexandre Duret-Lutz <adl@lrde.epita.fr>
|
||||||
|
|
||||||
|
Reduce the size of bddNode to improve cache efficiency.
|
||||||
|
|
||||||
|
The unicity table was mixed with the bddNode table for now
|
||||||
|
apparent reason. After the hash of some node is computed,
|
||||||
|
bddnodes[hash] did only contain some random node (not the one
|
||||||
|
looked for) whose .hash member would point to the actual node with
|
||||||
|
this hash. So that's a two step lookup. With this patch, we sill
|
||||||
|
have a two step lookup, but the .hash member have been moved to a
|
||||||
|
separate array. A consequence is that bddNode is now 16-byte long
|
||||||
|
(instead of 20) so it will never span across two cache lines.
|
||||||
|
|
||||||
|
* src/kernel.hh (bddNode): Remove the hash member, and move it...
|
||||||
|
(bddhash): ... as this new separate table.
|
||||||
|
* src/kernel.cc, src/reorder.cc: Adjust all code.
|
||||||
|
|
||||||
2012-06-19 Alexandre Duret-Lutz <adl@lrde.epita.fr>
|
2012-06-19 Alexandre Duret-Lutz <adl@lrde.epita.fr>
|
||||||
|
|
||||||
Adjust parser construction to support Automake 1.11 and 1.12.
|
Adjust parser construction to support Automake 1.11 and 1.12.
|
||||||
|
|
|
||||||
|
|
@ -90,6 +90,7 @@ int bddnodesize; /* Number of allocated nodes */
|
||||||
int bddmaxnodesize; /* Maximum allowed number of nodes */
|
int bddmaxnodesize; /* Maximum allowed number of nodes */
|
||||||
int bddmaxnodeincrease; /* Max. # of nodes used to inc. table */
|
int bddmaxnodeincrease; /* Max. # of nodes used to inc. table */
|
||||||
BddNode* bddnodes; /* All of the bdd nodes */
|
BddNode* bddnodes; /* All of the bdd nodes */
|
||||||
|
int* bddhash; /* Unicity hash table */
|
||||||
int bddfreepos; /* First free node */
|
int bddfreepos; /* First free node */
|
||||||
int bddfreenum; /* Number of free nodes */
|
int bddfreenum; /* Number of free nodes */
|
||||||
long int bddproduced; /* Number of new nodes ever produced */
|
long int bddproduced; /* Number of new nodes ever produced */
|
||||||
|
|
@ -183,13 +184,18 @@ int bdd_init(int initnodesize, int cs)
|
||||||
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)
|
||||||
|
{
|
||||||
|
free(bddnodes);
|
||||||
|
return bdd_error(BDD_MEMORY);
|
||||||
|
}
|
||||||
|
|
||||||
bddresized = 0;
|
bddresized = 0;
|
||||||
|
|
||||||
for (n=0 ; n<bddnodesize ; n++)
|
for (n=0 ; n<bddnodesize ; n++)
|
||||||
{
|
{
|
||||||
bddnodes[n].refcou = 0;
|
bddnodes[n].refcou = 0;
|
||||||
LOW(n) = -1;
|
LOW(n) = -1;
|
||||||
bddnodes[n].hash = 0;
|
|
||||||
LEVEL(n) = 0;
|
LEVEL(n) = 0;
|
||||||
bddnodes[n].next = n+1;
|
bddnodes[n].next = n+1;
|
||||||
}
|
}
|
||||||
|
|
@ -1018,8 +1024,8 @@ static void bdd_gbc_rehash(void)
|
||||||
register unsigned int hash;
|
register unsigned int hash;
|
||||||
|
|
||||||
hash = NODEHASH(LEVELp(node), LOWp(node), HIGHp(node));
|
hash = NODEHASH(LEVELp(node), LOWp(node), HIGHp(node));
|
||||||
node->next = bddnodes[hash].hash;
|
node->next = bddhash[hash];
|
||||||
bddnodes[hash].hash = n;
|
bddhash[hash] = n;
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
{
|
{
|
||||||
|
|
@ -1055,9 +1061,10 @@ void bdd_gbc(void)
|
||||||
{
|
{
|
||||||
if (bddnodes[n].refcou > 0)
|
if (bddnodes[n].refcou > 0)
|
||||||
bdd_mark(n);
|
bdd_mark(n);
|
||||||
bddnodes[n].hash = 0;
|
|
||||||
}
|
}
|
||||||
|
|
||||||
|
memset(bddhash, 0, bddnodesize*sizeof(*bddhash));
|
||||||
|
|
||||||
bddfreepos = 0;
|
bddfreepos = 0;
|
||||||
bddfreenum = 0;
|
bddfreenum = 0;
|
||||||
|
|
||||||
|
|
@ -1071,8 +1078,8 @@ void bdd_gbc(void)
|
||||||
|
|
||||||
LEVELp(node) &= MARKOFF;
|
LEVELp(node) &= MARKOFF;
|
||||||
hash = NODEHASH(LEVELp(node), LOWp(node), HIGHp(node));
|
hash = NODEHASH(LEVELp(node), LOWp(node), HIGHp(node));
|
||||||
node->next = bddnodes[hash].hash;
|
node->next = bddhash[hash];
|
||||||
bddnodes[hash].hash = n;
|
bddhash[hash] = n;
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
{
|
{
|
||||||
|
|
@ -1313,7 +1320,7 @@ int bdd_makenode(unsigned int level, int low, int high)
|
||||||
|
|
||||||
/* Try to find an existing node of this kind */
|
/* Try to find an existing node of this kind */
|
||||||
hash = NODEHASH(level, low, high);
|
hash = NODEHASH(level, low, high);
|
||||||
res = bddnodes[hash].hash;
|
res = bddhash[hash];
|
||||||
|
|
||||||
while(res != 0)
|
while(res != 0)
|
||||||
{
|
{
|
||||||
|
|
@ -1378,8 +1385,8 @@ int bdd_makenode(unsigned int level, int low, int high)
|
||||||
HIGHp(node) = high;
|
HIGHp(node) = high;
|
||||||
|
|
||||||
/* Insert node */
|
/* Insert node */
|
||||||
node->next = bddnodes[hash].hash;
|
node->next = bddhash[hash];
|
||||||
bddnodes[hash].hash = res;
|
bddhash[hash] = res;
|
||||||
|
|
||||||
return res;
|
return res;
|
||||||
}
|
}
|
||||||
|
|
@ -1412,14 +1419,26 @@ 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
|
||||||
|
the new bddhash should fit easily in the area freed by the old
|
||||||
|
bddnode. */
|
||||||
if (doRehash)
|
if (doRehash)
|
||||||
for (n=0 ; n<oldsize ; n++)
|
{
|
||||||
bddnodes[n].hash = 0;
|
free(bddhash);
|
||||||
|
if ((bddhash=(int*)calloc(bddnodesize, sizeof(*bddhash))) == NULL)
|
||||||
|
return bdd_error(BDD_MEMORY);
|
||||||
|
}
|
||||||
|
else
|
||||||
|
{
|
||||||
|
bddhash = (int*)realloc(bddhash, sizeof(*bddhash)*bddnodesize);
|
||||||
|
if (bddhash == NULL)
|
||||||
|
return bdd_error(BDD_MEMORY);
|
||||||
|
memset(bddhash + oldsize, 0, (bddnodesize-oldsize)*sizeof(*bddhash));
|
||||||
|
}
|
||||||
|
|
||||||
for (n=oldsize ; n<bddnodesize ; n++)
|
for (n=oldsize ; n<bddnodesize ; n++)
|
||||||
{
|
{
|
||||||
bddnodes[n].refcou = 0;
|
bddnodes[n].refcou = 0;
|
||||||
bddnodes[n].hash = 0;
|
|
||||||
LEVEL(n) = 0;
|
LEVEL(n) = 0;
|
||||||
LOW(n) = -1;
|
LOW(n) = -1;
|
||||||
bddnodes[n].next = n+1;
|
bddnodes[n].next = n+1;
|
||||||
|
|
|
||||||
|
|
@ -96,7 +96,6 @@ typedef struct s_BddNode /* Node table entry */
|
||||||
unsigned int level : 22;
|
unsigned int level : 22;
|
||||||
int low;
|
int low;
|
||||||
int high;
|
int high;
|
||||||
int hash;
|
|
||||||
int next;
|
int next;
|
||||||
} BddNode;
|
} BddNode;
|
||||||
|
|
||||||
|
|
@ -113,6 +112,7 @@ extern int bddnodesize; /* Number of allocated nodes */
|
||||||
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 */
|
||||||
|
extern int* bddhash; /* Unicity hash table */
|
||||||
extern int bddvarnum; /* Number of defined BDD variables */
|
extern int bddvarnum; /* Number of defined BDD variables */
|
||||||
extern int* bddrefstack; /* Internal node reference stack */
|
extern int* bddrefstack; /* Internal node reference stack */
|
||||||
extern int* bddrefstacktop; /* Internal node reference stack top */
|
extern int* bddrefstacktop; /* Internal node reference stack top */
|
||||||
|
|
|
||||||
|
|
@ -902,14 +902,11 @@ static int mark_roots(void)
|
||||||
|
|
||||||
addDependencies(dep);
|
addDependencies(dep);
|
||||||
}
|
}
|
||||||
|
|
||||||
/* Make sure the hash field is empty. This saves a loop in the
|
|
||||||
initial GBC */
|
|
||||||
node->hash = 0;
|
|
||||||
}
|
}
|
||||||
|
|
||||||
bddnodes[0].hash = 0;
|
/* Make sure the hash is empty. This saves a loop in the initial
|
||||||
bddnodes[1].hash = 0;
|
GBC */
|
||||||
|
memset(bddhash, 0, bddnodesize*sizeof(*bddhash));
|
||||||
|
|
||||||
free(dep);
|
free(dep);
|
||||||
return 0;
|
return 0;
|
||||||
|
|
@ -938,8 +935,8 @@ static void reorder_gbc(void)
|
||||||
register unsigned int hash;
|
register unsigned int hash;
|
||||||
|
|
||||||
hash = NODEHASH(VARp(node), LOWp(node), HIGHp(node));
|
hash = NODEHASH(VARp(node), LOWp(node), HIGHp(node));
|
||||||
node->next = bddnodes[hash].hash;
|
node->next = bddhash[hash];
|
||||||
bddnodes[hash].hash = n;
|
bddhash[hash] = n;
|
||||||
|
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
|
|
@ -987,8 +984,7 @@ static void reorder_rehashAll(void)
|
||||||
reorder_setLevellookup();
|
reorder_setLevellookup();
|
||||||
bddfreepos = 0;
|
bddfreepos = 0;
|
||||||
|
|
||||||
for (n=bddnodesize-1 ; n>=0 ; n--)
|
memset(bddhash, 0, sizeof(*bddhash)*bddnodesize);
|
||||||
bddnodes[n].hash = 0;
|
|
||||||
|
|
||||||
for (n=bddnodesize-1 ; n>=2 ; n--)
|
for (n=bddnodesize-1 ; n>=2 ; n--)
|
||||||
{
|
{
|
||||||
|
|
@ -999,8 +995,8 @@ static void reorder_rehashAll(void)
|
||||||
register unsigned int hash;
|
register unsigned int hash;
|
||||||
|
|
||||||
hash = NODEHASH(VARp(node), LOWp(node), HIGHp(node));
|
hash = NODEHASH(VARp(node), LOWp(node), HIGHp(node));
|
||||||
node->next = bddnodes[hash].hash;
|
node->next = bddhash[hash];
|
||||||
bddnodes[hash].hash = n;
|
bddhash[hash] = n;
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
{
|
{
|
||||||
|
|
@ -1038,7 +1034,7 @@ static int reorder_makenode(int var, int low, int high)
|
||||||
|
|
||||||
/* Try to find an existing node of this kind */
|
/* Try to find an existing node of this kind */
|
||||||
hash = NODEHASH(var, low, high);
|
hash = NODEHASH(var, low, high);
|
||||||
res = bddnodes[hash].hash;
|
res = bddhash[hash];
|
||||||
|
|
||||||
while(res != 0)
|
while(res != 0)
|
||||||
{
|
{
|
||||||
|
|
@ -1097,8 +1093,8 @@ static int reorder_makenode(int var, int low, int high)
|
||||||
HIGHp(node) = high;
|
HIGHp(node) = high;
|
||||||
|
|
||||||
/* Insert node in hash chain */
|
/* Insert node in hash chain */
|
||||||
node->next = bddnodes[hash].hash;
|
node->next = bddhash[hash];
|
||||||
bddnodes[hash].hash = res;
|
bddhash[hash] = res;
|
||||||
|
|
||||||
/* Make sure it is reference counted */
|
/* Make sure it is reference counted */
|
||||||
node->refcou = 1;
|
node->refcou = 1;
|
||||||
|
|
@ -1128,8 +1124,8 @@ static int reorder_downSimple(int var0)
|
||||||
{
|
{
|
||||||
int r;
|
int r;
|
||||||
|
|
||||||
r = bddnodes[n + vl0].hash;
|
r = bddhash[n + vl0];
|
||||||
bddnodes[n + vl0].hash = 0;
|
bddhash[n + vl0] = 0;
|
||||||
|
|
||||||
while (r != 0)
|
while (r != 0)
|
||||||
{
|
{
|
||||||
|
|
@ -1139,8 +1135,8 @@ static int reorder_downSimple(int var0)
|
||||||
if (VAR(LOWp(node)) != var1 && VAR(HIGHp(node)) != var1)
|
if (VAR(LOWp(node)) != var1 && VAR(HIGHp(node)) != var1)
|
||||||
{
|
{
|
||||||
/* Node does not depend on next var, let it stay in the chain */
|
/* Node does not depend on next var, let it stay in the chain */
|
||||||
node->next = bddnodes[n+vl0].hash;
|
node->next = bddhash[n+vl0];
|
||||||
bddnodes[n+vl0].hash = r;
|
bddhash[n+vl0] = r;
|
||||||
levels[var0].nodenum++;
|
levels[var0].nodenum++;
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
|
|
@ -1219,8 +1215,8 @@ static void reorder_swap(int toBeProcessed, int var0)
|
||||||
|
|
||||||
/* Rehash the node since it got new childs */
|
/* Rehash the node since it got new childs */
|
||||||
hash = NODEHASH(VARp(node), LOWp(node), HIGHp(node));
|
hash = NODEHASH(VARp(node), LOWp(node), HIGHp(node));
|
||||||
node->next = bddnodes[hash].hash;
|
node->next = bddhash[hash];
|
||||||
bddnodes[hash].hash = toBeProcessed;
|
bddhash[hash] = toBeProcessed;
|
||||||
|
|
||||||
toBeProcessed = next;
|
toBeProcessed = next;
|
||||||
}
|
}
|
||||||
|
|
@ -1241,8 +1237,8 @@ static void reorder_localGbc(int var0)
|
||||||
for (n=0 ; n<size1 ; n++)
|
for (n=0 ; n<size1 ; n++)
|
||||||
{
|
{
|
||||||
int hash = n+vl1;
|
int hash = n+vl1;
|
||||||
int r = bddnodes[hash].hash;
|
int r = bddhash[hash];
|
||||||
bddnodes[hash].hash = 0;
|
bddhash[hash] = 0;
|
||||||
|
|
||||||
while (r)
|
while (r)
|
||||||
{
|
{
|
||||||
|
|
@ -1251,8 +1247,8 @@ static void reorder_localGbc(int var0)
|
||||||
|
|
||||||
if (node->refcou > 0)
|
if (node->refcou > 0)
|
||||||
{
|
{
|
||||||
node->next = bddnodes[hash].hash;
|
node->next = bddhash[hash];
|
||||||
bddnodes[hash].hash = r;
|
bddhash[hash] = r;
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
{
|
{
|
||||||
|
|
@ -1343,8 +1339,8 @@ static void reorder_localGbcResize(int toBeProcessed, int var0)
|
||||||
for (n=0 ; n<size1 ; n++)
|
for (n=0 ; n<size1 ; n++)
|
||||||
{
|
{
|
||||||
int hash = n+vl1;
|
int hash = n+vl1;
|
||||||
int r = bddnodes[hash].hash;
|
int r = bddhash[hash];
|
||||||
bddnodes[hash].hash = 0;
|
bddhash[hash] = 0;
|
||||||
|
|
||||||
while (r)
|
while (r)
|
||||||
{
|
{
|
||||||
|
|
@ -1388,8 +1384,8 @@ static void reorder_localGbcResize(int toBeProcessed, int var0)
|
||||||
int next = node->next;
|
int next = node->next;
|
||||||
int hash = NODEHASH(VARp(node), LOWp(node), HIGHp(node));
|
int hash = NODEHASH(VARp(node), LOWp(node), HIGHp(node));
|
||||||
|
|
||||||
node->next = bddnodes[hash].hash;
|
node->next = bddhash[hash];
|
||||||
bddnodes[hash].hash = toBeProcessed;
|
bddhash[hash] = toBeProcessed;
|
||||||
|
|
||||||
toBeProcessed = next;
|
toBeProcessed = next;
|
||||||
}
|
}
|
||||||
|
|
@ -1420,7 +1416,7 @@ static void sanitycheck(void)
|
||||||
|
|
||||||
for (n=0 ; n<levels[v].size ; n++)
|
for (n=0 ; n<levels[v].size ; n++)
|
||||||
{
|
{
|
||||||
r = bddnodes[n+levels[v].start].hash;
|
r = bddhash[n+levels[v].start];
|
||||||
|
|
||||||
while (r)
|
while (r)
|
||||||
{
|
{
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue