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

reduce contention around the symbol table #2842

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-01-06 16:47:06 -08:00
parent 88fc4c82aa
commit 670e8f8d67
1 changed files with 44 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

55
src/util/symbol.cpp
View file

@ -23,7 +23,7 @@ Revision History:
#include "util/string_buffer.h" #include "util/string_buffer.h"
#include <cstring> #include <cstring>
static DECLARE_MUTEX(g_symbol_lock);
symbol symbol::m_dummy(TAG(void*, nullptr, 2)); symbol symbol::m_dummy(TAG(void*, nullptr, 2));
const symbol symbol::null; const symbol symbol::null;
@ -34,11 +34,21 @@ const symbol symbol::null;
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.
DECLARE_MUTEX(lock);
public: public:
internal_symbol_table() {
ALLOC_MUTEX(lock);
}
~internal_symbol_table() {
DEALLOC_MUTEX(lock);
}
char const * get_str(char const * d) { char const * get_str(char const * d) {
const char * result; const char * result;
lock_guard lock(*g_symbol_lock); lock_guard _lock(*lock);
str_hashtable::entry * e; str_hashtable::entry * e;
if (m_table.insert_if_not_there_core(d, e)) { if (m_table.insert_if_not_there_core(d, e)) {
// new entry // new entry
@ -60,30 +70,53 @@ public:
} }
}; };
static internal_symbol_table* g_symbol_table = nullptr; struct internal_symbol_tables {
unsigned sz;
internal_symbol_table** tables;
internal_symbol_tables(unsigned sz): sz(sz), tables(alloc_vect<internal_symbol_table*>(sz)) {
for (unsigned i = 0; i < sz; ++i) {
tables[i] = alloc(internal_symbol_table);
}
}
~internal_symbol_tables() {
for (unsigned i = 0; i < sz; ++i) {
dealloc(tables[i]);
}
dealloc_vect<internal_symbol_table*>(tables, sz);
}
char const * get_str(char const * d) {
auto* table = tables[string_hash(d, static_cast<unsigned>(strlen(d)), 251) % sz];
return table->get_str(d);
}
};
static internal_symbol_tables* g_symbol_tables = nullptr;
void initialize_symbols() { void initialize_symbols() {
if (!g_symbol_table) { if (!g_symbol_tables) {
ALLOC_MUTEX(g_symbol_lock); unsigned num_tables = 2 * std::min((unsigned) std::thread::hardware_concurrency(), 64u);
g_symbol_table = alloc(internal_symbol_table); g_symbol_tables = alloc(internal_symbol_tables, num_tables);
} }
} }
void finalize_symbols() { void finalize_symbols() {
DEALLOC_MUTEX(g_symbol_lock); dealloc(g_symbol_tables);
dealloc(g_symbol_table); g_symbol_tables = nullptr;
g_symbol_table = nullptr;
} }
symbol::symbol(char const * d) { symbol::symbol(char const * d) {
if (d == nullptr) if (d == nullptr)
m_data = nullptr; m_data = nullptr;
else else
m_data = g_symbol_table->get_str(d); m_data = g_symbol_tables->get_str(d);
} }
symbol & symbol::operator=(char const * d) { symbol & symbol::operator=(char const * d) {
m_data = g_symbol_table->get_str(d); m_data = g_symbol_tables->get_str(d);
return *this; return *this;
} }