1 /*
2 * This file is part of the Yices SMT Solver.
3 * Copyright (C) 2017 SRI International.
4 *
5 * Yices is free software: you can redistribute it and/or modify
6 * it under the terms of the GNU General Public License as published by
7 * the Free Software Foundation, either version 3 of the License, or
8 * (at your option) any later version.
9 *
10 * Yices is distributed in the hope that it will be useful,
11 * but WITHOUT ANY WARRANTY; without even the implied warranty of
12 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
13 * GNU General Public License for more details.
14 *
15 * You should have received a copy of the GNU General Public License
16 * along with Yices. If not, see <http://www.gnu.org/licenses/>.
17 */
18
19 /*
20 * SPARSE ARRAYS FOR REGISTERING ROOTS
21 */
22
23 /*
24 * For garbage collection, we must keep track of root terms and types (i.e.,
25 * terms and types that the application wants to keep).
26 *
27 * For this purpose, we use reference counting. When a term/type is registered
28 * as a root, we increment a counter for this term/type. We store the counts
29 * in a sparse array structure.
30 *
31 * The array is divided in blocks of equal size (block size = 64 for
32 * now), and we use one bit per block to record whether the block is
33 * used or not.
34 * - a block marked as dirty is not initialized and its
35 * content shouldn't be read
36 * - if a block is clean then all elements in the block have a valid value
37 * - a block is initialized (all elements set to 0) on the first write into that block
38 *
39 * So the reference count for i is 0 if i is in a dirty block or
40 * a->data[i] otherwise. We keep track of the total number of roots (i.e.,
41 * the number of i such that refcount for i is positive) in a->nelems.
42 *
43 * Overflow of a->data[i] is unlikely, but we take care of it anyway:
44 * - if a->data[i] reaches UINT32_MAX then the ref counter is frozen
45 * incrementing or decrementing the ref counter for i does nothing.
46 */
47
48 #ifndef __SPARSE_ARRAYS_H
49 #define __SPARSE_ARRAYS_H
50
51 #include <stdint.h>
52 #include <stdbool.h>
53 #include <assert.h>
54
55 #include "utils/bitvectors.h"
56
57
58 /*
59 * Data structure:
60 * - data = the array proper
61 * - clean = bit vector for marks:
62 * block i is dirty if clean[i] is 0
63 * block i is clean if clean[i] is 1
64 * - nblocks = number of blocks
65 * - nelems = number of elements i such that a[i] > 0
66 */
67 typedef struct sparse_array_s {
68 uint32_t *data;
69 byte_t *clean;
70 uint32_t nblocks;
71 uint32_t nelems;
72 } sparse_array_t;
73
74
75 /*
76 * Block size: must be a power of two
77 */
78 #define BSIZE_NBITS 6u
79 #define BSIZE (1u<<BSIZE_NBITS)
80
81
82 /*
83 * Default array size = 32 blocks
84 */
85 #define DEF_SPARSE_ARRAY_NBLOCKS 32u
86 #define DEF_SPARSE_ARRAY_SIZE (DEF_SPARSE_ARRAY_NBLOCKS * BSIZE)
87
88
89 /*
90 * Maximal number of blocks: block indices are in [0, MAX_NBLOCKS - 1]
91 */
92 #define MAX_SPARSE_ARRAY_SIZE (UINT32_MAX/sizeof(uint32_t))
93 #define MAX_NBLOCKS ((MAX_SPARSE_ARRAY_SIZE>>BSIZE_NBITS) + 1)
94
95
96 // block in which index i resides
block_of_index(uint32_t i)97 static inline uint32_t block_of_index(uint32_t i) {
98 return i >> BSIZE_NBITS;
99 }
100
101 // start and end indices of block k
block_start(uint32_t k)102 static inline uint32_t block_start(uint32_t k) {
103 assert(k < MAX_NBLOCKS);
104 return k << BSIZE_NBITS;
105 }
106
block_end(uint32_t k)107 static inline uint32_t block_end(uint32_t k) {
108 return block_start(k) + (BSIZE - 1);
109 }
110
111
112
113 /*
114 * MAIN OPERATIONS
115 */
116
117 /*
118 * Initialize a:
119 * - n = minimal size requested (number of elements in a)
120 * - if n is 0, the default size is used
121 * - all blocks are marked as dirty
122 */
123 extern void init_sparse_array(sparse_array_t *a, uint32_t n);
124
125
126 /*
127 * Delete: free all memory
128 */
129 extern void delete_sparse_array(sparse_array_t *a);
130
131
132 /*
133 * Reset: mark all blocks as dirty
134 */
135 extern void reset_sparse_array(sparse_array_t *a);
136
137
138 /*
139 * Increment the ref counter a[i]
140 */
141 extern void sparse_array_incr(sparse_array_t *a, uint32_t i);
142
143
144 /*
145 * Decrement a[i]: the ref counter must be positive (so i must be in a clean block).
146 */
147 extern void sparse_array_decr(sparse_array_t *a, uint32_t i);
148
149
150 /*
151 * Get the ref counter for i
152 * - return 0 if i is in a dirty block or outside a->data
153 */
154 extern uint32_t sparse_array_read(sparse_array_t *a, uint32_t i);
155
156
157 /*
158 * ITERATOR
159 */
160
161 /*
162 * Call f(aux, i) for all elements of a such that a[i] > 0
163 */
164 typedef void (*sparse_array_iterator_t)(void *aux, uint32_t i);
165
166 extern void sparse_array_iterate(sparse_array_t *a, void *aux, sparse_array_iterator_t f);
167
168
169
170 #endif /* __SPARSE_ARRAYS_H */
171