Skip to content

perf: outline lean_dec_ref_cold deletion case #11829

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
Kha wants to merge 2 commits into from
+25 −24
Closed

perf: outline lean_dec_ref_cold deletion case #11829

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
c23e64d
perf: outline `lean_dec_ref_cold` deletion case
Kha Dec 24, 2025
9f323e1
perf: outline `lean_dec_ref`
Kha Dec 29, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
15 changes: 7 additions & 8 deletions src/include/lean/lean.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -58,6 +58,12 @@ extern "C" {
#define LEAN_ALWAYS_INLINE
#endif

#if defined(__GNUC__) || defined(__clang__)
#define LEAN_NOINLINE __attribute__((noinline))
#else
#define LEAN_NOINLINE
#endif

#ifndef assert
#ifdef NDEBUG
#define assert(expr)
Expand Down Expand Up @@ -500,15 +506,8 @@ static inline void lean_inc_ref(lean_object * o) {
lean_inc_ref_n(o, 1);
}

LEAN_EXPORT void lean_dec_ref_cold(lean_object * o);
__attribute__((preserve_most)) LEAN_EXPORT void lean_dec_ref(lean_object * o);

static inline LEAN_ALWAYS_INLINE void lean_dec_ref(lean_object * o) {
if (LEAN_LIKELY(o->m_rc > 1)) {
o->m_rc--;
} else if (o->m_rc != 0) {
lean_dec_ref_cold(o);
}
}
static inline void LEAN_ALWAYS_INLINE 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_ALWAYS_INLINE lean_dec(lean_object * o) { if (!lean_is_scalar(o)) lean_dec_ref(o); }
Expand Down
6 changes: 0 additions & 6 deletions src/runtime/alloc.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,12 +16,6 @@ Author: Leonardo de Moura
#define LEAN_RUNTIME_STAT_CODE(c)
#endif

#if defined(__GNUC__) || defined(__clang__)
#define LEAN_NOINLINE __attribute__((noinline))
#else
#define LEAN_NOINLINE
#endif

#define LEAN_PAGE_SIZE 8192 // 8 Kb
#define LEAN_SEGMENT_SIZE 8*1024*1024 // 8 Mb
#define LEAN_NUM_SLOTS (LEAN_MAX_SMALL_OBJECT_SIZE / LEAN_OBJECT_SIZE_DELTA)
Expand Down
28 changes: 18 additions & 10 deletions src/runtime/object.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -391,19 +391,27 @@ static void lean_del_core(object * o, object * & todo) {
}
}

extern "C" LEAN_EXPORT void lean_dec_ref_cold(lean_object * o) {
if (o->m_rc == 1 || std::atomic_fetch_add_explicit(lean_get_rc_mt_addr(o), 1, std::memory_order_acq_rel) == -1) {
__attribute__((preserve_most)) void LEAN_NOINLINE lean_dec_ref_cold_cold(lean_object * o) {
#ifdef LEAN_LAZY_RC
push_back(g_to_free, o);
push_back(g_to_free, o);
#else
object * todo = nullptr;
while (true) {
lean_del_core(o, todo);
if (todo == nullptr)
return;
o = pop_back(todo);
}
object * todo = nullptr;
while (true) {
lean_del_core(o, todo);
if (todo == nullptr)
return;
o = pop_back(todo);
}
#endif
}

extern "C" LEAN_EXPORT void lean_dec_ref(lean_object * o) {
if (LEAN_LIKELY(o->m_rc > 1)) {
o->m_rc--;
} else if (o->m_rc != 0) {
if (o->m_rc == 1 || std::atomic_fetch_add_explicit(lean_get_rc_mt_addr(o), 1, std::memory_order_acq_rel) == -1) {
lean_dec_ref_cold_cold(o);
}
}
}

Expand Down
Loading