1 /***** tl_spin: tl_mem.c *****/
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 */
12 /* Based on the translation algorithm by Gerth, Peled, Vardi, and Wolper, */
13 /* presented at the PSTV Conference, held in 1995, Warsaw, Poland 1995. */
18 #define log(e, u, d) event[e][(int) u] += (long) d;
24 #define A_USER 0x55000000
25 #define NOTOOBIG 32768
32 extern unsigned long All_Mem;
33 extern int tl_verbose;
40 static union M *freelist[A_LARGE];
41 static long req[A_LARGE];
42 static long event[NREVENT][A_LARGE];
50 u = (long) ((U-1)/sizeof(union M) + 2);
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);
60 { r = req[u] += req[u] ? req[u] : 1;
62 r = req[u] = NOTOOBIG;
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)
73 freelist[u] = m->link;
87 { union M *m = (union M *) v;
91 if ((m->size&0xFF000000) != A_USER)
92 Fatal("releasing a free block", (char *)0);
94 u = (m->size &= 0xFFFFFF);
100 m->link = freelist[u];
110 printf(" size\t pool\tallocs\t frees\n");
111 for (i = 0; i < A_LARGE; i++)
112 { p = event[POOL][i];
117 printf("%5d\t%6ld\t%6ld\t%6ld\n",