chore: update stage0

src/include/lean/lean.h

@@ -89,46 +89,16 @@ LEAN_CASSERT(sizeof(void*) == 8);
 
 /* Lean object header */
 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;        /* > 0 - single thread object, < 0 - multi threaded object, == 0 - persistent object. */
+    unsigned m_cs_sz:16;  /* for small objects stored in compact regions, this field contains the object size. It is 0, otherwise */
+    unsigned m_other:8;   /* number of fields for constructors, element size for scalar arrays */
+    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 +348,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,145 +363,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 {
+        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);
+        lean_inc_ref_n_cold(o, n);
     }
-#endif
 }
 
+bool lean_dec_ref_core_cold(lean_object * o);
+
 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))) {
+    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 {
+        return lean_dec_ref_core_cold(o);
     }
-#endif
 }
 
 /* Generic Lean object delete operation. */
@@ -579,97 +450,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 +528,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/runtime/object.cpp

@@ -69,8 +69,26 @@ extern "C" object * lean_sorry(uint8) {
     lean_unreachable();
 }
 
+extern "C" void lean_inc_ref_cold(lean_object * o) {
+    if (o->m_rc == 0)
+        return;
+    atomic_fetch_sub_explicit(lean_get_rc_mt_addr(o), 1, memory_order_relaxed);
+}
+
+extern "C" void lean_inc_ref_n_cold(lean_object * o, unsigned n) {
+    if (o->m_rc == 0)
+        return;
+    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;
+}
+
 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 +104,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 +128,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) {
@@ -449,14 +462,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 +544,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 +915,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); }