src/calBdd/calGC.c File Reference

#include "calInt.h"
Include dependency graph for calGC.c:

Go to the source code of this file.

Functions

static int CeilLog2 (int number)
void Cal_BddSetGCMode (Cal_BddManager bddManager, int gcMode)
int Cal_BddManagerGC (Cal_BddManager bddManager)
void Cal_BddManagerSetGCLimit (Cal_BddManager manager)
void CalBddManagerGCCheck (Cal_BddManager_t *bddManager)
int CalHashTableGC (Cal_BddManager_t *bddManager, CalHashTable_t *hashTable)
void CalRepackNodesAfterGC (Cal_BddManager_t *bddManager)

Function Documentation

int Cal_BddManagerGC ( Cal_BddManager  bddManager  ) 

Function********************************************************************

Synopsis [Invokes the garbage collection at the manager level.]

Description [For each variable in the increasing id free nodes with reference count equal to zero freeing a node results in decrementing reference count of then and else nodes by one.]

SideEffects [None.]

Definition at line 110 of file calGC.c.

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 }

void Cal_BddManagerSetGCLimit ( Cal_BddManager  manager  ) 

Function********************************************************************

Synopsis [Sets the limit of the garbage collection.]

Description [It tries to set the limit at twice the number of nodes in the manager at the current point. However, the limit is not allowed to fall below the MIN_GC_LIMIT or to exceed the value of node limit (if one exists).]

SideEffects [None.]

Definition at line 154 of file calGC.c.

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 }

void Cal_BddSetGCMode ( Cal_BddManager  bddManager,
int  gcMode 
)

AutomaticEnd Function********************************************************************

Synopsis [Sets the garbage collection mode, 0 means the garbage collection should be turned off, 1 means garbage collection should be on.]

Description [Sets the garbage collection mode, 0 means the garbage collection should be turned off, 1 means garbage collection should be on.]

SideEffects [None.]

Definition at line 90 of file calGC.c.

00093 {
00094   bddManager->gcMode = gcMode;
00095 }

void CalBddManagerGCCheck ( Cal_BddManager_t *  bddManager  ) 

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 181 of file calGC.c.

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 }

int CalHashTableGC ( Cal_BddManager_t *  bddManager,
CalHashTable_t *  hashTable 
)

Function********************************************************************

Synopsis [This function performs the garbage collection operation for a particular index.]

Description [The input is the hash table containing the nodes belonging to that level. Each bin of the hash table is traversed and the Bdd nodes with 0 reference count are put at the appropriate level in the processing que of the manager.]

SideEffects [The number of nodes in the hash table can possibly decrease.]

SeeAlso [optional]

Definition at line 208 of file calGC.c.

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 }

void CalRepackNodesAfterGC ( Cal_BddManager_t *  bddManager  ) 

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 261 of file calGC.c.

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 }

static int CeilLog2 ( int  number  )  [static]

CFile***********************************************************************

FileName [calGC.c]

PackageName [cal]

Synopsis [Garbage collection routines]

Description [optional]

SeeAlso [optional]

Author [Jagesh Sanghavi (sanghavi@eecs.berkeley.edu) Rajeev Ranjan (rajeev@eecs.berkeley.edu)]

Copyright [Copyright (c) 1994-1996 The Regents of the Univ. of California. All rights reserved.

Permission is hereby granted, without written agreement and without license or royalty fees, to use, copy, modify, and distribute this software and its documentation for any purpose, provided that the above copyright notice and the following two paragraphs appear in all copies of this software.

IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS ON AN "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]

Revision [

Id
calGC.c,v 1.2 1998/09/16 16:08:40 ravi Exp

]AutomaticStart

Function********************************************************************

Synopsis [Returns the smallest integer greater than or equal to log2 of a number]

Description [Returns the smallest integer greater than or equal to log2 of a number (The assumption is that the number is >= 1)]

SideEffects [None]

Definition at line 442 of file calGC.c.

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 }

Generated on Tue Jan 12 13:57:11 2010 for glu-2.2 by  doxygen 1.6.1