1 | /**CFile*********************************************************************** |
---|
2 | |
---|
3 | FileName [calGC.c] |
---|
4 | |
---|
5 | PackageName [cal] |
---|
6 | |
---|
7 | Synopsis [Garbage collection routines] |
---|
8 | |
---|
9 | Description [optional] |
---|
10 | |
---|
11 | SeeAlso [optional] |
---|
12 | |
---|
13 | Author [Jagesh Sanghavi (sanghavi@eecs.berkeley.edu) |
---|
14 | Rajeev Ranjan (rajeev@eecs.berkeley.edu)] |
---|
15 | |
---|
16 | Copyright [Copyright (c) 1994-1996 The Regents of the Univ. of California. |
---|
17 | All rights reserved. |
---|
18 | |
---|
19 | Permission is hereby granted, without written agreement and without license |
---|
20 | or royalty fees, to use, copy, modify, and distribute this software and its |
---|
21 | documentation for any purpose, provided that the above copyright notice and |
---|
22 | the following two paragraphs appear in all copies of this software. |
---|
23 | |
---|
24 | IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR |
---|
25 | DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT |
---|
26 | OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF |
---|
27 | CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. |
---|
28 | |
---|
29 | THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES, |
---|
30 | INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND |
---|
31 | FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS ON AN |
---|
32 | "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE |
---|
33 | MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.] |
---|
34 | |
---|
35 | Revision [$Id: calGC.c,v 1.2 1998/09/16 16:08:40 ravi Exp $] |
---|
36 | |
---|
37 | ******************************************************************************/ |
---|
38 | |
---|
39 | #include "calInt.h" |
---|
40 | |
---|
41 | |
---|
42 | /*---------------------------------------------------------------------------*/ |
---|
43 | /* Constant declarations */ |
---|
44 | /*---------------------------------------------------------------------------*/ |
---|
45 | |
---|
46 | /*---------------------------------------------------------------------------*/ |
---|
47 | /* Type declarations */ |
---|
48 | /*---------------------------------------------------------------------------*/ |
---|
49 | |
---|
50 | /*---------------------------------------------------------------------------*/ |
---|
51 | /* Stucture declarations */ |
---|
52 | /*---------------------------------------------------------------------------*/ |
---|
53 | |
---|
54 | /*---------------------------------------------------------------------------*/ |
---|
55 | /* Variable declarations */ |
---|
56 | /*---------------------------------------------------------------------------*/ |
---|
57 | |
---|
58 | /*---------------------------------------------------------------------------*/ |
---|
59 | /* Macro declarations */ |
---|
60 | /*---------------------------------------------------------------------------*/ |
---|
61 | |
---|
62 | /**AutomaticStart*************************************************************/ |
---|
63 | |
---|
64 | /*---------------------------------------------------------------------------*/ |
---|
65 | /* Static function prototypes */ |
---|
66 | /*---------------------------------------------------------------------------*/ |
---|
67 | |
---|
68 | static int CeilLog2(int number); |
---|
69 | |
---|
70 | /**AutomaticEnd***************************************************************/ |
---|
71 | |
---|
72 | |
---|
73 | /*---------------------------------------------------------------------------*/ |
---|
74 | /* Definition of exported functions */ |
---|
75 | /*---------------------------------------------------------------------------*/ |
---|
76 | /**Function******************************************************************** |
---|
77 | |
---|
78 | Synopsis [Sets the garbage collection mode, 0 means the garbage |
---|
79 | collection should be turned off, 1 means garbage collection should |
---|
80 | be on.] |
---|
81 | |
---|
82 | Description [Sets the garbage collection mode, 0 means the garbage |
---|
83 | collection should be turned off, 1 means garbage collection should |
---|
84 | be on.] |
---|
85 | |
---|
86 | SideEffects [None.] |
---|
87 | |
---|
88 | ******************************************************************************/ |
---|
89 | void |
---|
90 | Cal_BddSetGCMode( |
---|
91 | Cal_BddManager bddManager, |
---|
92 | int gcMode) |
---|
93 | { |
---|
94 | bddManager->gcMode = gcMode; |
---|
95 | } |
---|
96 | |
---|
97 | |
---|
98 | /**Function******************************************************************** |
---|
99 | |
---|
100 | Synopsis [Invokes the garbage collection at the manager level.] |
---|
101 | |
---|
102 | Description [For each variable in the increasing id free nodes with reference |
---|
103 | count equal to zero freeing a node results in decrementing reference count of |
---|
104 | then and else nodes by one.] |
---|
105 | |
---|
106 | SideEffects [None.] |
---|
107 | |
---|
108 | ******************************************************************************/ |
---|
109 | int |
---|
110 | Cal_BddManagerGC(Cal_BddManager bddManager) |
---|
111 | { |
---|
112 | Cal_BddIndex_t index; |
---|
113 | Cal_BddId_t id; |
---|
114 | int numNodesFreed; |
---|
115 | /* unsigned long origNodes = bddManager->numNodes; */ |
---|
116 | |
---|
117 | if (bddManager->numPeakNodes < (bddManager->numNodes + |
---|
118 | bddManager->numForwardedNodes)){ |
---|
119 | bddManager->numPeakNodes = bddManager->numNodes + |
---|
120 | bddManager->numForwardedNodes ; |
---|
121 | } |
---|
122 | |
---|
123 | CalHashTableGC(bddManager, bddManager->uniqueTable[0]); |
---|
124 | for(index = 0; index < bddManager->numVars; index++){ |
---|
125 | id = bddManager->indexToId[index]; |
---|
126 | numNodesFreed = CalHashTableGC(bddManager, bddManager->uniqueTable[id]); |
---|
127 | bddManager->numNodes -= numNodesFreed; |
---|
128 | bddManager->numNodesFreed += numNodesFreed; |
---|
129 | } |
---|
130 | /* Free the cache entries related to unused BDD nodes */ |
---|
131 | /* The assumption is that during CalHashTableGC, the freed BDD nodes |
---|
132 | are marked. However, since they are not touched after being put |
---|
133 | on the free list, the mark should be unaffected and can be used |
---|
134 | for cleaning up the cache table. |
---|
135 | */ |
---|
136 | CalCacheTableTwoGCFlush(bddManager->cacheTable); |
---|
137 | bddManager->numGC++; |
---|
138 | return 0; |
---|
139 | } |
---|
140 | |
---|
141 | /**Function******************************************************************** |
---|
142 | |
---|
143 | Synopsis [Sets the limit of the garbage collection.] |
---|
144 | |
---|
145 | Description [It tries to set the limit at twice the number of nodes |
---|
146 | in the manager at the current point. However, the limit is not |
---|
147 | allowed to fall below the MIN_GC_LIMIT or to exceed the value of |
---|
148 | node limit (if one exists).] |
---|
149 | |
---|
150 | SideEffects [None.] |
---|
151 | |
---|
152 | ******************************************************************************/ |
---|
153 | void |
---|
154 | Cal_BddManagerSetGCLimit(Cal_BddManager manager) |
---|
155 | { |
---|
156 | manager->uniqueTableGCLimit = ((manager->numNodes) << 1); |
---|
157 | if(manager->uniqueTableGCLimit < CAL_MIN_GC_LIMIT){ |
---|
158 | manager->uniqueTableGCLimit = CAL_MIN_GC_LIMIT; |
---|
159 | } |
---|
160 | if (manager->nodeLimit && (manager->uniqueTableGCLimit > |
---|
161 | manager->nodeLimit)){ |
---|
162 | manager->uniqueTableGCLimit = manager->nodeLimit; |
---|
163 | } |
---|
164 | } |
---|
165 | |
---|
166 | /*---------------------------------------------------------------------------*/ |
---|
167 | /* Definition of internal functions */ |
---|
168 | /*---------------------------------------------------------------------------*/ |
---|
169 | /**Function******************************************************************** |
---|
170 | |
---|
171 | Synopsis [required] |
---|
172 | |
---|
173 | Description [optional] |
---|
174 | |
---|
175 | SideEffects [required] |
---|
176 | |
---|
177 | SeeAlso [optional] |
---|
178 | |
---|
179 | ******************************************************************************/ |
---|
180 | void |
---|
181 | CalBddManagerGCCheck(Cal_BddManager_t * bddManager) |
---|
182 | { |
---|
183 | if (bddManager->gcMode == 0) return; |
---|
184 | if (bddManager->gcCheck > 0) return; |
---|
185 | bddManager->gcCheck = CAL_GC_CHECK; |
---|
186 | if(bddManager->numNodes > bddManager->uniqueTableGCLimit){ |
---|
187 | Cal_BddManagerGC(bddManager); |
---|
188 | Cal_BddManagerSetGCLimit(bddManager); |
---|
189 | } |
---|
190 | } |
---|
191 | |
---|
192 | /**Function******************************************************************** |
---|
193 | |
---|
194 | Synopsis [This function performs the garbage collection operation |
---|
195 | for a particular index.] |
---|
196 | |
---|
197 | Description [The input is the hash table containing the nodes |
---|
198 | belonging to that level. Each bin of the hash table is traversed and |
---|
199 | the Bdd nodes with 0 reference count are put at the appropriate |
---|
200 | level in the processing que of the manager.] |
---|
201 | |
---|
202 | SideEffects [The number of nodes in the hash table can possibly decrease.] |
---|
203 | |
---|
204 | SeeAlso [optional] |
---|
205 | |
---|
206 | ******************************************************************************/ |
---|
207 | int |
---|
208 | CalHashTableGC(Cal_BddManager_t *bddManager, CalHashTable_t *hashTable) |
---|
209 | { |
---|
210 | CalBddNode_t *last, *next, *ptr, *thenBddNode, *elseBddNode; |
---|
211 | int i; |
---|
212 | int oldNumEntries; |
---|
213 | |
---|
214 | oldNumEntries = hashTable->numEntries; |
---|
215 | for(i = 0; i < hashTable->numBins; i++){ |
---|
216 | last = NULL; |
---|
217 | ptr = hashTable->bins[i]; |
---|
218 | while(ptr != Cal_Nil(CalBddNode_t)){ |
---|
219 | next = CalBddNodeGetNextBddNode(ptr); |
---|
220 | if(CalBddNodeIsRefCountZero(ptr)){ |
---|
221 | if (last == NULL){ |
---|
222 | hashTable->bins[i] = next; |
---|
223 | } |
---|
224 | else{ |
---|
225 | CalBddNodePutNextBddNode(last,next); |
---|
226 | } |
---|
227 | thenBddNode = CAL_BDD_POINTER(CalBddNodeGetThenBddNode(ptr)); |
---|
228 | elseBddNode = CAL_BDD_POINTER(CalBddNodeGetElseBddNode(ptr)); |
---|
229 | CalBddNodeDcrRefCount(thenBddNode); |
---|
230 | CalBddNodeDcrRefCount(elseBddNode); |
---|
231 | CalNodeManagerFreeNode(hashTable->nodeManager, ptr); |
---|
232 | /* Mark the freed node for cache table clean up */ |
---|
233 | /* We have to make sure that the clean up routine is called */ |
---|
234 | /* right after this function (so that the marking remains */ |
---|
235 | /* valid) */ |
---|
236 | CalBddNodeMark(ptr); |
---|
237 | hashTable->numEntries--; |
---|
238 | } |
---|
239 | else { |
---|
240 | last = ptr; |
---|
241 | } |
---|
242 | ptr = next; |
---|
243 | } |
---|
244 | } |
---|
245 | return oldNumEntries - hashTable->numEntries; |
---|
246 | } |
---|
247 | |
---|
248 | |
---|
249 | /**Function******************************************************************** |
---|
250 | |
---|
251 | Synopsis [required] |
---|
252 | |
---|
253 | Description [optional] |
---|
254 | |
---|
255 | SideEffects [required] |
---|
256 | |
---|
257 | SeeAlso [optional] |
---|
258 | |
---|
259 | ******************************************************************************/ |
---|
260 | void |
---|
261 | CalRepackNodesAfterGC(Cal_BddManager_t *bddManager) |
---|
262 | { |
---|
263 | int index, id, numPagesRequired, packingFlag, pageNum, nodeNum; |
---|
264 | int rehashFlag = 0; |
---|
265 | int newSizeIndex, hashValue; |
---|
266 | CalNodeManager_t *nodeManager; |
---|
267 | CalHashTable_t *uniqueTableForId; |
---|
268 | CalBddNode_t *bddNode, *thenBddNode, *elseBddNode, *freeNodeList; |
---|
269 | CalBddNode_t *newNode; |
---|
270 | Cal_Bdd_t thenBdd, elseBdd; |
---|
271 | |
---|
272 | packingFlag = 0; |
---|
273 | |
---|
274 | for (index = bddManager->numVars-1; index >= 0; index--){ |
---|
275 | id = bddManager->indexToId[index]; |
---|
276 | uniqueTableForId = bddManager->uniqueTable[id]; |
---|
277 | nodeManager = uniqueTableForId->nodeManager; |
---|
278 | if (CalBddIdNeedsRepacking(bddManager, id) == 0){ |
---|
279 | if (packingFlag == 0) continue; /* nothing needs to be done */ |
---|
280 | /* We just need to update the cofactors and continue; */ |
---|
281 | for (pageNum=0; pageNum < nodeManager->numPages; pageNum++){ |
---|
282 | for(nodeNum = 0, |
---|
283 | bddNode = (CalBddNode_t *)nodeManager->pageList[pageNum]; |
---|
284 | nodeNum < NUM_NODES_PER_PAGE; nodeNum++, bddNode += 1){ |
---|
285 | if (CalBddNodeIsRefCountZero(bddNode) || |
---|
286 | CalBddNodeIsForwarded(bddNode)) continue; |
---|
287 | thenBddNode = CalBddNodeGetThenBddNode(bddNode); |
---|
288 | elseBddNode = CalBddNodeGetElseBddNode(bddNode); |
---|
289 | CalBddNodeGetThenBdd(bddNode, thenBdd); |
---|
290 | CalBddNodeGetElseBdd(bddNode, elseBdd); |
---|
291 | if (CalBddIsForwarded(thenBdd)){ |
---|
292 | CalBddForward(thenBdd); |
---|
293 | CalBddNodePutThenBdd(bddNode, thenBdd); |
---|
294 | rehashFlag = 1; |
---|
295 | } |
---|
296 | if (CalBddIsForwarded(elseBdd)){ |
---|
297 | CalBddForward(elseBdd); |
---|
298 | CalBddNodePutElseBdd(bddNode, elseBdd); |
---|
299 | rehashFlag = 1; |
---|
300 | } |
---|
301 | Cal_Assert(!CalBddIsRefCountZero(thenBdd)); |
---|
302 | Cal_Assert(!CalBddIsRefCountZero(elseBdd)); |
---|
303 | Cal_Assert(bddManager->idToIndex[id] < |
---|
304 | bddManager->idToIndex[bddNode->thenBddId]); |
---|
305 | Cal_Assert(bddManager->idToIndex[id] < |
---|
306 | bddManager->idToIndex[bddNode->elseBddId]); |
---|
307 | if (rehashFlag){ |
---|
308 | CalUniqueTableForIdRehashNode(uniqueTableForId, bddNode, |
---|
309 | thenBddNode, elseBddNode); |
---|
310 | } |
---|
311 | } |
---|
312 | } |
---|
313 | continue; /* move to next higher index */ |
---|
314 | } |
---|
315 | packingFlag = 1; |
---|
316 | if ((uniqueTableForId->numBins > uniqueTableForId->numEntries) && |
---|
317 | (uniqueTableForId->sizeIndex > HASH_TABLE_DEFAULT_SIZE_INDEX)){ |
---|
318 | /* Free the old bins */ |
---|
319 | Cal_MemFree(uniqueTableForId->bins); |
---|
320 | /* Create the new set of bins */ |
---|
321 | newSizeIndex = |
---|
322 | CeilLog2(uniqueTableForId->numEntries/HASH_TABLE_DEFAULT_MAX_DENSITY); |
---|
323 | if (newSizeIndex < HASH_TABLE_DEFAULT_SIZE_INDEX){ |
---|
324 | newSizeIndex = HASH_TABLE_DEFAULT_SIZE_INDEX; |
---|
325 | } |
---|
326 | uniqueTableForId->sizeIndex = newSizeIndex; |
---|
327 | uniqueTableForId->numBins = TABLE_SIZE(uniqueTableForId->sizeIndex); |
---|
328 | uniqueTableForId->maxCapacity = |
---|
329 | uniqueTableForId->numBins * HASH_TABLE_DEFAULT_MAX_DENSITY; |
---|
330 | uniqueTableForId->bins = Cal_MemAlloc(CalBddNode_t *, |
---|
331 | uniqueTableForId->numBins); |
---|
332 | if(uniqueTableForId->bins == Cal_Nil(CalBddNode_t *)){ |
---|
333 | CalBddFatalMessage("out of memory"); |
---|
334 | } |
---|
335 | } |
---|
336 | /* Clear the unique table bins */ |
---|
337 | memset((char *)uniqueTableForId->bins, 0, |
---|
338 | uniqueTableForId->numBins*sizeof(CalBddNode_t *)); |
---|
339 | numPagesRequired = |
---|
340 | uniqueTableForId->numEntries/NUM_NODES_PER_PAGE+1; |
---|
341 | /* Traverse the first numPagesRequired pages of this nodeManager */ |
---|
342 | /* Create the new free list */ |
---|
343 | nodeManager->freeNodeList = freeNodeList = Cal_Nil(CalBddNode_t); |
---|
344 | for (pageNum = 0; pageNum < nodeManager->numPages; pageNum++){ |
---|
345 | for(nodeNum = 0, |
---|
346 | bddNode = (CalBddNode_t *)nodeManager->pageList[pageNum]; |
---|
347 | nodeNum < NUM_NODES_PER_PAGE; nodeNum++, bddNode += 1){ |
---|
348 | if(CalBddNodeIsRefCountZero(bddNode) || |
---|
349 | CalBddNodeIsForwarded(bddNode)){ |
---|
350 | if (pageNum < numPagesRequired){ |
---|
351 | bddNode->nextBddNode = freeNodeList; |
---|
352 | freeNodeList = bddNode; |
---|
353 | } |
---|
354 | continue; |
---|
355 | } |
---|
356 | CalBddNodeGetThenBdd(bddNode, thenBdd); |
---|
357 | CalBddNodeGetElseBdd(bddNode, elseBdd); |
---|
358 | if (CalBddIsForwarded(thenBdd)){ |
---|
359 | CalBddForward(thenBdd); |
---|
360 | CalBddNodePutThenBdd(bddNode, thenBdd); |
---|
361 | } |
---|
362 | if (CalBddIsForwarded(elseBdd)){ |
---|
363 | CalBddForward(elseBdd); |
---|
364 | CalBddNodePutElseBdd(bddNode, elseBdd); |
---|
365 | } |
---|
366 | if (pageNum < numPagesRequired){ |
---|
367 | /* Simply insert the node in the unique table */ |
---|
368 | hashValue = CalDoHash2(thenBdd.bddNode, elseBdd.bddNode, |
---|
369 | uniqueTableForId); |
---|
370 | CalBddNodePutNextBddNode(bddNode, uniqueTableForId->bins[hashValue]); |
---|
371 | uniqueTableForId->bins[hashValue] = bddNode; |
---|
372 | } |
---|
373 | else { |
---|
374 | /* Create a new node */ |
---|
375 | newNode = freeNodeList; |
---|
376 | freeNodeList = newNode->nextBddNode; |
---|
377 | newNode->thenBddNode = bddNode->thenBddNode; |
---|
378 | newNode->elseBddNode = bddNode->elseBddNode; |
---|
379 | newNode->thenBddId = bddNode->thenBddId; |
---|
380 | newNode->elseBddId = bddNode->elseBddId; |
---|
381 | newNode->nextBddNode = bddNode->nextBddNode; |
---|
382 | bddNode->elseBddNode = FORWARD_FLAG; |
---|
383 | bddNode->thenBddId = id; |
---|
384 | bddNode->thenBddNode = newNode; |
---|
385 | hashValue = CalDoHash2(thenBdd.bddNode, elseBdd.bddNode, |
---|
386 | uniqueTableForId); |
---|
387 | CalBddNodePutNextBddNode(newNode, uniqueTableForId->bins[hashValue]); |
---|
388 | uniqueTableForId->bins[hashValue] = newNode; |
---|
389 | } |
---|
390 | } |
---|
391 | if (pageNum >= numPagesRequired){ |
---|
392 | /* Free this page. I am assuming that there would not be any |
---|
393 | call to PageManagerAllocPage, until this function finishes */ |
---|
394 | /* Also, CalPageManagerFreePage overwrites only the first field of |
---|
395 | the bdd node (the nextBddNode field), hence no relevant |
---|
396 | information is lost */ |
---|
397 | CalPageManagerFreePage(nodeManager->pageManager, |
---|
398 | nodeManager->pageList[pageNum]); |
---|
399 | nodeManager->pageList[pageNum] = 0; |
---|
400 | } |
---|
401 | } |
---|
402 | #ifdef _CAL_VERBOSE |
---|
403 | printf("Recycled %4d pages for %3d id\n", |
---|
404 | nodeManager->numPages-numPagesRequired, id); |
---|
405 | #endif |
---|
406 | nodeManager->numPages = numPagesRequired; |
---|
407 | nodeManager->freeNodeList = freeNodeList; |
---|
408 | } |
---|
409 | /* Need to update the handles to the nodes being moved */ |
---|
410 | if (bddManager->pipelineState == CREATE){ |
---|
411 | /* There are some results computed in pipeline */ |
---|
412 | CalBddReorderFixProvisionalNodes(bddManager); |
---|
413 | } |
---|
414 | |
---|
415 | CalCacheTableTwoRepackUpdate(bddManager->cacheTable); |
---|
416 | |
---|
417 | /* Fix the user BDDs */ |
---|
418 | CalBddReorderFixUserBddPtrs(bddManager); |
---|
419 | |
---|
420 | /* Fix the association */ |
---|
421 | CalReorderAssociationFix(bddManager); |
---|
422 | |
---|
423 | Cal_Assert(CalCheckAssoc(bddManager)); |
---|
424 | } |
---|
425 | |
---|
426 | /*---------------------------------------------------------------------------*/ |
---|
427 | /* Definition of static functions */ |
---|
428 | /*---------------------------------------------------------------------------*/ |
---|
429 | |
---|
430 | /**Function******************************************************************** |
---|
431 | |
---|
432 | Synopsis [Returns the smallest integer greater than or equal to log2 of a |
---|
433 | number] |
---|
434 | |
---|
435 | Description [Returns the smallest integer greater than or equal to log2 of a |
---|
436 | number (The assumption is that the number is >= 1)] |
---|
437 | |
---|
438 | SideEffects [None] |
---|
439 | |
---|
440 | ******************************************************************************/ |
---|
441 | static int |
---|
442 | CeilLog2(int number) |
---|
443 | { |
---|
444 | int num, count; |
---|
445 | for (num=number, count=0; num > 1; num >>= 1, count++); |
---|
446 | if ((1 << count) != number) count++; |
---|
447 | return count; |
---|
448 | } |
---|