From 88eb902810e4523eb73b4d37f869604a873b6616 Mon Sep 17 00:00:00 2001 From: Maxim Menshikov Date: Wed, 5 Aug 2026 12:01:00 +0100 Subject: [PATCH 1/8] core: extract allocation and handle store into ACSL-specified C core Move all non-trivial uGC logic into plain C (ugc_core.c, ugc_zalloc.c) with ACSL contracts so Frama-C can verify it with WP and Eva; the C++ classes uGCHeap, uGCHandleStore and uGCHandleManager become thin wrappers over these functions. The zeroing allocator lives in its own translation unit so the core is verified against its contract only. Update build.sh and release.yml to pick up object files from the new subdirectory. Signed-off-by: Maxim Menshikov --- .github/workflows/release.yml | 4 +- build.sh | 2 +- ugc/CMakeLists.txt | 2 + ugc/core/ugc_core.c | 263 +++++++++++++++++++++++ ugc/core/ugc_core.h | 381 ++++++++++++++++++++++++++++++++++ ugc/core/ugc_zalloc.c | 19 ++ ugc/uGCHandleManager.cpp | 21 +- ugc/uGCHandleStore.cpp | 79 ++----- ugc/uGCHeap.cpp | 62 +----- 9 files changed, 697 insertions(+), 136 deletions(-) create mode 100644 ugc/core/ugc_core.c create mode 100644 ugc/core/ugc_core.h create mode 100644 ugc/core/ugc_zalloc.c diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index 9f1639d..4858ba9 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -62,7 +62,7 @@ jobs: prerelease: false files: | build/usr/lib/libugc-zero.a - build/usr/lib/objects/ugc-zero/*.obj + build/usr/lib/objects/ugc-zero/**/*.obj ugc-riscv64.tar.gz body: | ## uGC Release ${{ steps.version.outputs.version }} @@ -71,7 +71,7 @@ jobs: ### Files - `libugc-zero.a` - Static library - - `*.obj` - Individual object files (uGC.cpp.obj, uGCHandleManager.cpp.obj, uGCHandleStore.cpp.obj, uGCHeap.cpp.obj) + - `*.obj` - Individual object files (C++ wrappers and the formally verified C core) - `ugc-riscv64.tar.gz` - Complete archive with library and object files ### Usage diff --git a/build.sh b/build.sh index a46dae5..49b5e32 100755 --- a/build.sh +++ b/build.sh @@ -37,7 +37,7 @@ pushd "${TOP_DIR}" file="usr/lib/libugc-zero.a" printf '\x00' | dd of="$file" bs=1 seek=$((0x30)) count=1 conv=notrunc pushd usr/lib/objects/ugc-zero - for file in uGC.cpp.obj uGCHandleManager.cpp.obj uGCHandleStore.cpp.obj uGCHeap.cpp.obj ; do + for file in $(find . -name '*.obj') ; do printf '\x00' | dd of="$file" bs=1 seek=$((0x30)) count=1 conv=notrunc done popd diff --git a/ugc/CMakeLists.txt b/ugc/CMakeLists.txt index b0707c9..e41b54b 100644 --- a/ugc/CMakeLists.txt +++ b/ugc/CMakeLists.txt @@ -10,6 +10,8 @@ project(ugc-zero) add_library(${PROJECT_NAME} OBJECT + core/ugc_core.c + core/ugc_zalloc.c uGC.cpp uGCHandleManager.cpp uGCHandleStore.cpp diff --git a/ugc/core/ugc_core.c b/ugc/core/ugc_core.c new file mode 100644 index 0000000..0e55c1c --- /dev/null +++ b/ugc/core/ugc_core.c @@ -0,0 +1,263 @@ +/** + * @file + * @brief uGC - formally specified core (allocation + handle store) + * + * Copyright (C) 2026 Demerzel Solutions Limited (Nethermind) + * + * @author Maxim Menshikov + */ +#include "ugc_core.h" + +int ugc_handle_count = 0; +void *ugc_handles[UGC_HANDLE_COUNT] = { 0 }; +int ugc_handle_types[UGC_HANDLE_COUNT] = { 0 }; +void *ugc_handle_extra[UGC_HANDLE_COUNT] = { 0 }; +void *ugc_handle_dependent[UGC_HANDLE_COUNT] = { 0 }; + +/* Direct path: allocate object + header straight from the zeroing + * allocator, bypassing any allocation context. */ +/*@ + requires 1 <= header_size; + requires size <= SIZE_MAX - header_size; + assigns \nothing; + ensures \result == \null || + (\valid(\result + (0 .. size - 1)) && + (\forall integer i; 0 <= i < size ==> \result[i] == 0)); +*/ +static uint8_t * +ugc_alloc_direct(size_t size, size_t header_size) +{ + uint8_t *address = ugc_zalloc(size + header_size); + if (address == (uint8_t *)0) + return (uint8_t *)0; /* OOM: don't offset null to a bogus object */ + + /*@ assert step_valid_block: + \valid(address + (0 .. size + header_size - 1)); */ + /*@ assert step_valid_object: + \valid((address + header_size) + (0 .. size - 1)); */ + /*@ assert step_zeroed_elem: + \forall integer i; 0 <= i < size ==> + (address + header_size)[i] == 0; */ + return address + header_size; +} + +/* Refill path: hand the context a fresh zeroed quantum and carve the + * requested object out of its beginning (after the plug-skew header). */ +/*@ + requires 1 <= header_size <= UGC_ALLOC_QUANTUM / 2; + requires size + header_size <= UGC_ALLOC_QUANTUM; + requires \valid(alloc_ptr_p) && \valid(alloc_limit_p) && + \separated(alloc_ptr_p, alloc_limit_p); + assigns *alloc_ptr_p, *alloc_limit_p; + ensures \result == \null ==> + *alloc_ptr_p == \old(*alloc_ptr_p) && + *alloc_limit_p == \old(*alloc_limit_p); + ensures \result != \null ==> + *alloc_ptr_p == \result + size && + *alloc_limit_p == \result + (UGC_ALLOC_QUANTUM - header_size) && + \valid(\result + (0 .. UGC_ALLOC_QUANTUM - header_size - 1)) && + (\forall integer i; + 0 <= i < UGC_ALLOC_QUANTUM - header_size ==> + \result[i] == 0); +*/ +static uint8_t * +ugc_ctx_refill(uint8_t **alloc_ptr_p, uint8_t **alloc_limit_p, + size_t size, size_t header_size) +{ + uint8_t *base = ugc_zalloc(UGC_ALLOC_QUANTUM); + if (base == (uint8_t *)0) + return (uint8_t *)0; + + /*@ assert step_valid_block: + \valid(base + (0 .. UGC_ALLOC_QUANTUM - 1)); */ + /*@ assert step_valid_object: + \valid((base + header_size) + + (0 .. UGC_ALLOC_QUANTUM - header_size - 1)); */ + /*@ assert step_zeroed_elem: + \forall integer i; 0 <= i < UGC_ALLOC_QUANTUM - header_size ==> + (base + header_size)[i] == 0; */ + /*@ assert step_ptr_shift: + base + (header_size + size) == (base + header_size) + size; */ + /*@ assert step_limit_shift: + base + UGC_ALLOC_QUANTUM == + (base + header_size) + (UGC_ALLOC_QUANTUM - header_size); */ + *alloc_ptr_p = base + header_size + size; + *alloc_limit_p = base + UGC_ALLOC_QUANTUM; + return base + header_size; +} + +uint8_t * +ugc_core_alloc(uint8_t **alloc_ptr_p, uint8_t **alloc_limit_p, + size_t size, bool bypass_context, size_t header_size) +{ + /* size is size_t; truncating it into a narrower type could wrap for a + * large object and under-allocate. Keep the full width and reject an + * addition that would overflow size_t. */ + if (size > SIZE_MAX - header_size) + return (uint8_t *)0; /* overflow: signal OOM, don't under-allocate */ + + size_t sizeWithHeader = size + header_size; + + /* Large or old-heap-flagged objects bypass the allocation context, like + * the real GC does: the context quantum is deliberately smaller than the + * LOH threshold, and GC_ALLOC_USER_OLD_HEAP objects must not land in the + * ephemeral context region. */ + if (alloc_ptr_p == (uint8_t **)0 || bypass_context || + sizeWithHeader > UGC_ALLOC_QUANTUM) + { + return ugc_alloc_direct(size, header_size); + } + + /* Serve from the thread's context when the request still fits. (We only + * get here if the runtime's inline fast path failed, e.g. right after the + * context was created or exhausted, or from paths that skip it.) */ + uint8_t *ptr = *alloc_ptr_p; + if (ptr != (uint8_t *)0 && (size_t)(*alloc_limit_p - ptr) >= size) + { + *alloc_ptr_p = ptr + size; + return ptr; + } + + return ugc_ctx_refill(alloc_ptr_p, alloc_limit_p, size, header_size); +} + +bool +ugc_handle_store_contains(const void *hndl) +{ + uintptr_t handle = (uintptr_t)hndl; + uintptr_t handleStart = (uintptr_t)&ugc_handles[0]; + uintptr_t handleEnd = handleStart + sizeof(ugc_handles); + + return handle >= handleStart && handle < handleEnd; +} + +void ** +ugc_handle_create(void *object, int type) +{ + if (ugc_handle_count == UGC_HANDLE_COUNT) + return (void **)0; + + ugc_handles[ugc_handle_count] = object; + ugc_handle_types[ugc_handle_count] = type; + return &ugc_handles[ugc_handle_count++]; +} + +void ** +ugc_handle_create_with_extra(void *object, int type, void *extra) +{ + if (ugc_handle_count == UGC_HANDLE_COUNT) + return (void **)0; + + ugc_handles[ugc_handle_count] = object; + ugc_handle_types[ugc_handle_count] = type; + ugc_handle_extra[ugc_handle_count] = extra; + return &ugc_handles[ugc_handle_count++]; +} + +void ** +ugc_handle_create_dependent(void *primary, void *secondary) +{ + if (ugc_handle_count == UGC_HANDLE_COUNT) + return (void **)0; + + ugc_handles[ugc_handle_count] = primary; + ugc_handle_dependent[ugc_handle_count] = secondary; + return &ugc_handles[ugc_handle_count++]; +} + +size_t +ugc_handle_index(void **hndl) +{ + return (size_t)((uintptr_t)hndl - (uintptr_t)&ugc_handles[0]) / + sizeof(ugc_handles[0]); +} + +void ** +ugc_handle_dependent_slot_at(size_t idx) +{ + return &ugc_handle_dependent[idx]; +} + +void +ugc_handle_set_dependent_at(size_t idx, void *secondary) +{ + ugc_handle_dependent[idx] = secondary; +} + +int +ugc_handle_get_type_at(size_t idx) +{ + return ugc_handle_types[idx]; +} + +void +ugc_handle_set_type_at(size_t idx, int type) +{ + ugc_handle_types[idx] = type; +} + +void * +ugc_handle_get_extra_at(size_t idx) +{ + return ugc_handle_extra[idx]; +} + +void +ugc_handle_set_extra_at(size_t idx, void *extra) +{ + ugc_handle_extra[idx] = extra; +} + +void +ugc_handle_store_reset(void) +{ + /*@ + loop invariant 0 <= i <= UGC_HANDLE_COUNT; + loop invariant \forall integer k; 0 <= k < i ==> + ugc_handles[k] == \null && + ugc_handle_types[k] == 0 && + ugc_handle_extra[k] == \null && + ugc_handle_dependent[k] == \null; + loop assigns i, + ugc_handles[0 .. UGC_HANDLE_COUNT - 1], + ugc_handle_types[0 .. UGC_HANDLE_COUNT - 1], + ugc_handle_extra[0 .. UGC_HANDLE_COUNT - 1], + ugc_handle_dependent[0 .. UGC_HANDLE_COUNT - 1]; + loop variant UGC_HANDLE_COUNT - i; + */ + for (int i = 0; i < UGC_HANDLE_COUNT; i++) + { + ugc_handles[i] = (void *)0; + ugc_handle_types[i] = 0; + ugc_handle_extra[i] = (void *)0; + ugc_handle_dependent[i] = (void *)0; + } + ugc_handle_count = 0; +} + +void +ugc_handle_slot_store(void **slot, void *object) +{ + *slot = object; +} + +bool +ugc_handle_slot_store_if_null(void **slot, void *object) +{ + if (*slot == (void *)0) + { + *slot = object; + return true; + } + return false; +} + +void * +ugc_handle_slot_cas(void **slot, void *object, void *comparand) +{ + if (*slot == comparand) + { + *slot = object; + } + return *slot; +} diff --git a/ugc/core/ugc_core.h b/ugc/core/ugc_core.h new file mode 100644 index 0000000..ccd50bf --- /dev/null +++ b/ugc/core/ugc_core.h @@ -0,0 +1,381 @@ +/** + * @file + * @brief uGC - formally specified core (allocation + handle store) + * + * This module contains all the non-trivial logic of uGC in plain C with + * ACSL contracts so it can be analyzed by Frama-C (WP for functional + * correctness of the contracts, Eva for absence of undefined behavior). + * The C++ classes (uGCHeap, uGCHandleStore, uGCHandleManager) are thin + * wrappers over these functions. + * + * Copyright (C) 2026 Demerzel Solutions Limited (Nethermind) + * + * @author Maxim Menshikov + */ +#pragma once + +#include +#include +#ifndef __cplusplus +#include +#endif + +#ifdef __cplusplus +extern "C" { +#endif + +/* Allocation-context quantum. Refilling the context lets the runtime's own + * fast paths (coreclr/runtime//AllocFast.S: RhpNewFast & friends) bump + * inline on alloc_ptr/combined_limit without calling into the GC again; the + * runtime refreshes combined_limit itself after every GCHeap::Alloc + * (GCHelpers.cpp: GcAllocInternal -> UpdateCombinedLimit). Must stay below + * RH_LARGE_OBJECT_SIZE (85000): GcAllocInternal asserts in _DEBUG that + * alloc_limit - alloc_ptr never exceeds it. */ +#ifndef UGC_ALLOC_QUANTUM +#define UGC_ALLOC_QUANTUM (64 * 1024) +#endif + +/** Capacity of the global handle store */ +#define UGC_HANDLE_COUNT 65535 + +/* + * --------------------------------------------------------------------------- + * Abstract zeroing allocator + * --------------------------------------------------------------------------- + * The production implementation (ugc_zalloc.c) forwards to calloc. For WP + * verification only this contract is used: the function either fails (NULL) + * or returns a block of n valid, zero-initialized bytes. + */ +/*@ + assigns \nothing; + ensures zalloc_result: + \result == \null || + (\valid(\result + (0 .. n - 1)) && + (\forall integer i; 0 <= i < n ==> \result[i] == 0)); +*/ +uint8_t *ugc_zalloc(size_t n); + +/* + * --------------------------------------------------------------------------- + * Allocation + * --------------------------------------------------------------------------- + * ugc_core_alloc implements IGCHeap::Alloc: + * - rejects a size whose header-extended value overflows size_t; + * - serves large objects, GC_ALLOC_USER_OLD_HEAP objects and calls without + * an allocation context directly from the zeroing allocator; + * - otherwise bump-allocates from the thread allocation context window + * [*alloc_ptr_p, *alloc_limit_p), refilling it with a fresh zeroed + * quantum when the request does not fit. The first object's header + * occupies the first header_size bytes of a fresh quantum (plug skew); + * every object's base size already pre-pays the header of the object + * that follows it, so a plain alloc_ptr bump keeps headers intact. + * The remainder of the previous quantum is abandoned - this GC never + * frees memory anyway. + */ + +/*@ + requires header_size_range: 1 <= header_size <= UGC_ALLOC_QUANTUM / 2; + requires context_ptrs: + alloc_ptr_p == \null || + (\valid(alloc_ptr_p) && \valid(alloc_limit_p) && + \separated(alloc_ptr_p, alloc_limit_p)); + requires context_window: + alloc_ptr_p == \null || *alloc_ptr_p == \null || + (\base_addr(*alloc_ptr_p) == \base_addr(*alloc_limit_p) && + *alloc_ptr_p <= *alloc_limit_p && + *alloc_limit_p - *alloc_ptr_p <= UGC_ALLOC_QUANTUM && + \valid(*alloc_ptr_p + (0 .. *alloc_limit_p - *alloc_ptr_p - 1))); + + assigns *alloc_ptr_p, *alloc_limit_p; + + behavior overflow: + assumes size > SIZE_MAX - header_size; + assigns \nothing; + ensures \result == \null; + + behavior direct: + assumes size <= SIZE_MAX - header_size; + assumes alloc_ptr_p == \null || bypass_context || + size + header_size > UGC_ALLOC_QUANTUM; + assigns \nothing; + ensures \result == \null || + (\valid(\result + (0 .. size - 1)) && + (\forall integer i; 0 <= i < size ==> \result[i] == 0)); + + behavior bump: + assumes size <= SIZE_MAX - header_size; + assumes alloc_ptr_p != \null && !bypass_context && + size + header_size <= UGC_ALLOC_QUANTUM; + assumes *alloc_ptr_p != \null && + *alloc_limit_p - *alloc_ptr_p >= size; + assigns *alloc_ptr_p; + ensures \result == \old(*alloc_ptr_p); + ensures *alloc_ptr_p == \old(*alloc_ptr_p) + size; + ensures \valid(\result + (0 .. size - 1)); + + behavior refill: + assumes size <= SIZE_MAX - header_size; + assumes alloc_ptr_p != \null && !bypass_context && + size + header_size <= UGC_ALLOC_QUANTUM; + assumes !(*alloc_ptr_p != \null && + *alloc_limit_p - *alloc_ptr_p >= size); + assigns *alloc_ptr_p, *alloc_limit_p; + ensures \result == \null ==> + *alloc_ptr_p == \old(*alloc_ptr_p) && + *alloc_limit_p == \old(*alloc_limit_p); + ensures \result != \null ==> + *alloc_ptr_p == \result + size && + *alloc_limit_p == \result + (UGC_ALLOC_QUANTUM - header_size) && + \valid(\result + (0 .. UGC_ALLOC_QUANTUM - header_size - 1)) && + (\forall integer i; + 0 <= i < UGC_ALLOC_QUANTUM - header_size ==> + \result[i] == 0); + + complete behaviors; + disjoint behaviors; +*/ +uint8_t *ugc_core_alloc(uint8_t **alloc_ptr_p, uint8_t **alloc_limit_p, + size_t size, bool bypass_context, + size_t header_size); + +/* + * --------------------------------------------------------------------------- + * Handle store + * --------------------------------------------------------------------------- + * A handle is a pointer to a slot of ugc_handles. Parallel arrays keep the + * handle type, the extra info and the dependent-handle secondary object. + * Handles are never destroyed (this GC never frees anything), so the store + * is a monotonically growing array. + */ +extern int ugc_handle_count; +extern void *ugc_handles[UGC_HANDLE_COUNT]; +extern int ugc_handle_types[UGC_HANDLE_COUNT]; +extern void *ugc_handle_extra[UGC_HANDLE_COUNT]; +extern void *ugc_handle_dependent[UGC_HANDLE_COUNT]; + +/*@ + predicate ugc_valid_slot(void **h) = + \exists integer i; 0 <= i < UGC_HANDLE_COUNT && h == &ugc_handles[i]; + + predicate ugc_store_consistent = + 0 <= ugc_handle_count <= UGC_HANDLE_COUNT; +*/ + +/** + * Check whether hndl points into the handle array. + * + * The membership test is performed on integer representations of the + * pointers (as the CLR contract requires answering for arbitrary pointers), + * which is outside what can be expressed portably in ACSL for pointers not + * derived from the array, hence the intentionally weak contract. + */ +/*@ + assigns \nothing; +*/ +bool ugc_handle_store_contains(const void *hndl); + +/*@ + requires ugc_store_consistent; + assigns ugc_handle_count, + ugc_handles[ugc_handle_count], + ugc_handle_types[ugc_handle_count]; + + behavior full: + assumes ugc_handle_count == UGC_HANDLE_COUNT; + assigns \nothing; + ensures \result == \null; + + behavior ok: + assumes ugc_handle_count < UGC_HANDLE_COUNT; + ensures \result == &ugc_handles[\old(ugc_handle_count)]; + ensures ugc_handles[\old(ugc_handle_count)] == object; + ensures ugc_handle_types[\old(ugc_handle_count)] == type; + ensures ugc_handle_count == \old(ugc_handle_count) + 1; + + complete behaviors; + disjoint behaviors; +*/ +void **ugc_handle_create(void *object, int type); + +/*@ + requires ugc_store_consistent; + assigns ugc_handle_count, + ugc_handles[ugc_handle_count], + ugc_handle_types[ugc_handle_count], + ugc_handle_extra[ugc_handle_count]; + + behavior full: + assumes ugc_handle_count == UGC_HANDLE_COUNT; + assigns \nothing; + ensures \result == \null; + + behavior ok: + assumes ugc_handle_count < UGC_HANDLE_COUNT; + ensures \result == &ugc_handles[\old(ugc_handle_count)]; + ensures ugc_handles[\old(ugc_handle_count)] == object; + ensures ugc_handle_types[\old(ugc_handle_count)] == type; + ensures ugc_handle_extra[\old(ugc_handle_count)] == extra; + ensures ugc_handle_count == \old(ugc_handle_count) + 1; + + complete behaviors; + disjoint behaviors; +*/ +void **ugc_handle_create_with_extra(void *object, int type, void *extra); + +/*@ + requires ugc_store_consistent; + assigns ugc_handle_count, + ugc_handles[ugc_handle_count], + ugc_handle_dependent[ugc_handle_count]; + + behavior full: + assumes ugc_handle_count == UGC_HANDLE_COUNT; + assigns \nothing; + ensures \result == \null; + + behavior ok: + assumes ugc_handle_count < UGC_HANDLE_COUNT; + ensures \result == &ugc_handles[\old(ugc_handle_count)]; + ensures ugc_handles[\old(ugc_handle_count)] == primary; + ensures ugc_handle_dependent[\old(ugc_handle_count)] == secondary; + ensures ugc_handle_count == \old(ugc_handle_count) + 1; + + complete behaviors; + disjoint behaviors; +*/ +void **ugc_handle_create_dependent(void *primary, void *secondary); + +/** + * Convert a handle (a pointer to a slot of ugc_handles) into its index. + * + * The conversion is a pointer subtraction against the array base. Like + * ugc_handle_store_contains, relating an externally supplied pointer to + * the array base is outside what the WP memory model can reason about, + * hence the intentionally weak contract; the pointer/index round trip is + * covered by unit tests instead. For a hndl satisfying ugc_valid_slot the + * result is the index i such that hndl == &ugc_handles[i]. + */ +/*@ + requires valid_handle: ugc_valid_slot(hndl); + assigns \nothing; +*/ +size_t ugc_handle_index(void **hndl); + +/*@ + requires valid_index: 0 <= idx < UGC_HANDLE_COUNT; + assigns \nothing; + ensures \result == &ugc_handle_dependent[idx]; +*/ +void **ugc_handle_dependent_slot_at(size_t idx); + +/*@ + requires valid_index: 0 <= idx < UGC_HANDLE_COUNT; + assigns ugc_handle_dependent[idx]; + ensures ugc_handle_dependent[idx] == secondary; +*/ +void ugc_handle_set_dependent_at(size_t idx, void *secondary); + +/*@ + requires valid_index: 0 <= idx < UGC_HANDLE_COUNT; + assigns \nothing; + ensures \result == ugc_handle_types[idx]; +*/ +int ugc_handle_get_type_at(size_t idx); + +/*@ + requires valid_index: 0 <= idx < UGC_HANDLE_COUNT; + assigns ugc_handle_types[idx]; + ensures ugc_handle_types[idx] == type; +*/ +void ugc_handle_set_type_at(size_t idx, int type); + +/*@ + requires valid_index: 0 <= idx < UGC_HANDLE_COUNT; + assigns \nothing; + ensures \result == ugc_handle_extra[idx]; +*/ +void *ugc_handle_get_extra_at(size_t idx); + +/*@ + requires valid_index: 0 <= idx < UGC_HANDLE_COUNT; + assigns ugc_handle_extra[idx]; + ensures ugc_handle_extra[idx] == extra; +*/ +void ugc_handle_set_extra_at(size_t idx, void *extra); + +/*@ + assigns ugc_handle_count, + ugc_handles[0 .. UGC_HANDLE_COUNT - 1], + ugc_handle_types[0 .. UGC_HANDLE_COUNT - 1], + ugc_handle_extra[0 .. UGC_HANDLE_COUNT - 1], + ugc_handle_dependent[0 .. UGC_HANDLE_COUNT - 1]; + ensures ugc_handle_count == 0; + ensures \forall integer i; 0 <= i < UGC_HANDLE_COUNT ==> + ugc_handles[i] == \null && + ugc_handle_types[i] == 0 && + ugc_handle_extra[i] == \null && + ugc_handle_dependent[i] == \null; +*/ +void ugc_handle_store_reset(void); + +/* + * --------------------------------------------------------------------------- + * Handle slot operations (IGCHandleManager) + * --------------------------------------------------------------------------- + * These operate on the object slot a handle points to. + */ + +/*@ + requires \valid(slot); + assigns *slot; + ensures *slot == object; +*/ +void ugc_handle_slot_store(void **slot, void *object); + +/*@ + requires \valid(slot); + assigns *slot; + + behavior was_null: + assumes *slot == \null; + ensures *slot == object; + ensures \result == \true; + + behavior was_set: + assumes *slot != \null; + ensures *slot == \old(*slot); + ensures \result == \false; + + complete behaviors; + disjoint behaviors; +*/ +bool ugc_handle_slot_store_if_null(void **slot, void *object); + +/** + * Non-atomic compare-and-swap over a handle slot (uGC is single-threaded + * with respect to handle mutation). Note: unlike the CLR interlocked + * primitive, this returns the value of the slot after the operation - the + * behavior is inherited from the original implementation. + */ +/*@ + requires \valid(slot); + assigns *slot; + + behavior swapped: + assumes *slot == comparand; + ensures *slot == object; + ensures \result == object; + + behavior kept: + assumes *slot != comparand; + ensures *slot == \old(*slot); + ensures \result == \old(*slot); + + complete behaviors; + disjoint behaviors; +*/ +void *ugc_handle_slot_cas(void **slot, void *object, void *comparand); + +#ifdef __cplusplus +} +#endif diff --git a/ugc/core/ugc_zalloc.c b/ugc/core/ugc_zalloc.c new file mode 100644 index 0000000..e1df9de --- /dev/null +++ b/ugc/core/ugc_zalloc.c @@ -0,0 +1,19 @@ +/** + * @file + * @brief uGC - production zeroing allocator (calloc-backed) + * + * Kept in a separate translation unit so that Frama-C/WP verifies + * ugc_core.c against the ACSL contract of ugc_zalloc only. + * + * Copyright (C) 2026 Demerzel Solutions Limited (Nethermind) + * + * @author Maxim Menshikov + */ +#include "ugc_core.h" +#include + +uint8_t * +ugc_zalloc(size_t n) +{ + return (uint8_t *)calloc(n, sizeof(char)); +} diff --git a/ugc/uGCHandleManager.cpp b/ugc/uGCHandleManager.cpp index 81ff0d2..dd65170 100644 --- a/ugc/uGCHandleManager.cpp +++ b/ugc/uGCHandleManager.cpp @@ -8,6 +8,7 @@ */ #include "uGCHandleManager.h" #include "uGCHandleStore.h" +#include "core/ugc_core.h" bool uGCHandleManager::Initialize() @@ -77,21 +78,13 @@ uGCHandleManager::GetExtraInfoFromHandle(OBJECTHANDLE handle) void uGCHandleManager::StoreObjectInHandle(OBJECTHANDLE handle, Object *object) { - Object **handleObj = (Object **)handle; - *handleObj = object; + ugc_handle_slot_store((void **)handle, object); } bool uGCHandleManager::StoreObjectInHandleIfNull(OBJECTHANDLE handle, Object *object) { - Object **handleObj = (Object **)handle; - - if (*handleObj == NULL) - { - *handleObj = object; - return true; - } - return false; + return ugc_handle_slot_store_if_null((void **)handle, object); } void @@ -112,13 +105,7 @@ Object* uGCHandleManager::InterlockedCompareExchangeObjectInHandle(OBJECTHANDLE handle, Object *object, Object *oldObject) { - Object **handleObject = (Object **)handle; - - if (*handleObject == oldObject) - { - *handleObject = object; - } - return *handleObject; + return (Object *)ugc_handle_slot_cas((void **)handle, object, oldObject); } HandleType diff --git a/ugc/uGCHandleStore.cpp b/ugc/uGCHandleStore.cpp index ccb8b9c..57a405b 100644 --- a/ugc/uGCHandleStore.cpp +++ b/ugc/uGCHandleStore.cpp @@ -7,14 +7,7 @@ * @author Maxim Menshikov */ #include "uGCHandleStore.h" - -#define HANDLE_COUNT (65535) - -static int handlesCount = 0; -static Object *handles[HANDLE_COUNT] = { 0 }; -static HandleType handleTypes[HANDLE_COUNT] = { HandleType() }; -static void *extraInfos[HANDLE_COUNT] = { 0 }; -static Object *dependentHandles[HANDLE_COUNT] = { 0 }; +#include "core/ugc_core.h" void uGCHandleStore::Uproot() @@ -24,111 +17,69 @@ uGCHandleStore::Uproot() bool uGCHandleStore::ContainsHandle(OBJECTHANDLE hndl) { - uintptr_t handle = (uintptr_t) hndl; - uintptr_t handleStart = (uintptr_t)&handles; - uintptr_t handleEnd = (uintptr_t)&handles + sizeof(handles); - if (handle >= handleStart && handle < handleEnd) - return true; - return false; + return ugc_handle_store_contains((const void *)hndl); } OBJECTHANDLE uGCHandleStore::CreateHandleOfType(Object *object, HandleType type) { - if (handlesCount == HANDLE_COUNT) - return 0; - handles[handlesCount] = object; - handleTypes[handlesCount] = type; - return (OBJECTHANDLE)&handles[handlesCount++]; + return (OBJECTHANDLE)ugc_handle_create(object, (int)type); } OBJECTHANDLE uGCHandleStore::CreateHandleOfType(Object *object, HandleType type, int heapToAffinitizeTo) { - if (handlesCount == HANDLE_COUNT) - return 0; - - handles[handlesCount] = object; - handleTypes[handlesCount] = type; - return (OBJECTHANDLE)&handles[handlesCount++]; + return (OBJECTHANDLE)ugc_handle_create(object, (int)type); } OBJECTHANDLE uGCHandleStore::CreateHandleWithExtraInfo(Object *object, HandleType type, void * pExtraInfo) { - if (handlesCount == HANDLE_COUNT) - return 0; - - handles[handlesCount] = object; - handleTypes[handlesCount] = type; - extraInfos[handlesCount] = pExtraInfo; - return (OBJECTHANDLE)&handles[handlesCount++]; + return (OBJECTHANDLE)ugc_handle_create_with_extra(object, (int)type, + pExtraInfo); } OBJECTHANDLE uGCHandleStore::CreateDependentHandle(Object *primary, Object *secondary) { - if (handlesCount == HANDLE_COUNT) - return 0; - - handles[handlesCount] = primary; - dependentHandles[handlesCount] = secondary; - return (OBJECTHANDLE)&handles[handlesCount++]; + return (OBJECTHANDLE)ugc_handle_create_dependent(primary, secondary); } OBJECTHANDLE uGCHandleStore::uGetDependentHandle(OBJECTHANDLE hndl) { - int handleNumber = ((uintptr_t)hndl - (uintptr_t)&handles[0]) / - sizeof(handles[0]); - - return (OBJECTHANDLE)&dependentHandles[handleNumber]; + return (OBJECTHANDLE)ugc_handle_dependent_slot_at( + ugc_handle_index((void **)hndl)); } void uGCHandleStore::uSetDependentHandle(OBJECTHANDLE hndl, Object *secondary) { - int handleNumber = ((uintptr_t)hndl - (uintptr_t)&handles[0]) / - sizeof(handles[0]); - - dependentHandles[handleNumber] = secondary; + ugc_handle_set_dependent_at(ugc_handle_index((void **)hndl), secondary); } HandleType uGCHandleStore::uGetHandleType(OBJECTHANDLE hndl) { - int handleNumber = ((uintptr_t)hndl - (uintptr_t)&handles[0]) / - sizeof(handles[0]); - - return handleTypes[handleNumber]; + return (HandleType)ugc_handle_get_type_at(ugc_handle_index((void **)hndl)); } void uGCHandleStore::uSetHandleType(OBJECTHANDLE hndl, HandleType type) { - int handleNumber = ((uintptr_t)hndl - (uintptr_t)&handles[0]) / - sizeof(handles[0]); - - handleTypes[handleNumber] = type; + ugc_handle_set_type_at(ugc_handle_index((void **)hndl), (int)type); } - void * uGCHandleStore::uGetHandleExtraInfo(OBJECTHANDLE hndl) { - int handleNumber = ((uintptr_t)hndl - (uintptr_t)&handles[0]) / - sizeof(handles[0]); - - return extraInfos[handleNumber]; + return ugc_handle_get_extra_at(ugc_handle_index((void **)hndl)); } void uGCHandleStore::uSetHandleExtraInfo(OBJECTHANDLE hndl, void *extraInfo) { - int handleNumber = ((uintptr_t)hndl - (uintptr_t)&handles[0]) / - sizeof(handles[0]); - - extraInfos[handleNumber] = extraInfo; -} \ No newline at end of file + ugc_handle_set_extra_at(ugc_handle_index((void **)hndl), extraInfo); +} diff --git a/ugc/uGCHeap.cpp b/ugc/uGCHeap.cpp index a89df6c..4d094ce 100644 --- a/ugc/uGCHeap.cpp +++ b/ugc/uGCHeap.cpp @@ -7,7 +7,7 @@ * @author Maxim Menshikov */ #include "uGCHeap.h" -#include +#include "core/ugc_core.h" class ObjHeader { @@ -361,64 +361,22 @@ uGCHeap::GetNow() return size_t(); } -/* Allocation-context quantum. Refilling the context lets the runtime's own - * fast paths (coreclr/runtime//AllocFast.S: RhpNewFast & friends) bump - * inline on alloc_ptr/combined_limit without calling into the GC again; the - * runtime refreshes combined_limit itself after every GCHeap::Alloc - * (GCHelpers.cpp: GcAllocInternal -> UpdateCombinedLimit). Must stay below - * RH_LARGE_OBJECT_SIZE (85000): GcAllocInternal asserts in _DEBUG that - * alloc_limit - alloc_ptr never exceeds it. */ -#ifndef UGC_ALLOC_QUANTUM -#define UGC_ALLOC_QUANTUM (64 * 1024) -#endif - Object * uGCHeap::Alloc(gc_alloc_context * acontext, size_t size, uint32_t flags) { - /* size is size_t; the old code truncated it into an int, which for a - * large object could wrap to a small or negative value and under-allocate. - * Keep the full width and reject an addition that overflows size_t. */ - size_t sizeWithHeader = size + sizeof(ObjHeader); - if (sizeWithHeader < size) - return nullptr; /* overflow: signal OOM rather than under-allocate */ - - /* Large or old-heap-flagged objects bypass the allocation context, like - * the real GC does: the context quantum is deliberately smaller than the - * LOH threshold, and GC_ALLOC_USER_OLD_HEAP objects must not land in the - * ephemeral context region. */ - if (acontext == nullptr || sizeWithHeader > UGC_ALLOC_QUANTUM || - (flags & GC_ALLOC_USER_OLD_HEAP) != 0) - { - ObjHeader* address = (ObjHeader*)calloc(sizeWithHeader, sizeof(char)); - if (address == nullptr) - return nullptr; /* OOM: don't offset a null into a bogus object */ - - return (Object*)(address + 1); - } + /* All the allocation logic lives in the formally specified C core + * (core/ugc_core.h). Here we only unpack the allocation context. */ + uint8_t **alloc_ptr_p = nullptr; + uint8_t **alloc_limit_p = nullptr; - /* Serve from the thread's context when the request still fits. (We only - * get here if the runtime's inline fast path failed, e.g. right after the - * context was created or exhausted, or from paths that skip it.) */ - uint8_t* ptr = acontext->alloc_ptr; - if (ptr != nullptr && (size_t)(acontext->alloc_limit - ptr) >= size) + if (acontext != nullptr) { - acontext->alloc_ptr = ptr + size; - return (Object*)ptr; + alloc_ptr_p = &acontext->alloc_ptr; + alloc_limit_p = &acontext->alloc_limit; } - /* Refill: hand the context a fresh zeroed quantum. The first object's - * ObjHeader occupies the first sizeof(ObjHeader) bytes (plug skew); - * every object's base size already pre-pays the header of the object - * that follows it, so a plain alloc_ptr bump keeps headers intact. The - * remainder of the previous quantum is abandoned - this GC never frees - * memory anyway. */ - uint8_t* base = (uint8_t*)calloc(UGC_ALLOC_QUANTUM, sizeof(char)); - if (base == nullptr) - return nullptr; - - acontext->alloc_ptr = base + sizeof(ObjHeader) + size; - acontext->alloc_limit = base + UGC_ALLOC_QUANTUM; - return (Object*)(base + sizeof(ObjHeader)); + return (Object *)ugc_core_alloc(alloc_ptr_p, alloc_limit_p, size, + (flags & GC_ALLOC_USER_OLD_HEAP) != 0, sizeof(ObjHeader)); } void From 72c063849ff7b90d10669e60b92944c384cfaa39 Mon Sep 17 00:00:00 2001 From: Maxim Menshikov Date: Wed, 5 Aug 2026 12:01:10 +0100 Subject: [PATCH 2/8] tests: add unit tests for the core allocator and handle store Add a dependency-free test harness and CTest-driven suites covering the bump allocator (refill, exact fit, overflow, bypass) and the handle store (creation variants, dependent slots, exhaustion, slot CAS). The top-level CMakeLists gains a UGC_BUILD_TESTS option and skips the ugc-zero library when UGC_RUNTIME_INCLUDE_DIR is not set, enabling host-only test builds. Signed-off-by: Maxim Menshikov --- CMakeLists.txt | 15 ++- tests/CMakeLists.txt | 18 ++++ tests/test_core_alloc.c | 205 ++++++++++++++++++++++++++++++++++++++ tests/test_core_handles.c | 180 +++++++++++++++++++++++++++++++++ tests/ugc_test.h | 41 ++++++++ 5 files changed, 458 insertions(+), 1 deletion(-) create mode 100644 tests/CMakeLists.txt create mode 100644 tests/test_core_alloc.c create mode 100644 tests/test_core_handles.c create mode 100644 tests/ugc_test.h diff --git a/CMakeLists.txt b/CMakeLists.txt index 999812f..b3667b9 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -2,4 +2,17 @@ cmake_minimum_required(VERSION 3.20) project(ugc) -add_subdirectory(ugc) +option(UGC_BUILD_TESTS "Build uGC core unit tests" OFF) + +# The ugc-zero library needs the .NET runtime headers; skip it when they are +# not provided (e.g. host-only unit-test builds). +if(DEFINED UGC_RUNTIME_INCLUDE_DIR) + add_subdirectory(ugc) +else() + message(STATUS "UGC_RUNTIME_INCLUDE_DIR not set - skipping ugc-zero library") +endif() + +if(UGC_BUILD_TESTS) + enable_testing() + add_subdirectory(tests) +endif() diff --git a/tests/CMakeLists.txt b/tests/CMakeLists.txt new file mode 100644 index 0000000..a330a1e --- /dev/null +++ b/tests/CMakeLists.txt @@ -0,0 +1,18 @@ +# uGC unit tests +# +# Copyright (C) 2026 Demerzel Solutions Limited (Nethermind) +# Author: Maxim Menshikov + +add_library(ugc-core-host + STATIC + ${CMAKE_CURRENT_SOURCE_DIR}/../ugc/core/ugc_core.c + ${CMAKE_CURRENT_SOURCE_DIR}/../ugc/core/ugc_zalloc.c) +target_include_directories(ugc-core-host + PUBLIC + ${CMAKE_CURRENT_SOURCE_DIR}/../ugc/core) + +foreach(test test_core_alloc test_core_handles) + add_executable(${test} ${test}.c) + target_link_libraries(${test} PRIVATE ugc-core-host) + add_test(NAME ${test} COMMAND ${test}) +endforeach() diff --git a/tests/test_core_alloc.c b/tests/test_core_alloc.c new file mode 100644 index 0000000..cfb79ed --- /dev/null +++ b/tests/test_core_alloc.c @@ -0,0 +1,205 @@ +/** + * @file + * @brief uGC - unit tests for the core allocator + * + * Copyright (C) 2026 Demerzel Solutions Limited (Nethermind) + * + * @author Maxim Menshikov + */ +#include "ugc_core.h" +#include "ugc_test.h" +#include +#include + +/* Header size used by uGCHeap on 64-bit hosts (ObjHeader = alignpad + + * sync block value). */ +#define HDR 8 + +typedef struct +{ + uint8_t *alloc_ptr; + uint8_t *alloc_limit; +} test_context; + +static void * +ctx_alloc(test_context *ctx, size_t size, bool bypass) +{ + return ugc_core_alloc(&ctx->alloc_ptr, &ctx->alloc_limit, size, bypass, + HDR); +} + +static int +is_zeroed(const void *p, size_t n) +{ + const uint8_t *b = (const uint8_t *)p; + size_t i; + + for (i = 0; i < n; i++) + { + if (b[i] != 0) + return 0; + } + return 1; +} + +static void +test_no_context_alloc(void) +{ + void *obj = ugc_core_alloc(NULL, NULL, 128, false, HDR); + + CHECK(obj != NULL); + CHECK(is_zeroed(obj, 128)); + /* Object memory must be writable */ + memset(obj, 0xAA, 128); +} + +static void +test_overflow_returns_null(void) +{ + test_context ctx = { 0 }; + + CHECK(ugc_core_alloc(NULL, NULL, SIZE_MAX, false, HDR) == NULL); + CHECK(ugc_core_alloc(NULL, NULL, SIZE_MAX - HDR + 1, false, HDR) == NULL); + CHECK(ctx_alloc(&ctx, SIZE_MAX, false) == NULL); + /* Boundary that does not overflow must succeed or fail only due to OOM; + * SIZE_MAX - HDR would be a real OOM, so use a sane large size instead */ + CHECK(ctx_alloc(&ctx, UGC_ALLOC_QUANTUM, false) != NULL); +} + +static void +test_refill_initializes_context(void) +{ + test_context ctx = { 0 }; + size_t size = 100; + void *obj = ctx_alloc(&ctx, size, false); + + CHECK(obj != NULL); + /* First object of a fresh quantum sits right after the plug-skew + * header */ + CHECK(ctx.alloc_ptr == (uint8_t *)obj + size); + CHECK(ctx.alloc_limit == (uint8_t *)obj - HDR + UGC_ALLOC_QUANTUM); + CHECK(is_zeroed(obj, size)); + /* The whole handed-out window is zeroed */ + CHECK(is_zeroed(obj, (size_t)(ctx.alloc_limit - (uint8_t *)obj))); +} + +static void +test_bump_allocation(void) +{ + test_context ctx = { 0 }; + void *first = ctx_alloc(&ctx, 64, false); + uint8_t *ptr_after_first = ctx.alloc_ptr; + void *second = ctx_alloc(&ctx, 32, false); + + CHECK(first != NULL); + CHECK(second == ptr_after_first); + CHECK(ctx.alloc_ptr == ptr_after_first + 32); + /* Objects must not overlap */ + CHECK((uint8_t *)second >= (uint8_t *)first + 64); + memset(first, 0x11, 64); + memset(second, 0x22, 32); + CHECK(((uint8_t *)first)[63] == 0x11); + CHECK(((uint8_t *)second)[0] == 0x22); +} + +static void +test_exact_fit_bump(void) +{ + test_context ctx = { 0 }; + void *first = ctx_alloc(&ctx, 16, false); + size_t rest = (size_t)(ctx.alloc_limit - ctx.alloc_ptr); + uint8_t *expected = ctx.alloc_ptr; + void *second; + + CHECK(first != NULL); + CHECK(rest <= UGC_ALLOC_QUANTUM - HDR - 16); + second = ctx_alloc(&ctx, rest, false); + CHECK(second == expected); + CHECK(ctx.alloc_ptr == ctx.alloc_limit); +} + +static void +test_exhaustion_triggers_refill(void) +{ + test_context ctx = { 0 }; + void *first = ctx_alloc(&ctx, 16, false); + uint8_t *old_limit = ctx.alloc_limit; + size_t rest = (size_t)(ctx.alloc_limit - ctx.alloc_ptr); + /* Request one byte more than what remains: must come from a fresh + * quantum */ + void *second = ctx_alloc(&ctx, rest + 1, false); + + CHECK(first != NULL); + CHECK(second != NULL); + CHECK(ctx.alloc_limit != old_limit); + CHECK(ctx.alloc_ptr == (uint8_t *)second + rest + 1); + CHECK(ctx.alloc_limit == (uint8_t *)second - HDR + UGC_ALLOC_QUANTUM); +} + +static void +test_large_object_bypasses_context(void) +{ + test_context ctx = { 0 }; + void *seed = ctx_alloc(&ctx, 8, false); + uint8_t *saved_ptr = ctx.alloc_ptr; + uint8_t *saved_limit = ctx.alloc_limit; + /* size + header > quantum => direct path, context untouched */ + void *large = ctx_alloc(&ctx, UGC_ALLOC_QUANTUM - HDR + 1, false); + + CHECK(seed != NULL); + CHECK(large != NULL); + CHECK(ctx.alloc_ptr == saved_ptr); + CHECK(ctx.alloc_limit == saved_limit); + CHECK(is_zeroed(large, UGC_ALLOC_QUANTUM - HDR + 1)); +} + +static void +test_boundary_size_uses_context(void) +{ + test_context ctx = { 0 }; + /* size + header == quantum: still a context allocation */ + void *obj = ctx_alloc(&ctx, UGC_ALLOC_QUANTUM - HDR, false); + + CHECK(obj != NULL); + CHECK(ctx.alloc_ptr == ctx.alloc_limit); +} + +static void +test_bypass_flag_skips_context(void) +{ + test_context ctx = { 0 }; + void *seed = ctx_alloc(&ctx, 8, false); + uint8_t *saved_ptr = ctx.alloc_ptr; + void *obj = ctx_alloc(&ctx, 24, true); + + CHECK(seed != NULL); + CHECK(obj != NULL); + CHECK(ctx.alloc_ptr == saved_ptr); + CHECK(is_zeroed(obj, 24)); +} + +static void +test_zero_size_allocation(void) +{ + test_context ctx = { 0 }; + void *obj = ctx_alloc(&ctx, 0, false); + + CHECK(obj != NULL); + CHECK(ctx.alloc_ptr == (uint8_t *)obj); +} + +int +main(void) +{ + RUN_TEST(test_no_context_alloc); + RUN_TEST(test_overflow_returns_null); + RUN_TEST(test_refill_initializes_context); + RUN_TEST(test_bump_allocation); + RUN_TEST(test_exact_fit_bump); + RUN_TEST(test_exhaustion_triggers_refill); + RUN_TEST(test_large_object_bypasses_context); + RUN_TEST(test_boundary_size_uses_context); + RUN_TEST(test_bypass_flag_skips_context); + RUN_TEST(test_zero_size_allocation); + return ugc_test_summary(); +} diff --git a/tests/test_core_handles.c b/tests/test_core_handles.c new file mode 100644 index 0000000..27fcc5c --- /dev/null +++ b/tests/test_core_handles.c @@ -0,0 +1,180 @@ +/** + * @file + * @brief uGC - unit tests for the core handle store + * + * Copyright (C) 2026 Demerzel Solutions Limited (Nethermind) + * + * @author Maxim Menshikov + */ +#include "ugc_core.h" +#include "ugc_test.h" +#include + +static int obj_a, obj_b, obj_c, extra_a; + +static void +test_create_basic(void) +{ + void **h; + + ugc_handle_store_reset(); + h = ugc_handle_create(&obj_a, 1); + CHECK(h != NULL); + CHECK(*h == &obj_a); + CHECK(ugc_handle_count == 1); + CHECK(ugc_handle_get_type_at(ugc_handle_index(h)) == 1); + CHECK(ugc_handle_index(h) == 0); +} + +static void +test_create_sequential_slots(void) +{ + void **h1, **h2; + + ugc_handle_store_reset(); + h1 = ugc_handle_create(&obj_a, 1); + h2 = ugc_handle_create(&obj_b, 2); + CHECK(h1 != NULL && h2 != NULL); + CHECK(h2 == h1 + 1); + CHECK(ugc_handle_index(h2) == 1); + CHECK(ugc_handle_get_type_at(ugc_handle_index(h1)) == 1); + CHECK(ugc_handle_get_type_at(ugc_handle_index(h2)) == 2); +} + +static void +test_create_with_extra(void) +{ + void **h; + + ugc_handle_store_reset(); + h = ugc_handle_create_with_extra(&obj_a, 5, &extra_a); + CHECK(h != NULL); + CHECK(*h == &obj_a); + CHECK(ugc_handle_get_extra_at(ugc_handle_index(h)) == &extra_a); + CHECK(ugc_handle_get_type_at(ugc_handle_index(h)) == 5); +} + +static void +test_dependent_handles(void) +{ + void **h; + void **slot; + + ugc_handle_store_reset(); + h = ugc_handle_create_dependent(&obj_a, &obj_b); + CHECK(h != NULL); + CHECK(*h == &obj_a); + slot = ugc_handle_dependent_slot_at(ugc_handle_index(h)); + CHECK(slot != NULL); + CHECK(*slot == &obj_b); + ugc_handle_set_dependent_at(ugc_handle_index(h), &obj_c); + CHECK(*slot == &obj_c); +} + +static void +test_set_type_and_extra(void) +{ + void **h; + + ugc_handle_store_reset(); + h = ugc_handle_create(&obj_a, 1); + CHECK(h != NULL); + ugc_handle_set_type_at(ugc_handle_index(h), 7); + CHECK(ugc_handle_get_type_at(ugc_handle_index(h)) == 7); + ugc_handle_set_extra_at(ugc_handle_index(h), &extra_a); + CHECK(ugc_handle_get_extra_at(ugc_handle_index(h)) == &extra_a); +} + +static void +test_contains(void) +{ + void **h; + int local; + + ugc_handle_store_reset(); + h = ugc_handle_create(&obj_a, 1); + CHECK(ugc_handle_store_contains(h)); + CHECK(!ugc_handle_store_contains(&local)); + CHECK(!ugc_handle_store_contains(NULL)); + /* Any slot address is "contained", even unused ones (matches CLR + * semantics of a store-range check) */ + CHECK(ugc_handle_store_contains(&ugc_handles[UGC_HANDLE_COUNT - 1])); + /* One-past-the-end is not contained */ + CHECK(!ugc_handle_store_contains(&ugc_handles[0] + UGC_HANDLE_COUNT)); +} + +static void +test_store_exhaustion(void) +{ + int i; + void **h = NULL; + + ugc_handle_store_reset(); + for (i = 0; i < UGC_HANDLE_COUNT; i++) + { + h = ugc_handle_create(&obj_a, 0); + CHECK(h != NULL); + if (h == NULL) + break; + } + CHECK(ugc_handle_count == UGC_HANDLE_COUNT); + /* All variants must fail once the store is full, without touching + * the count */ + CHECK(ugc_handle_create(&obj_b, 0) == NULL); + CHECK(ugc_handle_create_with_extra(&obj_b, 0, &extra_a) == NULL); + CHECK(ugc_handle_create_dependent(&obj_b, &obj_c) == NULL); + CHECK(ugc_handle_count == UGC_HANDLE_COUNT); + ugc_handle_store_reset(); + CHECK(ugc_handle_count == 0); +} + +static void +test_slot_store(void) +{ + void *slot = NULL; + + ugc_handle_slot_store(&slot, &obj_a); + CHECK(slot == &obj_a); + ugc_handle_slot_store(&slot, NULL); + CHECK(slot == NULL); +} + +static void +test_slot_store_if_null(void) +{ + void *slot = NULL; + + CHECK(ugc_handle_slot_store_if_null(&slot, &obj_a)); + CHECK(slot == &obj_a); + CHECK(!ugc_handle_slot_store_if_null(&slot, &obj_b)); + CHECK(slot == &obj_a); +} + +static void +test_slot_cas(void) +{ + void *slot = &obj_a; + + /* Mismatch: slot kept, current value returned */ + CHECK(ugc_handle_slot_cas(&slot, &obj_c, &obj_b) == &obj_a); + CHECK(slot == &obj_a); + /* Match: swapped; this implementation returns the new value */ + CHECK(ugc_handle_slot_cas(&slot, &obj_c, &obj_a) == &obj_c); + CHECK(slot == &obj_c); +} + +int +main(void) +{ + RUN_TEST(test_create_basic); + RUN_TEST(test_create_sequential_slots); + RUN_TEST(test_create_with_extra); + RUN_TEST(test_dependent_handles); + RUN_TEST(test_set_type_and_extra); + RUN_TEST(test_contains); + RUN_TEST(test_store_exhaustion); + RUN_TEST(test_slot_store); + RUN_TEST(test_slot_store_if_null); + RUN_TEST(test_slot_cas); + return ugc_test_summary(); +} diff --git a/tests/ugc_test.h b/tests/ugc_test.h new file mode 100644 index 0000000..35a8575 --- /dev/null +++ b/tests/ugc_test.h @@ -0,0 +1,41 @@ +/** + * @file + * @brief uGC - minimal unit-test harness (no external dependencies) + * + * Copyright (C) 2026 Demerzel Solutions Limited (Nethermind) + * + * @author Maxim Menshikov + */ +#pragma once + +#include + +static int ugc_test_checks = 0; +static int ugc_test_failures = 0; + +#define CHECK(cond) \ + do \ + { \ + ugc_test_checks++; \ + if (!(cond)) \ + { \ + ugc_test_failures++; \ + fprintf(stderr, "FAIL %s:%d: %s\n", __FILE__, __LINE__, #cond); \ + } \ + } while (0) + +#define RUN_TEST(fn) \ + do \ + { \ + int before = ugc_test_failures; \ + fn(); \ + printf("%-40s %s\n", #fn, \ + ugc_test_failures == before ? "ok" : "FAILED"); \ + } while (0) + +static inline int +ugc_test_summary(void) +{ + printf("%d checks, %d failures\n", ugc_test_checks, ugc_test_failures); + return ugc_test_failures != 0; +} From 6bd4cc9fba1ee29f1dccd26e49df4ae389cc34fd Mon Sep 17 00:00:00 2001 From: Maxim Menshikov Date: Wed, 5 Aug 2026 12:01:17 +0100 Subject: [PATCH 3/8] formal: add Frama-C verification gate for the core Add verify.sh, which proves the ACSL contracts of ugc/core with WP (failing unless every goal is discharged) and runs Eva value analysis to check for absence of runtime errors. Add eva_main.c, a Frama-C-only driver that exercises allocation, handle store, and slot operations with unconstrained inputs. Signed-off-by: Maxim Menshikov --- formal/eva_main.c | 83 +++++++++++++++++++++++++++++++++++++++++++++++ formal/verify.sh | 68 ++++++++++++++++++++++++++++++++++++++ 2 files changed, 151 insertions(+) create mode 100644 formal/eva_main.c create mode 100755 formal/verify.sh diff --git a/formal/eva_main.c b/formal/eva_main.c new file mode 100644 index 0000000..ec7c614 --- /dev/null +++ b/formal/eva_main.c @@ -0,0 +1,83 @@ +/** + * @file + * @brief uGC - Frama-C/Eva driver: exercises the core with unconstrained + * inputs to verify absence of runtime errors (undefined behavior) + * + * This file is only compiled by Frama-C (formal/verify.sh); it is not part + * of the production library or the unit tests. + * + * Copyright (C) 2026 Demerzel Solutions Limited (Nethermind) + * + * @author Maxim Menshikov + */ +#include "ugc_core.h" +#include "__fc_builtin.h" + +static int object_a, object_b; + +int +main(void) +{ + /* --- Allocation: no context, arbitrary size (overflow + direct) --- */ + size_t size = Frama_C_size_t_interval(0, SIZE_MAX); + (void)ugc_core_alloc((uint8_t **)0, (uint8_t **)0, size, false, 8); + + /* --- Allocation: context paths (refill, then bump / direct) --- */ + uint8_t *alloc_ptr = (uint8_t *)0; + uint8_t *alloc_limit = (uint8_t *)0; + size_t s1 = Frama_C_size_t_interval(0, 2 * UGC_ALLOC_QUANTUM); + size_t s2 = Frama_C_size_t_interval(0, 2 * UGC_ALLOC_QUANTUM); + bool bypass = Frama_C_interval(0, 1); + + (void)ugc_core_alloc(&alloc_ptr, &alloc_limit, s1, false, 8); + + /* Re-establish the context invariant for the non-relational domain: + * at runtime alloc_ptr/alloc_limit are either both null or both point + * into the same quantum (the context_window precondition). */ + if (alloc_ptr == (uint8_t *)0 || alloc_limit == (uint8_t *)0) + { + alloc_ptr = (uint8_t *)0; + alloc_limit = (uint8_t *)0; + } + (void)ugc_core_alloc(&alloc_ptr, &alloc_limit, s2, bypass, 8); + + /* --- Handle store: creation up to exhaustion --- */ + ugc_handle_store_reset(); + + void **h1 = ugc_handle_create(&object_a, Frama_C_interval(0, 12)); + void **h2 = ugc_handle_create_with_extra(&object_a, + Frama_C_interval(0, 12), &object_b); + void **h3 = ugc_handle_create_dependent(&object_a, &object_b); + + if (h1 != (void **)0) + { + (void)ugc_handle_store_contains(h1); + (void)ugc_handle_index(h1); + } + (void)ugc_handle_store_contains(&object_a); + (void)ugc_handle_store_contains((const void *)0); + + /* --- Handle accessors over the whole index range --- */ + size_t idx = Frama_C_size_t_interval(0, UGC_HANDLE_COUNT - 1); + ugc_handle_set_type_at(idx, Frama_C_interval(0, 12)); + (void)ugc_handle_get_type_at(idx); + ugc_handle_set_extra_at(idx, &object_b); + (void)ugc_handle_get_extra_at(idx); + ugc_handle_set_dependent_at(idx, &object_b); + (void)ugc_handle_dependent_slot_at(idx); + + /* --- Handle slot operations --- */ + if (h2 != (void **)0) + { + ugc_handle_slot_store(h2, &object_b); + (void)ugc_handle_slot_store_if_null(h2, &object_a); + (void)ugc_handle_slot_cas(h2, &object_a, &object_b); + } + if (h3 != (void **)0) + { + (void)ugc_handle_slot_store_if_null(h3, &object_a); + } + + ugc_handle_store_reset(); + return 0; +} diff --git a/formal/verify.sh b/formal/verify.sh new file mode 100755 index 0000000..06730a2 --- /dev/null +++ b/formal/verify.sh @@ -0,0 +1,68 @@ +#!/usr/bin/env bash +# uGC formal verification gate (Frama-C). +# +# Runs two analyses over the formally specified core (ugc/core): +# 1. WP - deductive proof of the ACSL contracts (with RTE guards); +# fails unless every goal is discharged. +# 2. Eva - value analysis of formal/eva_main.c driver; fails if any +# alarm (potential undefined behavior) is reported. +# +# Usage: ./formal/verify.sh +# FRAMAC= (default: frama-c) +# WP_TIMEOUT= (default: 60) +# +# Copyright (C) 2026 Demerzel Solutions Limited (Nethermind) +# Author: Maxim Menshikov + +set -uo pipefail + +cd "$(dirname "$0")/.." + +FRAMAC="${FRAMAC:-frama-c}" +WP_TIMEOUT="${WP_TIMEOUT:-60}" +NPROC="$(nproc 2>/dev/null || echo 4)" + +fail=0 + +echo "=== WP: deductive verification of ACSL contracts ===" +wp_out=$("$FRAMAC" -wp -wp-rte \ + -wp-timeout "$WP_TIMEOUT" -wp-par "$NPROC" \ + ugc/core/ugc_core.c 2>&1) +wp_status=$? +echo "$wp_out" | grep -E "Proved goals|Qed:|Alt-Ergo|Timeout|Failed|Unknown" \ + | head -20 + +proved=$(echo "$wp_out" \ + | sed -n 's/.*Proved goals:[[:space:]]*\([0-9][0-9]*\)[[:space:]]*\/[[:space:]]*\([0-9][0-9]*\).*/\1 \2/p') +ok=$(echo "$proved" | awk '{print $1}') +total=$(echo "$proved" | awk '{print $2}') + +if [ "$wp_status" -ne 0 ] || [ -z "$ok" ] || [ -z "$total" ] || \ + [ "$ok" != "$total" ] || [ "$total" = "0" ]; then + echo "WP: FAILED (proved ${ok:-?}/${total:-?} goals)" >&2 + fail=1 +else + echo "WP: OK - all $total goals proved" +fi + +echo "" +echo "=== Eva: absence of runtime errors ===" +eva_out=$("$FRAMAC" -eva -eva-precision 2 \ + formal/eva_main.c ugc/core/ugc_core.c ugc/core/ugc_zalloc.c \ + -cpp-extra-args=-Iugc/core 2>&1) +eva_status=$? +echo "$eva_out" | grep -E "alarm|invalid|coverage|Assertions|Preconditions" \ + | head -20 + +if [ "$eva_status" -ne 0 ] || \ + ! echo "$eva_out" | grep -q "0 alarms generated by the analysis"; then + echo "Eva: FAILED (alarms or analysis error)" >&2 + fail=1 +elif echo "$eva_out" | grep -qE "[1-9][0-9]* invalid"; then + echo "Eva: FAILED (invalid logical properties)" >&2 + fail=1 +else + echo "Eva: OK - no alarms" +fi + +exit $fail From d5398bc214638c16c38010d57aa6ccde2ba237ed Mon Sep 17 00:00:00 2001 From: Maxim Menshikov Date: Wed, 5 Aug 2026 12:01:24 +0100 Subject: [PATCH 4/8] CI: add unit-test and Frama-C verification jobs Run unit tests on ubuntu with no sanitizer, ASan, and UBSan, and run the Frama-C WP + Eva gate in a docker container alongside the riscv64 cross-build. Harden the object-file check to fail when no .obj files are produced, and ignore the build-tests and .frama-c directories. Signed-off-by: Maxim Menshikov --- .github/workflows/ci.yml | 51 +++++++++++++++++++++++++++++++++++++--- .gitignore | 2 ++ 2 files changed, 50 insertions(+), 3 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 1dcac78..4982bbf 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -13,7 +13,51 @@ on: - develop jobs: + unit-tests: + name: Unit tests (${{ matrix.sanitizer }}) + runs-on: ubuntu-latest + strategy: + fail-fast: false + matrix: + sanitizer: [none, address, undefined] + + steps: + - name: Checkout code + uses: actions/checkout@v4 + + - name: Configure + run: | + if [ "${{ matrix.sanitizer }}" != "none" ]; then + export CFLAGS="-fsanitize=${{ matrix.sanitizer }} -fno-sanitize-recover=all -g" + export LDFLAGS="-fsanitize=${{ matrix.sanitizer }}" + fi + cmake -S . -B build-tests -DUGC_BUILD_TESTS=ON -DCMAKE_BUILD_TYPE=Debug + + - name: Build + run: cmake --build build-tests + + - name: Run tests + run: ctest --test-dir build-tests --output-on-failure + + formal-verification: + name: Formal verification (Frama-C) + runs-on: ubuntu-latest + + steps: + - name: Checkout code + uses: actions/checkout@v4 + + - name: Pull Frama-C image + run: docker pull framac/frama-c:30.0 + + - name: Run WP + Eva + run: | + chmod +x formal/verify.sh + docker run --rm -v "$PWD":/work -w /work framac/frama-c:30.0 \ + ./formal/verify.sh + build: + name: Cross-build (riscv64) runs-on: ubuntu-latest steps: @@ -42,7 +86,8 @@ jobs: - name: Check object files run: | echo "Checking object files..." - ls -lh build/usr/lib/objects/ugc-zero/ + find build/usr/lib/objects/ugc-zero -name '*.obj' | tee objects.txt + test -s objects.txt - name: Upload artifacts uses: actions/upload-artifact@v4 @@ -50,5 +95,5 @@ jobs: name: ugc-riscv64-build path: | build/usr/lib/libugc-zero.a - build/usr/lib/objects/ugc-zero/* - retention-days: 7 \ No newline at end of file + build/usr/lib/objects/ugc-zero/** + retention-days: 7 diff --git a/.gitignore b/.gitignore index cfc89fb..0ea0e27 100644 --- a/.gitignore +++ b/.gitignore @@ -41,4 +41,6 @@ *.dwo /build +/build-tests .DS_Store +/.frama-c From b13f3dacbeb14568e2e6487af976cc52d41e548b Mon Sep 17 00:00:00 2001 From: Maxim Menshikov Date: Wed, 5 Aug 2026 12:01:30 +0100 Subject: [PATCH 5/8] README: document architecture, testing, and formal verification Describe the ACSL-specified C core, host-side unit tests, and the Frama-C verification gate (WP + Eva) added in recent commits, including local run instructions via Docker. Signed-off-by: Maxim Menshikov --- README.md | 37 +++++++++++++++++++++++++++++++++++++ 1 file changed, 37 insertions(+) diff --git a/README.md b/README.md index 21a4eb5..5bdff01 100644 --- a/README.md +++ b/README.md @@ -15,6 +15,8 @@ This is a custom GC implementation designed to be used with [Nethermind's **bfla - Zero-dependency static library - Minimal overhead and memory footprint - No actual free() implementation +- Core logic (allocation, handle store) implemented in plain C with ACSL + contracts, formally verified with Frama-C (WP + Eva) ## Building @@ -45,6 +47,41 @@ Then run: ./build.sh ``` +## Architecture + +All non-trivial logic lives in `ugc/core/` as dependency-free C11 code with +ACSL specifications (`ugc_core.h`). The C++ classes implementing the CLR GC +interface (`uGCHeap`, `uGCHandleStore`, `uGCHandleManager`) are thin wrappers +over that core. + +## Testing + +Unit tests cover the core allocator and handle store and run on the host +(no .NET runtime headers required): + +```bash +cmake -S . -B build-tests -DUGC_BUILD_TESTS=ON -DCMAKE_BUILD_TYPE=Debug +cmake --build build-tests +ctest --test-dir build-tests --output-on-failure +``` + +## Formal Verification + +The ACSL contracts of the core are verified with [Frama-C](https://frama-c.com): + +- **WP** proves every contract (with runtime-error guards) deductively; +- **Eva** checks the absence of undefined behavior on a driver that + exercises the core with unconstrained inputs. + +Run the whole gate locally (requires Docker): + +```bash +docker run --rm -v "$PWD":/work -w /work framac/frama-c:30.0 ./formal/verify.sh +``` + +CI fails if a single proof obligation is not discharged or Eva reports any +alarm. + ## License This project is licensed under the terms of MIT license. From 93e1537ddfdb30134bdf086866d975e7a35e6396 Mon Sep 17 00:00:00 2001 From: Maxim Menshikov Date: Wed, 5 Aug 2026 12:01:36 +0100 Subject: [PATCH 6/8] ugc: add prebuilt riscv64 tarball Ship a prebuilt uGC archive for the riscv64 architecture so the library can be deployed on RISC-V targets without building from source. Signed-off-by: Maxim Menshikov --- ugc/uGC-riscv64.tar.gz | Bin 0 -> 29 bytes 1 file changed, 0 insertions(+), 0 deletions(-) create mode 100644 ugc/uGC-riscv64.tar.gz diff --git a/ugc/uGC-riscv64.tar.gz b/ugc/uGC-riscv64.tar.gz new file mode 100644 index 0000000000000000000000000000000000000000..a0e78f0b732927d724f119b0cf9d102114f113ea GIT binary patch literal 29 kcmb2|=3qDw*_Fw_oSY!Rx;R0kCxn4PZ~fNy3@i)`0DYJU9smFU literal 0 HcmV?d00001 From aba6fb2fd7f912e3d798807847ccdef9d2ebefec Mon Sep 17 00:00:00 2001 From: Maxim Menshikov Date: Wed, 5 Aug 2026 12:30:06 +0100 Subject: [PATCH 7/8] HandleStore: recycle destroyed handle slots via a LIFO free stack Handle slots were never reclaimed, so runtime GCHandle churn would exhaust the fixed-capacity store. Add ugc_handle_destroy_at, which scrubs the slot, guards against double destroy, and pushes the index on a free stack popped before the array grows; wire it into the manager's destroy paths, give dependent handles a HandleType, and extend the ACSL contracts, unit tests, and Eva harness. Signed-off-by: Maxim Menshikov --- formal/eva_main.c | 8 +- tests/test_core_handles.c | 92 ++++++++++++++++++- ugc/core/ugc_core.c | 105 +++++++++++++++++---- ugc/core/ugc_core.h | 189 +++++++++++++++++++++++++++++++------- ugc/uGCHandleManager.cpp | 14 ++- ugc/uGCHandleStore.cpp | 11 ++- ugc/uGCHandleStore.h | 1 + 7 files changed, 366 insertions(+), 54 deletions(-) diff --git a/formal/eva_main.c b/formal/eva_main.c index ec7c614..4bb70ec 100644 --- a/formal/eva_main.c +++ b/formal/eva_main.c @@ -47,12 +47,18 @@ main(void) void **h1 = ugc_handle_create(&object_a, Frama_C_interval(0, 12)); void **h2 = ugc_handle_create_with_extra(&object_a, Frama_C_interval(0, 12), &object_b); - void **h3 = ugc_handle_create_dependent(&object_a, &object_b); + void **h3 = ugc_handle_create_dependent(&object_a, &object_b, + Frama_C_interval(0, 12)); if (h1 != (void **)0) { (void)ugc_handle_store_contains(h1); (void)ugc_handle_index(h1); + + /* --- Destroy + recycle: double destroy must be harmless --- */ + ugc_handle_destroy_at(ugc_handle_index(h1)); + ugc_handle_destroy_at(ugc_handle_index(h1)); + h1 = ugc_handle_create(&object_b, Frama_C_interval(0, 12)); } (void)ugc_handle_store_contains(&object_a); (void)ugc_handle_store_contains((const void *)0); diff --git a/tests/test_core_handles.c b/tests/test_core_handles.c index 27fcc5c..9bf0fce 100644 --- a/tests/test_core_handles.c +++ b/tests/test_core_handles.c @@ -61,9 +61,11 @@ test_dependent_handles(void) void **slot; ugc_handle_store_reset(); - h = ugc_handle_create_dependent(&obj_a, &obj_b); + h = ugc_handle_create_dependent(&obj_a, &obj_b, 6); CHECK(h != NULL); CHECK(*h == &obj_a); + /* Dependent handles must carry their HandleType (HNDTYPE_DEPENDENT) */ + CHECK(ugc_handle_get_type_at(ugc_handle_index(h)) == 6); slot = ugc_handle_dependent_slot_at(ugc_handle_index(h)); CHECK(slot != NULL); CHECK(*slot == &obj_b); @@ -122,12 +124,95 @@ test_store_exhaustion(void) * the count */ CHECK(ugc_handle_create(&obj_b, 0) == NULL); CHECK(ugc_handle_create_with_extra(&obj_b, 0, &extra_a) == NULL); - CHECK(ugc_handle_create_dependent(&obj_b, &obj_c) == NULL); + CHECK(ugc_handle_create_dependent(&obj_b, &obj_c, 6) == NULL); CHECK(ugc_handle_count == UGC_HANDLE_COUNT); + /* Destroying a handle makes room again: the freed slot is recycled */ + ugc_handle_destroy_at(0); + h = ugc_handle_create(&obj_b, 3); + CHECK(h == &ugc_handles[0]); + CHECK(*h == &obj_b); + CHECK(ugc_handle_create(&obj_c, 0) == NULL); ugc_handle_store_reset(); CHECK(ugc_handle_count == 0); } +static void +test_destroy_and_reuse(void) +{ + void **h1, **h2, **h3; + + ugc_handle_store_reset(); + h1 = ugc_handle_create_with_extra(&obj_a, 1, &extra_a); + h2 = ugc_handle_create_dependent(&obj_b, &obj_c, 6); + CHECK(h1 != NULL && h2 != NULL); + + /* Destroy scrubs the slot completely */ + ugc_handle_destroy_at(ugc_handle_index(h1)); + CHECK(*h1 == NULL); + CHECK(ugc_handle_get_type_at(ugc_handle_index(h1)) == + UGC_HANDLE_TYPE_FREE); + CHECK(ugc_handle_get_extra_at(ugc_handle_index(h1)) == NULL); + CHECK(ugc_handle_free_count == 1); + + /* The freed slot is recycled (LIFO) and carries no stale state */ + h3 = ugc_handle_create(&obj_c, 2); + CHECK(h3 == h1); + CHECK(*h3 == &obj_c); + CHECK(ugc_handle_get_type_at(ugc_handle_index(h3)) == 2); + CHECK(ugc_handle_get_extra_at(ugc_handle_index(h3)) == NULL); + CHECK(*ugc_handle_dependent_slot_at(ugc_handle_index(h3)) == NULL); + CHECK(ugc_handle_free_count == 0); + CHECK(ugc_handle_count == 2); +} + +static void +test_double_destroy(void) +{ + void **h1, **h2; + + ugc_handle_store_reset(); + h1 = ugc_handle_create(&obj_a, 1); + CHECK(h1 != NULL); + + ugc_handle_destroy_at(ugc_handle_index(h1)); + CHECK(ugc_handle_free_count == 1); + /* A double destroy must not push the same index twice */ + ugc_handle_destroy_at(ugc_handle_index(h1)); + CHECK(ugc_handle_free_count == 1); + + /* ... otherwise two creates would alias the same slot */ + h1 = ugc_handle_create(&obj_b, 2); + h2 = ugc_handle_create(&obj_c, 3); + CHECK(h1 != NULL && h2 != NULL); + CHECK(h1 != h2); + CHECK(*h1 == &obj_b); + CHECK(*h2 == &obj_c); +} + +static void +test_destroy_lifo_order(void) +{ + void **h1, **h2, **h3, **r1, **r2; + + ugc_handle_store_reset(); + h1 = ugc_handle_create(&obj_a, 1); + h2 = ugc_handle_create(&obj_b, 1); + h3 = ugc_handle_create(&obj_c, 1); + CHECK(h1 != NULL && h2 != NULL && h3 != NULL); + + ugc_handle_destroy_at(ugc_handle_index(h1)); + ugc_handle_destroy_at(ugc_handle_index(h3)); + CHECK(ugc_handle_free_count == 2); + + /* Most recently destroyed slot is reused first */ + r1 = ugc_handle_create(&obj_a, 1); + CHECK(r1 == h3); + r2 = ugc_handle_create(&obj_a, 1); + CHECK(r2 == h1); + CHECK(ugc_handle_free_count == 0); + CHECK(ugc_handle_count == 3); +} + static void test_slot_store(void) { @@ -173,6 +258,9 @@ main(void) RUN_TEST(test_set_type_and_extra); RUN_TEST(test_contains); RUN_TEST(test_store_exhaustion); + RUN_TEST(test_destroy_and_reuse); + RUN_TEST(test_double_destroy); + RUN_TEST(test_destroy_lifo_order); RUN_TEST(test_slot_store); RUN_TEST(test_slot_store_if_null); RUN_TEST(test_slot_cas); diff --git a/ugc/core/ugc_core.c b/ugc/core/ugc_core.c index 0e55c1c..af9e83d 100644 --- a/ugc/core/ugc_core.c +++ b/ugc/core/ugc_core.c @@ -9,10 +9,12 @@ #include "ugc_core.h" int ugc_handle_count = 0; +int ugc_handle_free_count = 0; void *ugc_handles[UGC_HANDLE_COUNT] = { 0 }; int ugc_handle_types[UGC_HANDLE_COUNT] = { 0 }; void *ugc_handle_extra[UGC_HANDLE_COUNT] = { 0 }; void *ugc_handle_dependent[UGC_HANDLE_COUNT] = { 0 }; +int ugc_handle_free_stack[UGC_HANDLE_COUNT] = { 0 }; /* Direct path: allocate object + header straight from the zeroing * allocator, bypassing any allocation context. */ @@ -131,38 +133,105 @@ ugc_handle_store_contains(const void *hndl) return handle >= handleStart && handle < handleEnd; } +/* Take the index of a slot for a new handle: pop the most recently + * destroyed slot if one exists (LIFO keeps the touched-memory footprint + * small - a property that matters in a zkVM, where every newly touched + * page has a proving cost), otherwise grow the array. */ +/*@ + requires ugc_store_consistent; + assigns ugc_handle_count, ugc_handle_free_count; + ensures ugc_store_consistent; + + behavior full: + assumes ugc_handle_free_count == 0 && + ugc_handle_count == UGC_HANDLE_COUNT; + assigns \nothing; + ensures \result == -1; + ensures ugc_handle_count == \old(ugc_handle_count); + ensures ugc_handle_free_count == \old(ugc_handle_free_count); + + behavior recycled: + assumes ugc_handle_free_count > 0; + ensures ugc_handle_free_count == \old(ugc_handle_free_count) - 1; + ensures ugc_handle_count == \old(ugc_handle_count); + ensures \result == ugc_handle_free_stack[ugc_handle_free_count]; + ensures 0 <= \result < ugc_handle_count; + + behavior fresh: + assumes ugc_handle_free_count == 0 && + ugc_handle_count < UGC_HANDLE_COUNT; + ensures \result == \old(ugc_handle_count); + ensures ugc_handle_count == \old(ugc_handle_count) + 1; + ensures ugc_handle_free_count == 0; + ensures 0 <= \result < ugc_handle_count; + + complete behaviors; + disjoint behaviors; +*/ +static int +ugc_handle_slot_acquire(void) +{ + if (ugc_handle_free_count > 0) + return ugc_handle_free_stack[--ugc_handle_free_count]; + if (ugc_handle_count < UGC_HANDLE_COUNT) + return ugc_handle_count++; + return -1; +} + void ** ugc_handle_create(void *object, int type) { - if (ugc_handle_count == UGC_HANDLE_COUNT) + int idx = ugc_handle_slot_acquire(); + if (idx < 0) return (void **)0; - ugc_handles[ugc_handle_count] = object; - ugc_handle_types[ugc_handle_count] = type; - return &ugc_handles[ugc_handle_count++]; + ugc_handles[idx] = object; + ugc_handle_types[idx] = type; + ugc_handle_extra[idx] = (void *)0; /* scrub recycled slot state */ + ugc_handle_dependent[idx] = (void *)0; + return &ugc_handles[idx]; } void ** ugc_handle_create_with_extra(void *object, int type, void *extra) { - if (ugc_handle_count == UGC_HANDLE_COUNT) + int idx = ugc_handle_slot_acquire(); + if (idx < 0) return (void **)0; - ugc_handles[ugc_handle_count] = object; - ugc_handle_types[ugc_handle_count] = type; - ugc_handle_extra[ugc_handle_count] = extra; - return &ugc_handles[ugc_handle_count++]; + ugc_handles[idx] = object; + ugc_handle_types[idx] = type; + ugc_handle_extra[idx] = extra; + ugc_handle_dependent[idx] = (void *)0; + return &ugc_handles[idx]; } void ** -ugc_handle_create_dependent(void *primary, void *secondary) +ugc_handle_create_dependent(void *primary, void *secondary, int type) { - if (ugc_handle_count == UGC_HANDLE_COUNT) + int idx = ugc_handle_slot_acquire(); + if (idx < 0) return (void **)0; - ugc_handles[ugc_handle_count] = primary; - ugc_handle_dependent[ugc_handle_count] = secondary; - return &ugc_handles[ugc_handle_count++]; + ugc_handles[idx] = primary; + ugc_handle_types[idx] = type; + ugc_handle_extra[idx] = (void *)0; + ugc_handle_dependent[idx] = secondary; + return &ugc_handles[idx]; +} + +void +ugc_handle_destroy_at(size_t idx) +{ + if (ugc_handle_types[idx] < 0 || + ugc_handle_free_count == UGC_HANDLE_COUNT) + return; /* double destroy: never push the same index twice */ + + ugc_handles[idx] = (void *)0; + ugc_handle_types[idx] = UGC_HANDLE_TYPE_FREE; + ugc_handle_extra[idx] = (void *)0; + ugc_handle_dependent[idx] = (void *)0; + ugc_handle_free_stack[ugc_handle_free_count++] = (int)idx; } size_t @@ -217,12 +286,14 @@ ugc_handle_store_reset(void) ugc_handles[k] == \null && ugc_handle_types[k] == 0 && ugc_handle_extra[k] == \null && - ugc_handle_dependent[k] == \null; + ugc_handle_dependent[k] == \null && + ugc_handle_free_stack[k] == 0; loop assigns i, ugc_handles[0 .. UGC_HANDLE_COUNT - 1], ugc_handle_types[0 .. UGC_HANDLE_COUNT - 1], ugc_handle_extra[0 .. UGC_HANDLE_COUNT - 1], - ugc_handle_dependent[0 .. UGC_HANDLE_COUNT - 1]; + ugc_handle_dependent[0 .. UGC_HANDLE_COUNT - 1], + ugc_handle_free_stack[0 .. UGC_HANDLE_COUNT - 1]; loop variant UGC_HANDLE_COUNT - i; */ for (int i = 0; i < UGC_HANDLE_COUNT; i++) @@ -231,8 +302,10 @@ ugc_handle_store_reset(void) ugc_handle_types[i] = 0; ugc_handle_extra[i] = (void *)0; ugc_handle_dependent[i] = (void *)0; + ugc_handle_free_stack[i] = 0; } ugc_handle_count = 0; + ugc_handle_free_count = 0; } void diff --git a/ugc/core/ugc_core.h b/ugc/core/ugc_core.h index ccd50bf..b742693 100644 --- a/ugc/core/ugc_core.h +++ b/ugc/core/ugc_core.h @@ -38,6 +38,12 @@ extern "C" { /** Capacity of the global handle store */ #define UGC_HANDLE_COUNT 65535 +/** Type marker of a destroyed (recyclable) handle slot. Live handles always + * carry a non-negative HandleType, so a negative type unambiguously tags a + * slot that sits on the free stack; ugc_handle_destroy_at uses it to make + * a double destroy harmless instead of corrupting the free stack. */ +#define UGC_HANDLE_TYPE_FREE (-1) + /* * --------------------------------------------------------------------------- * Abstract zeroing allocator @@ -144,21 +150,32 @@ uint8_t *ugc_core_alloc(uint8_t **alloc_ptr_p, uint8_t **alloc_limit_p, * --------------------------------------------------------------------------- * A handle is a pointer to a slot of ugc_handles. Parallel arrays keep the * handle type, the extra info and the dependent-handle secondary object. - * Handles are never destroyed (this GC never frees anything), so the store - * is a monotonically growing array. + * + * Unlike object memory (which this GC never reclaims), handle slots ARE + * recycled: the runtime churns through GCHandle/WeakReference handles fast + * enough that a monotonically growing store would exhaust its fixed capacity. + * Destroyed slots are pushed on an explicit free stack (LIFO) and popped + * before the array is grown, so the live-handle high-water mark - not the + * total number of handles ever created - bounds memory use. Single-threaded + * by design (zkVM target has one hart): no atomics, no locks. */ extern int ugc_handle_count; +extern int ugc_handle_free_count; extern void *ugc_handles[UGC_HANDLE_COUNT]; extern int ugc_handle_types[UGC_HANDLE_COUNT]; extern void *ugc_handle_extra[UGC_HANDLE_COUNT]; extern void *ugc_handle_dependent[UGC_HANDLE_COUNT]; +extern int ugc_handle_free_stack[UGC_HANDLE_COUNT]; /*@ predicate ugc_valid_slot(void **h) = \exists integer i; 0 <= i < UGC_HANDLE_COUNT && h == &ugc_handles[i]; predicate ugc_store_consistent = - 0 <= ugc_handle_count <= UGC_HANDLE_COUNT; + 0 <= ugc_handle_count <= UGC_HANDLE_COUNT && + 0 <= ugc_handle_free_count <= UGC_HANDLE_COUNT && + (\forall integer k; 0 <= k < ugc_handle_free_count ==> + 0 <= ugc_handle_free_stack[k] < ugc_handle_count); */ /** @@ -176,21 +193,42 @@ bool ugc_handle_store_contains(const void *hndl); /*@ requires ugc_store_consistent; - assigns ugc_handle_count, - ugc_handles[ugc_handle_count], - ugc_handle_types[ugc_handle_count]; + requires type_live: 0 <= type; + assigns ugc_handle_count, ugc_handle_free_count, + ugc_handles[0 .. UGC_HANDLE_COUNT - 1], + ugc_handle_types[0 .. UGC_HANDLE_COUNT - 1], + ugc_handle_extra[0 .. UGC_HANDLE_COUNT - 1], + ugc_handle_dependent[0 .. UGC_HANDLE_COUNT - 1]; + ensures ugc_store_consistent; behavior full: - assumes ugc_handle_count == UGC_HANDLE_COUNT; - assigns \nothing; + assumes ugc_handle_free_count == 0 && + ugc_handle_count == UGC_HANDLE_COUNT; ensures \result == \null; - - behavior ok: - assumes ugc_handle_count < UGC_HANDLE_COUNT; + ensures ugc_handle_count == \old(ugc_handle_count); + ensures ugc_handle_free_count == \old(ugc_handle_free_count); + + behavior recycled: + assumes ugc_handle_free_count > 0; + ensures ugc_handle_free_count == \old(ugc_handle_free_count) - 1; + ensures ugc_handle_count == \old(ugc_handle_count); + ensures \let i = ugc_handle_free_stack[ugc_handle_free_count]; + \result == &ugc_handles[i] && + ugc_handles[i] == object && + ugc_handle_types[i] == type && + ugc_handle_extra[i] == \null && + ugc_handle_dependent[i] == \null; + + behavior fresh: + assumes ugc_handle_free_count == 0 && + ugc_handle_count < UGC_HANDLE_COUNT; ensures \result == &ugc_handles[\old(ugc_handle_count)]; ensures ugc_handles[\old(ugc_handle_count)] == object; ensures ugc_handle_types[\old(ugc_handle_count)] == type; + ensures ugc_handle_extra[\old(ugc_handle_count)] == \null; + ensures ugc_handle_dependent[\old(ugc_handle_count)] == \null; ensures ugc_handle_count == \old(ugc_handle_count) + 1; + ensures ugc_handle_free_count == 0; complete behaviors; disjoint behaviors; @@ -199,51 +237,134 @@ void **ugc_handle_create(void *object, int type); /*@ requires ugc_store_consistent; - assigns ugc_handle_count, - ugc_handles[ugc_handle_count], - ugc_handle_types[ugc_handle_count], - ugc_handle_extra[ugc_handle_count]; + requires type_live: 0 <= type; + assigns ugc_handle_count, ugc_handle_free_count, + ugc_handles[0 .. UGC_HANDLE_COUNT - 1], + ugc_handle_types[0 .. UGC_HANDLE_COUNT - 1], + ugc_handle_extra[0 .. UGC_HANDLE_COUNT - 1], + ugc_handle_dependent[0 .. UGC_HANDLE_COUNT - 1]; + ensures ugc_store_consistent; behavior full: - assumes ugc_handle_count == UGC_HANDLE_COUNT; - assigns \nothing; + assumes ugc_handle_free_count == 0 && + ugc_handle_count == UGC_HANDLE_COUNT; ensures \result == \null; - - behavior ok: - assumes ugc_handle_count < UGC_HANDLE_COUNT; + ensures ugc_handle_count == \old(ugc_handle_count); + ensures ugc_handle_free_count == \old(ugc_handle_free_count); + + behavior recycled: + assumes ugc_handle_free_count > 0; + ensures ugc_handle_free_count == \old(ugc_handle_free_count) - 1; + ensures ugc_handle_count == \old(ugc_handle_count); + ensures \let i = ugc_handle_free_stack[ugc_handle_free_count]; + \result == &ugc_handles[i] && + ugc_handles[i] == object && + ugc_handle_types[i] == type && + ugc_handle_extra[i] == extra && + ugc_handle_dependent[i] == \null; + + behavior fresh: + assumes ugc_handle_free_count == 0 && + ugc_handle_count < UGC_HANDLE_COUNT; ensures \result == &ugc_handles[\old(ugc_handle_count)]; ensures ugc_handles[\old(ugc_handle_count)] == object; ensures ugc_handle_types[\old(ugc_handle_count)] == type; ensures ugc_handle_extra[\old(ugc_handle_count)] == extra; + ensures ugc_handle_dependent[\old(ugc_handle_count)] == \null; ensures ugc_handle_count == \old(ugc_handle_count) + 1; + ensures ugc_handle_free_count == 0; complete behaviors; disjoint behaviors; */ void **ugc_handle_create_with_extra(void *object, int type, void *extra); +/* + * Dependent handles now record their HandleType (HNDTYPE_DEPENDENT) like + * every other kind: the EE's HandleFetchType must be able to classify them + * (ZeroGC does the same via HNDTYPE_DEPENDENT on AllocSlot). + */ /*@ requires ugc_store_consistent; - assigns ugc_handle_count, - ugc_handles[ugc_handle_count], - ugc_handle_dependent[ugc_handle_count]; + requires type_live: 0 <= type; + assigns ugc_handle_count, ugc_handle_free_count, + ugc_handles[0 .. UGC_HANDLE_COUNT - 1], + ugc_handle_types[0 .. UGC_HANDLE_COUNT - 1], + ugc_handle_extra[0 .. UGC_HANDLE_COUNT - 1], + ugc_handle_dependent[0 .. UGC_HANDLE_COUNT - 1]; + ensures ugc_store_consistent; behavior full: - assumes ugc_handle_count == UGC_HANDLE_COUNT; - assigns \nothing; + assumes ugc_handle_free_count == 0 && + ugc_handle_count == UGC_HANDLE_COUNT; ensures \result == \null; - - behavior ok: - assumes ugc_handle_count < UGC_HANDLE_COUNT; + ensures ugc_handle_count == \old(ugc_handle_count); + ensures ugc_handle_free_count == \old(ugc_handle_free_count); + + behavior recycled: + assumes ugc_handle_free_count > 0; + ensures ugc_handle_free_count == \old(ugc_handle_free_count) - 1; + ensures ugc_handle_count == \old(ugc_handle_count); + ensures \let i = ugc_handle_free_stack[ugc_handle_free_count]; + \result == &ugc_handles[i] && + ugc_handles[i] == primary && + ugc_handle_types[i] == type && + ugc_handle_extra[i] == \null && + ugc_handle_dependent[i] == secondary; + + behavior fresh: + assumes ugc_handle_free_count == 0 && + ugc_handle_count < UGC_HANDLE_COUNT; ensures \result == &ugc_handles[\old(ugc_handle_count)]; ensures ugc_handles[\old(ugc_handle_count)] == primary; + ensures ugc_handle_types[\old(ugc_handle_count)] == type; + ensures ugc_handle_extra[\old(ugc_handle_count)] == \null; ensures ugc_handle_dependent[\old(ugc_handle_count)] == secondary; ensures ugc_handle_count == \old(ugc_handle_count) + 1; + ensures ugc_handle_free_count == 0; + + complete behaviors; + disjoint behaviors; +*/ +void **ugc_handle_create_dependent(void *primary, void *secondary, int type); + +/** + * Destroy the handle slot at idx and make it available for reuse. + * + * The slot is fully scrubbed (object, type, extra, secondary) so a later + * recycled create never leaks stale state, and its index is pushed on the + * free stack. A slot whose type is already negative (== destroyed) is left + * untouched: a double destroy must not push the same index twice, or two + * later creates would hand out aliasing handles. + */ +/*@ + requires ugc_store_consistent; + requires valid_index: 0 <= idx < ugc_handle_count; + assigns ugc_handle_free_count, + ugc_handle_free_stack[0 .. UGC_HANDLE_COUNT - 1], + ugc_handles[idx], ugc_handle_types[idx], + ugc_handle_extra[idx], ugc_handle_dependent[idx]; + ensures ugc_store_consistent; + + behavior already_free: + assumes ugc_handle_types[idx] < 0 || + ugc_handle_free_count == UGC_HANDLE_COUNT; + assigns \nothing; + + behavior freed: + assumes ugc_handle_types[idx] >= 0 && + ugc_handle_free_count < UGC_HANDLE_COUNT; + ensures ugc_handles[idx] == \null; + ensures ugc_handle_types[idx] == UGC_HANDLE_TYPE_FREE; + ensures ugc_handle_extra[idx] == \null; + ensures ugc_handle_dependent[idx] == \null; + ensures ugc_handle_free_count == \old(ugc_handle_free_count) + 1; + ensures ugc_handle_free_stack[\old(ugc_handle_free_count)] == idx; complete behaviors; disjoint behaviors; */ -void **ugc_handle_create_dependent(void *primary, void *secondary); +void ugc_handle_destroy_at(size_t idx); /** * Convert a handle (a pointer to a slot of ugc_handles) into its index. @@ -304,17 +425,21 @@ void *ugc_handle_get_extra_at(size_t idx); void ugc_handle_set_extra_at(size_t idx, void *extra); /*@ - assigns ugc_handle_count, + assigns ugc_handle_count, ugc_handle_free_count, ugc_handles[0 .. UGC_HANDLE_COUNT - 1], ugc_handle_types[0 .. UGC_HANDLE_COUNT - 1], ugc_handle_extra[0 .. UGC_HANDLE_COUNT - 1], - ugc_handle_dependent[0 .. UGC_HANDLE_COUNT - 1]; + ugc_handle_dependent[0 .. UGC_HANDLE_COUNT - 1], + ugc_handle_free_stack[0 .. UGC_HANDLE_COUNT - 1]; ensures ugc_handle_count == 0; + ensures ugc_handle_free_count == 0; + ensures ugc_store_consistent; ensures \forall integer i; 0 <= i < UGC_HANDLE_COUNT ==> ugc_handles[i] == \null && ugc_handle_types[i] == 0 && ugc_handle_extra[i] == \null && - ugc_handle_dependent[i] == \null; + ugc_handle_dependent[i] == \null && + ugc_handle_free_stack[i] == 0; */ void ugc_handle_store_reset(void); diff --git a/ugc/uGCHandleManager.cpp b/ugc/uGCHandleManager.cpp index dd65170..3e74150 100644 --- a/ugc/uGCHandleManager.cpp +++ b/ugc/uGCHandleManager.cpp @@ -31,7 +31,12 @@ uGCHandleManager::GetGlobalHandleStore() IGCHandleStore * uGCHandleManager::CreateHandleStore() { - return nullptr; + /* Secondary stores (collectible AssemblyLoadContexts) share the global + * static-array-backed store: uGC never unloads anything, so isolation + * between stores buys nothing, and reusing the singleton avoids a heap + * allocation per store. DestroyHandleStore stays a no-op for the same + * reason. */ + return _handleStore; } void @@ -48,17 +53,22 @@ uGCHandleManager::CreateGlobalHandleOfType(Object *object, HandleType type) OBJECTHANDLE uGCHandleManager::CreateDuplicateHandle(OBJECTHANDLE handle) { - return OBJECTHANDLE(); + if (handle == OBJECTHANDLE()) + return OBJECTHANDLE(); + return _handleStore->CreateHandleOfType(*(Object **)handle, + _handleStore->uGetHandleType(handle)); } void uGCHandleManager::DestroyHandleOfType(OBJECTHANDLE handle, HandleType type) { + _handleStore->uDestroyHandle(handle); } void uGCHandleManager::DestroyHandleOfUnknownType(OBJECTHANDLE handle) { + _handleStore->uDestroyHandle(handle); } void diff --git a/ugc/uGCHandleStore.cpp b/ugc/uGCHandleStore.cpp index 57a405b..3871da9 100644 --- a/ugc/uGCHandleStore.cpp +++ b/ugc/uGCHandleStore.cpp @@ -44,7 +44,16 @@ uGCHandleStore::CreateHandleWithExtraInfo(Object *object, HandleType type, OBJECTHANDLE uGCHandleStore::CreateDependentHandle(Object *primary, Object *secondary) { - return (OBJECTHANDLE)ugc_handle_create_dependent(primary, secondary); + return (OBJECTHANDLE)ugc_handle_create_dependent(primary, secondary, + (int)HNDTYPE_DEPENDENT); +} + +void +uGCHandleStore::uDestroyHandle(OBJECTHANDLE hndl) +{ + if (!ugc_handle_store_contains((const void *)hndl)) + return; + ugc_handle_destroy_at(ugc_handle_index((void **)hndl)); } OBJECTHANDLE diff --git a/ugc/uGCHandleStore.h b/ugc/uGCHandleStore.h index 18f7228..bb512be 100644 --- a/ugc/uGCHandleStore.h +++ b/ugc/uGCHandleStore.h @@ -27,6 +27,7 @@ class uGCHandleStore : public IGCHandleStore virtual ~uGCHandleStore() {}; + void uDestroyHandle(OBJECTHANDLE hndl); OBJECTHANDLE uGetDependentHandle(OBJECTHANDLE hndl); void uSetDependentHandle(OBJECTHANDLE hndl, Object *secondary); HandleType uGetHandleType(OBJECTHANDLE hndl); From 11f04f95cace44ec4642eae8c78091597c273696 Mon Sep 17 00:00:00 2001 From: Maxim Menshikov Date: Wed, 5 Aug 2026 12:30:14 +0100 Subject: [PATCH 8/8] uGCHeap: track allocated bytes and fix stubbed API return values Count bytes served by the slow-path Alloc (including per-context SOH/UOH counters) and report them from GetTotalAllocatedBytes, GetTotalBytesInUse, GetCurrentObjSize and GetMemoryInfo. Correct stub returns the BCL depends on: MaxGeneration is 2, RegisterForFinalization and IsPromoted succeed, WaitForFullGC* report not-applicable, and GetLOHThreshold reports the standard large-object threshold. Signed-off-by: Maxim Menshikov --- ugc/uGCHeap.cpp | 48 ++++++++++++++++++++++++++++++++++++------------ ugc/uGCHeap.h | 7 +++++++ 2 files changed, 43 insertions(+), 12 deletions(-) diff --git a/ugc/uGCHeap.cpp b/ugc/uGCHeap.cpp index 4d094ce..c238bc9 100644 --- a/ugc/uGCHeap.cpp +++ b/ugc/uGCHeap.cpp @@ -108,9 +108,9 @@ uGCHeap::GetMemoryInfo(uint64_t* highMemLoadThresholdBytes, *highMemLoadThresholdBytes = 0; *totalAvailableMemoryBytes = 0; *lastRecordedMemLoadBytes = 0; - *lastRecordedHeapSizeBytes = 0; + *lastRecordedHeapSizeBytes = allocatedBytes; *lastRecordedFragmentationBytes = 0; - *totalCommittedBytes = 0; + *totalCommittedBytes = allocatedBytes; *promotedBytes = 0; *pinnedObjectCount = 0; *finalizationPendingCount = 0; @@ -168,13 +168,15 @@ uGCHeap::CancelFullGCNotification() int uGCHeap::WaitForFullGCApproach(int millisecondsTimeout) { - return 0; + /* Full-GC notifications are never registered (see + * RegisterForFullGCNotification), so "not applicable", not "success". */ + return wait_full_gc_na; } int uGCHeap::WaitForFullGCComplete(int millisecondsTimeout) { - return 0; + return wait_full_gc_na; } unsigned @@ -205,13 +207,13 @@ uGCHeap::EndNoGCRegion() size_t uGCHeap::GetTotalBytesInUse() { - return size_t(); + return (size_t)allocatedBytes; } uint64_t uGCHeap::GetTotalAllocatedBytes() { - return 0; + return allocatedBytes; } HRESULT @@ -223,7 +225,9 @@ uGCHeap::GarbageCollect(int generation, bool low_memory_p, int mode) unsigned uGCHeap::GetMaxGeneration() { - return 1; + /* The BCL sizes per-generation arrays from GC.MaxGeneration and expects + * the standard 2 (gen0/gen1/gen2) even from a non-collecting GC. */ + return 2; } void @@ -234,7 +238,10 @@ uGCHeap::SetFinalizationRun(Object * obj) bool uGCHeap::RegisterForFinalization(int gen, Object * obj) { - return false; + /* Finalizers never run (nothing ever becomes unreachable), but the + * registration itself must "succeed": GC.ReRegisterForFinalize turns a + * false here into an OutOfMemoryException. */ + return true; } int @@ -258,7 +265,8 @@ uGCHeap::Initialize() bool uGCHeap::IsPromoted(Object * object) { - return false; + /* Everything survives forever in a non-collecting GC. */ + return true; } bool @@ -312,7 +320,7 @@ uGCHeap::FixAllocContext(gc_alloc_context* acontext, void* arg, void* heap) size_t uGCHeap::GetCurrentObjSize() { - return size_t(); + return (size_t)allocatedBytes; } void @@ -375,8 +383,22 @@ uGCHeap::Alloc(gc_alloc_context * acontext, size_t size, uint32_t flags) alloc_limit_p = &acontext->alloc_limit; } - return (Object *)ugc_core_alloc(alloc_ptr_p, alloc_limit_p, size, + Object *obj = (Object *)ugc_core_alloc(alloc_ptr_p, alloc_limit_p, size, (flags & GC_ALLOC_USER_OLD_HEAP) != 0, sizeof(ObjHeader)); + if (obj != nullptr) + { + allocatedBytes += size; + if (acontext != nullptr) + { + /* GC.GetTotalAllocatedBytes(precise: true) sums these per-context + * counters; keep the SOH/UOH split the interface defines. */ + if ((flags & GC_ALLOC_USER_OLD_HEAP) != 0) + acontext->alloc_bytes_uoh += (int64_t)size; + else + acontext->alloc_bytes += (int64_t)size; + } + } + return obj; } void @@ -565,7 +587,9 @@ uGCHeap::GetGenerationBudget(int generation) size_t uGCHeap::GetLOHThreshold() { - return 0; + /* Report the standard threshold instead of 0 so managed callers that + * branch on it (array pooling, GC.GetConfiguration) see sane values. */ + return LARGE_OBJECT_SIZE; } void diff --git a/ugc/uGCHeap.h b/ugc/uGCHeap.h index 1b4ebb2..0fcc03d 100644 --- a/ugc/uGCHeap.h +++ b/ugc/uGCHeap.h @@ -16,12 +16,19 @@ class uGCHeap : public IGCHeap private: IGCToCLR* gcToCLR; int registeredSegments; + /* Bytes of objects served by Alloc (the slow path). The runtime's inline + * fast path bump-allocates within the context window without calling + * back, so this undercounts total allocation volume - but it is exact + * for the slow path, deterministic, and costs one plain add (the zkVM + * target is single-hart, so no atomics needed). */ + uint64_t allocatedBytes; public: uGCHeap(IGCToCLR* gcToCLR) { this->gcToCLR = gcToCLR; this->registeredSegments = 0; + this->allocatedBytes = 0; } /* Hosting APIs */