max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: cleanup

Browse source
This commit is contained in:
Leonardo de Moura 2021-07-19 19:28:27 -07:00
parent 974caa97e6
commit da66610fda
3 changed files with 20 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/include/lean/lean.h
View file

@ -402,21 +402,15 @@ static inline void lean_inc_ref_n(lean_object * o, size_t n) {
}
}
bool lean_dec_ref_core_cold(lean_object * o);
void lean_dec_ref_cold(lean_object * o);
static inline bool lean_dec_ref_core(lean_object * o) {
static inline void lean_dec_ref(lean_object * o) {
if (LEAN_LIKELY(o->m_rc > 1)) {
o->m_rc--;
return false;
} else {
return lean_dec_ref_core_cold(o);
lean_dec_ref_cold(o);
}
}
/* Generic Lean object delete operation. */
void lean_del(lean_object * o);
static inline void lean_dec_ref(lean_object * o) { if (lean_dec_ref_core(o)) lean_del(o); }
static inline void lean_inc(lean_object * o) { if (!lean_is_scalar(o)) lean_inc_ref(o); }
static inline void lean_inc_n(lean_object * o, size_t n) { if (!lean_is_scalar(o)) lean_inc_ref_n(o, n); }
static inline void lean_dec(lean_object * o) { if (!lean_is_scalar(o)) lean_dec_ref(o); }

1
src/include/lean/object.h
View file

@ -50,7 +50,6 @@ inline bool is_shared(object * o) { return lean_is_shared(o); }
inline bool is_exclusive(object * o) { return lean_is_exclusive(o); }
inline void inc_ref(object * o) { lean_inc_ref(o); }
inline void inc_ref(object * o, size_t n) { lean_inc_ref_n(o, n); }
inline bool dec_ref_core(object * o) { return lean_dec_ref_core(o); }
inline void dec_ref(object * o) { lean_dec_ref(o); }
inline void inc(object * o) { lean_inc(o); }
inline void inc(object * o, size_t n) { lean_inc_n(o, n); }

22
src/runtime/object.cpp
View file

@ -81,10 +81,15 @@ extern "C" void lean_inc_ref_n_cold(lean_object * o, unsigned n) {
atomic_fetch_sub_explicit(lean_get_rc_mt_addr(o), n, memory_order_relaxed);
}
extern "C" bool lean_dec_ref_core_cold(lean_object * o) {
if (o->m_rc == 1) return true;
if (o->m_rc == 0) return false;
return atomic_fetch_add_explicit(lean_get_rc_mt_addr(o), 1, memory_order_acq_rel) == -1;
static inline bool lean_dec_ref_core(lean_object * o) {
if (LEAN_LIKELY(o->m_rc >= 1)) {
o->m_rc--;
return o->m_rc == 0;
} else if (o->m_rc == 0) {
return false;
} else {
return atomic_fetch_add_explicit(lean_get_rc_mt_addr(o), 1, memory_order_acq_rel) == -1;
}
}
extern "C" size_t lean_object_byte_size(lean_object * o) {
@ -247,7 +252,7 @@ static void lean_del_core(object * o, object * & todo) {
}
}
extern "C" void lean_del(object * o) {
static inline void lean_del(object * o) {
#ifdef LEAN_LAZY_RC
push_back(g_to_free, o);
#else
@ -261,6 +266,13 @@ extern "C" void lean_del(object * o) {
#endif
}
extern "C" void lean_dec_ref_cold(lean_object * o) {
if (o->m_rc == 1) lean_del(o);
else if (o->m_rc == 0) return;
else if (atomic_fetch_add_explicit(lean_get_rc_mt_addr(o), 1, memory_order_acq_rel) == -1) lean_del(o);
}
// =======================================
// Closures