3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00

add initialization

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-06-11 19:28:08 -07:00
parent 583098b8b0
commit 71c38a08e5
13 changed files with 92 additions and 43 deletions

View file

@ -16,8 +16,9 @@ Author:
#include "util/rlimit.h"
#include "util/gparams.h"
#include <signal.h>
#include <mutex>
static std::mutex display_stats_mux;
extern std::mutex* g_stat_mux;
static lp::lp_solver<double, double>* 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<std::mutex> lock(display_stats_mux);
std::lock_guard<std::mutex> lock(*g_stat_mux);
display_statistics();
}
raise(SIGINT);
}
static void on_timeout() {
std::lock_guard<std::mutex> lock(display_stats_mux);
std::lock_guard<std::mutex> lock(*g_stat_mux);
display_statistics();
exit(0);
}

View file

@ -18,6 +18,7 @@ Revision History:
--*/
#include<iostream>
#include<mutex>
#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();

View file

@ -7,6 +7,7 @@ Copyright (c) 2015 Microsoft Corporation
#include<fstream>
#include<signal.h>
#include<time.h>
#include<mutex>
#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<std::mutex> lock(display_stats_mux);
std::lock_guard<std::mutex> 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<std::mutex> lock(display_stats_mux);
std::lock_guard<std::mutex> 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<std::mutex> lock(display_stats_mux);
std::lock_guard<std::mutex> lock(*g_stat_mux);
display_statistics();
register_on_timeout_proc(nullptr);
g_opt = nullptr;

View file

@ -21,6 +21,8 @@ Revision History:
#include<iostream>
#include<time.h>
#include<signal.h>
#include<mutex>
#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<std::mutex> lock(display_stats_mux);
std::lock_guard<std::mutex> 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<std::mutex> lock(display_stats_mux);
std::lock_guard<std::mutex> lock(*g_stat_mux);
display_statistics();
}
raise(SIGINT);
@ -99,7 +100,7 @@ unsigned read_smtlib2_commands(char const * file_name) {
{
std::lock_guard<std::mutex> lock(display_stats_mux);
std::lock_guard<std::mutex> lock(*g_stat_mux);
display_statistics();
g_cmd_context = nullptr;
}

View file

@ -26,7 +26,15 @@ Notes:
#include <mutex>
#include <thread>
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<std::thread::id> 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;
}

View file

@ -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

View file

@ -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;
}

View file

@ -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);
}

View file

@ -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<uint64_t> m_primes;
void process_next_k_numbers(uint64_t k);
public:
mutex *m_mux;
prime_generator();
uint64_t operator()(unsigned idx);
void finalize();

View file

@ -26,6 +26,7 @@ rational rational::m_zero;
rational rational::m_one;
rational rational::m_minus_one;
vector<rational> rational::m_powers_of_two;
static mutex* s_mux = nullptr;
static void mk_power_up_to(vector<rational> & pws, unsigned n) {
if (pws.empty()) {
@ -40,11 +41,10 @@ static void mk_power_up_to(vector<rational> & 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;
}

View file

@ -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);
}

View file

@ -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;

View file

@ -23,7 +23,7 @@ Revision History:
#include "util/string_buffer.h"
#include <cstring>
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) {