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_H
      11             : #define ATERMPP_DETAIL_THREAD_ATERM_POOL_H
      12             : 
      13             : #include "mcrl2/atermpp/detail/aterm_pool.h"
      14             : #include "mcrl2/atermpp/detail/aterm_container.h"
      15             : #include "mcrl2/utilities/hashtable.h"
      16             : #include "mcrl2/utilities/shared_mutex.h"
      17             : 
      18             : #include <atomic>
      19             : 
      20             : namespace atermpp
      21             : {
      22             : namespace detail
      23             : {
      24             : 
      25             : /// \brief This is a thread's specific access to the global aterm pool which ensures that
      26             : ///        garbage collection and hash table resizing can proceed.
      27             : class thread_aterm_pool final : public mcrl2::utilities::noncopyable
      28             : {
      29             : public:
      30         144 :   thread_aterm_pool(aterm_pool& global_pool)
      31         144 :     : m_pool(global_pool),
      32         144 :       m_shared_mutex(global_pool.shared_mutex()),
      33         144 :       m_variables(new mcrl2::utilities::hashtable<aterm*>()),
      34         144 :       m_containers(new mcrl2::utilities::hashtable<detail::aterm_container*>()),
      35         144 :       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))
      36             :   {
      37             :     /// Identify the first constructor call as the main thread.
      38             :     static bool is_main_thread = true;
      39         144 :     if (is_main_thread)
      40             :     {
      41         143 :       m_is_main_thread = true;
      42         143 :       is_main_thread = false;
      43             :     }
      44         144 :   }
      45             : 
      46         144 :   ~thread_aterm_pool() 
      47             :   {
      48             :       // We leak values for the global aterm pool since they contain global variables (for which initialisation order is undefined).
      49         144 :     if (!m_is_main_thread)
      50             :     {
      51             :       // We need to prematurely unregister this thread pool since we are going to delete reference variables.
      52           1 :       m_thread_interface.unregister();
      53           1 :       delete m_variables;
      54           1 :       delete m_containers;
      55             :     }
      56         144 :   }
      57             : 
      58             :   /// \details threadsafe
      59             :   inline function_symbol create_function_symbol(const std::string& name, const std::size_t arity, const bool check_for_registered_functions = false);
      60             : 
      61             :   /// \details threadsafe
      62             :   inline function_symbol create_function_symbol(std::string&& name, const std::size_t arity, const bool check_for_registered_functions = false);
      63             : 
      64             :   /// \details threadsafe
      65             :   inline void create_int(aterm& term, std::size_t val);
      66             : 
      67             :   /// \details threadsafe
      68             :   inline void create_term(aterm& term, const function_symbol& sym);
      69             : 
      70             :   /// \details threadsafe
      71             :   template<class ...Terms>
      72             :   inline void create_appl(aterm& term, const function_symbol& sym, const Terms&... arguments);
      73             : 
      74             :   /// \details threadsafe
      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             : 
      78             :   /// \details threadsafe
      79             :   template<typename ForwardIterator>
      80             :   inline void create_appl_dynamic(aterm& term,
      81             :       const function_symbol& sym,
      82             :       ForwardIterator begin,
      83             :       ForwardIterator end);
      84             : 
      85             :   /// \threadsafe
      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             : 
      93             :   /// \brief Consider the given variable when marking underlying terms.
      94             :   inline void register_variable(aterm* variable);
      95             : 
      96             :   /// \brief Removes the given variable from the active variables.
      97             :   inline void deregister_variable(aterm* variable);
      98             : 
      99             :   /// \brief Consider the given container when marking underlying terms.
     100             :   inline void register_container(aterm_container* variable);
     101             : 
     102             :   /// \brief Removes the given container from the active variables.
     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             : 
     110             :   /// Acquire a shared lock on this thread aterm pool.
     111   190108996 :   inline mcrl2::utilities::shared_guard lock_shared() { return m_shared_mutex.lock_shared(); }
     112             : 
     113             :   /// Acquire an exclusive lock
     114        4030 :   inline mcrl2::utilities::lock_guard lock() { return m_shared_mutex.lock(); }
     115             : 
     116             :   /// Returns true iff we are in a shared section.
     117           0 :   inline bool is_shared_locked() { return m_shared_mutex.is_shared_locked(); }
     118             : 
     119             :   /// Triggers a global garbage collection
     120        1002 :   inline void collect() { m_pool.collect(m_shared_mutex); }
     121             : 
     122             : private:
     123             :   aterm_pool& m_pool;
     124             : 
     125             :   /// Keeps track of pointers to all existing aterm variables and containers.
     126             :   mcrl2::utilities::shared_mutex m_shared_mutex;
     127             :   mcrl2::utilities::hashtable<aterm*>* m_variables;
     128             :   mcrl2::utilities::hashtable<detail::aterm_container*>* m_containers;
     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; ///< A reusable todo stack.
     133             : 
     134             :   bool m_is_main_thread = false;
     135             : 
     136             :   /// The registered thread aterm pool.
     137             :   thread_aterm_pool_interface m_thread_interface; 
     138             : };
     139             : 
     140             : /// \brief A reference to the thread local term pool storage
     141             : thread_aterm_pool& g_thread_term_pool();
     142             : 
     143             : } // namespace detail
     144             : } // namespace atermpp
     145             : 
     146             : #include "thread_aterm_pool_implementation.h"
     147             : 
     148             : #endif // ATERMPP_DETAIL_ATERM_POOL_H