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_THREAD_ATERM_POOL_IMPLEMENTATION_H
11 : #define ATERMPP_DETAIL_THREAD_ATERM_POOL_IMPLEMENTATION_H
12 : #pragma once
13 :
14 : #include <chrono>
15 :
16 : #include "thread_aterm_pool.h"
17 : #include "mcrl2/atermpp/detail/index_traits.h"
18 :
19 :
20 : namespace atermpp
21 : {
22 : namespace detail
23 : {
24 :
25 1081046 : function_symbol thread_aterm_pool::create_function_symbol(std::string&& name, const std::size_t arity, const bool check_for_registered_functions)
26 : {
27 1081046 : mcrl2::utilities::shared_guard guard = m_shared_mutex.lock_shared();
28 1081046 : function_symbol symbol = m_pool.create_function_symbol(std::move(name), arity, check_for_registered_functions);
29 2162092 : return symbol;
30 1081046 : }
31 :
32 1068474 : function_symbol thread_aterm_pool::create_function_symbol(const std::string& name, const std::size_t arity, const bool check_for_registered_functions)
33 : {
34 1068474 : std::string name_copy = name;
35 2136948 : return create_function_symbol(std::move(name_copy), arity, check_for_registered_functions);
36 1068474 : }
37 :
38 10815 : void thread_aterm_pool::create_int(aterm& term, size_t val)
39 : {
40 10815 : mcrl2::utilities::shared_guard guard = m_shared_mutex.lock_shared();
41 10815 : bool added = m_pool.create_int(term, val);
42 10815 : guard.unlock_shared();
43 :
44 10815 : if (added) { m_pool.created_term(!m_shared_mutex.is_shared_locked(), m_shared_mutex); }
45 10815 : }
46 :
47 894361 : void thread_aterm_pool::create_term(aterm& term, const atermpp::function_symbol& sym)
48 : {
49 894361 : mcrl2::utilities::shared_guard guard = m_shared_mutex.lock_shared();
50 894361 : bool added = m_pool.create_term(term, sym);
51 894361 : guard.unlock_shared();
52 :
53 894361 : if (added) { m_pool.created_term(!m_shared_mutex.is_shared_locked(), m_shared_mutex); }
54 894361 : }
55 :
56 : template<class ...Terms>
57 128124209 : void thread_aterm_pool::create_appl(aterm& term, const function_symbol& sym, const Terms&... arguments)
58 : {
59 128124209 : mcrl2::utilities::shared_guard guard = m_shared_mutex.lock_shared();
60 128124209 : bool added = m_pool.create_appl(term, sym, arguments...);
61 128124207 : guard.unlock_shared();
62 :
63 128124207 : if (added) { m_pool.created_term(!m_shared_mutex.is_shared_locked(), m_shared_mutex); }
64 128124209 : }
65 :
66 : template<class Term, class INDEX_TYPE, class ...Terms>
67 19721037 : void thread_aterm_pool::create_appl_index(aterm& term, const function_symbol& sym, const Terms&... arguments)
68 : {
69 19721037 : mcrl2::utilities::shared_guard guard = m_shared_mutex.lock_shared();
70 19721037 : std::array<unprotected_aterm, sizeof...(arguments)> argument_array;
71 19721037 : store_in_argument_array(argument_array, arguments...);
72 :
73 : bool added;
74 : if constexpr (sizeof...(arguments)==1)
75 : {
76 : /* Code below is more elegant than succeeding code, but it unnecessarily copies and protects a term.
77 : m_pool.create_int(term, atermpp::detail::index_traits<Term, INDEX_TYPE, 1>::
78 : insert(static_cast<INDEX_TYPE>(static_cast<aterm>(address(argument_array[0]))))); */
79 : m_pool.create_int(term,
80 : atermpp::detail::index_traits<Term, INDEX_TYPE, 1>::
81 : insert(*reinterpret_cast<INDEX_TYPE*>(&(argument_array[0]))));
82 : added = m_pool.create_appl(term, sym, argument_array[0], term);
83 : }
84 : else
85 : {
86 : /* Code below is more elegant than the actual succeeding code, but it unnecessarily creates an extra pair, which is costly.
87 : m_pool.create_int(
88 : term,
89 : atermpp::detail::index_traits<Term, INDEX_TYPE, 2>::
90 : insert(std::make_pair(static_cast<typename INDEX_TYPE::first_type>(static_cast<aterm>(address(argument_array[0]))),
91 : static_cast<typename INDEX_TYPE::second_type>(static_cast<aterm>(address(argument_array[1])))))); */
92 19721037 : m_pool.create_int(term,
93 : atermpp::detail::index_traits<Term, INDEX_TYPE, 2>::
94 19721037 : insert(*reinterpret_cast<INDEX_TYPE*>(&argument_array[0])));
95 19721037 : added = m_pool.create_appl(term, sym, argument_array[0], argument_array[1], term);
96 : }
97 19721037 : guard.unlock_shared();
98 :
99 19721037 : if (added) { m_pool.created_term(!m_shared_mutex.is_shared_locked(), m_shared_mutex); }
100 19721037 : }
101 :
102 : template<typename InputIterator>
103 1111055 : void thread_aterm_pool::create_appl_dynamic(aterm& term,
104 : const function_symbol& sym,
105 : InputIterator begin,
106 : InputIterator end)
107 : {
108 1111055 : mcrl2::utilities::shared_guard guard = m_shared_mutex.lock_shared();
109 1111055 : bool added = m_pool.create_appl_dynamic(term, sym, begin, end);
110 1111055 : guard.unlock_shared();
111 :
112 1111055 : if (added) { m_pool.created_term(!m_shared_mutex.is_shared_locked(), m_shared_mutex); }
113 1111055 : }
114 :
115 : template<typename InputIterator, typename ATermConverter>
116 10259649 : void thread_aterm_pool::create_appl_dynamic(aterm& term,
117 : const function_symbol& sym,
118 : ATermConverter convert_to_aterm,
119 : InputIterator begin,
120 : InputIterator end)
121 : {
122 10259649 : mcrl2::utilities::shared_guard guard = m_shared_mutex.lock_shared();
123 10259649 : bool added = m_pool.create_appl_dynamic(term, sym, convert_to_aterm, begin, end);
124 10259649 : guard.unlock_shared();
125 :
126 10259649 : if (added) { m_pool.created_term(!m_shared_mutex.is_shared_locked(), m_shared_mutex); }
127 10259649 : }
128 :
129 21756409179 : void thread_aterm_pool::register_variable(aterm* variable)
130 : {
131 : if constexpr (EnableVariableRegistrationMetrics) { ++m_variable_insertions; }
132 :
133 21756409179 : mcrl2::utilities::shared_guard guard = m_shared_mutex.lock_shared();
134 :
135 : // Resizing of the protection set should not interfere with garbage collection and rehashing
136 21756409179 : if (m_variables->must_resize())
137 : {
138 732 : m_variables->resize();
139 : }
140 :
141 21756409179 : auto [it, inserted] = m_variables->insert(variable);
142 :
143 : // The variable must be inserted.
144 21756409179 : assert(inserted);
145 21756409179 : mcrl2::utilities::mcrl2_unused(it);
146 21756409179 : mcrl2::utilities::mcrl2_unused(inserted);
147 21756409179 : }
148 :
149 21756366559 : void thread_aterm_pool::deregister_variable(aterm* variable)
150 : {
151 21756366559 : mcrl2::utilities::shared_guard guard = m_shared_mutex.lock_shared();
152 21756366559 : m_variables->erase(variable);
153 21756366559 : }
154 :
155 52057 : void thread_aterm_pool::register_container(aterm_container* container)
156 : {
157 : if constexpr (EnableVariableRegistrationMetrics) { ++m_container_insertions; }
158 :
159 52057 : mcrl2::utilities::shared_guard guard = m_shared_mutex.lock_shared();
160 52057 : if (m_containers->must_resize())
161 : {
162 0 : m_containers->resize();
163 : }
164 52057 : auto [it, inserted] = m_containers->insert(container);
165 :
166 : // The container must be inserted.
167 52057 : assert(inserted);
168 52057 : mcrl2::utilities::mcrl2_unused(it);
169 52057 : mcrl2::utilities::mcrl2_unused(inserted);
170 52057 : }
171 :
172 52057 : void thread_aterm_pool::deregister_container(aterm_container* container)
173 : {
174 52057 : mcrl2::utilities::shared_guard guard = m_shared_mutex.lock_shared();
175 52057 : m_containers->erase(container);
176 52057 : }
177 :
178 1931 : void thread_aterm_pool::mark()
179 : {
180 353931 : for (const aterm* variable : *m_variables)
181 : {
182 352000 : if (variable != nullptr)
183 : {
184 : // Mark all terms (and their subterms) that are reachable, i.e the root set.
185 29130 : _aterm* term = detail::address(*variable);
186 29130 : if (term != nullptr && !term->is_marked())
187 : {
188 : // This variable is not a default term and that term has not been marked.
189 8739 : mark_term(*term, m_todo);
190 : }
191 : }
192 : }
193 :
194 249099 : for (const aterm_container* container : *m_containers)
195 : {
196 247168 : if (container != nullptr)
197 : {
198 : // The container marks the contained terms itself.
199 994 : container->mark(m_todo);
200 : }
201 : }
202 1931 : }
203 :
204 1931 : void thread_aterm_pool::print_local_performance_statistics() const
205 : {
206 : if constexpr (EnableVariableRegistrationMetrics)
207 : {
208 : mCRL2log(mcrl2::log::info) << "thread_aterm_pool: " << m_variables->size() << " variables in root set (" << m_variable_insertions << " total insertions)"
209 : << " and " << m_containers->size() << " containers in root set (" << m_container_insertions << " total insertions).\n";
210 : }
211 1931 : }
212 :
213 1931 : std::size_t thread_aterm_pool::protection_set_size() const
214 : {
215 1931 : std::size_t result = m_variables->size();
216 :
217 249099 : for (const auto& container : *m_containers)
218 : {
219 247168 : if (container != nullptr)
220 : {
221 994 : result += container->size();
222 : }
223 : }
224 :
225 1931 : return result;
226 : }
227 :
228 : } // namespace detail
229 : } // namespace atermpp
230 :
231 : #endif // ATERMPP_DETAIL_ATERM_POOL_IMPLEMENTATION_H
|
