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_ATERM_POOL_H
      11             : #define ATERMPP_DETAIL_ATERM_POOL_H
      12             : 
      13             : #include "mcrl2/atermpp/detail/aterm_pool_storage.h"
      14             : #include "mcrl2/atermpp/detail/function_symbol_pool.h"
      15             : 
      16             : #include "mcrl2/utilities/shared_mutex.h"
      17             : 
      18             : namespace atermpp
      19             : {
      20             : namespace detail
      21             : {
      22             : 
      23             : /// Define several specializations of the term pool storage objects.
      24             : using integer_term_storage = aterm_pool_storage<_aterm_int, aterm_int_hasher, aterm_int_equals, 0>;
      25             : using term_storage = aterm_pool_storage<_aterm, aterm_hasher_finite<0>, aterm_equals_finite<0>, 0>;
      26             : using arbitrary_function_application_storage = aterm_pool_storage<_aterm_appl<1>,
      27             :   aterm_hasher<DynamicNumberOfArguments>,
      28             :   aterm_equals<DynamicNumberOfArguments>,
      29             :   DynamicNumberOfArguments>;
      30             : 
      31             : template<std::size_t N>
      32             : using function_application_storage = aterm_pool_storage<_aterm_appl<N>, aterm_hasher_finite<N>, aterm_equals_finite<N>, N>;
      33             : 
      34             : // There are some annoying circular dependencies between a aterm_pool and the contained thread_aterm_pool_interfaces
      35             : class aterm_pool;
      36             : 
      37             : /// \brief A thread specific aterm pool that provides a local interface to the global term pool.
      38             : ///        Ensures that terms created by this thread are protected during garbage collection.
      39             : class thread_aterm_pool_interface final
      40             : {
      41             : public:
      42             :   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);
      43             :   ~thread_aterm_pool_interface();
      44             : 
      45             :   /// \brief Mark the terms created by this thread to prevent them being garbage collected.
      46        1917 :   void mark()
      47             :   {
      48        1917 :     m_mark_function();
      49        1917 :   }
      50             : 
      51             :   /// \brief Print performance statistics for data stored for this thread.
      52        1917 :   void print_local_performance_statistics() const
      53             :   {
      54        1917 :     m_print_function();
      55        1917 :   }
      56             : 
      57             :   /// \returns The total number of terms residing in the pool.
      58        1917 :   std::size_t protection_set_size() const 
      59             :   {
      60        1917 :     return m_protection_set_size_function();
      61             :   }
      62             : 
      63             : private:
      64             :   aterm_pool& m_pool;
      65             :   std::function<void()> m_mark_function;
      66             :   std::function<void()> m_print_function;
      67             :   std::function<std::size_t()> m_protection_set_size_function;
      68             : };
      69             : 
      70             : class thread_aterm_pool;
      71             : 
      72             : /// \brief The interface for the term library. Provides the storage of
      73             : ///        of all classes of terms.
      74             : /// \details Internally uses different storage objects to store specific
      75             : ///          classes of terms. For a given term creation it can decide what
      76             : ///          storage to use at run-time using its function symbol.
      77             : class aterm_pool : public mcrl2::utilities::noncopyable
      78             : {
      79             : public:
      80             :   inline aterm_pool();
      81             :   inline ~aterm_pool();
      82             : 
      83             :   friend class thread_aterm_pool;
      84             : 
      85             :   /// \brief Creates a function symbol pair (name, arity).
      86             :   /// \see function_symbol_pool.
      87             :   inline function_symbol create_function_symbol(const std::string& name, const std::size_t arity, const bool check_for_registered_functions = false);
      88             : 
      89             :   /// \brief Creates a function symbol pair (name, arity).
      90             :   /// \see function_symbol_pool.
      91             :   inline function_symbol create_function_symbol(std::string&& name, const std::size_t arity, const bool check_for_registered_functions = false);
      92             : 
      93             :   /// \brief Register a thread specific aterm pool.
      94             :   /// \details threadsafe
      95             :   inline void register_thread_aterm_pool(thread_aterm_pool_interface& pool);
      96             : 
      97             :   /// \brief Remove thread specific aterm pool.
      98             :   /// \details threadsafe
      99             :   inline void remove_thread_aterm_pool(thread_aterm_pool_interface& pool);
     100             : 
     101             :   /// \brief The number of terms that can be stored without resizing.
     102             :   inline std::size_t capacity() const noexcept;
     103             : 
     104             :   /// \returns The total number of terms residing in the pool.
     105             :   inline std::size_t size() const;
     106             : 
     107             :   /// \brief Prints various performance statistics for the term pool.
     108             :   inline void print_performance_statistics() const;
     109             : 
     110             :   /// \returns A global term that indicates the empty list.
     111  2382669211 :   aterm& empty_list() noexcept { return m_empty_list; }
     112             : 
     113             :   /// \returns The function symbol used by integral terms.
     114         143 :   const function_symbol& as_int() noexcept { return m_function_symbol_pool.as_int(); }
     115             : 
     116             :   /// \returns The function symbol used by the list constructor.
     117  6927179666 :   const function_symbol& as_list() noexcept { return m_function_symbol_pool.as_list(); }
     118             : 
     119             :   /// \returns The function symbol used by the term indicating the empty list.
     120  2379951465 :   const function_symbol& as_empty_list() noexcept { return m_function_symbol_pool.as_empty_list(); }
     121             : 
     122             :   /// \brief Add a callback that is triggered whenever a term with the given function symbol is destroyed.
     123             :   inline void add_deletion_hook(function_symbol sym, term_callback callback);
     124             : 
     125             :   /// \brief Enable garbage collection when passing true and disable otherwise.
     126             :   inline void enable_garbage_collection(bool enable) { m_enable_garbage_collection = enable; };
     127             : 
     128        5223 :   inline function_symbol_pool& get_symbol_pool() { return m_function_symbol_pool; }
     129             : 
     130             :   // These functions of the aterm pool should be called through a thread_aterm_pool.
     131             : private:
     132             :   /// \brief Force garbage collection on all storages.
     133             :   /// \details threadsafe
     134             :   inline void collect(mcrl2::utilities::shared_mutex& mutex);
     135             : 
     136             :   /// \brief Triggers garbage collection and resizing when conditions are met.
     137             :   /// \param allow_collect Actually perform the garbage collection instead of only updating the counters.
     138             :   /// \param mutex The shared mutex that should be used for locking if necessary.
     139             :   /// \details threadsafe
     140             :   inline void created_term(bool allow_collect, mcrl2::utilities::shared_mutex& mutex);
     141             : 
     142             :   /// \brief Collect garbage on all storages.
     143             :   /// \details threadsafe
     144             :   inline void collect_impl(mcrl2::utilities::shared_mutex& mutex);
     145             : 
     146             :   /// \brief Creates a integral term with the given value.
     147             :   inline bool create_int(aterm& term, std::size_t val);
     148             : 
     149             :   /// \brief Creates a term with the given function symbol.
     150             :   inline bool create_term(aterm& term, const function_symbol& sym);
     151             : 
     152             :   /// \brief Creates a function application with the given function symbol and arguments.
     153             :   template<class ...Terms>
     154             :   inline bool create_appl(aterm& term, const function_symbol& sym, const Terms&... arguments);
     155             : 
     156             :   /// \brief Creates a function application with the given function symbol and the arguments
     157             :   ///       as provided by the given iterator. This function assumes that the arity of the
     158             :   ///       function symbol is equal to the number of elements in the iterator.
     159             :   template<typename ForwardIterator>
     160             :   bool create_appl_dynamic(aterm& term,
     161             :       const function_symbol& sym,
     162             :       ForwardIterator begin,
     163             :       ForwardIterator end);
     164             : 
     165             :   /// \brief Creates a function application with the given function symbol and the arguments
     166             :   ///       as provided by the given iterator. This function assumes that the arity of the
     167             :   ///       function symbol is equal to the number of elements in the iterator.
     168             :   template<typename InputIterator, typename ATermConverter>
     169             :   bool create_appl_dynamic(aterm& term,
     170             :       const function_symbol& sym,
     171             :       ATermConverter convert_to_aterm,
     172             :       InputIterator begin,
     173             :       InputIterator end);
     174             : 
     175             :   /// \brief Resizes all storages if necessary.
     176             :   /// \details threadsafe
     177             :   inline void resize_if_needed(mcrl2::utilities::shared_mutex& shared);
     178             : 
     179         144 :   mcrl2::utilities::shared_mutex& shared_mutex() { return m_shared_mutex; }
     180             : 
     181             :   /// \returns The total number of term variables residing in the protection sets.
     182             :   inline std::size_t protection_set_size() const;
     183             : 
     184             :   /// \brief The set of local aterm pools.
     185             :   std::vector<thread_aterm_pool_interface* > m_thread_pools;
     186             : 
     187             :   /// \brief Storage for the function symbols.
     188             :   function_symbol_pool m_function_symbol_pool;
     189             : 
     190             :   /// \brief Storage for integral terms.
     191             :   integer_term_storage m_int_storage;
     192             : 
     193             :   /// Storage for function applications with a fixed number of arguments.
     194             :   std::tuple<
     195             :     term_storage,
     196             :     function_application_storage<1>,
     197             :     function_application_storage<2>,
     198             :     function_application_storage<3>,
     199             :     function_application_storage<4>,
     200             :     function_application_storage<5>,
     201             :     function_application_storage<6>,
     202             :     function_application_storage<7>
     203             :   > m_appl_storage;
     204             : 
     205             :   /// Storage for term_appl with a dynamic number of arguments larger than 7.
     206             :   arbitrary_function_application_storage m_appl_dynamic_storage;
     207             : 
     208             :   /// Track the number of terms destroyed and reduce the freelist.
     209             :   std::atomic<long> m_count_until_collection = 0;
     210             :   std::atomic<long> m_count_until_resize = 0;
     211             : 
     212             :   std::atomic<bool> m_enable_garbage_collection = EnableGarbageCollection; /// Garbage collection is enabled.
     213             : 
     214             :   /// All the shared mutexes.
     215             :   mcrl2::utilities::shared_mutex m_shared_mutex;
     216             : 
     217             :   /// Represents an empty list.
     218             :   aterm m_empty_list;
     219             : };
     220             : 
     221             : inline
     222         144 : 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)
     223         144 :   : m_pool(pool), m_mark_function(mark_function), m_print_function(print_function), m_protection_set_size_function(protection_set_size_function)
     224             : {
     225         144 :   m_pool.register_thread_aterm_pool(*this);
     226         144 : }
     227             : 
     228             : inline
     229         144 : thread_aterm_pool_interface::~thread_aterm_pool_interface()
     230             : {
     231         144 :   m_pool.remove_thread_aterm_pool(*this);
     232         144 : }
     233             : 
     234             : } // namespace detail
     235             : } // namespace atermpp
     236             : 
     237             : #include "aterm_pool_implementation.h"
     238             : #include "aterm_pool_storage_implementation.h"
     239             : 
     240             : #endif // ATERMPP_DETAIL_ATERM_POOL_H