3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
The idea is to set _concurrent_dec_ref from the API
(function not yet provided externally, but you can experiment with it by setting the default of m_concurrent_dec_ref to true).
It then provides concurrency support for dec_ref operations.
This commit is contained in:
Nikolaj Bjorner 2022-07-15 03:53:15 -07:00
parent b29cdca936
commit 6688c1d62a
3 changed files with 57 additions and 8 deletions

View file

@ -35,11 +35,12 @@ namespace api {
object::object(context& c): m_ref_count(0), m_context(c) { this->m_id = m_context.add_object(this); }
void object::inc_ref() { m_ref_count++; }
void object::inc_ref() { ++m_ref_count; }
void object::dec_ref() { SASSERT(m_ref_count > 0); m_ref_count--; if (m_ref_count == 0) m_context.del_object(this); }
void object::dec_ref() { SASSERT(m_ref_count > 0); if (--m_ref_count == 0) m_context.del_object(this); }
unsigned context::add_object(api::object* o) {
flush_objects();
unsigned id = m_allocated_objects.size();
if (!m_free_object_ids.empty()) {
id = m_free_object_ids.back();
@ -50,9 +51,48 @@ namespace api {
}
void context::del_object(api::object* o) {
m_free_object_ids.push_back(o->id());
m_allocated_objects.remove(o->id());
dealloc(o);
if (m_concurrent_dec_ref) {
lock_guard lock(m_mux);
m_objects_to_flush.push_back(o);
}
else {
m_free_object_ids.push_back(o->id());
m_allocated_objects.remove(o->id());
dealloc(o);
}
}
void context::dec_ref(ast* a) {
if (m_concurrent_dec_ref) {
lock_guard lock(m_mux);
m_asts_to_flush.push_back(a);
}
else
m().dec_ref(a);
}
void context::flush_objects() {
if (!m_concurrent_dec_ref)
return;
{
lock_guard lock(m_mux);
if (m_asts_to_flush.empty() && m_objects_to_flush.empty())
return;
m_asts_to_flush2.append(m_asts_to_flush);
m_asts_to_flush.reset();
m_objects_to_flush2.append(m_objects_to_flush);
m_objects_to_flush.reset();
}
for (ast* a : m_asts_to_flush2)
m().dec_ref(a);
for (auto* o : m_objects_to_flush2) {
m_free_object_ids.push_back(o->id());
m_allocated_objects.remove(o->id());
dealloc(o);
}
m_objects_to_flush2.reset();
m_asts_to_flush2.reset();
}
static void default_error_handler(Z3_context ctx, Z3_error_code c) {
@ -106,6 +146,7 @@ namespace api {
context::~context() {
m_last_obj = nullptr;
flush_objects();
for (auto& kv : m_allocated_objects) {
api::object* val = kv.m_value;
DEBUG_CODE(warning_msg("Uncollected memory: %d: %s", kv.m_key, typeid(*val).name()););
@ -365,6 +406,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_inc_ref(c, a);
RESET_ERROR_CODE();
mk_c(c)->flush_objects();
mk_c(c)->m().inc_ref(to_ast(a));
Z3_CATCH;
}
@ -379,7 +421,7 @@ extern "C" {
return;
}
if (a) {
mk_c(c)->m().dec_ref(to_ast(a));
mk_c(c)->dec_ref(to_ast(a));
}
Z3_CATCH;
}

View file

@ -91,8 +91,11 @@ namespace api {
smt_params m_fparams;
// -------------------------------
ast_ref_vector m_ast_trail;
bool m_concurrent_dec_ref = false;
ptr_vector<ast> m_asts_to_flush, m_asts_to_flush2;
ptr_vector<api::object> m_objects_to_flush, m_objects_to_flush2;
ast_ref_vector m_ast_trail;
ref<api::object> m_last_obj; //!< reference to the last API object returned by the APIs
u_map<api::object*> m_allocated_objects; // !< table containing current set of allocated API objects
unsigned_vector m_free_object_ids; // !< free list of identifiers available for allocated objects.
@ -170,8 +173,11 @@ namespace api {
void set_error_code(Z3_error_code err, std::string &&opt_msg);
void set_error_handler(Z3_error_handler h) { m_error_handler = h; }
void set_concurrent_dec_ref() { m_concurrent_dec_ref = true; }
unsigned add_object(api::object* o);
void del_object(api::object* o);
void dec_ref(ast* a);
void flush_objects();
Z3_ast_print_mode get_print_mode() const { return m_print_mode; }
void set_print_mode(Z3_ast_print_mode m) { m_print_mode = m; }

View file

@ -20,6 +20,7 @@ Revision History:
#include "util/params.h"
#include "util/lbool.h"
#include "ast/ast.h"
#include <atomic>
#define Z3_TRY try {
#define Z3_CATCH_CORE(CODE) } catch (z3_exception & ex) { mk_c(c)->handle_exception(ex); CODE }
@ -34,7 +35,7 @@ namespace api {
// Generic wrapper for ref-count objects exposed by the API
class object {
unsigned m_ref_count;
atomic<unsigned> m_ref_count;
unsigned m_id;
context& m_context;
public: