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

00001 
00039 #include "calInt.h"
00040 
00041 
00042 /*---------------------------------------------------------------------------*/
00043 /* Constant declarations                                                     */
00044 /*---------------------------------------------------------------------------*/
00045 
00046 /*---------------------------------------------------------------------------*/
00047 /* Type declarations                                                         */
00048 /*---------------------------------------------------------------------------*/
00049 
00050 /*---------------------------------------------------------------------------*/
00051 /* Stucture declarations                                                     */
00052 /*---------------------------------------------------------------------------*/
00053 
00054 /*---------------------------------------------------------------------------*/
00055 /* Variable declarations                                                     */
00056 /*---------------------------------------------------------------------------*/
00057 
00058 /*---------------------------------------------------------------------------*/
00059 /* Macro declarations                                                        */
00060 /*---------------------------------------------------------------------------*/
00061 
00064 /*---------------------------------------------------------------------------*/
00065 /* Static function prototypes                                                */
00066 /*---------------------------------------------------------------------------*/
00067 
00068 static int CeilLog2(int number);
00069 
00073 /*---------------------------------------------------------------------------*/
00074 /* Definition of exported functions                                          */
00075 /*---------------------------------------------------------------------------*/
00089 void
00090 Cal_BddSetGCMode(
00091   Cal_BddManager bddManager,
00092   int  gcMode)
00093 {
00094   bddManager->gcMode = gcMode;
00095 }
00096 
00097 
00109 int
00110 Cal_BddManagerGC(Cal_BddManager bddManager)
00111 {
00112   Cal_BddIndex_t index;
00113   Cal_BddId_t id;
00114   int numNodesFreed;
00115   /* unsigned long origNodes = bddManager->numNodes; */
00116   
00117   if (bddManager->numPeakNodes < (bddManager->numNodes +
00118                                   bddManager->numForwardedNodes)){
00119     bddManager->numPeakNodes = bddManager->numNodes +
00120         bddManager->numForwardedNodes ;
00121   }
00122   
00123   CalHashTableGC(bddManager, bddManager->uniqueTable[0]);
00124   for(index = 0; index < bddManager->numVars; index++){
00125     id = bddManager->indexToId[index];
00126     numNodesFreed = CalHashTableGC(bddManager, bddManager->uniqueTable[id]);
00127     bddManager->numNodes -= numNodesFreed;
00128     bddManager->numNodesFreed += numNodesFreed;
00129   }
00130   /* Free the cache entries related to unused BDD nodes */
00131   /* The assumption is that during CalHashTableGC, the freed BDD nodes
00132      are marked. However, since they are not touched after being put
00133      on the free list, the mark should be unaffected and can be used
00134      for cleaning up the cache table.
00135      */
00136   CalCacheTableTwoGCFlush(bddManager->cacheTable);
00137   bddManager->numGC++;
00138   return 0;
00139 }
00140 
00153 void
00154 Cal_BddManagerSetGCLimit(Cal_BddManager manager)
00155 {
00156   manager->uniqueTableGCLimit = ((manager->numNodes) << 1);
00157   if(manager->uniqueTableGCLimit < CAL_MIN_GC_LIMIT){
00158     manager->uniqueTableGCLimit = CAL_MIN_GC_LIMIT;
00159   }
00160   if (manager->nodeLimit && (manager->uniqueTableGCLimit >
00161                              manager->nodeLimit)){
00162     manager->uniqueTableGCLimit = manager->nodeLimit;
00163   }
00164 }
00165 
00166 /*---------------------------------------------------------------------------*/
00167 /* Definition of internal functions                                          */
00168 /*---------------------------------------------------------------------------*/
00180 void
00181 CalBddManagerGCCheck(Cal_BddManager_t * bddManager)
00182 {
00183   if (bddManager->gcMode == 0) return;
00184   if (bddManager->gcCheck > 0) return;
00185   bddManager->gcCheck = CAL_GC_CHECK;
00186   if(bddManager->numNodes > bddManager->uniqueTableGCLimit){
00187     Cal_BddManagerGC(bddManager);
00188     Cal_BddManagerSetGCLimit(bddManager);
00189   }
00190 }
00191 
00207 int
00208 CalHashTableGC(Cal_BddManager_t *bddManager, CalHashTable_t *hashTable)
00209 {
00210   CalBddNode_t *last, *next, *ptr, *thenBddNode, *elseBddNode;
00211   int i;
00212   int oldNumEntries;
00213   
00214   oldNumEntries = hashTable->numEntries;
00215   for(i = 0; i < hashTable->numBins; i++){
00216     last = NULL;
00217     ptr = hashTable->bins[i];
00218     while(ptr != Cal_Nil(CalBddNode_t)){
00219       next = CalBddNodeGetNextBddNode(ptr);
00220       if(CalBddNodeIsRefCountZero(ptr)){
00221         if (last == NULL){
00222           hashTable->bins[i] = next;
00223         }
00224         else{
00225           CalBddNodePutNextBddNode(last,next);
00226         }
00227         thenBddNode = CAL_BDD_POINTER(CalBddNodeGetThenBddNode(ptr));
00228         elseBddNode = CAL_BDD_POINTER(CalBddNodeGetElseBddNode(ptr));
00229         CalBddNodeDcrRefCount(thenBddNode);
00230         CalBddNodeDcrRefCount(elseBddNode);
00231         CalNodeManagerFreeNode(hashTable->nodeManager, ptr);
00232         /* Mark the freed node for cache table clean up */
00233         /* We have to make sure that the clean up routine is called */
00234         /* right after this function (so that the marking remains */
00235         /* valid) */
00236         CalBddNodeMark(ptr);
00237         hashTable->numEntries--;
00238       }
00239       else {
00240         last = ptr;
00241       }
00242       ptr = next;
00243     }
00244   }
00245   return oldNumEntries - hashTable->numEntries;
00246 }
00247 
00248 
00260 void
00261 CalRepackNodesAfterGC(Cal_BddManager_t *bddManager)
00262 {
00263   int index, id, numPagesRequired, packingFlag, pageNum, nodeNum;
00264   int rehashFlag = 0;
00265   int newSizeIndex, hashValue;
00266   CalNodeManager_t *nodeManager;
00267   CalHashTable_t *uniqueTableForId;
00268   CalBddNode_t *bddNode, *thenBddNode, *elseBddNode, *freeNodeList;
00269   CalBddNode_t *newNode;
00270   Cal_Bdd_t thenBdd, elseBdd;
00271   
00272   packingFlag = 0;
00273   
00274   for (index = bddManager->numVars-1; index >= 0; index--){
00275     id = bddManager->indexToId[index];
00276     uniqueTableForId = bddManager->uniqueTable[id];
00277     nodeManager = uniqueTableForId->nodeManager;
00278     if (CalBddIdNeedsRepacking(bddManager, id) == 0){
00279       if (packingFlag == 0) continue; /* nothing needs to be done */
00280       /* We just need to update the cofactors and continue; */
00281       for (pageNum=0; pageNum < nodeManager->numPages; pageNum++){
00282         for(nodeNum = 0,
00283                 bddNode = (CalBddNode_t *)nodeManager->pageList[pageNum]; 
00284             nodeNum < NUM_NODES_PER_PAGE; nodeNum++, bddNode += 1){
00285           if (CalBddNodeIsRefCountZero(bddNode) ||
00286               CalBddNodeIsForwarded(bddNode)) continue;
00287           thenBddNode = CalBddNodeGetThenBddNode(bddNode);
00288           elseBddNode = CalBddNodeGetElseBddNode(bddNode);
00289           CalBddNodeGetThenBdd(bddNode, thenBdd);
00290           CalBddNodeGetElseBdd(bddNode, elseBdd);
00291           if (CalBddIsForwarded(thenBdd)){
00292             CalBddForward(thenBdd);
00293             CalBddNodePutThenBdd(bddNode, thenBdd);
00294             rehashFlag = 1;
00295           }
00296           if (CalBddIsForwarded(elseBdd)){
00297             CalBddForward(elseBdd);
00298             CalBddNodePutElseBdd(bddNode, elseBdd);
00299             rehashFlag = 1;
00300           }
00301           Cal_Assert(!CalBddIsRefCountZero(thenBdd));
00302           Cal_Assert(!CalBddIsRefCountZero(elseBdd));
00303           Cal_Assert(bddManager->idToIndex[id] <
00304                      bddManager->idToIndex[bddNode->thenBddId]);   
00305           Cal_Assert(bddManager->idToIndex[id] < 
00306                      bddManager->idToIndex[bddNode->elseBddId]);
00307           if (rehashFlag){
00308             CalUniqueTableForIdRehashNode(uniqueTableForId, bddNode,
00309                                           thenBddNode, elseBddNode);
00310           }
00311         }
00312       }
00313       continue; /* move to next higher index */
00314     }
00315     packingFlag = 1;
00316     if ((uniqueTableForId->numBins > uniqueTableForId->numEntries) &&
00317         (uniqueTableForId->sizeIndex > HASH_TABLE_DEFAULT_SIZE_INDEX)){
00318       /* Free the old bins */
00319       Cal_MemFree(uniqueTableForId->bins);
00320       /* Create the new set of bins */
00321       newSizeIndex =
00322           CeilLog2(uniqueTableForId->numEntries/HASH_TABLE_DEFAULT_MAX_DENSITY); 
00323       if (newSizeIndex < HASH_TABLE_DEFAULT_SIZE_INDEX){
00324         newSizeIndex = HASH_TABLE_DEFAULT_SIZE_INDEX;
00325       }
00326       uniqueTableForId->sizeIndex = newSizeIndex;
00327       uniqueTableForId->numBins =  TABLE_SIZE(uniqueTableForId->sizeIndex);
00328       uniqueTableForId->maxCapacity =
00329           uniqueTableForId->numBins * HASH_TABLE_DEFAULT_MAX_DENSITY; 
00330       uniqueTableForId->bins = Cal_MemAlloc(CalBddNode_t *,
00331                                             uniqueTableForId->numBins); 
00332       if(uniqueTableForId->bins == Cal_Nil(CalBddNode_t *)){
00333         CalBddFatalMessage("out of memory");
00334       }
00335     }
00336     /* Clear the unique table bins */
00337     memset((char *)uniqueTableForId->bins, 0,
00338            uniqueTableForId->numBins*sizeof(CalBddNode_t *));
00339     numPagesRequired =
00340         uniqueTableForId->numEntries/NUM_NODES_PER_PAGE+1;
00341     /* Traverse the first numPagesRequired pages of this nodeManager */
00342     /* Create the new free list */
00343     nodeManager->freeNodeList = freeNodeList = Cal_Nil(CalBddNode_t);
00344     for (pageNum = 0; pageNum < nodeManager->numPages; pageNum++){
00345       for(nodeNum = 0,
00346               bddNode = (CalBddNode_t *)nodeManager->pageList[pageNum]; 
00347           nodeNum < NUM_NODES_PER_PAGE; nodeNum++, bddNode += 1){
00348         if(CalBddNodeIsRefCountZero(bddNode) ||
00349            CalBddNodeIsForwarded(bddNode)){
00350           if (pageNum < numPagesRequired){
00351             bddNode->nextBddNode = freeNodeList;
00352             freeNodeList = bddNode;
00353           }
00354           continue;
00355         }
00356         CalBddNodeGetThenBdd(bddNode, thenBdd);
00357         CalBddNodeGetElseBdd(bddNode, elseBdd);
00358         if (CalBddIsForwarded(thenBdd)){
00359           CalBddForward(thenBdd);
00360           CalBddNodePutThenBdd(bddNode, thenBdd);
00361         }
00362         if (CalBddIsForwarded(elseBdd)){
00363           CalBddForward(elseBdd);
00364           CalBddNodePutElseBdd(bddNode, elseBdd); 
00365         }
00366         if (pageNum < numPagesRequired){
00367           /* Simply insert the node in the unique table */
00368           hashValue = CalDoHash2(thenBdd.bddNode, elseBdd.bddNode,
00369                                  uniqueTableForId); 
00370           CalBddNodePutNextBddNode(bddNode, uniqueTableForId->bins[hashValue]);
00371           uniqueTableForId->bins[hashValue] = bddNode;
00372         }
00373         else {
00374           /* Create a new node */
00375           newNode = freeNodeList;
00376           freeNodeList = newNode->nextBddNode;
00377           newNode->thenBddNode = bddNode->thenBddNode;
00378           newNode->elseBddNode = bddNode->elseBddNode;
00379           newNode->thenBddId = bddNode->thenBddId;
00380           newNode->elseBddId = bddNode->elseBddId;
00381           newNode->nextBddNode = bddNode->nextBddNode;
00382           bddNode->elseBddNode = FORWARD_FLAG;
00383           bddNode->thenBddId = id;
00384           bddNode->thenBddNode = newNode;
00385           hashValue = CalDoHash2(thenBdd.bddNode, elseBdd.bddNode,
00386                                  uniqueTableForId); 
00387           CalBddNodePutNextBddNode(newNode, uniqueTableForId->bins[hashValue]);
00388           uniqueTableForId->bins[hashValue] = newNode;
00389         }
00390       }
00391       if (pageNum >= numPagesRequired){
00392         /* Free this page. I am assuming that there would not be any
00393            call to PageManagerAllocPage, until this function finishes */
00394         /* Also, CalPageManagerFreePage overwrites only the first field of
00395            the bdd node (the nextBddNode field), hence no relevant
00396            information is lost */
00397         CalPageManagerFreePage(nodeManager->pageManager,
00398                                nodeManager->pageList[pageNum]);
00399         nodeManager->pageList[pageNum] = 0;
00400       }
00401     }
00402 #ifdef _CAL_VERBOSE    
00403     printf("Recycled %4d pages for %3d id\n",
00404            nodeManager->numPages-numPagesRequired, id);
00405 #endif
00406     nodeManager->numPages = numPagesRequired;
00407     nodeManager->freeNodeList = freeNodeList;
00408   }
00409   /* Need to update the handles to the nodes being moved */
00410   if (bddManager->pipelineState == CREATE){
00411     /* There are some results computed in pipeline */
00412     CalBddReorderFixProvisionalNodes(bddManager);
00413   }
00414   
00415   CalCacheTableTwoRepackUpdate(bddManager->cacheTable);
00416 
00417   /* Fix the user BDDs */
00418   CalBddReorderFixUserBddPtrs(bddManager);
00419 
00420   /* Fix the association */
00421   CalReorderAssociationFix(bddManager);
00422 
00423   Cal_Assert(CalCheckAssoc(bddManager));
00424 }
00425 
00426 /*---------------------------------------------------------------------------*/
00427 /* Definition of static functions                                            */
00428 /*---------------------------------------------------------------------------*/
00429 
00441 static int
00442 CeilLog2(int  number)
00443 {
00444   int num, count;
00445   for (num=number, count=0; num > 1; num >>= 1, count++);
00446   if ((1 << count) != number) count++;
00447   return count;
00448 }