aterm_pool.h

Go to the documentation of this file.

// Author(s): Maurice Laveaux.
// Copyright: see the accompanying file COPYING or copy at
// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
//
// Distributed under the Boost Software License, Version 1.0.
// (See accompanying file LICENSE_1_0.txt or copy at
// http://www.boost.org/LICENSE_1_0.txt)
//
 
#ifndef ATERMPP_DETAIL_ATERM_POOL_H
#define ATERMPP_DETAIL_ATERM_POOL_H
 
#include "mcrl2/atermpp/detail/aterm_pool_storage.h"
#include "mcrl2/atermpp/detail/function_symbol_pool.h"
 
#include "mcrl2/utilities/shared_mutex.h"
 
namespace atermpp
{
namespace detail
{
 
using integer_term_storage = aterm_pool_storage<_aterm_int, aterm_int_hasher, aterm_int_equals, 0>;
using term_storage = aterm_pool_storage<_aterm, aterm_hasher_finite<0>, aterm_equals_finite<0>, 0>;
using arbitrary_function_application_storage = aterm_pool_storage<_aterm_appl<1>,
  aterm_hasher<DynamicNumberOfArguments>,
  aterm_equals<DynamicNumberOfArguments>,
  DynamicNumberOfArguments>;
 
template<std::size_t N>
using function_application_storage = aterm_pool_storage<_aterm_appl<N>, aterm_hasher_finite<N>, aterm_equals_finite<N>, N>;
 
// There are some annoying circular dependencies between a aterm_pool and the contained thread_aterm_pool_interfaces
class aterm_pool;
 
class thread_aterm_pool_interface final
{
public:
  thread_aterm_pool_interface(aterm_pool& pool, std::function<void()> mark_function, std::function<void()> print_function, std::function<std::size_t()> protection_set_size_function);
  ~thread_aterm_pool_interface();
 
  void mark()
  {
    m_mark_function();
  }
 
  void print_local_performance_statistics() const
  {
    m_print_function();
  }
 
  std::size_t protection_set_size() const 
  {
    return m_protection_set_size_function();
  }
 
  // Prematurely unregister the thread_aterm_pool_interface.
  void unregister();
 
private:
  aterm_pool& m_pool;
  std::function<void()> m_mark_function;
  std::function<void()> m_print_function;
  std::function<std::size_t()> m_protection_set_size_function;
  bool m_registered = true;
};
 
class thread_aterm_pool;
 
class aterm_pool : public mcrl2::utilities::noncopyable
{
public:
  inline aterm_pool();
  inline ~aterm_pool();
 
  friend class thread_aterm_pool;
 
  inline function_symbol create_function_symbol(const std::string& name, const std::size_t arity, const bool check_for_registered_functions = false);
 
  inline function_symbol create_function_symbol(std::string&& name, const std::size_t arity, const bool check_for_registered_functions = false);
 
  inline void register_thread_aterm_pool(thread_aterm_pool_interface& pool);
 
  inline void remove_thread_aterm_pool(thread_aterm_pool_interface& pool);
 
  inline std::size_t capacity() const noexcept;
 
  inline std::size_t size() const;
 
  inline void print_performance_statistics() const;
 
  aterm& empty_list() noexcept { return reinterpret_cast<aterm&>(m_empty_list); }  // TODO remove this reinterpret cast by letting m_empty_list become an aterm.
 
  const function_symbol& as_int() noexcept { return m_function_symbol_pool.as_int(); }
 
  const function_symbol& as_list() noexcept { return m_function_symbol_pool.as_list(); }
 
  const function_symbol& as_empty_list() noexcept { return m_function_symbol_pool.as_empty_list(); }
 
  inline void add_deletion_hook(function_symbol sym, term_callback callback);
 
  inline void enable_garbage_collection(bool enable) { m_enable_garbage_collection = enable; };
 
  inline function_symbol_pool& get_symbol_pool() { return m_function_symbol_pool; }
 
  // These functions of the aterm pool should be called through a thread_aterm_pool.
private:
  inline void collect(mcrl2::utilities::shared_mutex& mutex);
 
  inline void created_term(bool allow_collect, mcrl2::utilities::shared_mutex& mutex);
 
  inline void collect_impl(mcrl2::utilities::shared_mutex& mutex);
 
  inline bool create_int(aterm& term, std::size_t val);
 
  inline bool create_term(aterm& term, const function_symbol& sym);
 
  template<class ...Terms>
  inline bool create_appl(aterm& term, const function_symbol& sym, const Terms&... arguments);
 
  template<typename ForwardIterator>
  bool create_appl_dynamic(aterm& term,
      const function_symbol& sym,
      ForwardIterator begin,
      ForwardIterator end);
 
  template<typename InputIterator, typename ATermConverter>
  bool create_appl_dynamic(aterm& term,
      const function_symbol& sym,
      ATermConverter convert_to_aterm,
      InputIterator begin,
      InputIterator end);
 
  inline void resize_if_needed(mcrl2::utilities::shared_mutex& shared);
 
  mcrl2::utilities::shared_mutex& shared_mutex() { return m_shared_mutex; }
 
  inline std::size_t protection_set_size() const;
 
  std::vector<thread_aterm_pool_interface* > m_thread_pools;
 
  function_symbol_pool m_function_symbol_pool;
 
  integer_term_storage m_int_storage;
 
  std::tuple<
    term_storage,
    function_application_storage<1>,
    function_application_storage<2>,
    function_application_storage<3>,
    function_application_storage<4>,
    function_application_storage<5>,
    function_application_storage<6>,
    function_application_storage<7>
  > m_appl_storage;
 
  arbitrary_function_application_storage m_appl_dynamic_storage;
 
  std::atomic<long> m_count_until_collection = 0;
  std::atomic<long> m_count_until_resize = 0;
 
  std::atomic<bool> m_enable_garbage_collection = EnableGarbageCollection; 
 
  mcrl2::utilities::shared_mutex m_shared_mutex;
 
  aterm_core m_empty_list;
};
 
inline
thread_aterm_pool_interface::thread_aterm_pool_interface(aterm_pool& pool, std::function<void()> mark_function, std::function<void()> print_function, std::function<std::size_t()> protection_set_size_function)
  : m_pool(pool), m_mark_function(mark_function), m_print_function(print_function), m_protection_set_size_function(protection_set_size_function)
{
  m_pool.register_thread_aterm_pool(*this);
}
 
inline
void thread_aterm_pool_interface::unregister()
{
  if (m_registered)
  {
    m_pool.remove_thread_aterm_pool(*this);
    m_registered = false;
  }
}
 
inline
thread_aterm_pool_interface::~thread_aterm_pool_interface()
{
  unregister();
}
 
} // namespace detail
} // namespace atermpp
 
#include "aterm_pool_implementation.h"
#include "aterm_pool_storage_implementation.h"
 
#endif // ATERMPP_DETAIL_ATERM_POOL_H