thread_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_THREAD_ATERM_POOL_H
#define ATERMPP_DETAIL_THREAD_ATERM_POOL_H
 
#include "mcrl2/atermpp/detail/aterm_pool.h"
#include "mcrl2/atermpp/detail/aterm_container.h"
#include "mcrl2/utilities/hashtable.h"
#include "mcrl2/utilities/shared_mutex.h"
 
#include <atomic>
 
namespace atermpp
{
namespace detail
{
 
class thread_aterm_pool final : public mcrl2::utilities::noncopyable
{
public:
  thread_aterm_pool(aterm_pool& global_pool)
    : m_pool(global_pool),
      m_shared_mutex(global_pool.shared_mutex()),
      m_variables(new mcrl2::utilities::hashtable<aterm_core*>()),
      m_containers(new mcrl2::utilities::hashtable<detail::aterm_container*>()),
      m_thread_interface(global_pool, std::bind(&thread_aterm_pool::mark, this), std::bind(&thread_aterm_pool::print_local_performance_statistics, this), std::bind(&thread_aterm_pool::protection_set_size, this))
  {
    static bool is_main_thread = true;
    if (is_main_thread)
    {
      m_is_main_thread = true;
      is_main_thread = false;
    }
  }
 
  ~thread_aterm_pool() 
  {
      // We leak values for the global aterm pool since they contain global variables (for which initialisation order is undefined).
    if (!m_is_main_thread)
    {
      // We need to prematurely unregister this thread pool since we are going to delete reference variables.
      m_thread_interface.unregister();
      delete m_variables;
      delete m_containers;
    }
  }
 
  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 create_int(aterm& term, std::size_t val);
 
  inline void create_term(aterm& term, const function_symbol& sym);
 
  template<class ...Terms>
  inline void create_appl(aterm& term, const function_symbol& sym, const Terms&... arguments);
 
  template<class Term, class INDEX_TYPE, class ...Terms>
  inline void create_appl_index(aterm& term, const function_symbol& sym, const Terms&... arguments);
 
  template<typename ForwardIterator>
  inline void create_appl_dynamic(aterm& term,
      const function_symbol& sym,
      ForwardIterator begin,
      ForwardIterator end);
 
  template<typename InputIterator, typename ATermConverter>
  inline void create_appl_dynamic(aterm& term,
      const function_symbol& sym,
      ATermConverter convert_to_aterm,
      InputIterator begin,
      InputIterator end);
 
  inline void register_variable(aterm_core* variable);
 
  inline void deregister_variable(aterm_core* variable);
 
  inline void register_container(aterm_container* variable);
 
  inline void deregister_container(aterm_container* variable);
 
  // Implementation of thread_aterm_pool_interface
  inline void mark();
  inline void print_local_performance_statistics() const;
  inline std::size_t protection_set_size() const;
 
  inline mcrl2::utilities::shared_guard lock_shared() { return m_shared_mutex.lock_shared(); }
 
  inline mcrl2::utilities::lock_guard lock() { return m_shared_mutex.lock(); }
 
  inline bool is_shared_locked() { return m_shared_mutex.is_shared_locked(); }
 
  inline void collect() { m_pool.collect(m_shared_mutex); }
 
private:
  aterm_pool& m_pool;
 
  mcrl2::utilities::shared_mutex m_shared_mutex;  
  mcrl2::utilities::hashtable<aterm_core*>* m_variables;
  mcrl2::utilities::hashtable<detail::aterm_container*>* m_containers;
 
  std::size_t m_variable_insertions = 0;
  std::size_t m_container_insertions = 0;
  std::stack<std::reference_wrapper<_aterm>> m_todo; 
 
  bool m_is_main_thread = false;
 
  thread_aterm_pool_interface m_thread_interface; 
};
 
thread_aterm_pool& g_thread_term_pool();
 
} // namespace detail
} // namespace atermpp
 
#include "thread_aterm_pool_implementation.h"
 
#endif // ATERMPP_DETAIL_ATERM_POOL_H