chore: update stage0

src/CMakeLists.txt

@@ -35,9 +35,6 @@ option(STATIC             "STATIC"             OFF)
 option(SPLIT_STACK        "SPLIT_STACK"        OFF)
 # When OFF we disable LLVM support
 option(LLVM               "LLVM"               OFF)
-option(COMPRESSED_OBJECT_HEADER "Use compressed object headers in 64-bit machines, this option is ignored in 32-bit machines, and assumes the 64-bit OS can only address 2^48 bytes" ON)
-option(SMALL_RC "Use only 32-bits for RC, this option is only relevant when COMPRESSED_OBJECT_HEARDER is ON" ON)
-option(CHECK_RC_OVERFLOW "Check for RC overflows when SMALL_RC is ON" OFF)
 
 # Include MSYS2 required DLLs and binaries in the binary distribution package
 option(INCLUDE_MSYS2_DLLS "INCLUDE_MSYS2_DLLS" OFF)
@@ -91,26 +88,6 @@ else()
   set(NumBits 32)
 endif()
 
-if ("${COMPRESSED_OBJECT_HEADER}" MATCHES "ON")
-  if (NumBits EQUAL "64")
-    if ("${SMALL_RC}" MATCHES "ON")
-        set(LEAN_COMPRESSED_OBJECT_HEADER_SMALL_RC "#define LEAN_COMPRESSED_OBJECT_HEADER_SMALL_RC")
-        message(STATUS "Using compressed object headers and only 32-bits for reference counter, this feature assume the OS only uses memory addresses < 2^48")
-        if ("${CHECK_RC_OVERFLOW}" MATCHES "ON")
-           set(LEAN_CHECK_RC_OVERFLOW "#define LEAN_CHECK_RC_OVERFLOW")
-           message(STATUS "RC overflow checks are enabled")
-        endif()
-    else()
-        set(LEAN_COMPRESSED_OBJECT_HEADER "#define LEAN_COMPRESSED_OBJECT_HEADER")
-        message(STATUS "Using compressed object headers, this feature assume the OS only uses memory addresses < 2^48")
-    endif()
-  else()
-    message(STATUS "Compressed object headers cannot be used in 32-bit machines")
-  endif()
-else()
-    message(STATUS "Using big object headers")
-endif()
-
 if ("${RUNTIME_STATS}" MATCHES "ON")
   set(LEAN_EXTRA_CXX_FLAGS "${LEAN_EXTRA_CXX_FLAGS} -D LEAN_RUNTIME_STATS")
   set(LEANC_EXTRA_FLAGS "${LEANC_EXTRA_FLAGS} -D LEAN_RUNTIME_STATS")

src/config.h.in

@@ -9,7 +9,4 @@ Author: Leonardo de Moura
 
 @LEAN_SMALL_ALLOCATOR@
 @LEAN_LAZY_RC@
-@LEAN_COMPRESSED_OBJECT_HEADER@
-@LEAN_COMPRESSED_OBJECT_HEADER_SMALL_RC@
-@LEAN_CHECK_RC_OVERFLOW@
 @LEAN_IS_STAGE0@

src/include/lean/lean.h

