ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
satMem.c
Go to the documentation of this file.
1
20
21#include <stdio.h>
22#include <stdlib.h>
23#include <string.h>
24#include <assert.h>
25
26#include "satMem.h"
27
29
30
34
36{
37 // information about individual entries
38 int nEntrySize; // the size of one entry
39 int nEntriesAlloc; // the total number of entries allocated
40 int nEntriesUsed; // the number of entries in use
41 int nEntriesMax; // the max number of entries in use
42 char * pEntriesFree; // the linked list of free entries
43
44 // this is where the memory is stored
45 int nChunkSize; // the size of one chunk
46 int nChunksAlloc; // the maximum number of memory chunks
47 int nChunks; // the current number of memory chunks
48 char ** pChunks; // the allocated memory
49
50 // statistics
51 int nMemoryUsed; // memory used in the allocated entries
52 int nMemoryAlloc; // memory allocated
53};
54
56{
57 // information about individual entries
58 int nEntriesUsed; // the number of entries allocated
59 char * pCurrent; // the current pointer to free memory
60 char * pEnd; // the first entry outside the free memory
61
62 // this is where the memory is stored
63 int nChunkSize; // the size of one chunk
64 int nChunksAlloc; // the maximum number of memory chunks
65 int nChunks; // the current number of memory chunks
66 char ** pChunks; // the allocated memory
67
68 // statistics
69 int nMemoryUsed; // memory used in the allocated entries
70 int nMemoryAlloc; // memory allocated
71};
72
74{
75 int nMems; // the number of fixed memory managers employed
76 Sat_MmFixed_t ** pMems; // memory managers: 2^1 words, 2^2 words, etc
77 int nMapSize; // the size of the memory array
78 Sat_MmFixed_t ** pMap; // maps the number of bytes into its memory manager
79 // additional memory chunks
80 int nChunksAlloc; // the maximum number of memory chunks
81 int nChunks; // the current number of memory chunks
82 char ** pChunks; // the allocated memory
83};
84
88
102{
104
105 p = ABC_ALLOC( Sat_MmFixed_t, 1 );
106 memset( p, 0, sizeof(Sat_MmFixed_t) );
107
108 p->nEntrySize = nEntrySize;
109 p->nEntriesAlloc = 0;
110 p->nEntriesUsed = 0;
111 p->pEntriesFree = NULL;
112
113 if ( nEntrySize * (1 << 10) < (1<<16) )
114 p->nChunkSize = (1 << 10);
115 else
116 p->nChunkSize = (1<<16) / nEntrySize;
117 if ( p->nChunkSize < 8 )
118 p->nChunkSize = 8;
119
120 p->nChunksAlloc = 64;
121 p->nChunks = 0;
122 p->pChunks = ABC_ALLOC( char *, p->nChunksAlloc );
123
124 p->nMemoryUsed = 0;
125 p->nMemoryAlloc = 0;
126 return p;
127}
128
140void Sat_MmFixedStop( Sat_MmFixed_t * p, int fVerbose )
141{
142 int i;
143 if ( p == NULL )
144 return;
145 if ( fVerbose )
146 {
147 printf( "Fixed memory manager: Entry = %5d. Chunk = %5d. Chunks used = %5d.\n",
148 p->nEntrySize, p->nChunkSize, p->nChunks );
149 printf( " Entries used = %8d. Entries peak = %8d. Memory used = %8d. Memory alloc = %8d.\n",
150 p->nEntriesUsed, p->nEntriesMax, p->nEntrySize * p->nEntriesUsed, p->nMemoryAlloc );
151 }
152 for ( i = 0; i < p->nChunks; i++ )
153 ABC_FREE( p->pChunks[i] );
154 ABC_FREE( p->pChunks );
155 ABC_FREE( p );
156}
157
170{
171 char * pTemp;
172 int i;
173
174 // check if there are still free entries
175 if ( p->nEntriesUsed == p->nEntriesAlloc )
176 { // need to allocate more entries
177 assert( p->pEntriesFree == NULL );
178 if ( p->nChunks == p->nChunksAlloc )
179 {
180 p->nChunksAlloc *= 2;
181 p->pChunks = ABC_REALLOC( char *, p->pChunks, p->nChunksAlloc );
182 }
183 p->pEntriesFree = ABC_ALLOC( char, p->nEntrySize * p->nChunkSize );
184 p->nMemoryAlloc += p->nEntrySize * p->nChunkSize;
185 // transform these entries into a linked list
186 pTemp = p->pEntriesFree;
187 for ( i = 1; i < p->nChunkSize; i++ )
188 {
189 *((char **)pTemp) = pTemp + p->nEntrySize;
190 pTemp += p->nEntrySize;
191 }
192 // set the last link
193 *((char **)pTemp) = NULL;
194 // add the chunk to the chunk storage
195 p->pChunks[ p->nChunks++ ] = p->pEntriesFree;
196 // add to the number of entries allocated
197 p->nEntriesAlloc += p->nChunkSize;
198 }
199 // incrememt the counter of used entries
200 p->nEntriesUsed++;
201 if ( p->nEntriesMax < p->nEntriesUsed )
202 p->nEntriesMax = p->nEntriesUsed;
203 // return the first entry in the free entry list
204 pTemp = p->pEntriesFree;
205 p->pEntriesFree = *((char **)pTemp);
206 return pTemp;
207}
208
221{
222 // decrement the counter of used entries
223 p->nEntriesUsed--;
224 // add the entry to the linked list of free entries
225 *((char **)pEntry) = p->pEntriesFree;
226 p->pEntriesFree = pEntry;
227}
228
241{
242 int i;
243 char * pTemp;
244 if ( p->nChunks == 0 )
245 return;
246 assert( p->nChunks > 0 );
247
248 // deallocate all chunks except the first one
249 for ( i = 1; i < p->nChunks; i++ )
250 ABC_FREE( p->pChunks[i] );
251 p->nChunks = 1;
252 // transform these entries into a linked list
253 pTemp = p->pChunks[0];
254 for ( i = 1; i < p->nChunkSize; i++ )
255 {
256 *((char **)pTemp) = pTemp + p->nEntrySize;
257 pTemp += p->nEntrySize;
258 }
259 // set the last link
260 *((char **)pTemp) = NULL;
261 // set the free entry list
262 p->pEntriesFree = p->pChunks[0];
263 // set the correct statistics
264 p->nMemoryAlloc = p->nEntrySize * p->nChunkSize;
265 p->nMemoryUsed = 0;
266 p->nEntriesAlloc = p->nChunkSize;
267 p->nEntriesUsed = 0;
268}
269
282{
283 return p->nMemoryAlloc;
284}
285
286
287
300{
301 Sat_MmFlex_t * p;
302
303 p = ABC_ALLOC( Sat_MmFlex_t, 1 );
304 memset( p, 0, sizeof(Sat_MmFlex_t) );
305
306 p->nEntriesUsed = 0;
307 p->pCurrent = NULL;
308 p->pEnd = NULL;
309
310 p->nChunkSize = (1 << 16);
311 p->nChunksAlloc = 64;
312 p->nChunks = 0;
313 p->pChunks = ABC_ALLOC( char *, p->nChunksAlloc );
314
315 p->nMemoryUsed = 0;
316 p->nMemoryAlloc = 0;
317 return p;
318}
319
331void Sat_MmFlexStop( Sat_MmFlex_t * p, int fVerbose )
332{
333 int i;
334 if ( p == NULL )
335 return;
336 if ( fVerbose )
337 {
338 printf( "Flexible memory manager: Chunk size = %d. Chunks used = %d.\n",
339 p->nChunkSize, p->nChunks );
340 printf( " Entries used = %d. Memory used = %d. Memory alloc = %d.\n",
341 p->nEntriesUsed, p->nMemoryUsed, p->nMemoryAlloc );
342 }
343 for ( i = 0; i < p->nChunks; i++ )
344 ABC_FREE( p->pChunks[i] );
345 ABC_FREE( p->pChunks );
346 ABC_FREE( p );
347}
348
360char * Sat_MmFlexEntryFetch( Sat_MmFlex_t * p, int nBytes )
361{
362 char * pTemp;
363 // check if there are still free entries
364 if ( p->pCurrent == NULL || p->pCurrent + nBytes > p->pEnd )
365 { // need to allocate more entries
366 if ( p->nChunks == p->nChunksAlloc )
367 {
368 p->nChunksAlloc *= 2;
369 p->pChunks = ABC_REALLOC( char *, p->pChunks, p->nChunksAlloc );
370 }
371 if ( nBytes > p->nChunkSize )
372 {
373 // resize the chunk size if more memory is requested than it can give
374 // (ideally, this should never happen)
375 p->nChunkSize = 2 * nBytes;
376 }
377 p->pCurrent = ABC_ALLOC( char, p->nChunkSize );
378 p->pEnd = p->pCurrent + p->nChunkSize;
379 p->nMemoryAlloc += p->nChunkSize;
380 // add the chunk to the chunk storage
381 p->pChunks[ p->nChunks++ ] = p->pCurrent;
382 }
383 assert( p->pCurrent + nBytes <= p->pEnd );
384 // increment the counter of used entries
385 p->nEntriesUsed++;
386 // keep track of the memory used
387 p->nMemoryUsed += nBytes;
388 // return the next entry
389 pTemp = p->pCurrent;
390 p->pCurrent += nBytes;
391 return pTemp;
392}
393
406{
407 return p->nMemoryAlloc;
408}
409
410
411
412
413
435{
436 Sat_MmStep_t * p;
437 int i, k;
438 p = ABC_ALLOC( Sat_MmStep_t, 1 );
439 p->nMems = nSteps;
440 // start the fixed memory managers
441 p->pMems = ABC_ALLOC( Sat_MmFixed_t *, p->nMems );
442 for ( i = 0; i < p->nMems; i++ )
443 p->pMems[i] = Sat_MmFixedStart( (8<<i) );
444 // set up the mapping of the required memory size into the corresponding manager
445 p->nMapSize = (4<<p->nMems);
446 p->pMap = ABC_ALLOC( Sat_MmFixed_t *, p->nMapSize+1 );
447 p->pMap[0] = NULL;
448 for ( k = 1; k <= 4; k++ )
449 p->pMap[k] = p->pMems[0];
450 for ( i = 0; i < p->nMems; i++ )
451 for ( k = (4<<i)+1; k <= (8<<i); k++ )
452 p->pMap[k] = p->pMems[i];
453//for ( i = 1; i < 100; i ++ )
454//printf( "%10d: size = %10d\n", i, p->pMap[i]->nEntrySize );
455 p->nChunksAlloc = 64;
456 p->nChunks = 0;
457 p->pChunks = ABC_ALLOC( char *, p->nChunksAlloc );
458 return p;
459}
460
472void Sat_MmStepStop( Sat_MmStep_t * p, int fVerbose )
473{
474 int i;
475 if ( p->nChunksAlloc )
476 {
477 for ( i = 0; i < p->nChunks; i++ )
478 ABC_FREE( p->pChunks[i] );
479 ABC_FREE( p->pChunks );
480 }
481 for ( i = 0; i < p->nMems; i++ )
482 Sat_MmFixedStop( p->pMems[i], fVerbose );
483 ABC_FREE( p->pMems );
484 ABC_FREE( p->pMap );
485 ABC_FREE( p );
486}
487
500{
501 int i;
502 if ( p->nChunksAlloc )
503 {
504 for ( i = 0; i < p->nChunks; i++ )
505 ABC_FREE( p->pChunks[i] );
506 p->nChunks = 0;
507 }
508 for ( i = 0; i < p->nMems; i++ )
509 Sat_MmFixedRestart( p->pMems[i] );
510}
511
523char * Sat_MmStepEntryFetch( Sat_MmStep_t * p, int nBytes )
524{
525 if ( nBytes == 0 )
526 return NULL;
527 if ( nBytes > p->nMapSize )
528 {
529 if ( p->nChunks == p->nChunksAlloc )
530 {
531 p->nChunksAlloc *= 2;
532 p->pChunks = ABC_REALLOC( char *, p->pChunks, p->nChunksAlloc );
533 }
534 p->pChunks[ p->nChunks++ ] = ABC_ALLOC( char, nBytes );
535 return p->pChunks[p->nChunks-1];
536 }
537 return Sat_MmFixedEntryFetch( p->pMap[nBytes] );
538}
539
540
552void Sat_MmStepEntryRecycle( Sat_MmStep_t * p, char * pEntry, int nBytes )
553{
554 if ( nBytes == 0 )
555 return;
556 if ( nBytes > p->nMapSize )
557 {
558// ABC_FREE( pEntry );
559 return;
560 }
561 Sat_MmFixedEntryRecycle( p->pMap[nBytes], pEntry );
562}
563
576{
577 int i, nMemTotal = 0;
578 for ( i = 0; i < p->nMems; i++ )
579 nMemTotal += p->pMems[i]->nMemoryAlloc;
580 return nMemTotal;
581}
583
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
#define ABC_REALLOC(type, obj, num)
Definition abc_global.h:268
#define ABC_FREE(obj)
Definition abc_global.h:267
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
Cube * p
Definition exorList.c:222
char * Sat_MmFlexEntryFetch(Sat_MmFlex_t *p, int nBytes)
Definition satMem.c:360
void Sat_MmFlexStop(Sat_MmFlex_t *p, int fVerbose)
Definition satMem.c:331
int Sat_MmFixedReadMemUsage(Sat_MmFixed_t *p)
Definition satMem.c:281
Sat_MmFlex_t * Sat_MmFlexStart()
Definition satMem.c:299
void Sat_MmFixedEntryRecycle(Sat_MmFixed_t *p, char *pEntry)
Definition satMem.c:220
int Sat_MmStepReadMemUsage(Sat_MmStep_t *p)
Definition satMem.c:575
Sat_MmFixed_t * Sat_MmFixedStart(int nEntrySize)
FUNCTION DEFINITIONS ///.
Definition satMem.c:101
Sat_MmStep_t * Sat_MmStepStart(int nSteps)
Definition satMem.c:434
void Sat_MmFixedStop(Sat_MmFixed_t *p, int fVerbose)
Definition satMem.c:140
void Sat_MmStepStop(Sat_MmStep_t *p, int fVerbose)
Definition satMem.c:472
int Sat_MmFlexReadMemUsage(Sat_MmFlex_t *p)
Definition satMem.c:405
char * Sat_MmStepEntryFetch(Sat_MmStep_t *p, int nBytes)
Definition satMem.c:523
void Sat_MmStepRestart(Sat_MmStep_t *p)
Definition satMem.c:499
void Sat_MmFixedRestart(Sat_MmFixed_t *p)
Definition satMem.c:240
void Sat_MmStepEntryRecycle(Sat_MmStep_t *p, char *pEntry, int nBytes)
Definition satMem.c:552
char * Sat_MmFixedEntryFetch(Sat_MmFixed_t *p)
Definition satMem.c:169
struct Sat_MmFlex_t_ Sat_MmFlex_t
Definition satMem.h:41
struct Sat_MmStep_t_ Sat_MmStep_t
Definition satMem.h:42
typedefABC_NAMESPACE_HEADER_START struct Sat_MmFixed_t_ Sat_MmFixed_t
INCLUDES ///.
Definition satMem.h:40
DECLARATIONS ///.
Definition satMem.c:36
int nChunksAlloc
Definition satMem.c:46
int nEntriesMax
Definition satMem.c:41
int nMemoryUsed
Definition satMem.c:51
int nEntriesUsed
Definition satMem.c:40
char ** pChunks
Definition satMem.c:48
int nEntriesAlloc
Definition satMem.c:39
int nChunkSize
Definition satMem.c:45
int nMemoryAlloc
Definition satMem.c:52
int nEntrySize
Definition satMem.c:38
char * pEntriesFree
Definition satMem.c:42
int nMemoryUsed
Definition satMem.c:69
int nChunks
Definition satMem.c:65
char ** pChunks
Definition satMem.c:66
int nMemoryAlloc
Definition satMem.c:70
char * pCurrent
Definition satMem.c:59
char * pEnd
Definition satMem.c:60
int nChunkSize
Definition satMem.c:63
int nChunksAlloc
Definition satMem.c:64
int nEntriesUsed
Definition satMem.c:58
Sat_MmFixed_t ** pMems
Definition satMem.c:76
int nChunksAlloc
Definition satMem.c:80
int nMapSize
Definition satMem.c:77
Sat_MmFixed_t ** pMap
Definition satMem.c:78
char ** pChunks
Definition satMem.c:82
int nChunks
Definition satMem.c:81
#define assert(ex)
Definition util_old.h:213
char * memset()