diff --git a/buddy/ChangeLog b/buddy/ChangeLog index a6606d055..c5d815702 100644 --- a/buddy/ChangeLog +++ b/buddy/ChangeLog @@ -1,3 +1,20 @@ +2012-06-08 Alexandre Duret-Lutz + + 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 Adjust parser construction to support Automake 1.11 and 1.12. diff --git a/buddy/src/kernel.c b/buddy/src/kernel.c index 2869dab9e..f7a8e2de8 100644 --- a/buddy/src/kernel.c +++ b/buddy/src/kernel.c @@ -90,6 +90,7 @@ int bddnodesize; /* Number of allocated nodes */ int bddmaxnodesize; /* Maximum allowed number of nodes */ int bddmaxnodeincrease; /* Max. # of nodes used to inc. table */ BddNode* bddnodes; /* All of the bdd nodes */ +int* bddhash; /* Unicity hash table */ int bddfreepos; /* First free node */ int bddfreenum; /* Number of free nodes */ 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) return bdd_error(BDD_MEMORY); + if ((bddhash=(int*)calloc(bddnodesize, sizeof(*bddhash))) == NULL) + { + free(bddnodes); + return bdd_error(BDD_MEMORY); + } + bddresized = 0; for (n=0 ; nnext = bddnodes[hash].hash; - bddnodes[hash].hash = n; + node->next = bddhash[hash]; + bddhash[hash] = n; } else { @@ -1055,9 +1061,10 @@ void bdd_gbc(void) { if (bddnodes[n].refcou > 0) bdd_mark(n); - bddnodes[n].hash = 0; } + memset(bddhash, 0, bddnodesize*sizeof(*bddhash)); + bddfreepos = 0; bddfreenum = 0; @@ -1071,8 +1078,8 @@ void bdd_gbc(void) LEVELp(node) &= MARKOFF; hash = NODEHASH(LEVELp(node), LOWp(node), HIGHp(node)); - node->next = bddnodes[hash].hash; - bddnodes[hash].hash = n; + node->next = bddhash[hash]; + bddhash[hash] = n; } else { @@ -1313,7 +1320,7 @@ int bdd_makenode(unsigned int level, int low, int high) /* Try to find an existing node of this kind */ hash = NODEHASH(level, low, high); - res = bddnodes[hash].hash; + res = bddhash[hash]; while(res != 0) { @@ -1378,8 +1385,8 @@ int bdd_makenode(unsigned int level, int low, int high) HIGHp(node) = high; /* Insert node */ - node->next = bddnodes[hash].hash; - bddnodes[hash].hash = res; + node->next = bddhash[hash]; + bddhash[hash] = res; return res; } @@ -1412,14 +1419,26 @@ 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 (doRehash) - for (n=0 ; nhash = 0; } - bddnodes[0].hash = 0; - bddnodes[1].hash = 0; + /* Make sure the hash is empty. This saves a loop in the initial + GBC */ + memset(bddhash, 0, bddnodesize*sizeof(*bddhash)); free(dep); return 0; @@ -938,8 +935,8 @@ static void reorder_gbc(void) register unsigned int hash; hash = NODEHASH(VARp(node), LOWp(node), HIGHp(node)); - node->next = bddnodes[hash].hash; - bddnodes[hash].hash = n; + node->next = bddhash[hash]; + bddhash[hash] = n; } else @@ -987,8 +984,7 @@ static void reorder_rehashAll(void) reorder_setLevellookup(); bddfreepos = 0; - for (n=bddnodesize-1 ; n>=0 ; n--) - bddnodes[n].hash = 0; + memset(bddhash, 0, sizeof(*bddhash)*bddnodesize); for (n=bddnodesize-1 ; n>=2 ; n--) { @@ -999,8 +995,8 @@ static void reorder_rehashAll(void) register unsigned int hash; hash = NODEHASH(VARp(node), LOWp(node), HIGHp(node)); - node->next = bddnodes[hash].hash; - bddnodes[hash].hash = n; + node->next = bddhash[hash]; + bddhash[hash] = n; } else { @@ -1038,7 +1034,7 @@ static int reorder_makenode(int var, int low, int high) /* Try to find an existing node of this kind */ hash = NODEHASH(var, low, high); - res = bddnodes[hash].hash; + res = bddhash[hash]; while(res != 0) { @@ -1097,8 +1093,8 @@ static int reorder_makenode(int var, int low, int high) HIGHp(node) = high; /* Insert node in hash chain */ - node->next = bddnodes[hash].hash; - bddnodes[hash].hash = res; + node->next = bddhash[hash]; + bddhash[hash] = res; /* Make sure it is reference counted */ node->refcou = 1; @@ -1128,8 +1124,8 @@ static int reorder_downSimple(int var0) { int r; - r = bddnodes[n + vl0].hash; - bddnodes[n + vl0].hash = 0; + r = bddhash[n + vl0]; + bddhash[n + vl0] = 0; while (r != 0) { @@ -1139,8 +1135,8 @@ static int reorder_downSimple(int var0) if (VAR(LOWp(node)) != var1 && VAR(HIGHp(node)) != var1) { /* Node does not depend on next var, let it stay in the chain */ - node->next = bddnodes[n+vl0].hash; - bddnodes[n+vl0].hash = r; + node->next = bddhash[n+vl0]; + bddhash[n+vl0] = r; levels[var0].nodenum++; } else @@ -1219,8 +1215,8 @@ static void reorder_swap(int toBeProcessed, int var0) /* Rehash the node since it got new childs */ hash = NODEHASH(VARp(node), LOWp(node), HIGHp(node)); - node->next = bddnodes[hash].hash; - bddnodes[hash].hash = toBeProcessed; + node->next = bddhash[hash]; + bddhash[hash] = toBeProcessed; toBeProcessed = next; } @@ -1241,8 +1237,8 @@ static void reorder_localGbc(int var0) for (n=0 ; nrefcou > 0) { - node->next = bddnodes[hash].hash; - bddnodes[hash].hash = r; + node->next = bddhash[hash]; + bddhash[hash] = r; } else { @@ -1343,8 +1339,8 @@ static void reorder_localGbcResize(int toBeProcessed, int var0) for (n=0 ; nnext; int hash = NODEHASH(VARp(node), LOWp(node), HIGHp(node)); - node->next = bddnodes[hash].hash; - bddnodes[hash].hash = toBeProcessed; + node->next = bddhash[hash]; + bddhash[hash] = toBeProcessed; toBeProcessed = next; } @@ -1420,7 +1416,7 @@ static void sanitycheck(void) for (n=0 ; n