trunk/verif/Spin/Src5.1.6/tl_mem.c

   1 /***** tl_spin: tl_mem.c *****/
   2
   3 /* Copyright (c) 1995-2003 by Lucent Technologies, Bell Laboratories.     */
   4 /* All Rights Reserved.  This software is for educational purposes only.  */
   5 /* No guarantee whatsoever is expressed or implied by the distribution of */
   6 /* this code.  Permission is given to distribute this code provided that  */
   7 /* this introductory message is not removed and no monies are exchanged.  */
   8 /* Software written by Gerard J. Holzmann.  For tool documentation see:   */
   9 /*             http://spinroot.com/                                       */
  10 /* Send all bug-reports and/or questions to: bugs@spinroot.com            */
  11
  12 /* Based on the translation algorithm by Gerth, Peled, Vardi, and Wolper, */
  13 /* presented at the PSTV Conference, held in 1995, Warsaw, Poland 1995.   */
  14
  15 #include "tl.h"
  16
  17 #if 1
  18 #define log(e, u, d)    event[e][(int) u] += (long) d;
  19 #else
  20 #define log(e, u, d)
  21 #endif
  22
  23 #define A_LARGE         80
  24 #define A_USER          0x55000000
  25 #define NOTOOBIG        32768
  26
  27 #define POOL            0
  28 #define ALLOC           1
  29 #define FREE            2
  30 #define NREVENT         3
  31
  32 extern  unsigned long All_Mem;
  33 extern  int tl_verbose;
  34
  35 union M {
  36         long size;
  37         union M *link;
  38 };
  39
  40 static union M *freelist[A_LARGE];
  41 static long     req[A_LARGE];
  42 static long     event[NREVENT][A_LARGE];
  43
  44 void *
  45 tl_emalloc(int U)
  46 {       union M *m;
  47         long r, u;
  48         void *rp;
  49
  50         u = (long) ((U-1)/sizeof(union M) + 2);
  51
  52         if (u >= A_LARGE)
  53         {       log(ALLOC, 0, 1);
  54                 if (tl_verbose)
  55                 printf("tl_spin: memalloc %ld bytes\n", u);
  56                 m = (union M *) emalloc((int) u*sizeof(union M));
  57                 All_Mem += (unsigned long) u*sizeof(union M);
  58         } else
  59         {       if (!freelist[u])
  60                 {       r = req[u] += req[u] ? req[u] : 1;
  61                         if (r >= NOTOOBIG)
  62                                 r = req[u] = NOTOOBIG;
  63                         log(POOL, u, r);
  64                         freelist[u] = (union M *)
  65                                 emalloc((int) r*u*sizeof(union M));
  66                         All_Mem += (unsigned long) r*u*sizeof(union M);
  67                         m = freelist[u] + (r-2)*u;
  68                         for ( ; m >= freelist[u]; m -= u)
  69                                 m->link = m+u;
  70                 }
  71                 log(ALLOC, u, 1);
  72                 m = freelist[u];
  73                 freelist[u] = m->link;
  74         }
  75         m->size = (u|A_USER);
  76
  77         for (r = 1; r < u; )
  78                 (&m->size)[r++] = 0;
  79
  80         rp = (void *) (m+1);
  81         memset(rp, 0, U);
  82         return rp;
  83 }
  84
  85 void
  86 tfree(void *v)
  87 {       union M *m = (union M *) v;
  88         long u;
  89
  90         --m;
  91         if ((m->size&0xFF000000) != A_USER)
  92                 Fatal("releasing a free block", (char *)0);
  93
  94         u = (m->size &= 0xFFFFFF);
  95         if (u >= A_LARGE)
  96         {       log(FREE, 0, 1);
  97                 /* free(m); */
  98         } else
  99         {       log(FREE, u, 1);
 100                 m->link = freelist[u];
 101                 freelist[u] = m;
 102         }
 103 }
 104
 105 void
 106 a_stats(void)
 107 {       long    p, a, f;
 108         int     i;
 109
 110         printf(" size\t  pool\tallocs\t frees\n");
 111         for (i = 0; i < A_LARGE; i++)
 112         {       p = event[POOL][i];
 113                 a = event[ALLOC][i];
 114                 f = event[FREE][i];
 115
 116                 if(p|a|f)
 117                 printf("%5d\t%6ld\t%6ld\t%6ld\n",
 118                         i, p, a, f);
 119         }
 120 }