mCRL2
Loading...
Searching...
No Matches
thread_aterm_pool.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_H
11#define ATERMPP_DETAIL_THREAD_ATERM_POOL_H
12
17
18#include <atomic>
19
20namespace atermpp
21{
22namespace detail
23{
24
28{
29public:
31 : m_pool(global_pool),
32 m_shared_mutex(global_pool.shared_mutex()),
33 m_variables(new mcrl2::utilities::hashtable<aterm*>()),
34 m_containers(new mcrl2::utilities::hashtable<detail::aterm_container*>()),
36 {
38 static bool is_main_thread = true;
39 if (is_main_thread)
40 {
41 m_is_main_thread = true;
42 is_main_thread = false;
43 }
44 }
45
47 {
48 // We leak values for the global aterm pool since they contain global variables (for which initialisation order is undefined).
50 {
51 // We need to prematurely unregister this thread pool since we are going to delete reference variables.
53 delete m_variables;
54 delete m_containers;
55 }
56 }
57
59 inline function_symbol create_function_symbol(const std::string& name, const std::size_t arity, const bool check_for_registered_functions = false);
60
62 inline function_symbol create_function_symbol(std::string&& name, const std::size_t arity, const bool check_for_registered_functions = false);
63
65 inline void create_int(aterm& term, std::size_t val);
66
68 inline void create_term(aterm& term, const function_symbol& sym);
69
71 template<class ...Terms>
72 inline void create_appl(aterm& term, const function_symbol& sym, const Terms&... arguments);
73
75 template<class Term, class INDEX_TYPE, class ...Terms>
76 inline void create_appl_index(aterm& term, const function_symbol& sym, const Terms&... arguments);
77
79 template<typename ForwardIterator>
80 inline void create_appl_dynamic(aterm& term,
81 const function_symbol& sym,
82 ForwardIterator begin,
83 ForwardIterator end);
84
86 template<typename InputIterator, typename ATermConverter>
87 inline void create_appl_dynamic(aterm& term,
88 const function_symbol& sym,
89 ATermConverter convert_to_aterm,
90 InputIterator begin,
91 InputIterator end);
92
94 inline void register_variable(aterm* variable);
95
97 inline void deregister_variable(aterm* variable);
98
100 inline void register_container(aterm_container* variable);
101
103 inline void deregister_container(aterm_container* variable);
104
105 // Implementation of thread_aterm_pool_interface
106 inline void mark();
107 inline void print_local_performance_statistics() const;
108 inline std::size_t protection_set_size() const;
109
112
115
118
121
122private:
124
129
130 std::size_t m_variable_insertions = 0;
131 std::size_t m_container_insertions = 0;
132 std::stack<std::reference_wrapper<_aterm>> m_todo;
133
134 bool m_is_main_thread = false;
135
138};
139
142
143} // namespace detail
144} // namespace atermpp
145
147
148#endif // ATERMPP_DETAIL_ATERM_POOL_H
The aterm base class that provides protection of the underlying shared terms.
Definition aterm.h:186
Provides safe storage of unprotected_aterm instances in a container by marking them during garbage co...
The interface for the term library. Provides the storage of of all classes of terms.
Definition aterm_pool.h:82
void collect(mcrl2::utilities::shared_mutex &mutex)
Force garbage collection on all storages.
A thread specific aterm pool that provides a local interface to the global term pool....
Definition aterm_pool.h:40
This is a thread's specific access to the global aterm pool which ensures that garbage collection and...
void collect()
Triggers a global garbage collection.
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)
thread_aterm_pool_interface m_thread_interface
The registered thread aterm pool.
void create_appl(aterm &term, const function_symbol &sym, const Terms &... arguments)
thread_aterm_pool(aterm_pool &global_pool)
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)
bool is_shared_locked()
Returns true iff we are in a shared section.
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.
mcrl2::utilities::lock_guard lock()
Acquire an exclusive lock.
void create_appl_index(aterm &term, const function_symbol &sym, const Terms &... arguments)
mcrl2::utilities::shared_guard lock_shared()
Acquire a shared lock on this thread aterm pool.
A set that assigns each element an unique index.
Definition hashtable.h:27
An exclusive lock guard for the shared_mutex.
Inherit from this class to prevent it from being copyable.
Definition noncopyable.h:21
A shared lock guard for the shared_mutex.
thread_aterm_pool & g_thread_term_pool()
A reference to the thread local term pool storage.
The main namespace for the aterm++ library.
Definition algorithm.h:21
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
STL namespace.