ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
msatMem.c
Go to the documentation of this file.
1
20
21#include "msatInt.h"
22
24
25
29
31{
32 // information about individual entries
33 int nEntrySize; // the size of one entry
34 int nEntriesAlloc; // the total number of entries allocated
35 int nEntriesUsed; // the number of entries in use
36 int nEntriesMax; // the max number of entries in use
37 char * pEntriesFree; // the linked list of free entries
38
39 // this is where the memory is stored
40 int nChunkSize; // the size of one chunk
41 int nChunksAlloc; // the maximum number of memory chunks
42 int nChunks; // the current number of memory chunks
43 char ** pChunks; // the allocated memory
44
45 // statistics
46 int nMemoryUsed; // memory used in the allocated entries
47 int nMemoryAlloc; // memory allocated
48};
49
51{
52 // information about individual entries
53 int nEntriesUsed; // the number of entries allocated
54 char * pCurrent; // the current pointer to free memory
55 char * pEnd; // the first entry outside the free memory
56
57 // this is where the memory is stored
58 int nChunkSize; // the size of one chunk
59 int nChunksAlloc; // the maximum number of memory chunks
60 int nChunks; // the current number of memory chunks
61 char ** pChunks; // the allocated memory
62
63 // statistics
64 int nMemoryUsed; // memory used in the allocated entries
65 int nMemoryAlloc; // memory allocated
66};
67
68
70{
71 int nMems; // the number of fixed memory managers employed
72 Msat_MmFixed_t ** pMems; // memory managers: 2^1 words, 2^2 words, etc
73 int nMapSize; // the size of the memory array
74 Msat_MmFixed_t ** pMap; // maps the number of bytes into its memory manager
75};
76
80
94{
96
98 memset( p, 0, sizeof(Msat_MmFixed_t) );
99
100 p->nEntrySize = nEntrySize;
101 p->nEntriesAlloc = 0;
102 p->nEntriesUsed = 0;
103 p->pEntriesFree = NULL;
104
105 if ( nEntrySize * (1 << 10) < (1<<16) )
106 p->nChunkSize = (1 << 10);
107 else
108 p->nChunkSize = (1<<16) / nEntrySize;
109 if ( p->nChunkSize < 8 )
110 p->nChunkSize = 8;
111
112 p->nChunksAlloc = 64;
113 p->nChunks = 0;
114 p->pChunks = ABC_ALLOC( char *, p->nChunksAlloc );
115
116 p->nMemoryUsed = 0;
117 p->nMemoryAlloc = 0;
118 return p;
119}
120
132void Msat_MmFixedStop( Msat_MmFixed_t * p, int fVerbose )
133{
134 int i;
135 if ( p == NULL )
136 return;
137 if ( fVerbose )
138 {
139 printf( "Fixed memory manager: Entry = %5d. Chunk = %5d. Chunks used = %5d.\n",
140 p->nEntrySize, p->nChunkSize, p->nChunks );
141 printf( " Entries used = %8d. Entries peak = %8d. Memory used = %8d. Memory alloc = %8d.\n",
142 p->nEntriesUsed, p->nEntriesMax, p->nEntrySize * p->nEntriesUsed, p->nMemoryAlloc );
143 }
144 for ( i = 0; i < p->nChunks; i++ )
145 ABC_FREE( p->pChunks[i] );
146 ABC_FREE( p->pChunks );
147 ABC_FREE( p );
148}
149
162{
163 char * pTemp;
164 int i;
165
166 // check if there are still free entries
167 if ( p->nEntriesUsed == p->nEntriesAlloc )
168 { // need to allocate more entries
169 assert( p->pEntriesFree == NULL );
170 if ( p->nChunks == p->nChunksAlloc )
171 {
172 p->nChunksAlloc *= 2;
173 p->pChunks = ABC_REALLOC( char *, p->pChunks, p->nChunksAlloc );
174 }
175 p->pEntriesFree = ABC_ALLOC( char, p->nEntrySize * p->nChunkSize );
176 p->nMemoryAlloc += p->nEntrySize * p->nChunkSize;
177 // transform these entries into a linked list
178 pTemp = p->pEntriesFree;
179 for ( i = 1; i < p->nChunkSize; i++ )
180 {
181 *((char **)pTemp) = pTemp + p->nEntrySize;
182 pTemp += p->nEntrySize;
183 }
184 // set the last link
185 *((char **)pTemp) = NULL;
186 // add the chunk to the chunk storage
187 p->pChunks[ p->nChunks++ ] = p->pEntriesFree;
188 // add to the number of entries allocated
189 p->nEntriesAlloc += p->nChunkSize;
190 }
191 // incrememt the counter of used entries
192 p->nEntriesUsed++;
193 if ( p->nEntriesMax < p->nEntriesUsed )
194 p->nEntriesMax = p->nEntriesUsed;
195 // return the first entry in the free entry list
196 pTemp = p->pEntriesFree;
197 p->pEntriesFree = *((char **)pTemp);
198 return pTemp;
199}
200
213{
214 // decrement the counter of used entries
215 p->nEntriesUsed--;
216 // add the entry to the linked list of free entries
217 *((char **)pEntry) = p->pEntriesFree;
218 p->pEntriesFree = pEntry;
219}
220
233{
234 int i;
235 char * pTemp;
236
237 // deallocate all chunks except the first one
238 for ( i = 1; i < p->nChunks; i++ )
239 ABC_FREE( p->pChunks[i] );
240 p->nChunks = 1;
241 // transform these entries into a linked list
242 pTemp = p->pChunks[0];
243 for ( i = 1; i < p->nChunkSize; i++ )
244 {
245 *((char **)pTemp) = pTemp + p->nEntrySize;
246 pTemp += p->nEntrySize;
247 }
248 // set the last link
249 *((char **)pTemp) = NULL;
250 // set the free entry list
251 p->pEntriesFree = p->pChunks[0];
252 // set the correct statistics
253 p->nMemoryAlloc = p->nEntrySize * p->nChunkSize;
254 p->nMemoryUsed = 0;
255 p->nEntriesAlloc = p->nChunkSize;
256 p->nEntriesUsed = 0;
257}
258
271{
272 return p->nMemoryAlloc;
273}
274
275
276
289{
291
292 p = ABC_ALLOC( Msat_MmFlex_t, 1 );
293 memset( p, 0, sizeof(Msat_MmFlex_t) );
294
295 p->nEntriesUsed = 0;
296 p->pCurrent = NULL;
297 p->pEnd = NULL;
298
299 p->nChunkSize = (1 << 12);
300 p->nChunksAlloc = 64;
301 p->nChunks = 0;
302 p->pChunks = ABC_ALLOC( char *, p->nChunksAlloc );
303
304 p->nMemoryUsed = 0;
305 p->nMemoryAlloc = 0;
306 return p;
307}
308
320void Msat_MmFlexStop( Msat_MmFlex_t * p, int fVerbose )
321{
322 int i;
323 if ( p == NULL )
324 return;
325 if ( fVerbose )
326 {
327 printf( "Flexible memory manager: Chunk size = %d. Chunks used = %d.\n",
328 p->nChunkSize, p->nChunks );
329 printf( " Entries used = %d. Memory used = %d. Memory alloc = %d.\n",
330 p->nEntriesUsed, p->nMemoryUsed, p->nMemoryAlloc );
331 }
332 for ( i = 0; i < p->nChunks; i++ )
333 ABC_FREE( p->pChunks[i] );
334 ABC_FREE( p->pChunks );
335 ABC_FREE( p );
336}
337
349char * Msat_MmFlexEntryFetch( Msat_MmFlex_t * p, int nBytes )
350{
351 char * pTemp;
352 // check if there are still free entries
353 if ( p->pCurrent == NULL || p->pCurrent + nBytes > p->pEnd )
354 { // need to allocate more entries
355 if ( p->nChunks == p->nChunksAlloc )
356 {
357 p->nChunksAlloc *= 2;
358 p->pChunks = ABC_REALLOC( char *, p->pChunks, p->nChunksAlloc );
359 }
360 if ( nBytes > p->nChunkSize )
361 {
362 // resize the chunk size if more memory is requested than it can give
363 // (ideally, this should never happen)
364 p->nChunkSize = 2 * nBytes;
365 }
366 p->pCurrent = ABC_ALLOC( char, p->nChunkSize );
367 p->pEnd = p->pCurrent + p->nChunkSize;
368 p->nMemoryAlloc += p->nChunkSize;
369 // add the chunk to the chunk storage
370 p->pChunks[ p->nChunks++ ] = p->pCurrent;
371 }
372 assert( p->pCurrent + nBytes <= p->pEnd );
373 // increment the counter of used entries
374 p->nEntriesUsed++;
375 // keep track of the memory used
376 p->nMemoryUsed += nBytes;
377 // return the next entry
378 pTemp = p->pCurrent;
379 p->pCurrent += nBytes;
380 return pTemp;
381}
382
395{
396 return p->nMemoryAlloc;
397}
398
399
400
401
402
424{
426 int i, k;
427 p = ABC_ALLOC( Msat_MmStep_t, 1 );
428 p->nMems = nSteps;
429 // start the fixed memory managers
430 p->pMems = ABC_ALLOC( Msat_MmFixed_t *, p->nMems );
431 for ( i = 0; i < p->nMems; i++ )
432 p->pMems[i] = Msat_MmFixedStart( (8<<i) );
433 // set up the mapping of the required memory size into the corresponding manager
434 p->nMapSize = (4<<p->nMems);
435 p->pMap = ABC_ALLOC( Msat_MmFixed_t *, p->nMapSize+1 );
436 p->pMap[0] = NULL;
437 for ( k = 1; k <= 4; k++ )
438 p->pMap[k] = p->pMems[0];
439 for ( i = 0; i < p->nMems; i++ )
440 for ( k = (4<<i)+1; k <= (8<<i); k++ )
441 p->pMap[k] = p->pMems[i];
442//for ( i = 1; i < 100; i ++ )
443//printf( "%10d: size = %10d\n", i, p->pMap[i]->nEntrySize );
444 return p;
445}
446
458void Msat_MmStepStop( Msat_MmStep_t * p, int fVerbose )
459{
460 int i;
461 for ( i = 0; i < p->nMems; i++ )
462 Msat_MmFixedStop( p->pMems[i], fVerbose );
463 ABC_FREE( p->pMems );
464 ABC_FREE( p->pMap );
465 ABC_FREE( p );
466}
467
479char * Msat_MmStepEntryFetch( Msat_MmStep_t * p, int nBytes )
480{
481 if ( nBytes == 0 )
482 return NULL;
483 if ( nBytes > p->nMapSize )
484 {
485// printf( "Allocating %d bytes.\n", nBytes );
486 return ABC_ALLOC( char, nBytes );
487 }
488 return Msat_MmFixedEntryFetch( p->pMap[nBytes] );
489}
490
491
503void Msat_MmStepEntryRecycle( Msat_MmStep_t * p, char * pEntry, int nBytes )
504{
505 if ( nBytes == 0 )
506 return;
507 if ( nBytes > p->nMapSize )
508 {
509 ABC_FREE( pEntry );
510 return;
511 }
512 Msat_MmFixedEntryRecycle( p->pMap[nBytes], pEntry );
513}
514
527{
528 int i, nMemTotal = 0;
529 for ( i = 0; i < p->nMems; i++ )
530 nMemTotal += p->pMems[i]->nMemoryAlloc;
531 return nMemTotal;
532}
534
#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
struct Msat_MmFlex_t_ Msat_MmFlex_t
Definition msatInt.h:62
struct Msat_MmFixed_t_ Msat_MmFixed_t
Definition msatInt.h:61
Msat_MmFixed_t * Msat_MmFixedStart(int nEntrySize)
FUNCTION DEFINITIONS ///.
Definition msatMem.c:93
struct Msat_MmStep_t_ Msat_MmStep_t
Definition msatInt.h:63
int Msat_MmFlexReadMemUsage(Msat_MmFlex_t *p)
Definition msatMem.c:394
void Msat_MmFixedStop(Msat_MmFixed_t *p, int fVerbose)
Definition msatMem.c:132
void Msat_MmFixedEntryRecycle(Msat_MmFixed_t *p, char *pEntry)
Definition msatMem.c:212
int Msat_MmStepReadMemUsage(Msat_MmStep_t *p)
Definition msatMem.c:526
void Msat_MmStepStop(Msat_MmStep_t *p, int fVerbose)
Definition msatMem.c:458
char * Msat_MmStepEntryFetch(Msat_MmStep_t *p, int nBytes)
Definition msatMem.c:479
Msat_MmFlex_t * Msat_MmFlexStart()
Definition msatMem.c:288
Msat_MmFixed_t * Msat_MmFixedStart(int nEntrySize)
FUNCTION DEFINITIONS ///.
Definition msatMem.c:93
void Msat_MmFlexStop(Msat_MmFlex_t *p, int fVerbose)
Definition msatMem.c:320
void Msat_MmStepEntryRecycle(Msat_MmStep_t *p, char *pEntry, int nBytes)
Definition msatMem.c:503
char * Msat_MmFlexEntryFetch(Msat_MmFlex_t *p, int nBytes)
Definition msatMem.c:349
void Msat_MmFixedRestart(Msat_MmFixed_t *p)
Definition msatMem.c:232
int Msat_MmFixedReadMemUsage(Msat_MmFixed_t *p)
Definition msatMem.c:270
Msat_MmStep_t * Msat_MmStepStart(int nSteps)
Definition msatMem.c:423
char * Msat_MmFixedEntryFetch(Msat_MmFixed_t *p)
Definition msatMem.c:161
DECLARATIONS ///.
Definition msatMem.c:31
int nEntriesAlloc
Definition msatMem.c:34
char ** pChunks
Definition msatMem.c:43
char * pEntriesFree
Definition msatMem.c:37
int nMemoryAlloc
Definition msatMem.c:65
int nMemoryUsed
Definition msatMem.c:64
char * pEnd
Definition msatMem.c:55
char * pCurrent
Definition msatMem.c:54
int nChunksAlloc
Definition msatMem.c:59
char ** pChunks
Definition msatMem.c:61
int nEntriesUsed
Definition msatMem.c:53
Msat_MmFixed_t ** pMap
Definition msatMem.c:74
Msat_MmFixed_t ** pMems
Definition msatMem.c:72
#define assert(ex)
Definition util_old.h:213
char * memset()