From 71c38a08e5a18d39bd3b5fb8ee9ed715ebc51cd1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 11 Jun 2019 19:28:08 -0700 Subject: [PATCH] add initialization Signed-off-by: Nikolaj Bjorner --- src/shell/lp_frontend.cpp | 7 ++++--- src/shell/main.cpp | 4 ++++ src/shell/opt_frontend.cpp | 9 +++++---- src/shell/smtlib_frontend.cpp | 11 ++++++----- src/util/cooperate.cpp | 14 +++++++++++--- src/util/cooperate.h | 8 ++++++++ src/util/gparams.cpp | 27 ++++++++++++++------------- src/util/prime_generator.cpp | 7 +++---- src/util/prime_generator.h | 2 ++ src/util/rational.cpp | 7 +++++-- src/util/rlimit.cpp | 23 ++++++++++++++++------- src/util/rlimit.h | 7 +++++++ src/util/symbol.cpp | 9 +++++++-- 13 files changed, 92 insertions(+), 43 deletions(-) diff --git a/src/shell/lp_frontend.cpp b/src/shell/lp_frontend.cpp index 96284230d..04efc3d3c 100644 --- a/src/shell/lp_frontend.cpp +++ b/src/shell/lp_frontend.cpp @@ -16,8 +16,9 @@ Author: #include "util/rlimit.h" #include "util/gparams.h" #include +#include -static std::mutex display_stats_mux; +extern std::mutex* g_stat_mux; static lp::lp_solver* g_solver = nullptr; @@ -30,14 +31,14 @@ static void display_statistics() { static void STD_CALL on_ctrl_c(int) { signal (SIGINT, SIG_DFL); { - std::lock_guard lock(display_stats_mux); + std::lock_guard lock(*g_stat_mux); display_statistics(); } raise(SIGINT); } static void on_timeout() { - std::lock_guard lock(display_stats_mux); + std::lock_guard lock(*g_stat_mux); display_statistics(); exit(0); } diff --git a/src/shell/main.cpp b/src/shell/main.cpp index 1718e7314..2a9e1be32 100644 --- a/src/shell/main.cpp +++ b/src/shell/main.cpp @@ -18,6 +18,7 @@ Revision History: --*/ #include +#include #include "util/memory_manager.h" #include "util/trace.h" #include "util/debug.h" @@ -50,6 +51,7 @@ static char const * g_input_file = nullptr; static bool g_standard_input = false; static input_kind g_input_kind = IN_UNSPECIFIED; bool g_display_statistics = false; +std::mutex* g_stat_mux = nullptr; static bool g_display_istatistics = false; static void error(const char * msg) { @@ -311,6 +313,7 @@ int STD_CALL main(int argc, char ** argv) { unsigned return_value = 0; memory::initialize(0); memory::exit_when_out_of_memory(true, "ERROR: out of memory"); + g_stat_mux = alloc(std::mutex); parse_cmd_line_args(argc, argv); env_params::updt_params(); @@ -381,6 +384,7 @@ int STD_CALL main(int argc, char ** argv) { default: UNREACHABLE(); } + dealloc(g_stat_mux); memory::finalize(); #ifdef _WINDOWS _CrtDumpMemoryLeaks(); diff --git a/src/shell/opt_frontend.cpp b/src/shell/opt_frontend.cpp index e9e294eb9..62a6819c7 100644 --- a/src/shell/opt_frontend.cpp +++ b/src/shell/opt_frontend.cpp @@ -7,6 +7,7 @@ Copyright (c) 2015 Microsoft Corporation #include #include #include +#include #include "util/gparams.h" #include "util/timeout.h" #include "util/cancel_eh.h" @@ -21,11 +22,11 @@ Copyright (c) 2015 Microsoft Corporation #include "opt/opt_parse.h" extern bool g_display_statistics; +extern std::mutex* g_stat_mux; static bool g_first_interrupt = true; static opt::context* g_opt = nullptr; static double g_start_time = 0; static unsigned_vector g_handles; -static std::mutex display_stats_mux; @@ -70,7 +71,7 @@ static void STD_CALL on_ctrl_c(int) { else { signal (SIGINT, SIG_DFL); { - std::lock_guard lock(display_stats_mux); + std::lock_guard lock(*g_stat_mux); display_statistics(); } raise(SIGINT); @@ -79,7 +80,7 @@ static void STD_CALL on_ctrl_c(int) { static void on_timeout() { { - std::lock_guard lock(display_stats_mux); + std::lock_guard lock(*g_stat_mux); display_statistics(); } exit(0); @@ -133,7 +134,7 @@ static unsigned parse_opt(std::istream& in, opt_format f) { std::cerr << ex.msg() << "\n"; } { - std::lock_guard lock(display_stats_mux); + std::lock_guard lock(*g_stat_mux); display_statistics(); register_on_timeout_proc(nullptr); g_opt = nullptr; diff --git a/src/shell/smtlib_frontend.cpp b/src/shell/smtlib_frontend.cpp index ca0cbfaab..d8f47268d 100644 --- a/src/shell/smtlib_frontend.cpp +++ b/src/shell/smtlib_frontend.cpp @@ -21,6 +21,8 @@ Revision History: #include #include #include +#include + #include "util/timeout.h" #include "parsers/smt2/smt2parser.h" #include "muz/fp/dl_cmds.h" @@ -32,8 +34,7 @@ Revision History: #include "tactic/portfolio/smt_strategic_solver.h" #include "smt/smt_solver.h" -static std::mutex display_stats_mux; - +extern std::mutex* g_stat_mux; extern bool g_display_statistics; static clock_t g_start_time; static cmd_context * g_cmd_context = nullptr; @@ -51,7 +52,7 @@ static void display_statistics() { } static void on_timeout() { - std::lock_guard lock(display_stats_mux); + std::lock_guard lock(*g_stat_mux); display_statistics(); exit(0); } @@ -59,7 +60,7 @@ static void on_timeout() { static void STD_CALL on_ctrl_c(int) { signal (SIGINT, SIG_DFL); { - std::lock_guard lock(display_stats_mux); + std::lock_guard lock(*g_stat_mux); display_statistics(); } raise(SIGINT); @@ -99,7 +100,7 @@ unsigned read_smtlib2_commands(char const * file_name) { { - std::lock_guard lock(display_stats_mux); + std::lock_guard lock(*g_stat_mux); display_statistics(); g_cmd_context = nullptr; } diff --git a/src/util/cooperate.cpp b/src/util/cooperate.cpp index fa9ac7986..4a11cdb02 100644 --- a/src/util/cooperate.cpp +++ b/src/util/cooperate.cpp @@ -26,7 +26,15 @@ Notes: #include #include -static std::mutex lock; +static std::mutex* s_mux = nullptr; + +void initialize_cooperate() { + s_mux = new std::mutex(); +} +void finalize_cooperate() { + delete s_mux; +} + static std::atomic owner_thread; bool cooperation_ctx::g_cooperate = false; @@ -37,13 +45,13 @@ void cooperation_ctx::checkpoint(char const * task) { std::thread::id tid = std::this_thread::get_id(); if (owner_thread == tid) { owner_thread = std::thread::id(); - lock.unlock(); + s_mux->unlock(); } // this critical section is used to force the owner thread to give a chance to // another thread to get the lock std::this_thread::yield(); - lock.lock(); + s_mux->lock(); TRACE("cooperate_detail", tout << task << ", tid: " << tid << "\n";); owner_thread = tid; } diff --git a/src/util/cooperate.h b/src/util/cooperate.h index 7e75a50c3..7d58d947d 100644 --- a/src/util/cooperate.h +++ b/src/util/cooperate.h @@ -31,6 +31,14 @@ inline void cooperate(char const * task) { if (cooperation_ctx::enabled()) cooperation_ctx::checkpoint(task); } +void initialize_cooperate(); +void finalize_cooperate(); + +/* + ADD_INITIALIZER('initialize_cooperate();') + ADD_FINALIZER('finalize_cooperate();') +*/ + #else inline void cooperate(char const *) {} #endif diff --git a/src/util/gparams.cpp b/src/util/gparams.cpp index 0983189da..ec3620705 100644 --- a/src/util/gparams.cpp +++ b/src/util/gparams.cpp @@ -21,7 +21,7 @@ Notes: #include "util/trace.h" #include "util/mutex.h" -static mutex gparams_mux; +static mutex* s_mux = nullptr; extern void gparams_register_modules(); @@ -113,7 +113,7 @@ public: } void reset() { - lock_guard lock(gparams_mux); + lock_guard lock(*s_mux); m_params.reset(); for (auto & kv : m_module_params) { dealloc(kv.m_value); @@ -329,7 +329,7 @@ public: bool error = false; std::string error_msg; { - lock_guard lock(gparams_mux); + lock_guard lock(*s_mux); try { symbol m, p; normalize(name, m, p); @@ -381,7 +381,7 @@ public: bool error = false; std::string error_msg; { - lock_guard lock(gparams_mux); + lock_guard lock(*s_mux); try { symbol m, p; normalize(name, m, p); @@ -428,7 +428,7 @@ public: params_ref result; params_ref * ps = nullptr; { - lock_guard lock(gparams_mux); + lock_guard lock(*s_mux); if (m_module_params.find(module_name, ps)) { result.copy(*ps); } @@ -448,7 +448,7 @@ public: void display(std::ostream & out, unsigned indent, bool smt2_style, bool include_descr) { { - lock_guard lock(gparams_mux); + lock_guard lock(*s_mux); out << "Global parameters\n"; get_param_descrs().display(out, indent + 4, smt2_style, include_descr); out << "\n"; @@ -470,7 +470,7 @@ public: } void display_modules(std::ostream & out) { - lock_guard lock(gparams_mux); + lock_guard lock(*s_mux); for (auto & kv : get_module_param_descrs()) { out << "[module] " << kv.m_key; char const * descr = nullptr; @@ -484,7 +484,7 @@ public: void display_module(std::ostream & out, symbol const & module_name) { bool error = false; std::string error_msg; - lock_guard lock(gparams_mux); + lock_guard lock(*s_mux); try { param_descrs * d = nullptr; if (!get_module_param_descrs().find(module_name, d)) { @@ -513,7 +513,7 @@ public: bool error = false; std::string error_msg; { - lock_guard lock(gparams_mux); + lock_guard lock(*s_mux); try { symbol m, p; normalize(name, m, p); @@ -631,15 +631,16 @@ void gparams::display_parameter(std::ostream & out, char const * name) { void gparams::init() { TRACE("gparams", tout << "gparams::init()\n";); + s_mux = alloc(mutex); g_imp = alloc(imp); } void gparams::finalize() { TRACE("gparams", tout << "gparams::finalize()\n";); - if (g_imp != nullptr) { - dealloc(g_imp); - g_imp = nullptr; - } + dealloc(g_imp); + g_imp = nullptr; + dealloc(s_mux); + s_mux = nullptr; } diff --git a/src/util/prime_generator.cpp b/src/util/prime_generator.cpp index c659403ca..58647fd83 100644 --- a/src/util/prime_generator.cpp +++ b/src/util/prime_generator.cpp @@ -17,13 +17,13 @@ Notes: --*/ #include "util/prime_generator.h" -#include "util/mutex.h" #define PRIME_LIST_MAX_SIZE 1<<20 prime_generator::prime_generator() { m_primes.push_back(2); m_primes.push_back(3); + m_mux = alloc(mutex); process_next_k_numbers(128); } @@ -82,6 +82,7 @@ void prime_generator::process_next_k_numbers(uint64_t k) { void prime_generator::finalize() { m_primes.finalize(); + dealloc(m_mux); } uint64_t prime_generator::operator()(unsigned idx) { @@ -110,8 +111,6 @@ prime_iterator::prime_iterator(prime_generator * g):m_idx(0) { } } -static mutex g_prime_iterator; - uint64_t prime_iterator::next() { unsigned idx = m_idx; m_idx++; @@ -120,7 +119,7 @@ uint64_t prime_iterator::next() { } else { uint64_t r; - lock_guard lock(g_prime_iterator); + lock_guard lock(*m_generator->m_mux); { r = (*m_generator)(idx); } diff --git a/src/util/prime_generator.h b/src/util/prime_generator.h index bd388954c..924e9a2fc 100644 --- a/src/util/prime_generator.h +++ b/src/util/prime_generator.h @@ -22,6 +22,7 @@ Notes: #include "util/vector.h" #include "util/z3_exception.h" #include "util/util.h" +#include "util/mutex.h" class prime_generator_exception : public default_exception { public: @@ -35,6 +36,7 @@ class prime_generator { svector m_primes; void process_next_k_numbers(uint64_t k); public: + mutex *m_mux; prime_generator(); uint64_t operator()(unsigned idx); void finalize(); diff --git a/src/util/rational.cpp b/src/util/rational.cpp index 5e5ebe9e0..e32fd86d0 100644 --- a/src/util/rational.cpp +++ b/src/util/rational.cpp @@ -26,6 +26,7 @@ rational rational::m_zero; rational rational::m_one; rational rational::m_minus_one; vector rational::m_powers_of_two; +static mutex* s_mux = nullptr; static void mk_power_up_to(vector & pws, unsigned n) { if (pws.empty()) { @@ -40,11 +41,10 @@ static void mk_power_up_to(vector & pws, unsigned n) { } } -static mutex g_powers_of_two; rational rational::power_of_two(unsigned k) { rational result; - lock_guard lock(g_powers_of_two); + lock_guard lock(*s_mux); { if (k >= m_powers_of_two.size()) mk_power_up_to(m_powers_of_two, k+1); @@ -64,6 +64,7 @@ void finalize_inf_int_rational(); void rational::initialize() { if (!g_mpq_manager) { g_mpq_manager = alloc(synch_mpq_manager); + s_mux = alloc(mutex); m().set(m_zero.m_val, 0); m().set(m_one.m_val, 1); m().set(m_minus_one.m_val, -1); @@ -81,5 +82,7 @@ void rational::finalize() { m_minus_one.~rational(); dealloc(g_mpq_manager); g_mpq_manager = nullptr; + dealloc(s_mux); + s_mux = nullptr; } diff --git a/src/util/rlimit.cpp b/src/util/rlimit.cpp index ac596a118..629514fc2 100644 --- a/src/util/rlimit.cpp +++ b/src/util/rlimit.cpp @@ -21,7 +21,16 @@ Revision History: #include "util/mutex.h" -static mutex g_rlimit_mux; +static mutex* s_mux = nullptr; + +void initialize_rlimits() { + s_mux = new mutex; +} +void finalize_rlimit() { + delete s_mux; + s_mux = nullptr; +} + reslimit::reslimit(): m_cancel(0), @@ -73,32 +82,32 @@ char const* reslimit::get_cancel_msg() const { } void reslimit::push_child(reslimit* r) { - lock_guard lock(g_rlimit_mux); + lock_guard lock(*s_mux); m_children.push_back(r); } void reslimit::pop_child() { - lock_guard lock(g_rlimit_mux); + lock_guard lock(*s_mux); m_children.pop_back(); } void reslimit::cancel() { - lock_guard lock(g_rlimit_mux); + lock_guard lock(*s_mux); set_cancel(m_cancel+1); } void reslimit::reset_cancel() { - lock_guard lock(g_rlimit_mux); + lock_guard lock(*s_mux); set_cancel(0); } void reslimit::inc_cancel() { - lock_guard lock(g_rlimit_mux); + lock_guard lock(*s_mux); set_cancel(m_cancel+1); } void reslimit::dec_cancel() { - lock_guard lock(g_rlimit_mux); + lock_guard lock(*s_mux); if (m_cancel > 0) { set_cancel(m_cancel-1); } diff --git a/src/util/rlimit.h b/src/util/rlimit.h index 18124717a..8215e8e02 100644 --- a/src/util/rlimit.h +++ b/src/util/rlimit.h @@ -21,6 +21,13 @@ Revision History: #include "util/vector.h" +void initialize_rlimits(); +void finalize_rlimit(); +/* + ADD_INITIALIZER('initialize_rlimit();') + ADD_FINALIZER('finalize_rlimit();') +*/ + class reslimit { volatile unsigned m_cancel; bool m_suspend; diff --git a/src/util/symbol.cpp b/src/util/symbol.cpp index 36ea344fa..257b24100 100644 --- a/src/util/symbol.cpp +++ b/src/util/symbol.cpp @@ -23,7 +23,7 @@ Revision History: #include "util/string_buffer.h" #include -static mutex g_symbol_lock; +static mutex* s_mux = nullptr; symbol symbol::m_dummy(TAG(void*, nullptr, 2)); const symbol symbol::null; @@ -38,7 +38,7 @@ public: char const * get_str(char const * d) { const char * result; - lock_guard lock(g_symbol_lock); + lock_guard lock(*s_mux); str_hashtable::entry * e; if (m_table.insert_if_not_there_core(d, e)) { // new entry @@ -66,11 +66,16 @@ void initialize_symbols() { if (!g_symbol_table) { g_symbol_table = alloc(internal_symbol_table); } + if (!s_mux) { + s_mux = alloc(mutex); + } } void finalize_symbols() { dealloc(g_symbol_table); + dealloc(s_mux); g_symbol_table = nullptr; + s_mux = nullptr; } symbol::symbol(char const * d) {