glu-2.2: src/calBdd/calCacheTableTwo.c Source File

00001 
00038 #include "calInt.h"
00039 
00040 
00041 /*---------------------------------------------------------------------------*/
00042 /* Constant declarations                                                     */
00043 /*---------------------------------------------------------------------------*/
00044 /* cache table management related constants */
00045 #define CACHE_TABLE_DEFAULT_SIZE_INDEX 16
00046 #define CACHE_TABLE_DEFAULT_CACHE_RATIO 4
00047 
00048 /*---------------------------------------------------------------------------*/
00049 /* Type declarations                                                         */
00050 /*---------------------------------------------------------------------------*/
00051 typedef struct CacheEntryStruct CacheEntry_t;
00052 
00053 /*---------------------------------------------------------------------------*/
00054 /* Stucture declarations                                                     */
00055 /*---------------------------------------------------------------------------*/
00056 struct CalCacheTableStruct {
00057   long numBins;
00058   int sizeIndex;
00059   CacheEntry_t *bins;
00060   int cacheRatio;
00061   long numInsertions;
00062   long numEntries;
00063   long numHits;
00064   long numLookups;
00065   long numCollisions;
00066 };
00067 
00068 struct CacheEntryStruct {
00069   CalBddNode_t *operand1;
00070   CalBddNode_t *operand2;
00071   CalBddNode_t *resultBddNode;
00072   Cal_BddId_t resultBddId;
00073   unsigned short opCode;
00074 };
00075 
00076 
00077 /*---------------------------------------------------------------------------*/
00078 /* Variable declarations                                                     */
00079 /*---------------------------------------------------------------------------*/
00080 
00081 /*---------------------------------------------------------------------------*/
00082 /* Macro declarations                                                        */
00083 /*---------------------------------------------------------------------------*/
00084 #ifdef USE_POWER_OF_2
00085 #  define CacheTableTwoDoHash(table, operand1, operand2, opCode) \
00086    (((((((CalAddress_t)(operand1)) +    ((CalAddress_t)(operand2))) / NODE_SIZE) << 2) + opCode + ((CalAddress_t)operand1 & 0x1)+ (((CalAddress_t)operand2 & 0x1)<<1)) &((table)->numBins - 1))
00087 #else
00088 #  define CacheTableTwoDoHash(table, operand1, operand2, opCode) \
00089    ((((((CalAddress_t)(operand1)) +     ((CalAddress_t)(operand2))) / NODE_SIZE) + opCode + ((CalAddress_t)operand1 & 0x1)+ ((CalAddress_t)operand2 & 0x1)) %((table)->numBins))
00090 /*(((((CalAddress_t)(operand1)) +       ((CalAddress_t)(operand2))) + opCode) &((table)->numBins - 1))
00091 ((opCode + (((CalAddress_t)(operand1)) << 1) + (((CalAddress_t)(operand2)) <<2)) &((table)->numBins - 1))
00092 ((opCode + ((((CalAddress_t)(operand1)) + ((CalAddress_t)(operand2))) )+(((CalAddress_t)operand1 & 0x1) << (table->sizeIndex-1)) + (((CalAddress_t)operand2 & 0x1) << (table->sizeIndex-2))) &((table)->numBins - 1))
00093 ((opCode + (((CalAddress_t)(operand1)) << 1) + (((CalAddress_t)(operand2)) << 2)) &((table)->numBins - 1))
00094 */
00095 #endif
00096 
00097 #define CacheTableTwoCompareCacheEntry(entry, _operand1, _operand2, _opCode)  \
00098 ((((CalBddNode_t *)(((CalAddress_t)((entry)->operand1)) & ~0x2)) == (_operand1))\
00099  &&                                                             \
00100  ((entry)->operand2 == (_operand2))\
00101  &&                                                             \
00102  ((entry)->opCode == _opCode))
00103 
00104 #define CacheResultNodeIsForwardedTo(resultBddNode, resultBddId) \
00105 { \
00106   CalBddNode_t *__resultBddNode;\
00107   __resultBddNode = CAL_BDD_POINTER(resultBddNode); \
00108   if(CalRequestNodeGetElseRequestNode(__resultBddNode) == FORWARD_FLAG){ \
00109     resultBddId = __resultBddNode->thenBddId; \
00110     resultBddNode = (CalBddNode_t*) \
00111                     (((CalAddress_t)(__resultBddNode->thenBddNode) & ~0xe)        \
00112                          ^(CAL_TAG0(resultBddNode))); \
00113   } \
00114 }
00115 
00118 /*---------------------------------------------------------------------------*/
00119 /* Static function prototypes                                                */
00120 /*---------------------------------------------------------------------------*/
00121 
00122 static void CacheTableTwoRehash(CalCacheTable_t *cacheTable, int grow);
00123 static void CacheTablePrint(CalCacheTable_t *cacheTable);
00124 
00128 /*---------------------------------------------------------------------------*/
00129 /* Definition of exported functions                                          */
00130 /*---------------------------------------------------------------------------*/
00131 
00132 
00133 /*---------------------------------------------------------------------------*/
00134 /* Definition of internal functions                                          */
00135 /*---------------------------------------------------------------------------*/
00147 CalCacheTable_t *
00148 CalCacheTableTwoInit(Cal_BddManager_t *bddManager)
00149 {
00150   CalCacheTable_t  *cacheTable;
00151   cacheTable = Cal_MemAlloc(CalCacheTable_t, 1);
00152   if (cacheTable == Cal_Nil(CalCacheTable_t)){
00153     CalBddFatalMessage("out of memory");
00154   }
00155   cacheTable->sizeIndex = CACHE_TABLE_DEFAULT_SIZE_INDEX;
00156   cacheTable->numBins = TABLE_SIZE(cacheTable->sizeIndex);
00157   cacheTable->cacheRatio = CACHE_TABLE_DEFAULT_CACHE_RATIO;
00158   cacheTable->bins = Cal_MemAlloc(CacheEntry_t, cacheTable->numBins);
00159   if(cacheTable->bins == Cal_Nil(CacheEntry_t)){
00160     CalBddFatalMessage("out of memory");
00161   }             
00162   memset((char *)cacheTable->bins, 0,
00163          cacheTable->numBins*sizeof(CacheEntry_t));
00164   cacheTable->numInsertions = 0;
00165   cacheTable->numEntries = 0;
00166   cacheTable->numHits = 0;
00167   cacheTable->numLookups = 0;
00168   cacheTable->numCollisions = 0;
00169   return cacheTable;
00170 }
00171 
00172 
00184 int
00185 CalCacheTableTwoQuit(CalCacheTable_t *cacheTable)
00186 {
00187   if(cacheTable == Cal_Nil(CalCacheTable_t))return 1;
00188   Cal_MemFree(cacheTable->bins);
00189   Cal_MemFree(cacheTable);
00190   return 0;
00191 }
00192 
00193 
00205 void
00206 CalCacheTableTwoInsert(Cal_BddManager_t *bddManager, Cal_Bdd_t f,
00207                        Cal_Bdd_t g, Cal_Bdd_t result, unsigned long
00208                        opCode, int cacheLevel)
00209 {
00210   int hashValue;
00211   CalCacheTable_t *cacheTable;
00212   CacheEntry_t *bin;
00213   CalBddNode_t *operand1Node, *operand2Node;
00214 
00215   cacheTable = bddManager->cacheTable;
00216   cacheTable->numInsertions++;
00217   hashValue = CacheTableTwoDoHash(cacheTable, CalBddGetBddNode(f),
00218                                   CalBddGetBddNode(g), opCode); 
00219 
00220   bin = cacheTable->bins + hashValue;
00221   if (bin->opCode != CAL_OP_INVALID){
00222     cacheTable->numCollisions++;
00223   }
00224   else{
00225     cacheTable->numEntries++;
00226   }
00227   
00228   bin->opCode = opCode;
00229   if ((CalAddress_t)CalBddGetBddNode(f) >
00230       (CalAddress_t)CalBddGetBddNode(g)){ 
00231     operand1Node = CalBddGetBddNode(g);
00232     operand2Node = CalBddGetBddNode(f);
00233   }
00234   else{
00235     operand1Node = CalBddGetBddNode(f);
00236     operand2Node = CalBddGetBddNode(g);
00237   }
00238   
00239   if (cacheLevel){
00240   /*
00241    * Mark this result as temporary node to be forwarded at the end of
00242    * operation. The reason we can use this tagging is because the
00243    * size of the structure is 16 bytes and we are requiring 8 or 16 byte
00244    * alignment (at least last 3 bits should be zero).
00245    */
00246     bin->operand1 = (CalBddNode_t *) (((CalAddress_t)operand1Node) | 0x2);
00247   }
00248   else {
00249     bin->operand1 = operand1Node;
00250   }
00251   bin->operand2 = operand2Node;
00252   bin->resultBddNode = CalBddGetBddNode(result);
00253   bin->resultBddId = CalBddGetBddId(result);
00254   return;
00255 }
00256 
00257   
00269 int
00270 CalCacheTableTwoLookup(Cal_BddManager_t *bddManager, Cal_Bdd_t f,
00271                        Cal_Bdd_t g, unsigned long opCode, Cal_Bdd_t
00272                        *resultBddPtr)  
00273 {
00274   int hashValue;
00275   CalCacheTable_t *cacheTable;
00276   CacheEntry_t *bin;
00277   CalBddNode_t *operand1Node, *operand2Node;
00278   
00279   cacheTable = bddManager->cacheTable;
00280   cacheTable->numLookups++;
00281   hashValue = CacheTableTwoDoHash(cacheTable, CalBddGetBddNode(f),
00282                                   CalBddGetBddNode(g), opCode); 
00283 
00284   bin = cacheTable->bins+hashValue;
00285   
00286   if ((CalAddress_t)CalBddGetBddNode(f) > (CalAddress_t)CalBddGetBddNode(g)){
00287     operand1Node = CalBddGetBddNode(g);
00288     operand2Node = CalBddGetBddNode(f);
00289   }
00290   else{
00291     operand1Node = CalBddGetBddNode(f);
00292     operand2Node = CalBddGetBddNode(g);
00293   }
00294   if (CacheTableTwoCompareCacheEntry(bin, operand1Node, operand2Node,
00295                                      opCode)){
00296     CalBddPutBddId((*resultBddPtr), bin->resultBddId);
00297     CalBddPutBddNode((*resultBddPtr), bin->resultBddNode);
00298     cacheTable->numHits++;
00299     return 1;
00300   }
00301   *resultBddPtr = bddManager->bddNull;
00302   return 0;
00303 }
00304 
00316 void
00317 CalCacheTableTwoFlush(CalCacheTable_t *cacheTable)
00318 {
00319   memset((char *)cacheTable->bins, 0,
00320          cacheTable->numBins*sizeof(CacheEntry_t));
00321   cacheTable->numEntries = 0;
00322 }
00323 
00335 int
00336 CalCacheTableTwoFlushAll(CalCacheTable_t *cacheTable)
00337 {
00338   CalCacheTableTwoFlush(cacheTable);
00339   cacheTable->numInsertions = 0;
00340   cacheTable->numCollisions = 0;
00341   cacheTable->numLookups = 0;
00342   cacheTable->numHits = 0;
00343   return 0;
00344 }
00356 void
00357 CalCacheTableTwoGCFlush(CalCacheTable_t *cacheTable)
00358 {
00359   int i;
00360   CacheEntry_t *bin = cacheTable->bins;
00361   int numBins = cacheTable->numBins;
00362   if (cacheTable->numEntries == 0) return;
00363   for (i=0; i<numBins; bin++,i++){
00364     if (bin->opCode != CAL_OP_INVALID){
00365       if (CalBddNodeIsMarked((CAL_BDD_POINTER(bin->operand1))) ||
00366           CalBddNodeIsMarked((CAL_BDD_POINTER(bin->operand2))) ||
00367           CalBddNodeIsMarked((CAL_BDD_POINTER(bin->resultBddNode)))){
00368         /* This entry needs to be freed */
00369         cacheTable->numEntries--;
00370         memset((char *)bin, 0, sizeof(CacheEntry_t));
00371       }
00372     }
00373   }
00374 }
00375 
00387 void
00388 CalCacheTableTwoRepackUpdate(CalCacheTable_t *cacheTable)
00389 {
00390   int i;
00391   CacheEntry_t *bin = cacheTable->bins;
00392   int numBins = cacheTable->numBins;
00393   
00394   for (i=0; i<numBins; bin++,i++){
00395     if (bin->opCode != CAL_OP_INVALID){
00396       if (CalBddNodeIsForwarded(CAL_BDD_POINTER(bin->operand1))){
00397         CalBddNodeForward(bin->operand1);
00398       }
00399       if (CalBddNodeIsForwarded(CAL_BDD_POINTER(bin->operand2))){
00400         CalBddNodeForward(bin->operand2);
00401       }
00402       if (CalBddNodeIsForwarded(CAL_BDD_POINTER(bin->resultBddNode))){
00403         CalBddNodeForward(bin->resultBddNode);
00404       }
00405     }
00406   }
00407 }
00408 
00420 void
00421 CalCheckCacheTableValidity(Cal_BddManager bddManager)
00422 {
00423   CalCacheTable_t *cacheTable = bddManager->cacheTable;
00424   int i;
00425   CacheEntry_t *bin = cacheTable->bins;
00426   int numBins = cacheTable->numBins;
00427   
00428   for (i=0; i<numBins; bin++,i++){
00429     if (bin->opCode != CAL_OP_INVALID){
00430       Cal_Assert(CalBddNodeIsForwarded(CAL_BDD_POINTER(bin->operand1))
00431                  == 0);
00432       Cal_Assert(CalBddNodeIsForwarded(CAL_BDD_POINTER(bin->operand2))
00433                  == 0);
00434       Cal_Assert(CalBddNodeIsForwarded(CAL_BDD_POINTER(bin->resultBddNode))
00435                  == 0);
00436     }
00437   }
00438 }
00439 
00451 void
00452 CalCacheTableTwoFixResultPointers(Cal_BddManager_t *bddManager)
00453 {
00454   CalCacheTable_t *cacheTable = bddManager->cacheTable;
00455   int i;
00456   CacheEntry_t *bin = cacheTable->bins;
00457   int numBins = cacheTable->numBins;
00458   
00459   for (i=0; i<numBins; bin++,i++){
00460     if ((CalAddress_t)bin->operand1 & 0x2){ /* If the result node is temporary
00461                                    node */
00462       CacheResultNodeIsForwardedTo(bin->resultBddNode, bin->resultBddId);
00463       bin->operand1 = (CalBddNode_t *)((CalAddress_t)bin->operand1 &
00464                                        ~0x2); /* It is no longer temporary */
00465     }
00466   }
00467 }
00468 
00469 
00470 
00482 void
00483 CalCacheTablePrint(Cal_BddManager_t *bddManager)
00484 {
00485   CacheTablePrint(bddManager->cacheTable);
00486 }
00487 
00499 void
00500 CalBddManagerGetCacheTableData(Cal_BddManager_t *bddManager,
00501                                unsigned long *cacheSize,
00502                                unsigned long *cacheEntries,
00503                                unsigned long *cacheInsertions,
00504                                unsigned long *cacheLookups,
00505                                unsigned long *cacheHits,
00506                                unsigned long *cacheCollisions)
00507 {
00508   CalCacheTable_t *cacheTable = bddManager->cacheTable;
00509   *cacheSize += cacheTable->numBins;
00510   *cacheEntries += cacheTable->numEntries;
00511   *cacheInsertions += cacheTable->numInsertions;
00512   *cacheLookups += cacheTable->numLookups;
00513   *cacheHits += cacheTable->numHits;
00514   *cacheCollisions += cacheTable->numCollisions;
00515 }
00516 
00528 void
00529 CalCacheTableRehash(Cal_BddManager_t *bddManager)
00530 {
00531   CalCacheTable_t *cacheTable = bddManager->cacheTable;
00532   if((3*cacheTable->numBins < cacheTable->cacheRatio*cacheTable->numEntries) &&
00533      (32*cacheTable->numBins <
00534       8*(bddManager->numNodes))){
00535     CacheTableTwoRehash(cacheTable, 1);
00536   }
00537 }
00550 void
00551 CalCacheTableTwoFlushAssociationId(Cal_BddManager_t *bddManager, int
00552                                    associationId)
00553 {
00554   CalCacheTable_t *cacheTable =   bddManager->cacheTable;
00555   int i;
00556   CacheEntry_t *bin;
00557   
00558   for (i=0; i < cacheTable->numBins; i++){
00559     bin = cacheTable->bins+i;
00560     if ((bin->opCode == (CAL_OP_QUANT+associationId)) ||
00561         (bin->opCode == (CAL_OP_REL_PROD+associationId)) ||
00562         (bin->opCode == (CAL_OP_VAR_SUBSTITUTE+associationId))){
00563       /* This entry needs to be freed */
00564       cacheTable->numEntries--;
00565       memset((char *)bin, 0, sizeof(CacheEntry_t));
00566     }
00567   }
00568 }
00569 
00581 unsigned long
00582 CalCacheTableMemoryConsumption(CalCacheTable_t *cacheTable)
00583 {
00584   return (unsigned long) (sizeof(cacheTable)+cacheTable->numBins*sizeof(CacheEntry_t));
00585 }
00586 
00587 /*---------------------------------------------------------------------------*/
00588 /* Definition of static functions                                            */
00589 /*---------------------------------------------------------------------------*/
00590 
00591 
00603 static void
00604 CacheTableTwoRehash(CalCacheTable_t *cacheTable,int grow)
00605 {
00606   CacheEntry_t *oldBins = cacheTable->bins;
00607   int i, hashValue;
00608   int oldNumBins = cacheTable->numBins;
00609   CacheEntry_t *bin, *newBin;
00610   
00611   
00612   if(grow){
00613     cacheTable->sizeIndex++;
00614   }
00615   else{
00616     if (cacheTable->sizeIndex <= CACHE_TABLE_DEFAULT_SIZE_INDEX){/* No need to Rehash */
00617       return;
00618     }
00619     cacheTable->sizeIndex--;
00620   }
00621 
00622   cacheTable->numBins = TABLE_SIZE(cacheTable->sizeIndex);
00623   cacheTable->bins = Cal_MemAlloc(CacheEntry_t, cacheTable->numBins);
00624   if(cacheTable->bins == Cal_Nil(CacheEntry_t)){
00625     CalBddFatalMessage("out of memory");
00626   }
00627   
00628   memset((char *)cacheTable->bins, 0, 
00629          cacheTable->numBins*sizeof(CacheEntry_t));
00630 
00631   for(i = 0; i < oldNumBins; i++){
00632       bin  = oldBins+i;
00633       if (bin->opCode == CAL_OP_INVALID) continue;
00634       hashValue = CacheTableTwoDoHash(cacheTable,
00635                                       bin->operand1,
00636                                       bin->operand2,
00637                                       bin->opCode);
00638       newBin = cacheTable->bins+hashValue;
00639       if (newBin->opCode != CAL_OP_INVALID){
00640         cacheTable->numEntries--;
00641       }
00642       newBin->opCode = bin->opCode;
00643       newBin->operand1 = bin->operand1;
00644       newBin->operand2 = bin->operand2;
00645       newBin->resultBddId = bin->resultBddId;
00646       newBin->resultBddNode = bin->resultBddNode;
00647   }
00648   Cal_MemFree(oldBins);
00649 }
00650 
00662 static void
00663 CacheTablePrint(CalCacheTable_t *cacheTable)
00664 {
00665   int i;
00666   unsigned long opCode;
00667   CacheEntry_t *bin;
00668   
00669   printf("cacheTable entries(%ld) bins(%ld)\n",
00670          cacheTable->numEntries, cacheTable->numBins);
00671   for(i = 0; i < cacheTable->numBins; i++){
00672     bin = cacheTable->bins+i;
00673     opCode = bin->opCode;
00674     if (opCode != CAL_OP_INVALID){
00675       fprintf(stdout,"Op = %s O1 = %lx, O2 = %lx RId = %d, RNode = %lx\n",
00676               ((opCode == CAL_OP_OR) ? "OR" : ((opCode == CAL_OP_AND) ? "AND" :
00677                                                ((opCode ==
00678                                                             CAL_OP_QUANT) ?
00679                                                            "QUANT" :
00680                                                            ((opCode ==
00681                                                              CAL_OP_REL_PROD)   
00682                                                             ?
00683                                                             "RELPROD"
00684                                                             :
00685                                                             "Nothing")))), 
00686               (CalAddress_t)bin->operand1,
00687               (CalAddress_t)bin->operand2, bin->resultBddId, 
00688               (CalAddress_t)bin->resultBddNode);
00689     }
00690   }
00691 }
00692 
00693 
00694 #ifdef CACHE_TABLE_TWO_TEST
00695 main(int argc, char **argv)
00696 {
00697   Cal_Bdd_t f1, f2, f3, f4, f5, result;
00698   Cal_BddManager_t *bddManager = Cal_BddManagerInit();
00699   int i;
00700   CalCacheTable_t *cacheTable;
00701   
00702   for (i=0; i<5; i++){
00703     Cal_BddManagerCreateNewVarLast(bddManager);
00704   }
00705 
00706   CalCacheTablePrint(bddManager);
00707   
00708   f1 = bddManager->varBdds[1];
00709   f2 = bddManager->varBdds[2];
00710   f3 = bddManager->varBdds[3];
00711   f4 = bddManager->varBdds[4];
00712   f5 = bddManager->varBdds[5];
00713   
00714   CalCacheTableTwoInsert(bddManager, f1, f2, f3, CAL_OP_OR, 0);
00715   CalCacheTableTwoInsert(bddManager, f3, f2, f4, CAL_OP_AND,0);
00716   CalCacheTableTwoInsert(bddManager, f3, f4, f5, CAL_OP_REL_PROD,0);
00717   /*CacheTableTwoRehash(bddManager->cacheTableArray[2], 1);*/
00718   CalCacheTablePrint(bddManager);
00719   
00720   /* Look up */
00721   CalCacheTableTwoLookup(bddManager, f3, f2, CAL_OP_AND, &result);
00722   assert(CalBddIsEqual(result, f4));
00723 
00724   CalCacheTableTwoLookup(bddManager, f3, f2, CAL_OP_OR, &result);
00725   assert(CalBddIsEqual(result, bddManager->bddNull));
00726   
00727   CalCacheTableTwoLookup(bddManager, f3, f1, CAL_OP_OR, &result);
00728   assert(CalBddIsEqual(result, bddManager->bddNull));
00729 
00730   /* Another look up */
00731   CalCacheTableTwoLookup(bddManager, f4, f3, CAL_OP_REL_PROD, &result);
00732   assert(CalBddIsEqual(result, f5));
00733 
00734   /* It will bump off the entry (f2, f2, AND, f4)*/
00735   CalCacheTableTwoInsert(bddManager, f3, f2, f1, CAL_OP_AND,0);
00736   /* Do lookup and see if that's what happened */
00737   CalCacheTableTwoLookup(bddManager, f3, f2, CAL_OP_AND, &result);
00738   assert(CalBddIsEqual(result, f1));
00739 
00740   /*
00741    * Rehashing will visit (f2, f3, AND, f4) first and then (f2, f3,
00742    * AND, f1)
00743    * Hence the we should have (f2, f3, AND, f1) in the first slot
00744    */
00745   CacheTableTwoRehash(bddManager->cacheTable, 1);
00746   CalCacheTableTwoLookup(bddManager, f3, f2, CAL_OP_AND, &result);
00747   assert(CalBddIsEqual(result, f1));
00748   Cal_BddManagerQuit(bddManager);
00749   
00750 }
00751 #endif