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

chore: document simplified object header and remove obsolete cmake options

Browse source
This commit is contained in:
Leonardo de Moura 2021-07-20 09:31:03 -07:00
parent 10122ba38b
commit a019d8071f
3 changed files with 18 additions and 34 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

23
src/CMakeLists.txt
View file

@ -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")

3
src/config.h.in
View file

@ -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@

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

@ -82,16 +82,26 @@ 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 {
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 */
int m_rc;
unsigned m_cs_sz:16;
unsigned m_other:8;
unsigned m_tag:8;
} lean_object;