From 9262908ebb7bdb4875a4316fdb607754ad9e72be Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 3 Jun 2019 19:50:25 -0700 Subject: [PATCH] mux Signed-off-by: Nikolaj Bjorner --- CMakeLists.txt | 38 --------- ...z3_append_linker_flag_list_to_target.cmake | 2 +- src/api/api_context.cpp | 26 +++--- src/api/api_context.h | 2 + src/api/api_log.cpp | 8 +- src/ast/rewriter/der.cpp | 7 +- src/cmd_context/echo_tactic.cpp | 22 ++---- src/sat/sat_parallel.cpp | 38 ++++----- src/sat/sat_parallel.h | 1 + src/sat/sat_solver.cpp | 12 --- src/shell/lp_frontend.cpp | 13 ++- src/shell/opt_frontend.cpp | 9 ++- src/shell/smtlib_frontend.cpp | 14 ++-- src/smt/smt_kernel.cpp | 7 +- src/solver/parallel_tactic.cpp | 2 +- src/tactic/tactical.cpp | 27 +++---- src/util/cooperate.cpp | 32 +++----- src/util/gparams.cpp | 79 +++++++++---------- src/util/memory_manager.cpp | 29 +++---- src/util/mpn.cpp | 2 - src/util/mpn.h | 10 +-- src/util/mpz.cpp | 4 - src/util/mpz.h | 12 +-- src/util/prime_generator.cpp | 5 +- src/util/rational.cpp | 5 +- src/util/rlimit.cpp | 42 ++++------ src/util/symbol.cpp | 8 +- src/util/util.cpp | 4 + src/util/util.h | 34 +++----- src/util/z3_omp.h | 38 --------- 30 files changed, 191 insertions(+), 341 deletions(-) delete mode 100644 src/util/z3_omp.h diff --git a/CMakeLists.txt b/CMakeLists.txt index fb0fc6a87..fca5520ab 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -272,41 +272,6 @@ else() message(STATUS "Not using libgmp") endif() -################################################################################ -# OpenMP support -################################################################################ -find_package(OpenMP) -if (OPENMP_FOUND) - set(USE_OPENMP_DEFAULT ON) -else() - set(USE_OPENMP_DEFAULT OFF) -endif() -# By setting `USE_OPENMP` this way configuration will fail during the first -# configure if the user explicitly passes `-DUSE_OPENMP=ON` and the compiler -# does not support OpenMP. However if the option is not set explicitly during -# the first configure OpenMP support will be automatically enabled/disabled -# depending on whether OpenMP is available. -option(USE_OPENMP "Use OpenMP" ${USE_OPENMP_DEFAULT}) - -if (USE_OPENMP) - if (NOT OPENMP_FOUND) - message(FATAL_ERROR "USE_OPENMP is ON but your compiler does not support OpenMP") - endif() - - list(APPEND Z3_COMPONENT_CXX_FLAGS ${OpenMP_CXX_FLAGS}) - # GCC and Clang need to have additional flags passed to the linker. - # We can't do ``target_link_libraries(libz3 INTERFACE ${OpenMP_CXX_FLAGS})`` - # because ``/openmp`` is interpreted as file name rather than a linker - # flag by MSVC and breaks the build - if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang") OR - ("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU")) - list(APPEND Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS ${OpenMP_CXX_FLAGS}) - endif() - message(STATUS "Using OpenMP") -else() - list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_NO_OMP_") - message(STATUS "Not using OpenMP") -endif() ################################################################################ # API Log sync @@ -316,9 +281,6 @@ option(API_LOG_SYNC OFF ) if (API_LOG_SYNC) - if (NOT USE_OPENMP) - message(FATAL_ERROR "API_LOG_SYNC feature requires OpenMP") - endif() list(APPEND Z3_COMPONENT_CXX_DEFINES "-DZ3_LOG_SYNC") message(STATUS "Using API_LOG_SYNC") else() diff --git a/cmake/z3_append_linker_flag_list_to_target.cmake b/cmake/z3_append_linker_flag_list_to_target.cmake index 3eb1e2d34..6e1378270 100644 --- a/cmake/z3_append_linker_flag_list_to_target.cmake +++ b/cmake/z3_append_linker_flag_list_to_target.cmake @@ -3,7 +3,7 @@ # them to append them as strings to the ``LINK_FLAGS`` property of # the specified target. # E.g. -# z3_append_linker_flag_list_to_target(mytarget "-fopenmp" "-static") +# z3_append_linker_flag_list_to_target(mytarget "-static") function(z3_append_linker_flag_list_to_target target) if (NOT (TARGET "${target}")) message(FATAL_ERROR "Specified target \"${target}\" is not a target") diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index 7fbbd965e..3b946bd21 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -119,28 +119,22 @@ namespace api { context::set_interruptable::set_interruptable(context & ctx, event_handler & i): m_ctx(ctx) { - #pragma omp critical (set_interruptable) - { - SASSERT(m_ctx.m_interruptable == 0); - m_ctx.m_interruptable = &i; - } + std::lock_guard lock(ctx.m_mux); + SASSERT(m_ctx.m_interruptable == 0); + m_ctx.m_interruptable = &i; } context::set_interruptable::~set_interruptable() { - #pragma omp critical (set_interruptable) - { - m_ctx.m_interruptable = nullptr; - } + std::lock_guard lock(m_ctx.m_mux); + m_ctx.m_interruptable = nullptr; } void context::interrupt() { - #pragma omp critical (set_interruptable) - { - if (m_interruptable) - (*m_interruptable)(API_INTERRUPT_EH_CALLER); - m_limit.cancel(); - m().limit().cancel(); - } + std::lock_guard lock(m_mux); + if (m_interruptable) + (*m_interruptable)(API_INTERRUPT_EH_CALLER); + m_limit.cancel(); + m().limit().cancel(); } void context::set_error_code(Z3_error_code err, char const* opt_msg) { diff --git a/src/api/api_context.h b/src/api/api_context.h index 917d3f0af..ff239438a 100644 --- a/src/api/api_context.h +++ b/src/api/api_context.h @@ -42,6 +42,7 @@ Revision History: #include "ast/rewriter/seq_rewriter.h" #include "smt/smt_solver.h" #include "solver/solver.h" +#include namespace smtlib { class parser; @@ -79,6 +80,7 @@ namespace api { scoped_ptr m_manager; scoped_ptr m_cmd; add_plugins m_plugins; + std::mutex m_mux; arith_util m_arith_util; bv_util m_bv_util; diff --git a/src/api/api_log.cpp b/src/api/api_log.cpp index d338407bf..d6dccc670 100644 --- a/src/api/api_log.cpp +++ b/src/api/api_log.cpp @@ -16,6 +16,7 @@ Revision History: --*/ #include +#include #include "api/z3.h" #include "api/api_log_macros.h" #include "util/util.h" @@ -23,6 +24,7 @@ Revision History: std::ostream * g_z3_log = nullptr; bool g_z3_log_enabled = false; +static std::mutex g_log_mux; extern "C" { void Z3_close_log_unsafe(void) { @@ -37,7 +39,7 @@ extern "C" { bool res = true; #ifdef Z3_LOG_SYNC - #pragma omp critical (z3_log) + std::lock_guard lock(g_log_mux); { #endif if (g_z3_log != nullptr) @@ -64,7 +66,7 @@ extern "C" { if (g_z3_log == nullptr) return; #ifdef Z3_LOG_SYNC - #pragma omp critical (z3_log) + std::lock_guard lock(g_log_mux); { #endif if (g_z3_log != nullptr) @@ -77,7 +79,7 @@ extern "C" { void Z3_API Z3_close_log(void) { if (g_z3_log != nullptr) { #ifdef Z3_LOG_SYNC - #pragma omp critical (z3_log) + std::lock_guard lock(g_log_mux); { #endif Z3_close_log_unsafe(); diff --git a/src/ast/rewriter/der.cpp b/src/ast/rewriter/der.cpp index c95c07f63..196750a46 100644 --- a/src/ast/rewriter/der.cpp +++ b/src/ast/rewriter/der.cpp @@ -436,11 +436,8 @@ void der_rewriter::operator()(expr * t, expr_ref & result, proof_ref & result_pr void der_rewriter::cleanup() { ast_manager & m = m_imp->m(); - #pragma omp critical (th_rewriter) - { - dealloc(m_imp); - m_imp = alloc(imp, m); - } + dealloc(m_imp); + m_imp = alloc(imp, m); } void der_rewriter::reset() { diff --git a/src/cmd_context/echo_tactic.cpp b/src/cmd_context/echo_tactic.cpp index 1ea556bef..d722b9351 100644 --- a/src/cmd_context/echo_tactic.cpp +++ b/src/cmd_context/echo_tactic.cpp @@ -29,12 +29,9 @@ public: void operator()(goal_ref const & in, goal_ref_buffer & result) override { - #pragma omp critical (echo_tactic) - { - m_ctx.regular_stream() << m_msg; - if (m_newline) - m_ctx.regular_stream() << std::endl; - } + m_ctx.regular_stream() << m_msg; + if (m_newline) + m_ctx.regular_stream() << std::endl; skip_tactic::operator()(in, result); } }; @@ -61,14 +58,11 @@ public: void operator()(goal_ref const & in, goal_ref_buffer & result) override { double val = (*m_p)(*(in.get())).get_value(); - #pragma omp critical (probe_value_tactic) - { - if (m_msg) - m_ctx.diagnostic_stream() << m_msg << " "; - m_ctx.diagnostic_stream() << val; - if (m_newline) - m_ctx.diagnostic_stream() << std::endl; - } + if (m_msg) + m_ctx.diagnostic_stream() << m_msg << " "; + m_ctx.diagnostic_stream() << val; + if (m_newline) + m_ctx.diagnostic_stream() << std::endl; skip_tactic::operator()(in, result); } }; diff --git a/src/sat/sat_parallel.cpp b/src/sat/sat_parallel.cpp index 77a5f973d..c66552ac5 100644 --- a/src/sat/sat_parallel.cpp +++ b/src/sat/sat_parallel.cpp @@ -129,8 +129,8 @@ namespace sat { void parallel::exchange(solver& s, literal_vector const& in, unsigned& limit, literal_vector& out) { if (s.get_config().m_num_threads == 1 || s.m_par_syncing_clauses) return; flet _disable_sync_clause(s.m_par_syncing_clauses, true); - #pragma omp critical (par_solver) { + std::lock_guard lock(m_mux); if (limit < m_units.size()) { // this might repeat some literals. out.append(m_units.size() - limit, m_units.c_ptr() + limit); @@ -150,8 +150,8 @@ namespace sat { if (s.get_config().m_num_threads == 1 || s.m_par_syncing_clauses) return; flet _disable_sync_clause(s.m_par_syncing_clauses, true); IF_VERBOSE(3, verbose_stream() << s.m_par_id << ": share " << l1 << " " << l2 << "\n";); - #pragma omp critical (par_solver) { + std::lock_guard lock(m_mux); m_pool.begin_add_vector(s.m_par_id, 2); m_pool.add_vector_elem(l1.index()); m_pool.add_vector_elem(l2.index()); @@ -165,23 +165,19 @@ namespace sat { unsigned n = c.size(); unsigned owner = s.m_par_id; IF_VERBOSE(3, verbose_stream() << owner << ": share " << c << "\n";); - #pragma omp critical (par_solver) - { - m_pool.begin_add_vector(owner, n); - for (unsigned i = 0; i < n; ++i) { - m_pool.add_vector_elem(c[i].index()); - } - m_pool.end_add_vector(); + std::lock_guard lock(m_mux); + m_pool.begin_add_vector(owner, n); + for (unsigned i = 0; i < n; ++i) { + m_pool.add_vector_elem(c[i].index()); } + m_pool.end_add_vector(); } void parallel::get_clauses(solver& s) { if (s.m_par_syncing_clauses) return; flet _disable_sync_clause(s.m_par_syncing_clauses, true); - #pragma omp critical (par_solver) - { - _get_clauses(s); - } + std::lock_guard lock(m_mux); + _get_clauses(s); } void parallel::_get_clauses(solver& s) { @@ -241,17 +237,13 @@ namespace sat { } void parallel::set_phase(solver& s) { - #pragma omp critical (par_solver) - { - _set_phase(s); - } + std::lock_guard lock(m_mux); + _set_phase(s); } void parallel::get_phase(solver& s) { - #pragma omp critical (par_solver) - { - _get_phase(s); - } + std::lock_guard lock(m_mux); + _get_phase(s); } void parallel::_get_phase(solver& s) { @@ -269,8 +261,8 @@ namespace sat { bool parallel::get_phase(local_search& s) { bool copied = false; - #pragma omp critical (par_solver) { + std::lock_guard lock(m_mux); m_consumer_ready = true; if (m_solver_copy && s.num_non_binary_clauses() > m_solver_copy->m_clauses.size()) { copied = true; @@ -288,8 +280,8 @@ namespace sat { bool parallel::copy_solver(solver& s) { bool copied = false; - #pragma omp critical (par_solver) { + std::lock_guard lock(m_mux); m_consumer_ready = true; if (m_solver_copy && s.m_clauses.size() > m_solver_copy->m_clauses.size()) { s.copy(*m_solver_copy, true); diff --git a/src/sat/sat_parallel.h b/src/sat/sat_parallel.h index afb148ed4..22dbfc490 100644 --- a/src/sat/sat_parallel.h +++ b/src/sat/sat_parallel.h @@ -60,6 +60,7 @@ namespace sat { index_set m_unit_set; literal_vector m_lits; vector_pool m_pool; + std::mutex m_mux; // for exchange with local search: svector m_phase; diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 9241c4eaa..81f1793a9 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -1731,18 +1731,6 @@ namespace sat { } if (m_par) m_par->set_phase(*this); - -#if 0 - static unsigned file_no = 0; - #pragma omp critical (print_sat) - { - ++file_no; - std::ostringstream ostrm; - ostrm << "s" << file_no << ".txt"; - std::ofstream ous(ostrm.str()); - display(ous); - } -#endif } bool solver::set_root(literal l, literal r) { diff --git a/src/shell/lp_frontend.cpp b/src/shell/lp_frontend.cpp index 718f59854..96284230d 100644 --- a/src/shell/lp_frontend.cpp +++ b/src/shell/lp_frontend.cpp @@ -17,6 +17,8 @@ Author: #include "util/gparams.h" #include +static std::mutex display_stats_mux; + static lp::lp_solver* g_solver = nullptr; static void display_statistics() { @@ -27,19 +29,17 @@ static void display_statistics() { static void STD_CALL on_ctrl_c(int) { signal (SIGINT, SIG_DFL); - #pragma omp critical (g_display_stats) { + std::lock_guard lock(display_stats_mux); display_statistics(); } raise(SIGINT); } static void on_timeout() { - #pragma omp critical (g_display_stats) - { - display_statistics(); - exit(0); - } + std::lock_guard lock(display_stats_mux); + display_statistics(); + exit(0); } struct front_end_resource_limit : public lp::lp_resource_limit { @@ -92,7 +92,6 @@ void run_solver(lp_params & params, char const * mps_file_name) { solver->print_model(std::cout); } -// #pragma omp critical (g_display_stats) { display_statistics(); register_on_timeout_proc(nullptr); diff --git a/src/shell/opt_frontend.cpp b/src/shell/opt_frontend.cpp index afa7b79c5..e9e294eb9 100644 --- a/src/shell/opt_frontend.cpp +++ b/src/shell/opt_frontend.cpp @@ -25,6 +25,7 @@ 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; @@ -68,8 +69,8 @@ static void STD_CALL on_ctrl_c(int) { } else { signal (SIGINT, SIG_DFL); - #pragma omp critical (g_display_stats) { + std::lock_guard lock(display_stats_mux); display_statistics(); } raise(SIGINT); @@ -77,11 +78,11 @@ static void STD_CALL on_ctrl_c(int) { } static void on_timeout() { - #pragma omp critical (g_display_stats) { + std::lock_guard lock(display_stats_mux); display_statistics(); - exit(0); } + exit(0); } static unsigned parse_opt(std::istream& in, opt_format f) { @@ -131,8 +132,8 @@ static unsigned parse_opt(std::istream& in, opt_format f) { catch (z3_exception & ex) { std::cerr << ex.msg() << "\n"; } - #pragma omp critical (g_display_stats) { + std::lock_guard lock(display_stats_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 0f156bced..ca0cbfaab 100644 --- a/src/shell/smtlib_frontend.cpp +++ b/src/shell/smtlib_frontend.cpp @@ -32,6 +32,8 @@ Revision History: #include "tactic/portfolio/smt_strategic_solver.h" #include "smt/smt_solver.h" +static std::mutex display_stats_mux; + extern bool g_display_statistics; static clock_t g_start_time; static cmd_context * g_cmd_context = nullptr; @@ -49,17 +51,15 @@ static void display_statistics() { } static void on_timeout() { - #pragma omp critical (g_display_stats) - { - display_statistics(); - exit(0); - } + std::lock_guard lock(display_stats_mux); + display_statistics(); + exit(0); } static void STD_CALL on_ctrl_c(int) { signal (SIGINT, SIG_DFL); - #pragma omp critical (g_display_stats) { + std::lock_guard lock(display_stats_mux); display_statistics(); } raise(SIGINT); @@ -98,8 +98,8 @@ unsigned read_smtlib2_commands(char const * file_name) { } - #pragma omp critical (g_display_stats) { + std::lock_guard lock(display_stats_mux); display_statistics(); g_cmd_context = nullptr; } diff --git a/src/smt/smt_kernel.cpp b/src/smt/smt_kernel.cpp index 323efeb12..9c8e08d3d 100644 --- a/src/smt/smt_kernel.cpp +++ b/src/smt/smt_kernel.cpp @@ -295,11 +295,8 @@ namespace smt { ast_manager & _m = m(); smt_params & fps = m_imp->fparams(); params_ref ps = m_imp->params(); - #pragma omp critical (smt_kernel) - { - m_imp->~imp(); - m_imp = new (m_imp) imp(_m, fps, ps); - } + m_imp->~imp(); + m_imp = new (m_imp) imp(_m, fps, ps); } bool kernel::inconsistent() { diff --git a/src/solver/parallel_tactic.cpp b/src/solver/parallel_tactic.cpp index 053a584c1..1dbb5c090 100644 --- a/src/solver/parallel_tactic.cpp +++ b/src/solver/parallel_tactic.cpp @@ -337,7 +337,7 @@ private: void init() { parallel_params pp(m_params); - m_num_threads = std::min((unsigned)omp_get_num_procs(), pp.threads_max()); + m_num_threads = std::min((unsigned) std::thread::hardware_concurrency(), pp.threads_max()); m_progress = 0; m_has_undef = false; m_allsat = false; diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp index 00ea59869..9d64fa373 100644 --- a/src/tactic/tactical.cpp +++ b/src/tactic/tactical.cpp @@ -20,7 +20,6 @@ Notes: #include "util/cancel_eh.h" #include "util/cooperate.h" #include "util/scoped_ptr_vector.h" -#include "util/z3_omp.h" #include "tactic/tactical.h" class binary_tactical : public tactic { @@ -378,11 +377,7 @@ public: void operator()(goal_ref const & in, goal_ref_buffer& result) override { bool use_seq; -#ifdef _NO_OMP_ - use_seq = true; -#else - use_seq = 0 != omp_in_parallel(); -#endif + use_seq = false; if (use_seq) { // execute tasks sequentially or_else_tactical::operator()(in, result); @@ -409,7 +404,8 @@ public: par_exception_kind ex_kind = DEFAULT_EX; std::string ex_msg; unsigned error_code = 0; - + std::mutex mux; + #pragma omp parallel for for (int i = 0; i < static_cast(sz); i++) { goal_ref_buffer _result; @@ -420,8 +416,8 @@ public: try { t(in_copy, _result); bool first = false; - #pragma omp critical (par_tactical) { + std::lock_guard lock(mux); if (finished_id == UINT_MAX) { finished_id = i; first = true; @@ -499,11 +495,7 @@ public: void operator()(goal_ref const & in, goal_ref_buffer& result) override { bool use_seq; -#ifdef _NO_OMP_ - use_seq = true; -#else - use_seq = 0 != omp_in_parallel(); -#endif + use_seq = false; if (use_seq) { // execute tasks sequentially and_then_tactical::operator()(in, result); @@ -554,6 +546,7 @@ public: par_exception_kind ex_kind = DEFAULT_EX; unsigned error_code = 0; std::string ex_msg; + std::mutex mux; #pragma omp parallel for for (int i = 0; i < static_cast(r1_size); i++) { @@ -568,8 +561,8 @@ public: ts2[i]->operator()(new_g, r2); } catch (tactic_exception & ex) { - #pragma omp critical (par_and_then_tactical) { + std::lock_guard lock(mux); if (!failed && !found_solution) { curr_failed = true; failed = true; @@ -579,8 +572,8 @@ public: } } catch (z3_error & err) { - #pragma omp critical (par_and_then_tactical) { + std::lock_guard lock(mux); if (!failed && !found_solution) { curr_failed = true; failed = true; @@ -590,8 +583,8 @@ public: } } catch (z3_exception & z3_ex) { - #pragma omp critical (par_and_then_tactical) { + std::lock_guard lock(mux); if (!failed && !found_solution) { curr_failed = true; failed = true; @@ -614,8 +607,8 @@ public: if (is_decided_sat(r2)) { // found solution... bool first = false; - #pragma omp critical (par_and_then_tactical) { + std::lock_guard lock(mux); if (!found_solution) { failed = false; found_solution = true; diff --git a/src/util/cooperate.cpp b/src/util/cooperate.cpp index df8f67968..029ac2b87 100644 --- a/src/util/cooperate.cpp +++ b/src/util/cooperate.cpp @@ -17,24 +17,20 @@ Notes: --*/ -#ifndef _NO_OMP_ #include "util/cooperate.h" #include "util/trace.h" #include "util/debug.h" -#include "util/z3_omp.h" +#include +#include struct cooperation_lock { - omp_nest_lock_t m_lock; + std::recursive_mutex m_lock; char const * m_task; - volatile int m_owner_thread; + std::thread::id m_owner_thread; cooperation_lock() { - omp_set_nested(1); - omp_init_nest_lock(&m_lock); m_task = nullptr; - m_owner_thread = -1; } ~cooperation_lock() { - omp_destroy_nest_lock(&m_lock); } }; @@ -45,20 +41,18 @@ bool cooperation_ctx::g_cooperate = false; void cooperation_ctx::checkpoint(char const * task) { SASSERT(cooperation_ctx::enabled()); - int tid = omp_get_thread_num(); + std::thread::id tid = std::this_thread::get_id(); if (g_lock.m_owner_thread == tid) { - g_lock.m_owner_thread = -1; - omp_unset_nest_lock(&(g_lock.m_lock)); + g_lock.m_owner_thread = std::thread::id(); + g_lock.m_lock.unlock(); } + // this critical section is used to force the owner thread to give a chance to // another thread to get the lock - #pragma omp critical (z3_cooperate) - { - omp_set_nest_lock(&(g_lock.m_lock)); - TRACE("cooperate_detail", tout << task << ", tid: " << tid << "\n";); - CTRACE("cooperate", g_lock.m_task != task, tout << "moving to task: " << task << "\n";); - g_lock.m_owner_thread = tid; - } + std::this_thread::yield(); + g_lock.m_lock.lock(); + TRACE("cooperate_detail", tout << task << ", tid: " << tid << "\n";); + CTRACE("cooperate", g_lock.m_task != task, tout << "moving to task: " << task << "\n";); + g_lock.m_owner_thread = tid; } -#endif diff --git a/src/util/gparams.cpp b/src/util/gparams.cpp index ea9b3603c..06cc67211 100644 --- a/src/util/gparams.cpp +++ b/src/util/gparams.cpp @@ -19,6 +19,9 @@ Notes: #include "util/gparams.h" #include "util/dictionary.h" #include "util/trace.h" +#include + +static std::mutex gparams_mux; extern void gparams_register_modules(); @@ -110,14 +113,12 @@ public: } void reset() { - #pragma omp critical (gparams) - { - m_params.reset(); - for (auto & kv : m_module_params) { - dealloc(kv.m_value); - } - m_module_params.reset(); + std::lock_guard lock(gparams_mux); + m_params.reset(); + for (auto & kv : m_module_params) { + dealloc(kv.m_value); } + m_module_params.reset(); } // ----------------------------------------------- @@ -327,8 +328,8 @@ public: void set(char const * name, char const * value) { bool error = false; std::string error_msg; - #pragma omp critical (gparams) { + std::lock_guard lock(gparams_mux); try { symbol m, p; normalize(name, m, p); @@ -379,8 +380,8 @@ public: std::string r; bool error = false; std::string error_msg; - #pragma omp critical (gparams) { + std::lock_guard lock(gparams_mux); try { symbol m, p; normalize(name, m, p); @@ -426,8 +427,8 @@ public: params_ref get_module(symbol const & module_name) { params_ref result; params_ref * ps = nullptr; - #pragma omp critical (gparams) { + std::lock_guard lock(gparams_mux); if (m_module_params.find(module_name, ps)) { result.copy(*ps); } @@ -446,8 +447,8 @@ public: // ----------------------------------------------- void display(std::ostream & out, unsigned indent, bool smt2_style, bool include_descr) { - #pragma omp critical (gparams) { + std::lock_guard lock(gparams_mux); out << "Global parameters\n"; get_param_descrs().display(out, indent + 4, smt2_style, include_descr); out << "\n"; @@ -469,44 +470,40 @@ public: } void display_modules(std::ostream & out) { - #pragma omp critical (gparams) - { - for (auto & kv : get_module_param_descrs()) { - out << "[module] " << kv.m_key; - char const * descr = nullptr; - if (get_module_descrs().find(kv.m_key, descr)) { - out << ", description: " << descr; - } - out << "\n"; + std::lock_guard lock(gparams_mux); + for (auto & kv : get_module_param_descrs()) { + out << "[module] " << kv.m_key; + char const * descr = nullptr; + if (get_module_descrs().find(kv.m_key, descr)) { + out << ", description: " << descr; } + out << "\n"; } } void display_module(std::ostream & out, symbol const & module_name) { bool error = false; std::string error_msg; - #pragma omp critical (gparams) - { - try { - param_descrs * d = nullptr; - if (!get_module_param_descrs().find(module_name, d)) { - std::stringstream strm; - strm << "unknown module '" << module_name << "'"; - throw exception(strm.str()); - } - out << "[module] " << module_name; - char const * descr = nullptr; - if (get_module_descrs().find(module_name, descr)) { - out << ", description: " << descr; - } - out << "\n"; - d->display(out, 4, false); + std::lock_guard lock(gparams_mux); + try { + param_descrs * d = nullptr; + if (!get_module_param_descrs().find(module_name, d)) { + std::stringstream strm; + strm << "unknown module '" << module_name << "'"; + throw exception(strm.str()); } - catch (z3_exception & ex) { - // Exception cannot cross critical section boundaries. - error = true; - error_msg = ex.msg(); + out << "[module] " << module_name; + char const * descr = nullptr; + if (get_module_descrs().find(module_name, descr)) { + out << ", description: " << descr; } + out << "\n"; + d->display(out, 4, false); + } + catch (z3_exception & ex) { + // Exception cannot cross critical section boundaries. + error = true; + error_msg = ex.msg(); } if (error) throw exception(std::move(error_msg)); @@ -515,8 +512,8 @@ public: void display_parameter(std::ostream & out, char const * name) { bool error = false; std::string error_msg; - #pragma omp critical (gparams) { + std::lock_guard lock(gparams_mux); try { symbol m, p; normalize(name, m, p); diff --git a/src/util/memory_manager.cpp b/src/util/memory_manager.cpp index 6ef94e880..e1a763567 100644 --- a/src/util/memory_manager.cpp +++ b/src/util/memory_manager.cpp @@ -7,10 +7,10 @@ Copyright (c) 2015 Microsoft Corporation #include #include #include +#include #include "util/trace.h" #include "util/memory_manager.h" #include "util/error_codes.h" -#include "util/z3_omp.h" #include "util/debug.h" // The following two function are automatically generated by the mk_make.py script. // The script collects ADD_INITIALIZER and ADD_FINALIZER commands in the .h files. @@ -35,6 +35,7 @@ out_of_memory_error::out_of_memory_error():z3_error(ERR_MEMOUT) { } +static std::mutex g_memory_mux; static volatile bool g_memory_out_of_memory = false; static bool g_memory_initialized = false; static long long g_memory_alloc_size = 0; @@ -54,8 +55,8 @@ void memory::exit_when_out_of_memory(bool flag, char const * msg) { } static void throw_out_of_memory() { - #pragma omp critical (z3_memory_manager) { + std::lock_guard lock(g_memory_mux); g_memory_out_of_memory = true; } @@ -90,8 +91,8 @@ mem_usage_report g_info; void memory::initialize(size_t max_size) { bool initialize = false; - #pragma omp critical (z3_memory_manager) { + std::lock_guard lock(g_memory_mux); // only update the maximum size if max_size != UINT_MAX if (max_size != UINT_MAX) g_memory_max_size = max_size; @@ -116,8 +117,8 @@ void memory::initialize(size_t max_size) { bool memory::is_out_of_memory() { bool r = false; - #pragma omp critical (z3_memory_manager) { + std::lock_guard lock(g_memory_mux); r = g_memory_out_of_memory; } return r; @@ -131,12 +132,8 @@ void memory::set_high_watermark(size_t watermark) { bool memory::above_high_watermark() { if (g_memory_watermark == 0) return false; - bool r; - #pragma omp critical (z3_memory_manager) - { - r = g_memory_watermark < g_memory_alloc_size; - } - return r; + std::lock_guard lock(g_memory_mux); + return g_memory_watermark < g_memory_alloc_size; } // The following methods are only safe to invoke at @@ -163,8 +160,8 @@ void memory::finalize() { unsigned long long memory::get_allocation_size() { long long r; - #pragma omp critical (z3_memory_manager) { + std::lock_guard lock(g_memory_mux); r = g_memory_alloc_size; } if (r < 0) @@ -174,8 +171,8 @@ unsigned long long memory::get_allocation_size() { unsigned long long memory::get_max_used_memory() { unsigned long long r; - #pragma omp critical (z3_memory_manager) { + std::lock_guard lock(g_memory_mux); r = g_memory_max_used_size; } return r; @@ -258,8 +255,8 @@ static void synchronize_counters(bool allocating) { bool out_of_mem = false; bool counts_exceeded = false; - #pragma omp critical (z3_memory_manager) { + std::lock_guard lock(g_memory_mux); g_memory_alloc_size += g_memory_thread_alloc_size; g_memory_alloc_count += g_memory_thread_alloc_count; if (g_memory_alloc_size > g_memory_max_used_size) @@ -339,8 +336,8 @@ void memory::deallocate(void * p) { size_t * sz_p = reinterpret_cast(p) - 1; size_t sz = *sz_p; void * real_p = reinterpret_cast(sz_p); - #pragma omp critical (z3_memory_manager) { + std::lock_guard lock(g_memory_mux); g_memory_alloc_size -= sz; } free(real_p); @@ -349,8 +346,8 @@ void memory::deallocate(void * p) { void * memory::allocate(size_t s) { s = s + sizeof(size_t); // we allocate an extra field! bool out_of_mem = false, counts_exceeded = false; - #pragma omp critical (z3_memory_manager) { + std::lock_guard lock(g_memory_mux); g_memory_alloc_size += s; g_memory_alloc_count += 1; if (g_memory_alloc_size > g_memory_max_used_size) @@ -379,8 +376,8 @@ void* memory::reallocate(void *p, size_t s) { void * real_p = reinterpret_cast(sz_p); s = s + sizeof(size_t); // we allocate an extra field! bool out_of_mem = false, counts_exceeded = false; - #pragma omp critical (z3_memory_manager) { + std::lock_guard lock(g_memory_mux); g_memory_alloc_size += s - sz; g_memory_alloc_count += 1; if (g_memory_alloc_size > g_memory_max_used_size) diff --git a/src/util/mpn.cpp b/src/util/mpn.cpp index 25445bc89..7142fbad1 100644 --- a/src/util/mpn.cpp +++ b/src/util/mpn.cpp @@ -29,11 +29,9 @@ static_assert(sizeof(mpn_double_digit) == 2 * sizeof(mpn_digit), "size alignment const mpn_digit mpn_manager::zero = 0; mpn_manager::mpn_manager() { - omp_init_nest_lock(&m_lock); } mpn_manager::~mpn_manager() { - omp_destroy_nest_lock(&m_lock); } int mpn_manager::compare(mpn_digit const * a, size_t const lnga, diff --git a/src/util/mpn.h b/src/util/mpn.h index bae972b0c..63d3f771c 100644 --- a/src/util/mpn.h +++ b/src/util/mpn.h @@ -20,18 +20,16 @@ Revision History: #define MPN_H_ #include +#include #include "util/util.h" #include "util/buffer.h" -#include "util/z3_omp.h" typedef unsigned int mpn_digit; class mpn_manager { -#ifndef _NO_OMP_ - omp_nest_lock_t m_lock; -#endif -#define MPN_BEGIN_CRITICAL() omp_set_nest_lock(&m_lock); -#define MPN_END_CRITICAL() omp_unset_nest_lock(&m_lock); + std::recursive_mutex m_lock; +#define MPN_BEGIN_CRITICAL() m_lock.lock(); +#define MPN_END_CRITICAL() m_lock.unlock(); public: mpn_manager(); diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp index 1e74c2e9e..73697512d 100644 --- a/src/util/mpz.cpp +++ b/src/util/mpz.cpp @@ -139,8 +139,6 @@ uint64_t u64_gcd(uint64_t u, uint64_t v) { template mpz_manager::mpz_manager(): m_allocator("mpz_manager") { - if (SYNCH) - omp_init_nest_lock(&m_lock); #ifndef _MP_GMP if (sizeof(digit_t) == sizeof(uint64_t)) { // 64-bit machine @@ -197,8 +195,6 @@ mpz_manager::~mpz_manager() { mpz_clear(m_int64_max); mpz_clear(m_int64_min); #endif - if (SYNCH) - omp_destroy_nest_lock(&m_lock); } #ifndef _MP_GMP diff --git a/src/util/mpz.h b/src/util/mpz.h index 0faf13d18..a8916fc64 100644 --- a/src/util/mpz.h +++ b/src/util/mpz.h @@ -20,12 +20,12 @@ Revision History: #define MPZ_H_ #include +#include #include "util/util.h" #include "util/small_object_allocator.h" #include "util/trace.h" #include "util/scoped_numeral.h" #include "util/scoped_numeral_vector.h" -#include "util/z3_omp.h" #include "util/mpn.h" unsigned u_gcd(unsigned u, unsigned v); @@ -135,9 +135,9 @@ inline void swap(mpz & m1, mpz & m2) { m1.swap(m2); } template class mpz_manager { mutable small_object_allocator m_allocator; - mutable omp_nest_lock_t m_lock; -#define MPZ_BEGIN_CRITICAL() if (SYNCH) omp_set_nest_lock(&m_lock); -#define MPZ_END_CRITICAL() if (SYNCH) omp_unset_nest_lock(&m_lock); + mutable std::recursive_mutex m_lock; +#define MPZ_BEGIN_CRITICAL() if (SYNCH) m_lock.lock(); +#define MPZ_END_CRITICAL() if (SYNCH) m_lock.unlock(); mutable mpn_manager m_mpn_manager; #ifndef _MP_GMP @@ -702,11 +702,7 @@ public: bool decompose(mpz const & n, svector & digits); }; -#ifndef _NO_OMP_ typedef mpz_manager synch_mpz_manager; -#else -typedef mpz_manager synch_mpz_manager; -#endif typedef mpz_manager unsynch_mpz_manager; typedef _scoped_numeral scoped_mpz; diff --git a/src/util/prime_generator.cpp b/src/util/prime_generator.cpp index 9d3936edf..6e17cddb7 100644 --- a/src/util/prime_generator.cpp +++ b/src/util/prime_generator.cpp @@ -17,6 +17,7 @@ Notes: --*/ #include "util/prime_generator.h" +#include #define PRIME_LIST_MAX_SIZE 1<<20 @@ -109,6 +110,8 @@ prime_iterator::prime_iterator(prime_generator * g):m_idx(0) { } } +static std::mutex g_prime_iterator; + uint64_t prime_iterator::next() { unsigned idx = m_idx; m_idx++; @@ -117,7 +120,7 @@ uint64_t prime_iterator::next() { } else { uint64_t r; - #pragma omp critical (prime_iterator) + std::lock_guard lock(g_prime_iterator); { r = (*m_generator)(idx); } diff --git a/src/util/rational.cpp b/src/util/rational.cpp index e8c2d52d1..3acb40422 100644 --- a/src/util/rational.cpp +++ b/src/util/rational.cpp @@ -17,6 +17,7 @@ Revision History: --*/ #include +#include #include "util/util.h" #include "util/rational.h" #ifdef _WINDOWS @@ -42,9 +43,11 @@ static void mk_power_up_to(vector & pws, unsigned n) { } } +static std::mutex g_powers_of_two; + rational rational::power_of_two(unsigned k) { rational result; - #pragma omp critical (powers_of_two) + std::lock_guard lock(g_powers_of_two); { if (k >= m_powers_of_two.size()) mk_power_up_to(m_powers_of_two, k+1); diff --git a/src/util/rlimit.cpp b/src/util/rlimit.cpp index e3afd0d92..52816316b 100644 --- a/src/util/rlimit.cpp +++ b/src/util/rlimit.cpp @@ -18,6 +18,10 @@ Revision History: --*/ #include "util/rlimit.h" #include "util/common_msgs.h" +#include + +static std::mutex g_reslimit_cancel; + reslimit::reslimit(): m_cancel(0), @@ -69,48 +73,36 @@ char const* reslimit::get_cancel_msg() const { } void reslimit::push_child(reslimit* r) { - #pragma omp critical (reslimit_cancel) - { - m_children.push_back(r); - } + std::lock_guard lock(g_reslimit_cancel); + m_children.push_back(r); } void reslimit::pop_child() { - #pragma omp critical (reslimit_cancel) - { - m_children.pop_back(); - } + std::lock_guard lock(g_reslimit_cancel); + m_children.pop_back(); } void reslimit::cancel() { - #pragma omp critical (reslimit_cancel) - { - set_cancel(m_cancel+1); - } + std::lock_guard lock(g_reslimit_cancel); + set_cancel(m_cancel+1); } void reslimit::reset_cancel() { - #pragma omp critical (reslimit_cancel) - { - set_cancel(0); - } + std::lock_guard lock(g_reslimit_cancel); + set_cancel(0); } void reslimit::inc_cancel() { - #pragma omp critical (reslimit_cancel) - { - set_cancel(m_cancel+1); - } + std::lock_guard lock(g_reslimit_cancel); + set_cancel(m_cancel+1); } void reslimit::dec_cancel() { - #pragma omp critical (reslimit_cancel) - { - if (m_cancel > 0) { - set_cancel(m_cancel-1); - } + std::lock_guard lock(g_reslimit_cancel); + if (m_cancel > 0) { + set_cancel(m_cancel-1); } } diff --git a/src/util/symbol.cpp b/src/util/symbol.cpp index 3f0e7c967..418f96569 100644 --- a/src/util/symbol.cpp +++ b/src/util/symbol.cpp @@ -20,8 +20,10 @@ Revision History: #include "util/str_hashtable.h" #include "util/region.h" #include "util/string_buffer.h" -#include "util/z3_omp.h" #include +#include + +static std::mutex g_symbol_lock; symbol symbol::m_dummy(TAG(void*, nullptr, 2)); const symbol symbol::null; @@ -36,8 +38,7 @@ public: char const * get_str(char const * d) { const char * result; - #pragma omp critical (cr_symbol) - { + std::lock_guard lock(g_symbol_lock); str_hashtable::entry * e; if (m_table.insert_if_not_there_core(d, e)) { // new entry @@ -55,7 +56,6 @@ public: result = e->get_data(); } SASSERT(m_table.contains(result)); - } return result; } }; diff --git a/src/util/util.cpp b/src/util/util.cpp index 4fb361475..4b5489dc2 100644 --- a/src/util/util.cpp +++ b/src/util/util.cpp @@ -23,6 +23,10 @@ Revision History: #include #include "util/util.h" +static std::mutex g_verbose_mux; +void verbose_lock() { g_verbose_mux.lock(); } +void verbose_unlock() { g_verbose_mux.unlock(); } + static unsigned g_verbosity_level = 0; void set_verbosity_level(unsigned lvl) { diff --git a/src/util/util.h b/src/util/util.h index 9bc4f8a41..39ca45701 100644 --- a/src/util/util.h +++ b/src/util/util.h @@ -21,10 +21,10 @@ Revision History: #include "util/debug.h" #include "util/memory_manager.h" -#include "util/z3_omp.h" #include #include #include +#include #include #ifndef SIZE_MAX @@ -174,11 +174,8 @@ void set_verbosity_level(unsigned lvl); unsigned get_verbosity_level(); std::ostream& verbose_stream(); void set_verbose_stream(std::ostream& str); -#ifdef _NO_OMP_ -# define is_threaded() false -#else bool is_threaded(); -#endif + #define IF_VERBOSE(LVL, CODE) { \ @@ -191,25 +188,16 @@ bool is_threaded(); } \ } } ((void) 0) -#ifdef _MSC_VER -#define DO_PRAGMA(x) __pragma(x) -#define PRAGMA_LOCK __pragma(omp critical (verbose_lock)) -#else -#define DO_PRAGMA(x) _Pragma(#x) -#define PRAGMA_LOCK _Pragma("omp critical (verbose_lock)") -#endif -#ifdef _NO_OMP_ -#define LOCK_CODE(CODE) CODE; -#else -#define LOCK_CODE(CODE) \ - { \ - PRAGMA_LOCK \ - { \ - CODE; \ - } \ - } -#endif +void verbose_lock(); +void verbose_unlock(); + +#define LOCK_CODE(CODE) \ + { \ + verbose_lock(); \ + CODE; \ + verbose_unlock(); \ + } \ template struct default_eq { diff --git a/src/util/z3_omp.h b/src/util/z3_omp.h deleted file mode 100644 index 6c618192e..000000000 --- a/src/util/z3_omp.h +++ /dev/null @@ -1,38 +0,0 @@ -/*++ -Copyright (c) 2012 Microsoft Corporation - -Module Name: - - z3_omp.h - -Abstract: - - Wrapper for OMP functions and data-structures - -Author: - - Leonardo (leonardo) 2012-01-05 - -Notes: - ---*/ -#ifndef Z3_OMP_H_ -#define Z3_OMP_H_ - -#ifndef _NO_OMP_ -#include -#else -#define omp_in_parallel() false -#define omp_set_num_threads(SZ) ((void)0) -#define omp_get_thread_num() 0 -#define omp_get_num_procs() 1 -#define omp_set_nested(V) ((void)0) -#define omp_init_nest_lock(L) ((void) 0) -#define omp_destroy_nest_lock(L) ((void) 0) -#define omp_set_nest_lock(L) ((void) 0) -#define omp_unset_nest_lock(L) ((void) 0) -struct omp_nest_lock_t { -}; -#endif - -#endif