ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
satMem.c File Reference
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <assert.h>
#include "satMem.h"
Include dependency graph for satMem.c:

Go to the source code of this file.

Classes

struct  Sat_MmFixed_t_
 DECLARATIONS ///. More...
 
struct  Sat_MmFlex_t_
 
struct  Sat_MmStep_t_
 

Functions

Sat_MmFixed_tSat_MmFixedStart (int nEntrySize)
 FUNCTION DEFINITIONS ///.
 
void Sat_MmFixedStop (Sat_MmFixed_t *p, int fVerbose)
 
char * Sat_MmFixedEntryFetch (Sat_MmFixed_t *p)
 
void Sat_MmFixedEntryRecycle (Sat_MmFixed_t *p, char *pEntry)
 
void Sat_MmFixedRestart (Sat_MmFixed_t *p)
 
int Sat_MmFixedReadMemUsage (Sat_MmFixed_t *p)
 
Sat_MmFlex_tSat_MmFlexStart ()
 
void Sat_MmFlexStop (Sat_MmFlex_t *p, int fVerbose)
 
char * Sat_MmFlexEntryFetch (Sat_MmFlex_t *p, int nBytes)
 
int Sat_MmFlexReadMemUsage (Sat_MmFlex_t *p)
 
Sat_MmStep_tSat_MmStepStart (int nSteps)
 
void Sat_MmStepStop (Sat_MmStep_t *p, int fVerbose)
 
void Sat_MmStepRestart (Sat_MmStep_t *p)
 
char * Sat_MmStepEntryFetch (Sat_MmStep_t *p, int nBytes)
 
void Sat_MmStepEntryRecycle (Sat_MmStep_t *p, char *pEntry, int nBytes)
 
int Sat_MmStepReadMemUsage (Sat_MmStep_t *p)
 

Function Documentation

◆ Sat_MmFixedEntryFetch()

char * Sat_MmFixedEntryFetch ( Sat_MmFixed_t * p)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 169 of file satMem.c.

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}
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
#define ABC_REALLOC(type, obj, num)
Definition abc_global.h:268
Cube * p
Definition exorList.c:222
#define assert(ex)
Definition util_old.h:213
Here is the caller graph for this function:

◆ Sat_MmFixedEntryRecycle()

void Sat_MmFixedEntryRecycle ( Sat_MmFixed_t * p,
char * pEntry )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 220 of file satMem.c.

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}
Here is the caller graph for this function:

◆ Sat_MmFixedReadMemUsage()

int Sat_MmFixedReadMemUsage ( Sat_MmFixed_t * p)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 281 of file satMem.c.

282{
283 return p->nMemoryAlloc;
284}

◆ Sat_MmFixedRestart()

void Sat_MmFixedRestart ( Sat_MmFixed_t * p)

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

Synopsis []

Description [Relocates all the memory except the first chunk.]

SideEffects []

SeeAlso []

Definition at line 240 of file satMem.c.

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}
#define ABC_FREE(obj)
Definition abc_global.h:267
Here is the caller graph for this function:

◆ Sat_MmFixedStart()

Sat_MmFixed_t * Sat_MmFixedStart ( int nEntrySize)

FUNCTION DEFINITIONS ///.

GLOBAL VARIABLES ///.

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

Synopsis [Allocates memory pieces of fixed size.]

Description [The size of the chunk is computed as the minimum of 1024 entries and 64K. Can only work with entry size at least 4 byte long.]

SideEffects []

SeeAlso []

Definition at line 101 of file satMem.c.

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}
typedefABC_NAMESPACE_HEADER_START struct Sat_MmFixed_t_ Sat_MmFixed_t
INCLUDES ///.
Definition satMem.h:40
char * memset()
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Sat_MmFixedStop()

void Sat_MmFixedStop ( Sat_MmFixed_t * p,
int fVerbose )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 140 of file satMem.c.

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}
Here is the caller graph for this function:

◆ Sat_MmFlexEntryFetch()

