abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
msatMem.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [msatMem.c]
4 
5  PackageName [A C version of SAT solver MINISAT, originally developed
6  in C++ by Niklas Een and Niklas Sorensson, Chalmers University of
7  Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.]
8 
9  Synopsis [Memory managers borrowed from Extra.]
10 
11  Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - January 1, 2004.]
16 
17  Revision [$Id: msatMem.c,v 1.0 2004/01/01 1:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "msatInt.h"
22 
24 
25 
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
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 
77 ////////////////////////////////////////////////////////////////////////
78 /// FUNCTION DEFINITIONS ///
79 ////////////////////////////////////////////////////////////////////////
80 
81 /**Function*************************************************************
82 
83  Synopsis [Allocates memory pieces of fixed size.]
84 
85  Description [The size of the chunk is computed as the minimum of
86  1024 entries and 64K. Can only work with entry size at least 4 byte long.]
87 
88  SideEffects []
89 
90  SeeAlso []
91 
92 ***********************************************************************/
93 Msat_MmFixed_t * Msat_MmFixedStart( int nEntrySize )
94 {
95  Msat_MmFixed_t * p;
96 
97  p = ABC_ALLOC( Msat_MmFixed_t, 1 );
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 
121 /**Function*************************************************************
122 
123  Synopsis []
124 
125  Description []
126 
127  SideEffects []
128 
129  SeeAlso []
130 
131 ***********************************************************************/
132 void 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",
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 
150 /**Function*************************************************************
151 
152  Synopsis []
153 
154  Description []
155 
156  SideEffects []
157 
158  SeeAlso []
159 
160 ***********************************************************************/
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 
201 /**Function*************************************************************
202 
203  Synopsis []
204 
205  Description []
206 
207  SideEffects []
208 
209  SeeAlso []
210 
211 ***********************************************************************/
212 void Msat_MmFixedEntryRecycle( Msat_MmFixed_t * p, char * pEntry )
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 
221 /**Function*************************************************************
222 
223  Synopsis []
224 
225  Description [Relocates all the memory except the first chunk.]
226 
227  SideEffects []
228 
229  SeeAlso []
230 
231 ***********************************************************************/
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 
259 /**Function*************************************************************
260 
261  Synopsis []
262 
263  Description []
264 
265  SideEffects []
266 
267  SeeAlso []
268 
269 ***********************************************************************/
271 {
272  return p->nMemoryAlloc;
273 }
274 
275 
276 
277 /**Function*************************************************************
278 
279  Synopsis [Allocates entries of flexible size.]
280 
281  Description [Can only work with entry size at least 4 byte long.]
282 
283  SideEffects []
284 
285  SeeAlso []
286 
287 ***********************************************************************/
289 {
290  Msat_MmFlex_t * p;
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 
309 /**Function*************************************************************
310 
311  Synopsis []
312 
313  Description []
314 
315  SideEffects []
316 
317  SeeAlso []
318 
319 ***********************************************************************/
320 void 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",
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 
338 /**Function*************************************************************
339 
340  Synopsis []
341 
342  Description []
343 
344  SideEffects []
345 
346  SeeAlso []
347 
348 ***********************************************************************/
349 char * 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 
383 /**Function*************************************************************
384 
385  Synopsis []
386 
387  Description []
388 
389  SideEffects []
390 
391  SeeAlso []
392 
393 ***********************************************************************/
395 {
396  return p->nMemoryAlloc;
397 }
398 
399 
400 
401 
402 
403 /**Function*************************************************************
404 
405  Synopsis [Starts the hierarchical memory manager.]
406 
407  Description [This manager can allocate entries of any size.
408  Iternally they are mapped into the entries with the number of bytes
409  equal to the power of 2. The smallest entry size is 8 bytes. The
410  next one is 16 bytes etc. So, if the user requests 6 bytes, he gets
411  8 byte entry. If we asks for 25 bytes, he gets 32 byte entry etc.
412  The input parameters "nSteps" says how many fixed memory managers
413  are employed internally. Calling this procedure with nSteps equal
414  to 10 results in 10 hierarchically arranged internal memory managers,
415  which can allocate up to 4096 (1Kb) entries. Requests for larger
416  entries are handed over to malloc() and then ABC_FREE()ed.]
417 
418  SideEffects []
419 
420  SeeAlso []
421 
422 ***********************************************************************/
424 {
425  Msat_MmStep_t * p;
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 
447 /**Function*************************************************************
448 
449  Synopsis [Stops the memory manager.]
450 
451  Description []
452 
453  SideEffects []
454 
455  SeeAlso []
456 
457 ***********************************************************************/
458 void 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 
468 /**Function*************************************************************
469 
470  Synopsis [Creates the entry.]
471 
472  Description []
473 
474  SideEffects []
475 
476  SeeAlso []
477 
478 ***********************************************************************/
479 char * 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 
492 /**Function*************************************************************
493 
494  Synopsis [Recycles the entry.]
495 
496  Description []
497 
498  SideEffects []
499 
500  SeeAlso []
501 
502 ***********************************************************************/
503 void 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 
515 /**Function*************************************************************
516 
517  Synopsis []
518 
519  Description []
520 
521  SideEffects []
522 
523  SeeAlso []
524 
525 ***********************************************************************/
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 
char * memset()
char * pEnd
Definition: msatMem.c:55
static Llb_Mgr_t * p
Definition: llb3Image.c:950
int nMemoryAlloc
Definition: msatMem.c:65
int nChunkSize
Definition: msatMem.c:58
#define ABC_REALLOC(type, obj, num)
Definition: abc_global.h:233
int nMemoryUsed
Definition: msatMem.c:64
void Msat_MmFixedEntryRecycle(Msat_MmFixed_t *p, char *pEntry)
Definition: msatMem.c:212
int nChunksAlloc
Definition: msatMem.c:59
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
int nEntriesUsed
Definition: msatMem.c:53
for(p=first;p->value< newval;p=p->next)
int Msat_MmFixedReadMemUsage(Msat_MmFixed_t *p)
Definition: msatMem.c:270
Msat_MmFixed_t ** pMap
Definition: msatMem.c:74
int Msat_MmStepReadMemUsage(Msat_MmStep_t *p)
Definition: msatMem.c:526
char * Msat_MmFlexEntryFetch(Msat_MmFlex_t *p, int nBytes)
Definition: msatMem.c:349
Msat_MmFixed_t ** pMems
Definition: msatMem.c:72
void Msat_MmFixedStop(Msat_MmFixed_t *p, int fVerbose)
Definition: msatMem.c:132
Msat_MmFlex_t * Msat_MmFlexStart()
Definition: msatMem.c:288
int Msat_MmFlexReadMemUsage(Msat_MmFlex_t *p)
Definition: msatMem.c:394
char * pEntriesFree
Definition: msatMem.c:37
Msat_MmStep_t * Msat_MmStepStart(int nSteps)
Definition: msatMem.c:423
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
DECLARATIONS ///.
Definition: msatMem.c:30
int nEntriesMax
Definition: msatMem.c:36
void Msat_MmFixedRestart(Msat_MmFixed_t *p)
Definition: msatMem.c:232
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
int nMemoryUsed
Definition: msatMem.c:46
char ** pChunks
Definition: msatMem.c:43
int nMemoryAlloc
Definition: msatMem.c:47
int nChunkSize
Definition: msatMem.c:40
char * pCurrent
Definition: msatMem.c:54
int nEntrySize
Definition: msatMem.c:33
char ** pChunks
Definition: msatMem.c:61
#define ABC_FREE(obj)
Definition: abc_global.h:232
void Msat_MmStepStop(Msat_MmStep_t *p, int fVerbose)
Definition: msatMem.c:458
void Msat_MmFlexStop(Msat_MmFlex_t *p, int fVerbose)
Definition: msatMem.c:320
#define assert(ex)
Definition: util_old.h:213
int nEntriesAlloc
Definition: msatMem.c:34
char * Msat_MmStepEntryFetch(Msat_MmStep_t *p, int nBytes)
Definition: msatMem.c:479
void Msat_MmStepEntryRecycle(Msat_MmStep_t *p, char *pEntry, int nBytes)
Definition: msatMem.c:503
int nMapSize
Definition: msatMem.c:73
Msat_MmFixed_t * Msat_MmFixedStart(int nEntrySize)
FUNCTION DEFINITIONS ///.
Definition: msatMem.c:93
int nEntriesUsed
Definition: msatMem.c:35
int nChunksAlloc
Definition: msatMem.c:41
char * Msat_MmFixedEntryFetch(Msat_MmFixed_t *p)
Definition: msatMem.c:161