mCRL2
Loading...
Searching...
No Matches
thread_aterm_pool_implementation.h
Go to the documentation of this file.
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"
18
19
20namespace atermpp
21{
22namespace detail
23{
24
25function_symbol thread_aterm_pool::create_function_symbol(std::string&& name, const std::size_t arity, const bool check_for_registered_functions)
26{
28 function_symbol symbol = m_pool.create_function_symbol(std::move(name), arity, check_for_registered_functions);
29 return symbol;
30}
31
32function_symbol thread_aterm_pool::create_function_symbol(const std::string& name, const std::size_t arity, const bool check_for_registered_functions)
33{
34 std::string name_copy = name;
35 return create_function_symbol(std::move(name_copy), arity, check_for_registered_functions);
36}
37
38void thread_aterm_pool::create_int(aterm& term, size_t val)
39{
41 bool added = m_pool.create_int(term, val);
42 guard.unlock_shared();
43
45}
46
48{
50 bool added = m_pool.create_term(term, sym);
51 guard.unlock_shared();
52
54}
55
56template<class ...Terms>
57void thread_aterm_pool::create_appl(aterm& term, const function_symbol& sym, const Terms&... arguments)
58{
60 bool added = m_pool.create_appl(term, sym, arguments...);
61 guard.unlock_shared();
62
64}
65
66template<class Term, class INDEX_TYPE, class ...Terms>
67void thread_aterm_pool::create_appl_index(aterm& term, const function_symbol& sym, const Terms&... arguments)
68{
70 std::array<unprotected_aterm, sizeof...(arguments)> argument_array;
71 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,
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 m_pool.create_int(term,
94 insert(*reinterpret_cast<INDEX_TYPE*>(&argument_array[0])));
95 added = m_pool.create_appl(term, sym, argument_array[0], argument_array[1], term);
96 }
97 guard.unlock_shared();
98
100}
101
102template<typename InputIterator>
104 const function_symbol& sym,
105 InputIterator begin,
106 InputIterator end)
107{
109 bool added = m_pool.create_appl_dynamic(term, sym, begin, end);
110 guard.unlock_shared();
111
113}
114
115template<typename InputIterator, typename ATermConverter>
117 const function_symbol& sym,
118 ATermConverter convert_to_aterm,
119 InputIterator begin,
120 InputIterator end)
121{
123 bool added = m_pool.create_appl_dynamic(term, sym, convert_to_aterm, begin, end);
124 guard.unlock_shared();
125
127}
128
130{
132
134
135 // Resizing of the protection set should not interfere with garbage collection and rehashing
136 if (m_variables->must_resize())
137 {
138 m_variables->resize();
139 }
140
141 auto [it, inserted] = m_variables->insert(variable);
142
143 // The variable must be inserted.
144 assert(inserted);
147}
148
150{
152 m_variables->erase(variable);
153}
154
156{
158
160 if (m_containers->must_resize())
161 {
162 m_containers->resize();
163 }
164 auto [it, inserted] = m_containers->insert(container);
165
166 // The container must be inserted.
167 assert(inserted);
170}
171
173{
175 m_containers->erase(container);
176}
177
179{
180 for (const aterm* variable : *m_variables)
181 {
182 if (variable != nullptr)
183 {
184 // Mark all terms (and their subterms) that are reachable, i.e the root set.
185 _aterm* term = detail::address(*variable);
186 if (term != nullptr && !term->is_marked())
187 {
188 // This variable is not a default term and that term has not been marked.
189 mark_term(*term, m_todo);
190 }
191 }
192 }
193
194 for (const aterm_container* container : *m_containers)
195 {
196 if (container != nullptr)
197 {
198 // The container marks the contained terms itself.
199 container->mark(m_todo);
200 }
201 }
202}
203
205{
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}
212
214{
215 std::size_t result = m_variables->size();
216
217 for (const auto& container : *m_containers)
218 {
219 if (container != nullptr)
220 {
221 result += container->size();
222 }
223 }
224
225 return result;
226}
227
228} // namespace detail
229} // namespace atermpp
230
231#endif // ATERMPP_DETAIL_ATERM_POOL_IMPLEMENTATION_H
The aterm base class that provides protection of the underlying shared terms.
Definition aterm.h:186
This is the class to which an aterm points.
Definition aterm.h:48
bool is_marked() const
Check if the term is already marked.
Definition aterm.h:73
Provides safe storage of unprotected_aterm instances in a container by marking them during garbage co...
void created_term(bool allow_collect, mcrl2::utilities::shared_mutex &mutex)
Triggers garbage collection and resizing when conditions are met.
bool create_appl(aterm &term, const function_symbol &sym, const Terms &... arguments)
Creates a function application with the given function symbol and arguments.
bool create_int(aterm &term, std::size_t val)
Creates a integral term with the given value.
function_symbol create_function_symbol(const std::string &name, const std::size_t arity, const bool check_for_registered_functions=false)
Creates a function symbol pair (name, arity).
bool create_term(aterm &term, const function_symbol &sym)
Creates a term with the given function symbol.
bool create_appl_dynamic(aterm &term, const function_symbol &sym, ForwardIterator begin, ForwardIterator end)
Creates a function application with the given function symbol and the arguments as provided by the gi...
mcrl2::utilities::hashtable< aterm * > * m_variables
void deregister_container(aterm_container *variable)
Removes the given container from the active variables.
void register_container(aterm_container *variable)
Consider the given container when marking underlying terms.
mcrl2::utilities::shared_mutex m_shared_mutex
Keeps track of pointers to all existing aterm variables and containers.
void create_int(aterm &term, std::size_t val)
void create_appl(aterm &term, const function_symbol &sym, const Terms &... arguments)
function_symbol create_function_symbol(const std::string &name, const std::size_t arity, const bool check_for_registered_functions=false)
void register_variable(aterm *variable)
Consider the given variable when marking underlying terms.
void create_term(aterm &term, const function_symbol &sym)
mcrl2::utilities::hashtable< detail::aterm_container * > * m_containers
std::stack< std::reference_wrapper< _aterm > > m_todo
A reusable todo stack.
void create_appl_dynamic(aterm &term, const function_symbol &sym, ForwardIterator begin, ForwardIterator end)
void deregister_variable(aterm *variable)
Removes the given variable from the active variables.
void create_appl_index(aterm &term, const function_symbol &sym, const Terms &... arguments)
An unprotected term does not change the reference count of the shared term when it is copied or moved...
Definition aterm.h:36
A shared lock guard for the shared_mutex.
void unlock_shared()
Unlocks the acquired shared guard explicitly. Otherwise, performed in destructor.
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
Definition logger.h:395
void store_in_argument_array(std::array< unprotected_aterm, N > &argument_array, const Args &... args)
_aterm * address(const unprotected_aterm &t)
Definition aterm.h:347
static constexpr bool EnableVariableRegistrationMetrics
Keep track of the number of variables registered.
void mark_term(const _aterm &root, std::stack< std::reference_wrapper< _aterm > > &todo)
Marks a term and recursively all arguments that are not reachable.
The main namespace for the aterm++ library.
Definition algorithm.h:21
void mcrl2_unused(T &&...)
Function that can be used to silence unused parameter warnings.
Definition unused.h:20
For several variable types in mCRL2 an implicit mapping of these variables to integers is available....