char * Sat_MmFlexEntryFetch ( Sat_MmFlex_t * p,
int nBytes )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 360 of file satMem.c.

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}

◆ Sat_MmFlexReadMemUsage()

int Sat_MmFlexReadMemUsage ( Sat_MmFlex_t * p)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 405 of file satMem.c.

406{
407 return p->nMemoryAlloc;
408}

◆ Sat_MmFlexStart()

Sat_MmFlex_t * Sat_MmFlexStart ( )

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

Synopsis [Allocates entries of flexible size.]

Description [Can only work with entry size at least 4 byte long.]

SideEffects []

SeeAlso []

Definition at line 299 of file satMem.c.

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}
struct Sat_MmFlex_t_ Sat_MmFlex_t
Definition satMem.h:41
Here is the call graph for this function:

◆ Sat_MmFlexStop()

void Sat_MmFlexStop ( Sat_MmFlex_t * p,
int fVerbose )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 331 of file satMem.c.

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}

◆ Sat_MmStepEntryFetch()

char * Sat_MmStepEntryFetch ( Sat_MmStep_t * p,
int nBytes )

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

Synopsis [Creates the entry.]

Description []

SideEffects []

SeeAlso []

Definition at line 523 of file satMem.c.

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}
char * Sat_MmFixedEntryFetch(Sat_MmFixed_t *p)
Definition satMem.c:169
Here is the call graph for this function:

◆ Sat_MmStepEntryRecycle()

void Sat_MmStepEntryRecycle ( Sat_MmStep_t * p,
char * pEntry,
int nBytes )

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

Synopsis [Recycles the entry.]

Description []

SideEffects []

SeeAlso []

Definition at line 552 of file satMem.c.

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}
void Sat_MmFixedEntryRecycle(Sat_MmFixed_t *p, char *pEntry)
Definition satMem.c:220
Here is the call graph for this function:

◆ Sat_MmStepReadMemUsage()

int Sat_MmStepReadMemUsage ( Sat_MmStep_t * p)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 575 of file satMem.c.

576{
577 int i, nMemTotal = 0;
578 for ( i = 0; i < p->nMems; i++ )
579 nMemTotal += p->pMems[i]->nMemoryAlloc;
580 return nMemTotal;
581}

◆ Sat_MmStepRestart()

void Sat_MmStepRestart ( Sat_MmStep_t * p)

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

Synopsis [Stops the memory manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 499 of file satMem.c.

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}
void Sat_MmFixedRestart(Sat_MmFixed_t *p)
Definition satMem.c:240
Here is the call graph for this function:

◆ Sat_MmStepStart()

Sat_MmStep_t * Sat_MmStepStart ( int nSteps)

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

Synopsis [Starts the hierarchical memory manager.]

Description [This manager can allocate entries of any size. Iternally they are mapped into the entries with the number of bytes equal to the power of 2. The smallest entry size is 8 bytes. The next one is 16 bytes etc. So, if the user requests 6 bytes, he gets 8 byte entry. If we asks for 25 bytes, he gets 32 byte entry etc. The input parameters "nSteps" says how many fixed memory managers are employed internally. Calling this procedure with nSteps equal to 10 results in 10 hierarchically arranged internal memory managers, which can allocate up to 4096 (1Kb) entries. Requests for larger entries are handed over to malloc() and then ABC_FREE()ed.]

SideEffects []

SeeAlso []

Definition at line 434 of file satMem.c.

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}
Sat_MmFixed_t * Sat_MmFixedStart(int nEntrySize)
FUNCTION DEFINITIONS ///.
Definition satMem.c:101
struct Sat_MmStep_t_ Sat_MmStep_t
Definition satMem.h:42
Here is the call graph for this function:

◆ Sat_MmStepStop()

void Sat_MmStepStop ( Sat_MmStep_t * p,
int fVerbose )

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

Synopsis [Stops the memory manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 472 of file satMem.c.

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}
void Sat_MmFixedStop(Sat_MmFixed_t *p, int fVerbose)
Definition satMem.c:140
Here is the call graph for this function: