mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

optimize symbol table for single-threaded mode

Browse source 
remotes a bunch of mem allocs + unnecessary computations on every string lookup
This commit is contained in:
Nuno Lopes 2021-05-23 16:35:44 +01:00
parent aef38099bf
commit f1545b04d2
1 changed files with 21 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

30
src/util/symbol.cpp
View file

@ -23,6 +23,7 @@ Revision History:
#include "util/region.h" #include "util/region.h"
#include "util/string_buffer.h" #include "util/string_buffer.h"
#include <cstring> #include <cstring>
#include <optional>
#ifndef SINGLE_THREAD #ifndef SINGLE_THREAD
#include <thread> #include <thread>
#endif #endif
@ -35,6 +36,7 @@ const symbol symbol::null;
/** /**
\brief Symbol table manager. It stores the symbol strings created at runtime. \brief Symbol table manager. It stores the symbol strings created at runtime.
*/ */
namespace {
class internal_symbol_table { class internal_symbol_table {
region m_region; //!< Region used to store symbol strings. region m_region; //!< Region used to store symbol strings.
str_hashtable m_table; //!< Table of created symbol strings. str_hashtable m_table; //!< Table of created symbol strings.
@ -73,6 +75,22 @@ public:
return result; return result;
} }
}; };
}
#ifdef SINGLE_THREAD
static std::optional<internal_symbol_table> g_symbol_tables;
void initialize_symbols() {
if (!g_symbol_tables) {
g_symbol_tables.emplace();
}
}
void finalize_symbols() {
g_symbol_tables.reset();
}
#else
struct internal_symbol_tables { struct internal_symbol_tables {
unsigned sz; unsigned sz;
@ -101,11 +119,7 @@ static internal_symbol_tables* g_symbol_tables = nullptr;
void initialize_symbols() { void initialize_symbols() {
if (!g_symbol_tables) { if (!g_symbol_tables) {
#ifdef SINGLE_THREAD
unsigned num_tables = 1;
#else
unsigned num_tables = 2 * std::min((unsigned) std::thread::hardware_concurrency(), 64u); unsigned num_tables = 2 * std::min((unsigned) std::thread::hardware_concurrency(), 64u);
#endif
g_symbol_tables = alloc(internal_symbol_tables, num_tables); g_symbol_tables = alloc(internal_symbol_tables, num_tables);
} }
@ -115,6 +129,7 @@ void finalize_symbols() {
dealloc(g_symbol_tables); dealloc(g_symbol_tables);
g_symbol_tables = nullptr; g_symbol_tables = nullptr;
} }
#endif
symbol::symbol(char const * d) { symbol::symbol(char const * d) {
if (d == nullptr) if (d == nullptr)
@ -130,11 +145,8 @@ symbol & symbol::operator=(char const * d) {
std::string symbol::str() const { std::string symbol::str() const {
SASSERT(!is_marked()); SASSERT(!is_marked());
if (GET_TAG(m_data) == 0) { if (GET_TAG(m_data) == 0) {
if (m_data) return m_data ? m_data : "<null>";
return m_data;
else
return "<null>";
} }
else { else {
string_buffer<128> buffer; string_buffer<128> buffer;