From c23e64d8c7ae361e4a07311c2e0137c572bdbb08 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 24 Dec 2025 11:55:32 +0000 Subject: [PATCH 1/2] perf: outline `lean_dec_ref_cold` deletion case --- src/include/lean/lean.h | 6 ++++++ src/runtime/alloc.cpp | 6 ------ src/runtime/object.cpp | 24 ++++++++++++++---------- 3 files changed, 20 insertions(+), 16 deletions(-) diff --git a/src/include/lean/lean.h b/src/include/lean/lean.h index 10085909729c..b0008665d5e9 100644 --- a/src/include/lean/lean.h +++ b/src/include/lean/lean.h @@ -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) diff --git a/src/runtime/alloc.cpp b/src/runtime/alloc.cpp index d35dafefdc0f..c6774165f52e 100644 --- a/src/runtime/alloc.cpp +++ b/src/runtime/alloc.cpp @@ -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) diff --git a/src/runtime/object.cpp b/src/runtime/object.cpp index c03af87615e2..2c3d7973e8a1 100644 --- a/src/runtime/object.cpp +++ b/src/runtime/object.cpp @@ -391,19 +391,23 @@ 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) { +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_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) { + lean_dec_ref_cold_cold(o); } } From 9f323e1a3f26fad8f562c4c4861c8b3e09fbb754 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Mon, 29 Dec 2025 12:35:26 +0000 Subject: [PATCH 2/2] perf: outline `lean_dec_ref` --- src/include/lean/lean.h | 9 +-------- src/runtime/object.cpp | 12 ++++++++---- 2 files changed, 9 insertions(+), 12 deletions(-) diff --git a/src/include/lean/lean.h b/src/include/lean/lean.h index b0008665d5e9..ffaf0e927f65 100644 --- a/src/include/lean/lean.h +++ b/src/include/lean/lean.h @@ -506,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); } diff --git a/src/runtime/object.cpp b/src/runtime/object.cpp index 2c3d7973e8a1..a04419cbc7f1 100644 --- a/src/runtime/object.cpp +++ b/src/runtime/object.cpp @@ -391,7 +391,7 @@ static void lean_del_core(object * o, object * & todo) { } } -void LEAN_NOINLINE lean_dec_ref_cold_cold(lean_object * o) { +__attribute__((preserve_most)) void LEAN_NOINLINE lean_dec_ref_cold_cold(lean_object * o) { #ifdef LEAN_LAZY_RC push_back(g_to_free, o); #else @@ -405,9 +405,13 @@ void LEAN_NOINLINE lean_dec_ref_cold_cold(lean_object * o) { #endif } -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) { - lean_dec_ref_cold_cold(o); +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); + } } }