convert from svn repository: remove tags directory
[lttv.git] / trunk / verif / Spin / Src5.1.6 / tl_mem.c
CommitLineData
0b55f123 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
32extern unsigned long All_Mem;
33extern int tl_verbose;
34
35union M {
36 long size;
37 union M *link;
38};
39
40static union M *freelist[A_LARGE];
41static long req[A_LARGE];
42static long event[NREVENT][A_LARGE];
43
44void *
45tl_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
85void
86tfree(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
105void
106a_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}
This page took 0.026607 seconds and 4 git commands to generate.