@@ -82,53 +82,33 @@ static inline bool lean_is_big_object_tag(uint8_t tag) {
 
 LEAN_CASSERT(sizeof(size_t) == sizeof(void*));
 
-#if defined(LEAN_COMPRESSED_OBJECT_HEADER) || defined(LEAN_COMPRESSED_OBJECT_HEADER_SMALL_RC)
-/* Compressed headers are only supported in 64-bit machines */
-LEAN_CASSERT(sizeof(void*) == 8);
-#endif
+/*
+Lean object header.
 
-/* Lean object header */
+The reference counter `m_rc` field also encodes whether the object is single threaded (> 0), multi threaded (< 0), or
+reference counting is not needed (== 0). We don't use reference counting for objects stored in compact regions, or
+marked as persistent.
+
+For "small" objects stored in compact regions, the field `m_cs_sz` contains the object size. For "small" objects not
+stored in compact regions, we use the page information to retrieve its size.
+
+During deallocation and 64-bit machines, the fields `m_rc` and `m_cs_sz` store the next object in the deletion TODO list.
+These two fields together have 48-bits, and this is enough for modern computers.
+In 32-bit machines, the field `m_rc` is sufficient.
+
+The field `m_other` is used to store the number of fields in a constructor object and the element size in a scalar array.
+*/
 typedef struct {
-#if defined(LEAN_COMPRESSED_OBJECT_HEADER)
-    /* (high) 8-bits  : tag
-              8-bits  : num fields for constructors, element size for scalar arrays
-              1-bit   : single-threaded
-              1-bit   : multi-threaded
-              1-bit   : persistent
-       (low)  45-bits : RC */
-    size_t          m_header;
-#define LEAN_RC_NBITS 45
-#define LEAN_PERSISTENT_BIT 45
-#define LEAN_MT_BIT 46
-#define LEAN_ST_BIT 47
-#elif defined(LEAN_COMPRESSED_OBJECT_HEADER_SMALL_RC)
-    /* (high) 8-bits  : tag
-              8-bits  : num fields for constructors, element size for scalar arrays
-              8-bits  : memory kind
-              8-bits  : <unused>
-       (low)  32-bits : RC */
-    size_t          m_header;
-#define LEAN_RC_NBITS 32
-#define LEAN_ST_MEM_KIND 0
-#define LEAN_MT_MEM_KIND 1
-#define LEAN_PERSISTENT_MEM_KIND 2
-#define LEAN_OTHER_MEM_KIND 3
-#else
-    size_t          m_rc;
-    uint8_t         m_tag;
-    uint8_t         m_mem_kind;
-    uint16_t        m_other;  /* num fields for constructors, element size for scalar arrays, etc. */
-#define LEAN_ST_MEM_KIND 0
-#define LEAN_MT_MEM_KIND 1
-#define LEAN_PERSISTENT_MEM_KIND 2
-#define LEAN_OTHER_MEM_KIND 3
-#endif
+    int      m_rc;
+    unsigned m_cs_sz:16;
+    unsigned m_other:8;
+    unsigned m_tag:8;
 } lean_object;
 
 /*
 In our runtime, a Lean function consume the reference counter (RC) of its argument or not.
 We say this behavior is part of the "calling convention" for the function. We say an argument uses:
-
+x
 1- "standard" calling convention if it consumes/decrements the RC.
    In this calling convention each argument should be viewed as a resource that is consumed by the function.
    This is roughly equivalent to `S && a` in C++, where `S` is a smart pointer, and `a` is the argument.
@@ -378,19 +358,11 @@ lean_object * lean_alloc_object(size_t sz);
 void lean_free_object(lean_object * o);
 
 static inline uint8_t lean_ptr_tag(lean_object * o) {
-#if defined(LEAN_COMPRESSED_OBJECT_HEADER) || defined(LEAN_COMPRESSED_OBJECT_HEADER_SMALL_RC)
-    return LEAN_BYTE(o->m_header, 7);
-#else
     return o->m_tag;
-#endif
 }
 
 static inline unsigned lean_ptr_other(lean_object * o) {
-#if defined(LEAN_COMPRESSED_OBJECT_HEADER) || defined(LEAN_COMPRESSED_OBJECT_HEADER_SMALL_RC)
-    return LEAN_BYTE(o->m_header, 6);
-#else
     return o->m_other;
-#endif
 }
 
 /* The object size may be slightly bigger for constructor objects.
@@ -401,151 +373,54 @@ static inline unsigned lean_ptr_other(lean_object * o) {
 size_t lean_object_byte_size(lean_object * o);
 
 static inline bool lean_is_mt(lean_object * o) {
-#if defined(LEAN_COMPRESSED_OBJECT_HEADER)
-    return ((o->m_header >> LEAN_MT_BIT) & 1) != 0;
-#elif defined(LEAN_COMPRESSED_OBJECT_HEADER_SMALL_RC)
-    return LEAN_BYTE(o->m_header, 5) == LEAN_MT_MEM_KIND;
-#else
-    return o->m_mem_kind == LEAN_MT_MEM_KIND;
-#endif
+    return o->m_rc < 0;
 }
 
 static inline bool lean_is_st(lean_object * o) {
-#if defined(LEAN_COMPRESSED_OBJECT_HEADER)
-    return ((o->m_header >> LEAN_ST_BIT) & 1) != 0;
-#elif defined(LEAN_COMPRESSED_OBJECT_HEADER_SMALL_RC)
-    return LEAN_BYTE(o->m_header, 5) == LEAN_ST_MEM_KIND;
-#else
-    return o->m_mem_kind == LEAN_ST_MEM_KIND;
-#endif
+    return o->m_rc > 0;
 }
 
+/* We never update the reference counter of objects stored in compact regions and allocated at initialization time. */
 static inline bool lean_is_persistent(lean_object * o) {
-#if defined(LEAN_COMPRESSED_OBJECT_HEADER)
-    return ((o->m_header >> LEAN_PERSISTENT_BIT) & 1) != 0;
-#elif defined(LEAN_COMPRESSED_OBJECT_HEADER_SMALL_RC)
-    return LEAN_BYTE(o->m_header, 5) == LEAN_PERSISTENT_MEM_KIND;
-#else
-    return o->m_mem_kind == LEAN_PERSISTENT_MEM_KIND;
-#endif
+    return o->m_rc == 0;
 }
 
 static inline bool lean_has_rc(lean_object * o) {
-    return lean_is_st(o) || lean_is_mt(o);
+    return o->m_rc != 0;
 }
 
-static inline _Atomic(size_t) * lean_get_rc_mt_addr(lean_object* o) {
-#if defined(LEAN_COMPRESSED_OBJECT_HEADER) || defined(LEAN_COMPRESSED_OBJECT_HEADER_SMALL_RC)
-    return (_Atomic(size_t)*)(&(o->m_header));
-#else
-    return (_Atomic(size_t)*)(&(o->m_rc));
-#endif
+static inline _Atomic(int) * lean_get_rc_mt_addr(lean_object* o) {
+    return (_Atomic(int)*)(&(o->m_rc));
 }
 
+void lean_inc_ref_cold(lean_object * o);
+void lean_inc_ref_n_cold(lean_object * o, unsigned n);
+
 static inline void lean_inc_ref(lean_object * o) {
-#if defined(LEAN_COMPRESSED_OBJECT_HEADER)
-    if (LEAN_LIKELY(lean_is_st(o))) {
-        o->m_header++;
-    } else if (lean_is_mt(o)) {
-        LEAN_USING_STD;
-        atomic_fetch_add_explicit(lean_get_rc_mt_addr(o), (size_t)1, memory_order_relaxed);
-    }
-#elif defined(LEAN_COMPRESSED_OBJECT_HEADER_SMALL_RC)
-    if (LEAN_LIKELY(lean_is_st(o))) {
-        o->m_header++;
-        #ifdef LEAN_CHECK_RC_OVERFLOW
-        if (LEAN_UNLIKELY(((uint32_t)o->m_header) == 0)) {
-            lean_internal_panic_rc_overflow();
-        }
-        #endif
-    } else if (lean_is_mt(o)) {
-        LEAN_USING_STD;
-        #ifdef LEAN_CHECK_RC_OVERFLOW
-        uint32_t old_rc = (uint32_t)
-        #endif
-        atomic_fetch_add_explicit(lean_get_rc_mt_addr(o), (size_t)1, memory_order_relaxed);
-        #ifdef LEAN_CHECK_RC_OVERFLOW
-        if (LEAN_UNLIKELY(old_rc + 1 == 0)) {
-            lean_internal_panic_rc_overflow();
-        }
-        #endif
-    }
-#else
     if (LEAN_LIKELY(lean_is_st(o))) {
         o->m_rc++;
-    } else if (lean_is_mt(o)) {
-        LEAN_USING_STD;
-        atomic_fetch_add_explicit(lean_get_rc_mt_addr(o), (size_t)1, memory_order_relaxed);
+    } else if (o->m_rc != 0) {
+        lean_inc_ref_cold(o);
     }
-#endif
 }
 
 static inline void lean_inc_ref_n(lean_object * o, size_t n) {
-#if defined(LEAN_COMPRESSED_OBJECT_HEADER)
-    if (LEAN_LIKELY(lean_is_st(o))) {
-        o->m_header += n;
-    } else if (lean_is_mt(o)) {
-        LEAN_USING_STD;
-        atomic_fetch_add_explicit(lean_get_rc_mt_addr(o), n, memory_order_relaxed);
-    }
-#elif defined(LEAN_COMPRESSED_OBJECT_HEADER_SMALL_RC)
-    if (LEAN_LIKELY(lean_is_st(o))) {
-        o->m_header += n;
-        #ifdef LEAN_CHECK_RC_OVERFLOW
-        if (LEAN_UNLIKELY(((uint32_t)o->m_header) < n)) {
-            lean_internal_panic_rc_overflow();
-        }
-        #endif
-    } else if (lean_is_mt(o)) {
-        LEAN_USING_STD;
-        #ifdef LEAN_CHECK_RC_OVERFLOW
-        uint32_t old_rc = (uint32_t)
-        #endif
-        atomic_fetch_add_explicit(lean_get_rc_mt_addr(o), n, memory_order_relaxed);
-        #ifdef LEAN_CHECK_RC_OVERFLOW
-        if (LEAN_UNLIKELY(old_rc + n < n)) {
-            lean_internal_panic_rc_overflow();
-        }
-        #endif
-    }
-#else
     if (LEAN_LIKELY(lean_is_st(o))) {
         o->m_rc += n;
-    } else if (lean_is_mt(o)) {
-        LEAN_USING_STD;
-        atomic_fetch_add_explicit(lean_get_rc_mt_addr(o), n, memory_order_relaxed);
+    } else if (o->m_rc != 0) {
+        lean_inc_ref_n_cold(o, n);
     }
-#endif
 }
 
-static inline bool lean_dec_ref_core(lean_object * o) {
-#if defined(LEAN_COMPRESSED_OBJECT_HEADER) || defined(LEAN_COMPRESSED_OBJECT_HEADER_SMALL_RC)
-    if (LEAN_LIKELY(lean_is_st(o))) {
-        o->m_header--;
-        return ((o->m_header) & ((1ull << LEAN_RC_NBITS) - 1)) == 0;
-    } else if (lean_is_mt(o)) {
-        LEAN_USING_STD;
-        return (atomic_fetch_sub_explicit(lean_get_rc_mt_addr(o), (size_t)1, memory_order_acq_rel) & ((1ull << LEAN_RC_NBITS) - 1)) == 1;
-    } else {
-        return false;
-    }
-#else
-    if (LEAN_LIKELY(lean_is_st(o))) {
+void lean_dec_ref_cold(lean_object * o);
+
+static inline void lean_dec_ref(lean_object * o) {
+    if (LEAN_LIKELY(o->m_rc > 1)) {
         o->m_rc--;
-        return o->m_rc == 0;
-    } else if (lean_is_mt(o)) {
-        LEAN_USING_STD;
-        return atomic_fetch_sub_explicit(lean_get_rc_mt_addr(o), (size_t)1, memory_order_acq_rel) == 1;
-    } else {
-        return false;
+    } else if (o->m_rc != 0) {
+        lean_dec_ref_cold(o);
     }
-#endif
 }
-
-/* 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); }
@@ -579,97 +454,41 @@ static inline lean_ref_object * lean_to_ref(lean_object * o) { assert(lean_is_re
 static inline lean_external_object * lean_to_external(lean_object * o) { assert(lean_is_external(o)); return (lean_external_object*)(o); }
 
 static inline bool lean_is_exclusive(lean_object * o) {
-#if defined(LEAN_COMPRESSED_OBJECT_HEADER) || defined(LEAN_COMPRESSED_OBJECT_HEADER_SMALL_RC)
-    if (LEAN_LIKELY(lean_is_st(o))) {
-        return ((o->m_header) & ((1ull << LEAN_RC_NBITS) - 1)) == 1;
-    } else {
-        // In theory, an MT object with RC 1 can also be used for destructive updates as long as
-        // the single reference is reachable only from a single thread (which is the case when
-        // it is on the stack/passed to a primitive, in contrast to stored in another object).
-        // However, we would need to add an additional check to this function (which is inlined)
-        // and also reset the mem kind of `o` to ST, and the object will be iterated over anyway
-        // when we put it back in an MT context. So we focus on the more common ST case instead.
-        return false;
-    }
-#else
     if (LEAN_LIKELY(lean_is_st(o))) {
         return o->m_rc == 1;
     } else {
         return false;
     }
-#endif
 }
 
 static inline bool lean_is_shared(lean_object * o) {
-#if defined(LEAN_COMPRESSED_OBJECT_HEADER) || defined(LEAN_COMPRESSED_OBJECT_HEADER_SMALL_RC)
-    if (LEAN_LIKELY(lean_is_st(o))) {
-        return ((o->m_header) & ((1ull << LEAN_RC_NBITS) - 1)) > 1;
-    } else {
-        return false;
-    }
-#else
     if (LEAN_LIKELY(lean_is_st(o))) {
         return o->m_rc > 1;
     } else {
         return false;
     }
-#endif
-}
-
-static inline bool lean_nonzero_rc(lean_object * o) {
-#if defined(LEAN_COMPRESSED_OBJECT_HEADER) || defined(LEAN_COMPRESSED_OBJECT_HEADER_SMALL_RC)
-    if (LEAN_LIKELY(lean_is_st(o))) {
-        return ((o->m_header) & ((1ull << LEAN_RC_NBITS) - 1)) > 0;
-    } else if (lean_is_mt(o)) {
-        LEAN_USING_STD;
-        return (atomic_load_explicit(lean_get_rc_mt_addr(o), memory_order_acquire) & ((1ull << LEAN_RC_NBITS) - 1)) > 0;
-    } else {
-        return false;
-    }
-#else
-    if (LEAN_LIKELY(lean_is_st(o))) {
-        return o->m_rc > 0;
-    } else if (lean_is_mt(o)) {
-        LEAN_USING_STD;
-        return atomic_load_explicit(lean_get_rc_mt_addr(o), memory_order_acquire) > 0;
-    } else {
-        return false;
-    }
-#endif
 }
 
 void lean_mark_mt(lean_object * o);
 void lean_mark_persistent(lean_object * o);
 
 static inline void lean_set_st_header(lean_object * o, unsigned tag, unsigned other) {
-#if defined(LEAN_COMPRESSED_OBJECT_HEADER)
-    o->m_header   = ((size_t)(tag) << 56) | ((size_t)(other) << 48) | (1ull << LEAN_ST_BIT) | 1;
-#elif defined(LEAN_COMPRESSED_OBJECT_HEADER_SMALL_RC)
-    o->m_header   = ((size_t)(tag) << 56) | ((size_t)(other) << 48) | ((size_t)LEAN_ST_MEM_KIND << 40) | 1;
-#else
     o->m_rc       = 1;
     o->m_tag      = tag;
-    o->m_mem_kind = LEAN_ST_MEM_KIND;
     o->m_other    = other;
-#endif
+    o->m_cs_sz    = 0;
 }
 
 /* Remark: we don't need a reference counter for objects that are not stored in the heap.
    Thus, we use the area to store the object size for small objects. */
 static inline void lean_set_non_heap_header(lean_object * o, size_t sz, unsigned tag, unsigned other) {
     assert(sz > 0);
-    assert(sz < (1ull << 45));
+    assert(sz < (1ull << 16));
     assert(sz == 1 || !lean_is_big_object_tag(tag));
-#if defined(LEAN_COMPRESSED_OBJECT_HEADER)
-    o->m_header   = ((size_t)(tag) << 56) | ((size_t)(other) << 48) | sz;
-#elif defined(LEAN_COMPRESSED_OBJECT_HEADER_SMALL_RC)
-    o->m_header   = ((size_t)(tag) << 56) | ((size_t)(other) << 48) | ((size_t)LEAN_OTHER_MEM_KIND << 40) | sz;
-#else
-    o->m_rc       = sz;
+    o->m_rc       = 0;
     o->m_tag      = tag;
-    o->m_mem_kind = LEAN_OTHER_MEM_KIND;
     o->m_other    = other;
-#endif
+    o->m_cs_sz    = sz;
 }
 
 /* `lean_set_non_heap_header` for (potentially) big objects such as arrays and strings. */
@@ -713,11 +532,7 @@ static inline void lean_ctor_set(b_lean_obj_arg o, unsigned i, lean_obj_arg v) {
 
 static inline void lean_ctor_set_tag(b_lean_obj_arg o, uint8_t new_tag) {
     assert(new_tag <= LeanMaxCtorTag);
-#if defined(LEAN_COMPRESSED_OBJECT_HEADER) || defined(LEAN_COMPRESSED_OBJECT_HEADER_SMALL_RC)
-    LEAN_BYTE(o->m_header, 7) = new_tag;
-#else
     o->m_tag = new_tag;
-#endif
 }
 
 static inline void lean_ctor_release(b_lean_obj_arg o, unsigned i) {

src/include/lean/object.h

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

src/runtime/object.cpp

@@ -69,8 +69,16 @@ extern "C" object * lean_sorry(uint8) {
     lean_unreachable();
 }
 
+extern "C" void lean_inc_ref_cold(lean_object * o) {
+    std::atomic_fetch_sub_explicit(lean_get_rc_mt_addr(o), 1, std::memory_order_relaxed);
+}
+
+extern "C" void lean_inc_ref_n_cold(lean_object * o, unsigned n) {
+    std::atomic_fetch_sub_explicit(lean_get_rc_mt_addr(o), (int)n, std::memory_order_relaxed);
+}
+
 extern "C" size_t lean_object_byte_size(lean_object * o) {
-    if (lean_is_mt(o) || lean_is_st(o) || lean_is_persistent(o)) {
+    if (o->m_cs_sz == 0) {
         /* Recall that multi-threaded, single-threaded and persistent objects are stored in the heap.
            Persistent objects are multi-threaded and/or single-threaded that have been "promoted" to
            a persistent status. */
@@ -86,15 +94,7 @@ extern "C" size_t lean_object_byte_size(lean_object * o) {
         case LeanArray:       return lean_array_byte_size(o);
         case LeanScalarArray: return lean_sarray_byte_size(o);
         case LeanString:      return lean_string_byte_size(o);
-        default:
-            /* For potentially big objects, we cannot store the size in the RC field when `defined(LEAN_COMPRESSED_OBJECT_HEADER_SMALL_RC)`.
-               In this case, the RC is 32-bits, and it is not enough for big arrays/strings.
-               Thus, we compute them using the respective *_byte_size operations. */
-#if defined(LEAN_COMPRESSED_OBJECT_HEADER) || defined(LEAN_COMPRESSED_OBJECT_HEADER_SMALL_RC)
-            return o->m_header & ((1ull << LEAN_RC_NBITS) - 1);
-#else
-            return o->m_rc;
-#endif
+        default:              return o->m_cs_sz;
         }
     }
 }
@@ -118,25 +118,28 @@ extern "C" void lean_free_object(lean_object * o) {
 }
 
 static inline lean_object * get_next(lean_object * o) {
-#if defined(LEAN_COMPRESSED_OBJECT_HEADER) || defined(LEAN_COMPRESSED_OBJECT_HEADER_SMALL_RC)
-    size_t header = o->m_header;
-    LEAN_BYTE(header, 6) = 0;
-    LEAN_BYTE(header, 7) = 0;
-    return (lean_object*)(header);
-#else
-    return (lean_object*)((size_t)(o->m_rc));
-#endif
+    if (sizeof(void*) == 8) {
+        size_t header = ((size_t*)o)[0];
+        LEAN_BYTE(header, 7) = 0;
+        LEAN_BYTE(header, 6) = 0;
+        return (lean_object*)(header);
+    } else {
+        // 32-bit version
+        return ((lean_object**)o)[0];
+    }
 }
 
 static inline void set_next(lean_object * o, lean_object * n) {
-#if defined(LEAN_COMPRESSED_OBJECT_HEADER) || defined(LEAN_COMPRESSED_OBJECT_HEADER_SMALL_RC)
-    size_t new_header = (size_t)n;
-    LEAN_BYTE(new_header, 6) = LEAN_BYTE(o->m_header, 6);
-    LEAN_BYTE(new_header, 7) = LEAN_BYTE(o->m_header, 7);
-    o->m_header = new_header;
-#else
-    o->m_rc = (size_t)n;
-#endif
+    if (sizeof(void*) == 8) {
+        size_t new_header = (size_t)n;
+        LEAN_BYTE(new_header, 7) = o->m_tag;
+        LEAN_BYTE(new_header, 6) = o->m_other;
+        ((size_t*)o)[0] = new_header;
+        lean_assert(get_next(o) == n);
+    } else {
+        // 32-bit version
+        ((lean_object**)o)[0] = n;
+    }
 }
 
 static inline void push_back(lean_object * & todo, lean_object * v) {
@@ -151,8 +154,17 @@ static inline lean_object * pop_back(lean_object * & todo) {
 }
 
 static inline void dec(lean_object * o, lean_object* & todo) {
-    if (!lean_is_scalar(o) && lean_dec_ref_core(o))
+    if (lean_is_scalar(o))
+        return;
+    if (LEAN_LIKELY(o->m_rc > 1)) {
+        o->m_rc--;
+    } else if (o->m_rc == 1) {
         push_back(todo, o);
+    } else if (o->m_rc == 0) {
+        return;
+    } else if (std::atomic_fetch_add_explicit(lean_get_rc_mt_addr(o), 1, std::memory_order_acq_rel) == -1) {
+        push_back(todo, o);
+    }
 }
 
 #ifdef LEAN_LAZY_RC
@@ -234,20 +246,23 @@ static void lean_del_core(object * o, object * & todo) {
     }
 }
 
-extern "C" void lean_del(object * o) {
+extern "C" 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) {
 #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
+    }
 }
 
+
 // =======================================
 // Closures
 
@@ -449,14 +464,7 @@ extern "C" void lean_mark_persistent(object * o) {
         object * o = todo.back();
         todo.pop_back();
         if (!lean_is_scalar(o) && lean_has_rc(o)) {
-#if defined(LEAN_COMPRESSED_OBJECT_HEADER)
-            o->m_header &= ~((1ull << LEAN_ST_BIT) | (1ull << LEAN_MT_BIT));
-            o->m_header |=  (1ull << LEAN_PERSISTENT_BIT);
-#elif defined(LEAN_COMPRESSED_OBJECT_HEADER_SMALL_RC)
-            LEAN_BYTE(o->m_header, 5) = LEAN_PERSISTENT_MEM_KIND;
-#else
-            o->m_mem_kind = LEAN_PERSISTENT_MEM_KIND;
-#endif
+            o->m_rc = 0;
 #if defined(__has_feature)
 #if __has_feature(address_sanitizer)
             // do not report as leak
@@ -538,14 +546,7 @@ extern "C" void lean_mark_mt(object * o) {
         object * o = todo.back();
         todo.pop_back();
         if (!lean_is_scalar(o) && lean_is_st(o)) {
-#if defined(LEAN_COMPRESSED_OBJECT_HEADER)
-            o->m_header &= ~(1ull << LEAN_ST_BIT);
-            o->m_header |=  (1ull << LEAN_MT_BIT);
-#elif defined(LEAN_COMPRESSED_OBJECT_HEADER_SMALL_RC)
-            LEAN_BYTE(o->m_header, 5) = LEAN_MT_MEM_KIND;
-#else
-            o->m_mem_kind = LEAN_MT_MEM_KIND;
-#endif
+            o->m_rc = -o->m_rc;
             uint8_t tag = lean_ptr_tag(o);
             if (tag <= LeanMaxCtorTag) {
                 object ** it  = lean_ctor_obj_cptr(o);
@@ -916,16 +917,10 @@ void deactivate_task(lean_task_object * t) {
 }
 
 static inline void lean_set_task_header(lean_object * o) {
-#if defined(LEAN_COMPRESSED_OBJECT_HEADER)
-    o->m_header   = ((size_t)(LeanTask) << 56) | (1ull << LEAN_MT_BIT) | 1;
-#elif defined(LEAN_COMPRESSED_OBJECT_HEADER_SMALL_RC)
-    o->m_header   = ((size_t)(LeanTask) << 56) | ((size_t)LEAN_MT_MEM_KIND << 40) | 1;
-#else
-    o->m_rc       = 1;
+    o->m_rc       = -1;
     o->m_tag      = LeanTask;
-    o->m_mem_kind = LEAN_MT_MEM_KIND;
     o->m_other    = 0;
-#endif
+    o->m_cs_sz    = 0;
 }
 
 static lean_task_object * alloc_task(obj_arg c, unsigned prio, bool keep_alive) {

src/util/object_ref.h

@@ -18,7 +18,7 @@ protected:
     object * m_obj;
 public:
     object_ref():m_obj(box(0)) {}
-    explicit object_ref(obj_arg o):m_obj(o) { lean_assert(is_scalar(o) || !is_heap_obj(o) || lean_nonzero_rc(o)); }
+    explicit object_ref(obj_arg o):m_obj(o) {}
     object_ref(b_obj_arg o, bool):m_obj(o) { inc(o); }
     object_ref(object_ref const & s):m_obj(s.m_obj) { inc(m_obj); }
     object_ref(object_ref && s):m_obj(s.m_obj) { s.m_obj = box(0); }