Line data Source code
1 : // Author(s): Maurice Laveaux.
2 : // Copyright: see the accompanying file COPYING or copy at
3 : // https://github.com/mCRL2org/mCRL2/blob/master/COPYING
4 : //
5 : // Distributed under the Boost Software License, Version 1.0.
6 : // (See accompanying file LICENSE_1_0.txt or copy at
7 : // http://www.boost.org/LICENSE_1_0.txt)
8 : //
9 :
10 : #ifndef ATERMPP_DETAIL_ATERM_POOL_IMPLEMENTATION_H
11 : #define ATERMPP_DETAIL_ATERM_POOL_IMPLEMENTATION_H
12 : #pragma once
13 :
14 : #include <chrono>
15 : #include "aterm_pool.h"
16 : #include "aterm_pool_storage_implementation.h" // For store_in_argument_array.
17 :
18 :
19 : namespace atermpp
20 : {
21 : namespace detail
22 : {
23 :
24 143 : aterm_pool::aterm_pool() :
25 143 : m_int_storage(*this),
26 143 : m_appl_storage(
27 : *this,
28 : *this,
29 : *this,
30 : *this,
31 : *this,
32 : *this,
33 : *this,
34 : *this
35 : ),
36 286 : m_appl_dynamic_storage(*this)
37 : {
38 143 : m_count_until_collection = capacity();
39 143 : m_count_until_resize = m_int_storage.capacity();
40 :
41 : if constexpr (EnableAggressiveGarbageCollection)
42 : {
43 : m_count_until_collection = 1;
44 : }
45 :
46 : // Initialize the empty list.
47 143 : create_appl(m_empty_list, m_function_symbol_pool.as_empty_list());
48 143 : }
49 :
50 1 : void aterm_pool::add_deletion_hook(function_symbol sym, term_callback callback)
51 : {
52 1 : const std::size_t arity = sym.arity();
53 :
54 1 : switch (arity)
55 : {
56 0 : case 0:
57 : {
58 0 : if (sym == get_symbol_pool().as_int())
59 : {
60 0 : m_int_storage.add_deletion_hook(sym, callback);
61 : }
62 : else
63 : {
64 0 : std::get<0>(m_appl_storage).add_deletion_hook(sym, callback);
65 : }
66 : }
67 0 : break;
68 1 : case 1:
69 1 : std::get<1>(m_appl_storage).add_deletion_hook(sym, callback);
70 1 : break;
71 0 : case 2:
72 0 : std::get<2>(m_appl_storage).add_deletion_hook(sym, callback);
73 0 : break;
74 0 : case 3:
75 0 : std::get<3>(m_appl_storage).add_deletion_hook(sym, callback);
76 0 : break;
77 0 : case 4:
78 0 : std::get<4>(m_appl_storage).add_deletion_hook(sym, callback);
79 0 : break;
80 0 : case 5:
81 0 : std::get<5>(m_appl_storage).add_deletion_hook(sym, callback);
82 0 : break;
83 0 : case 6:
84 0 : std::get<6>(m_appl_storage).add_deletion_hook(sym, callback);
85 0 : break;
86 0 : case 7:
87 0 : std::get<7>(m_appl_storage).add_deletion_hook(sym, callback);
88 0 : break;
89 0 : default:
90 0 : m_appl_dynamic_storage.add_deletion_hook(sym, callback);
91 : }
92 1 : }
93 :
94 1002 : void aterm_pool::collect(mcrl2::utilities::shared_mutex& mutex)
95 : {
96 1002 : m_count_until_collection = 0;
97 1002 : collect_impl(mutex);
98 1002 : }
99 :
100 144 : void aterm_pool::register_thread_aterm_pool(thread_aterm_pool_interface& pool)
101 : {
102 144 : mcrl2::utilities::lock_guard guard = m_shared_mutex.lock();
103 144 : m_thread_pools.insert(m_thread_pools.end(), &pool);
104 144 : }
105 :
106 144 : void aterm_pool::remove_thread_aterm_pool(thread_aterm_pool_interface& pool)
107 : {
108 144 : mcrl2::utilities::lock_guard guard = m_shared_mutex.lock();
109 :
110 144 : auto it = std::find(m_thread_pools.begin(), m_thread_pools.end(), &pool);
111 144 : if (it != m_thread_pools.end())
112 : {
113 144 : m_thread_pools.erase(it); // This only removes the pointer, not the underlying data
114 : // structure, which only disappears when the thread is removed.
115 : }
116 144 : }
117 :
118 1015 : void aterm_pool::print_performance_statistics() const
119 : {
120 1015 : m_int_storage.print_performance_stats("integral_storage");
121 1015 : std::get<0>(m_appl_storage).print_performance_stats("term_storage");
122 1015 : std::get<1>(m_appl_storage).print_performance_stats("function_application_storage_1");
123 1015 : std::get<2>(m_appl_storage).print_performance_stats("function_application_storage_2");
124 1015 : std::get<3>(m_appl_storage).print_performance_stats("function_application_storage_3");
125 1015 : std::get<4>(m_appl_storage).print_performance_stats("function_application_storage_4");
126 1015 : std::get<5>(m_appl_storage).print_performance_stats("function_application_storage_5");
127 1015 : std::get<6>(m_appl_storage).print_performance_stats("function_application_storage_6");
128 1015 : std::get<7>(m_appl_storage).print_performance_stats("function_application_storage_7");
129 :
130 1015 : m_appl_dynamic_storage.print_performance_stats("arbitrary_function_application_storage");
131 :
132 : // Print information for the local aterm pools.
133 2932 : for (const thread_aterm_pool_interface* local : m_thread_pools)
134 : {
135 1917 : local->print_local_performance_statistics();
136 : }
137 1015 : }
138 :
139 181 : std::size_t aterm_pool::capacity() const noexcept
140 : {
141 : // Determine the total number of terms in any storage.
142 181 : return m_int_storage.capacity()
143 181 : + std::get<0>(m_appl_storage).capacity()
144 181 : + std::get<1>(m_appl_storage).capacity()
145 181 : + std::get<2>(m_appl_storage).capacity()
146 181 : + std::get<3>(m_appl_storage).capacity()
147 181 : + std::get<4>(m_appl_storage).capacity()
148 181 : + std::get<5>(m_appl_storage).capacity()
149 181 : + std::get<6>(m_appl_storage).capacity()
150 181 : + std::get<7>(m_appl_storage).capacity()
151 181 : + m_appl_dynamic_storage.capacity();
152 : }
153 :
154 2030 : std::size_t aterm_pool::size() const
155 : {
156 : // Determine the total number of terms in any storage.
157 2030 : return m_int_storage.size()
158 2030 : + std::get<0>(m_appl_storage).size()
159 2030 : + std::get<1>(m_appl_storage).size()
160 2030 : + std::get<2>(m_appl_storage).size()
161 2030 : + std::get<3>(m_appl_storage).size()
162 2030 : + std::get<4>(m_appl_storage).size()
163 2030 : + std::get<5>(m_appl_storage).size()
164 2030 : + std::get<6>(m_appl_storage).size()
165 2030 : + std::get<7>(m_appl_storage).size()
166 2030 : + m_appl_dynamic_storage.size();
167 : }
168 :
169 : // private
170 :
171 1049346 : void aterm_pool::created_term(bool allow_collect, mcrl2::utilities::shared_mutex& shared_mutex)
172 : {
173 : // Defer garbage collection when it happens too often.
174 2098692 : if (m_count_until_collection.load(std::memory_order_relaxed) <= 0)
175 : {
176 16 : if (allow_collect)
177 : {
178 13 : collect_impl(shared_mutex);
179 : }
180 : }
181 : else
182 : {
183 1049330 : m_count_until_collection.fetch_sub(1, std::memory_order_relaxed);
184 : }
185 :
186 2098692 : if (m_count_until_resize.load(std::memory_order_relaxed) <= 0)
187 : {
188 68 : if (allow_collect)
189 : {
190 38 : resize_if_needed(shared_mutex);
191 : }
192 : }
193 : else
194 : {
195 1049278 : m_count_until_resize.fetch_sub(1, std::memory_order_relaxed);
196 : }
197 1049346 : }
198 :
199 1015 : void aterm_pool::collect_impl(mcrl2::utilities::shared_mutex& shared_mutex)
200 : {
201 1015 : if (m_enable_garbage_collection)
202 : {
203 1015 : mcrl2::utilities::lock_guard guard = shared_mutex.lock();
204 1015 : if (m_count_until_collection > 0)
205 : {
206 : // Another thread has performed garbage collection, so we can ignore it.
207 0 : return;
208 : }
209 :
210 1015 : auto timestamp = std::chrono::system_clock::now();
211 1015 : std::size_t old_size = size();
212 :
213 : // Mark the terms referenced by all thread pools.
214 2932 : for (const auto& pool : m_thread_pools)
215 : {
216 1917 : pool->mark();
217 : }
218 :
219 1015 : assert(std::get<0>(m_appl_storage).verify_mark());
220 1015 : assert(std::get<1>(m_appl_storage).verify_mark());
221 1015 : assert(std::get<2>(m_appl_storage).verify_mark());
222 1015 : assert(std::get<3>(m_appl_storage).verify_mark());
223 1015 : assert(std::get<4>(m_appl_storage).verify_mark());
224 1015 : assert(std::get<5>(m_appl_storage).verify_mark());
225 1015 : assert(std::get<6>(m_appl_storage).verify_mark());
226 1015 : assert(std::get<7>(m_appl_storage).verify_mark());
227 1015 : assert(m_appl_dynamic_storage.verify_mark());
228 :
229 : // Keep track of the duration for marking and reset for sweep.
230 1015 : auto mark_duration = std::chrono::duration_cast<std::chrono::milliseconds>(std::chrono::system_clock::now() - timestamp).count();
231 1015 : timestamp = std::chrono::system_clock::now();
232 : // Collect all terms that are not marked.
233 1015 : m_appl_dynamic_storage.sweep();
234 1015 : std::get<7>(m_appl_storage).sweep();
235 1015 : std::get<6>(m_appl_storage).sweep();
236 1015 : std::get<5>(m_appl_storage).sweep();
237 1015 : std::get<4>(m_appl_storage).sweep();
238 1015 : std::get<3>(m_appl_storage).sweep();
239 1015 : std::get<2>(m_appl_storage).sweep();
240 1015 : std::get<1>(m_appl_storage).sweep();
241 1015 : std::get<0>(m_appl_storage).sweep();
242 1015 : m_int_storage.sweep();
243 :
244 : // Check that after sweeping the terms are consistent.
245 1015 : assert(m_int_storage.verify_sweep());
246 1015 : assert(std::get<0>(m_appl_storage).verify_sweep());
247 1015 : assert(std::get<1>(m_appl_storage).verify_sweep());
248 1015 : assert(std::get<2>(m_appl_storage).verify_sweep());
249 1015 : assert(std::get<3>(m_appl_storage).verify_sweep());
250 1015 : assert(std::get<4>(m_appl_storage).verify_sweep());
251 1015 : assert(std::get<5>(m_appl_storage).verify_sweep());
252 1015 : assert(std::get<6>(m_appl_storage).verify_sweep());
253 1015 : assert(std::get<7>(m_appl_storage).verify_sweep());
254 1015 : assert(m_appl_dynamic_storage.verify_sweep());
255 :
256 : // Print some statistics.
257 : if (EnableGarbageCollectionMetrics)
258 : {
259 : // Update the times
260 : auto sweep_duration = std::chrono::duration_cast<std::chrono::milliseconds>(std::chrono::system_clock::now() - timestamp).count();
261 :
262 : // Print the relevant information.
263 : mCRL2log(mcrl2::log::info) << "g_term_pool(): Garbage collected " << old_size - size() << " terms, " << size() << " terms remaining in "
264 : << mark_duration + sweep_duration << " ms (marking " << mark_duration << " ms + sweep " << sweep_duration << " ms).\n";
265 : }
266 :
267 : // Garbage collect function symbols.
268 1015 : m_function_symbol_pool.sweep();
269 :
270 1015 : print_performance_statistics();
271 :
272 : // Use some heuristics to determine when the next collect should be called automatically.
273 1015 : m_count_until_collection = size() + protection_set_size();
274 :
275 : if constexpr (EnableAggressiveGarbageCollection)
276 : {
277 : m_count_until_collection = 1;
278 : }
279 1015 : }
280 : }
281 :
282 20218 : function_symbol aterm_pool::create_function_symbol(const std::string& name, const std::size_t arity, const bool check_for_registered_functions)
283 : {
284 20218 : return m_function_symbol_pool.create(name, arity, check_for_registered_functions);
285 : }
286 :
287 1081046 : function_symbol aterm_pool::create_function_symbol(std::string&& name, const std::size_t arity, const bool check_for_registered_functions)
288 : {
289 1081046 : return m_function_symbol_pool.create(std::forward<std::string>(name), arity, check_for_registered_functions);
290 : }
291 :
292 19731852 : bool aterm_pool::create_int(aterm& term, size_t val)
293 : {
294 19731852 : return m_int_storage.create_int(term, val);
295 : }
296 :
297 894361 : bool aterm_pool::create_term(aterm& term, const atermpp::function_symbol& sym)
298 : {
299 894361 : return std::get<0>(m_appl_storage).create_term(term, sym);
300 : }
301 :
302 : template<class ...Terms>
303 147850637 : bool aterm_pool::create_appl(aterm& term, const function_symbol& sym, const Terms&... arguments)
304 : {
305 : if constexpr (sizeof...(Terms) <= 7)
306 : {
307 147850635 : return std::get<sizeof...(Terms)>(m_appl_storage).create_appl(term, sym, arguments...);
308 : }
309 : else
310 : {
311 2 : std::array<unprotected_aterm, sizeof...(Terms)> array;
312 2 : store_in_argument_array(array, arguments...);
313 4 : return m_appl_dynamic_storage.create_appl_dynamic(term, sym, array.begin(), array.end());
314 : }
315 : }
316 :
317 : template<typename ForwardIterator>
318 1112177 : bool aterm_pool::create_appl_dynamic(aterm& term,
319 : const function_symbol& sym,
320 : ForwardIterator begin,
321 : ForwardIterator end)
322 : {
323 1112177 : const std::size_t arity = sym.arity();
324 :
325 1112177 : switch(arity)
326 : {
327 99517 : case 0:
328 99517 : return std::get<0>(m_appl_storage).create_term(term, sym);
329 45602 : case 1:
330 45602 : return std::get<1>(m_appl_storage).template create_appl_iterator<ForwardIterator>(term, sym, begin, end);
331 309885 : case 2:
332 309885 : return std::get<2>(m_appl_storage).template create_appl_iterator<ForwardIterator>(term, sym, begin, end);
333 616003 : case 3:
334 616003 : return std::get<3>(m_appl_storage).template create_appl_iterator<ForwardIterator>(term, sym, begin, end);
335 38380 : case 4:
336 38380 : return std::get<4>(m_appl_storage).template create_appl_iterator<ForwardIterator>(term, sym, begin, end);
337 1510 : case 5:
338 1510 : return std::get<5>(m_appl_storage).template create_appl_iterator<ForwardIterator>(term, sym, begin, end);
339 376 : case 6:
340 376 : return std::get<6>(m_appl_storage).template create_appl_iterator<ForwardIterator>(term, sym, begin, end);
341 422 : case 7:
342 422 : return std::get<7>(m_appl_storage).template create_appl_iterator<ForwardIterator>(term, sym, begin, end);
343 482 : default:
344 482 : return m_appl_dynamic_storage.create_appl_dynamic(term, sym, begin, end);
345 : }
346 : }
347 :
348 : template<typename InputIterator, typename ATermConverter>
349 10261477 : bool aterm_pool::create_appl_dynamic(aterm& term,
350 : const function_symbol& sym,
351 : ATermConverter converter,
352 : InputIterator begin,
353 : InputIterator end)
354 : {
355 10261477 : const std::size_t arity = sym.arity();
356 10261477 : switch(arity)
357 : {
358 194145 : case 0:
359 194145 : return std::get<0>(m_appl_storage).create_term(term, sym);
360 90376 : case 1:
361 90376 : return std::get<1>(m_appl_storage).template create_appl_iterator<InputIterator, ATermConverter>(term, sym, converter, begin, end);
362 3366534 : case 2:
363 3366534 : return std::get<2>(m_appl_storage).template create_appl_iterator<InputIterator, ATermConverter>(term, sym, converter, begin, end);
364 5543562 : case 3:
365 5543562 : return std::get<3>(m_appl_storage).template create_appl_iterator<InputIterator, ATermConverter>(term, sym, converter, begin, end);
366 937167 : case 4:
367 937167 : return std::get<4>(m_appl_storage).template create_appl_iterator<InputIterator, ATermConverter>(term, sym, converter, begin, end);
368 126745 : case 5:
369 126745 : return std::get<5>(m_appl_storage).template create_appl_iterator<InputIterator, ATermConverter>(term, sym, converter, begin, end);
370 653 : case 6:
371 653 : return std::get<6>(m_appl_storage).template create_appl_iterator<InputIterator, ATermConverter>(term, sym, converter, begin, end);
372 1128 : case 7:
373 1128 : return std::get<7>(m_appl_storage).template create_appl_iterator<InputIterator, ATermConverter>(term, sym, converter, begin, end);
374 1167 : default:
375 1167 : return m_appl_dynamic_storage.create_appl_dynamic(term, sym, converter, begin, end);
376 : }
377 : }
378 :
379 38 : void aterm_pool::resize_if_needed(mcrl2::utilities::shared_mutex& mutex)
380 : {
381 38 : mcrl2::utilities::lock_guard guard = mutex.lock();
382 38 : if (m_count_until_resize > 0)
383 : {
384 : // Another thread has resized the tables, so we can ignore it.
385 0 : return;
386 : }
387 :
388 38 : auto timestamp = std::chrono::system_clock::now();
389 38 : std::size_t old_capacity = capacity();
390 38 : std::size_t old_symbols_capacity = m_function_symbol_pool.capacity();
391 :
392 : // Attempt to resize all storages.
393 38 : m_function_symbol_pool.resize_if_needed();
394 :
395 38 : m_int_storage.resize_if_needed();
396 38 : std::get<0>(m_appl_storage).resize_if_needed();
397 38 : std::get<1>(m_appl_storage).resize_if_needed();
398 38 : std::get<2>(m_appl_storage).resize_if_needed();
399 38 : std::get<3>(m_appl_storage).resize_if_needed();
400 38 : std::get<4>(m_appl_storage).resize_if_needed();
401 38 : std::get<5>(m_appl_storage).resize_if_needed();
402 38 : std::get<6>(m_appl_storage).resize_if_needed();
403 38 : std::get<7>(m_appl_storage).resize_if_needed();
404 38 : m_appl_dynamic_storage.resize_if_needed();
405 :
406 : // Attempt to resize ever so often.
407 38 : m_count_until_resize = 10000;
408 :
409 : if (EnableGarbageCollectionMetrics && (old_capacity != capacity() || old_symbols_capacity != m_function_symbol_pool.capacity()))
410 : {
411 : // Only print if a resize actually took place.
412 : auto duration = std::chrono::duration_cast<std::chrono::milliseconds>(std::chrono::system_clock::now() - timestamp).count();
413 :
414 : mCRL2log(mcrl2::log::info) << "aterm_pool: Resized hash tables from " << old_capacity << " to " << capacity() << " capacity in "
415 : << duration << " ms.\n";
416 : }
417 38 : }
418 :
419 1015 : std::size_t aterm_pool::protection_set_size() const
420 : {
421 1015 : std::size_t result = 0;
422 :
423 2932 : for (const auto& pool : m_thread_pools)
424 : {
425 1917 : result += pool->protection_set_size();
426 : }
427 :
428 1015 : return result;
429 : }
430 :
431 : } // namespace detail
432 : } // namespace atermpp
433 :
434 : #endif // ATERMPP_DETAIL_ATERM_POOL_IMPLEMENTATION_H
|
