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             : #include "mcrl2/atermpp/detail/function_symbol_pool.h"
      11             : 
      12             : #include "mcrl2/utilities/unused.h"
      13             : 
      14             : using namespace atermpp;
      15             : using namespace atermpp::detail;
      16             : using namespace mcrl2::utilities;
      17             : using namespace mcrl2::utilities::detail;
      18             : 
      19         143 : function_symbol_pool::function_symbol_pool()
      20             : {
      21             :   // Initialize the default function symbols.
      22         143 :   m_as_int = create("<aterm_int>", 0);
      23         143 :   m_as_list = create("<list_constructor>", 2);
      24         143 :   m_as_empty_list = create("<empty_list>", 0);
      25             : 
      26             :   // Initialize the global copies of these default function symbols.
      27         143 :   g_as_int = m_as_int;
      28         143 :   g_as_list = m_as_list;
      29         143 :   g_as_empty_list = m_as_empty_list;
      30         143 : }
      31             : 
      32       53797 : void function_symbol_pool::create_helper(const std::string& name)
      33             : {
      34       53797 :   if constexpr (GlobalThreadSafe) { m_mutex.lock(); }
      35             : 
      36             :   // Check whether there is a registered prefix p such that name equal pn where n is a number.
      37             :   // In that case prevent that pn will be generated as a fresh function name.
      38       53797 :   std::size_t start_of_index = name.find_last_not_of("0123456789") + 1;
      39             : 
      40       53797 :   if (start_of_index < name.size()) // Otherwise there is no trailing number.
      41             :   {
      42        4832 :     std::string potential_number = name.substr(start_of_index); // Get the trailing string after prefix_ of function_name.
      43        4832 :     std::string prefix = name.substr(0, start_of_index);
      44        4832 :     auto prefix_it = m_prefix_to_register_function_map.find(prefix);
      45        4832 :     if (prefix_it != m_prefix_to_register_function_map.end())  // points to the prefix.
      46             :     {
      47             :       try
      48             :       {
      49           1 :         std::size_t number = std::stoul(potential_number);
      50           1 :         *prefix_it->second = std::max(*prefix_it->second, number + 1); // Set the index belonging to the found prefix to at least a safe number+1.
      51             :       }
      52           0 :       catch (std::exception&)
      53             :       {
      54             :         // Can be std::invalid_argument or an out_of_range exception.
      55             :         // In both cases nothing needs to be done, and the exception can be ignored.
      56           0 :       }
      57             :     }
      58        4832 :   }
      59             : 
      60       53797 :   if  constexpr (GlobalThreadSafe) { m_mutex.unlock(); }
      61       53797 : }
      62             : 
      63     1081475 : function_symbol function_symbol_pool::create(std::string&& name, const std::size_t arity, const bool check_for_registered_functions)
      64             : {
      65     1081475 :   auto it = m_symbol_set.find(name, arity);
      66     1081475 :   if (it != m_symbol_set.end())
      67             :   {
      68             :     if constexpr (EnableCreationMetrics) { m_function_symbol_metrics.hit(); }
      69             : 
      70             :     // The element already exists so return it.
      71     1023764 :     return function_symbol(_function_symbol::ref(&(*it)));
      72             :   }
      73             :   else
      74             :   {
      75             :     if constexpr (EnableCreationMetrics) { m_function_symbol_metrics.miss(); }
      76             : 
      77       57711 :     const _function_symbol& symbol = *m_symbol_set.emplace(std::forward<std::string>(name), arity).first;
      78       57711 :     if (check_for_registered_functions)
      79             :     {
      80       33795 :       create_helper(symbol.name());
      81             :     }
      82             : 
      83       57711 :     return function_symbol(_function_symbol::ref(&symbol));
      84             :   }
      85             : }
      86             : 
      87       20218 : function_symbol function_symbol_pool::create(const std::string& name, const std::size_t arity, const bool check_for_registered_functions)
      88             : {
      89       20218 :   auto it = m_symbol_set.find(name, arity);
      90       20218 :   if (it != m_symbol_set.end())
      91             :   {
      92             :     if constexpr (EnableCreationMetrics) { m_function_symbol_metrics.hit(); }
      93             : 
      94             :     // The element already exists so return it.
      95         216 :     return function_symbol(_function_symbol::ref(&(*it)));
      96             :   }
      97             :   else
      98             :   {
      99             :     if constexpr (EnableCreationMetrics) { m_function_symbol_metrics.miss(); }
     100             : 
     101       20002 :     const _function_symbol& symbol = *m_symbol_set.emplace(name, arity).first;
     102       20002 :     if (check_for_registered_functions)
     103             :     {
     104       20002 :       create_helper(name);
     105             :     }
     106             : 
     107       20002 :     return function_symbol(_function_symbol::ref(&symbol));
     108             :   }
     109             : }
     110             : 
     111        2680 : void function_symbol_pool::deregister(const std::string& prefix)
     112             : {
     113        2680 :   m_mutex.lock();
     114        2680 :   m_prefix_to_register_function_map.erase(prefix);
     115        2680 :   m_mutex.unlock();
     116        2680 : }
     117             : 
     118        2543 : std::shared_ptr<std::size_t> function_symbol_pool::register_prefix(const std::string& prefix)
     119             : {
     120        2543 :   m_mutex.lock();
     121             : 
     122        2543 :   auto it = m_prefix_to_register_function_map.find(prefix);
     123        2543 :   if (it != m_prefix_to_register_function_map.end())
     124             :   {
     125           0 :     auto result = it->second;
     126           0 :     m_mutex.unlock();
     127           0 :     return result;
     128           0 :   }
     129             :   else
     130             :   {
     131        2543 :     std::size_t index = get_sufficiently_large_postfix_index(prefix);
     132        2543 :     std::shared_ptr<std::size_t> shared_index = std::make_shared<std::size_t>(index);
     133        2543 :     m_prefix_to_register_function_map[prefix] = shared_index;
     134             : 
     135        2543 :     m_mutex.unlock();
     136        2543 :     return shared_index;
     137        2543 :   }
     138             : }
     139             : 
     140        2543 : std::size_t function_symbol_pool::get_sufficiently_large_postfix_index(const std::string& prefix) const
     141             : {
     142        2543 :   std::size_t index = 0;
     143     1402068 :   for (const auto& f : m_symbol_set)
     144             :   {
     145     1399525 :     const std::string& function_name = f.name();
     146             : 
     147     1399525 :     if (function_name.compare(0, prefix.size(), prefix) == 0)   // The function name starts with the prefix
     148             :     {
     149           0 :       std::string potential_number = function_name.substr(prefix.size()); // Get the trailing string after prefix_ of function_name.
     150             :       std::size_t end_of_number;
     151             :       try
     152             :       {
     153           0 :         std::size_t number = std::stoul(potential_number, &end_of_number);
     154           0 :         if (end_of_number == potential_number.size()) // A proper number was read.
     155             :         {
     156           0 :           if (number >= index)
     157             :           {
     158           0 :             index = number + 1;
     159             :           }
     160             :         }
     161             :       }
     162           0 :       catch (std::exception&)
     163             :       {
     164             :         // Can be std::invalid_argument or an out_of_range exception.
     165             :         // In both cases nothing needs to be done, and the exception can be ignored.
     166           0 :       }
     167           0 :     }
     168             :   }
     169             : 
     170        2543 :   return index;
     171             : }
     172             : 
     173        1015 : void function_symbol_pool::sweep()
     174             : {
     175             :   // Prevents changes to the symbol_set
     176        1015 :   std::unique_lock lock(m_mutex);
     177             : 
     178        1015 :   auto timestamp = std::chrono::system_clock::now();
     179        1015 :   std::size_t old_size = size();
     180             : 
     181             :   // Clean up function symbols with a zero reference count.
     182       30624 :   for (auto it = m_symbol_set.begin(); it != m_symbol_set.end(); )
     183             :   {
     184       29609 :     if (it->reference_count() == 0)
     185             :     {
     186       20975 :       it = m_symbol_set.erase(it);
     187             :     }
     188             :     else
     189             :     {
     190        8634 :       ++it;
     191             :     }
     192             :   }
     193             : 
     194        1015 :   std::size_t erased_blocks = 0; //m_symbol_set.get_allocator().consolidate();
     195             : 
     196             :   if (EnableGarbageCollectionMetrics)
     197             :   {
     198             :     auto sweep_duration = std::chrono::duration_cast<std::chrono::milliseconds>(std::chrono::system_clock::now() - timestamp).count();
     199             : 
     200             :     // Print the relevant information.
     201             :     mCRL2log(mcrl2::log::info) << "function_symbol_pool: Garbage collected " << old_size - size() << " function symbols, " << size() << " function symbols remaining in "
     202             :       << sweep_duration << " ms.\n";
     203             : 
     204             :     mCRL2log(mcrl2::log::info) << "function_symbol_pool: Consolidate removed " << erased_blocks << " blocks.\n";
     205             :   }
     206             : 
     207             :   if constexpr (EnableHashtableMetrics)
     208             :   {
     209             :     print_performance_statistics(m_symbol_set);
     210             :   }
     211             : 
     212             :   if (EnableCreationMetrics)
     213             :   {
     214             :     mCRL2log(mcrl2::log::info) << "g_function_symbol_pool: Stores " << size() << " function symbols. create() " << m_function_symbol_metrics.message() << ".\n";
     215             :   }
     216             : 
     217             :   if (EnableReferenceCountMetrics)
     218             :   {
     219             :     mCRL2log(mcrl2::log::info) << "g_function_symbol_pool: all reference counts changed " << _function_symbol::reference_count_changes() << " times.\n";
     220             :   }
     221        1015 : }
     222          38 : void function_symbol_pool::resize_if_needed()
     223             : {
     224          38 :   m_symbol_set.rehash_if_needed();
     225          38 : }