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/.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/.gitignore b/.gitignore index cfc89fb..0ea0e27 100644 --- a/.gitignore +++ b/.gitignore @@ -41,4 +41,6 @@ *.dwo /build +/build-tests .DS_Store +/.frama-c 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/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. 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/formal/eva_main.c b/formal/eva_main.c new file mode 100644 index 0000000..4bb70ec --- /dev/null +++ b/formal/eva_main.c @@ -0,0 +1,89 @@ +/** + * @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, + 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); + + /* --- 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 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..9bf0fce --- /dev/null +++ b/tests/test_core_handles.c @@ -0,0 +1,268 @@ +/** + * @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, 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); + 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, 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) +{ + 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_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); + 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; +} 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..af9e83d --- /dev/null +++ b/ugc/core/ugc_core.c @@ -0,0 +1,336 @@ +/** + * @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; +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. */ +/*@ + 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; +} + +/* 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) +{ + int idx = ugc_handle_slot_acquire(); + if (idx < 0) + return (void **)0; + + 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) +{ + int idx = ugc_handle_slot_acquire(); + if (idx < 0) + return (void **)0; + + 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, int type) +{ + int idx = ugc_handle_slot_acquire(); + if (idx < 0) + return (void **)0; + + 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 +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 && + 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_free_stack[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_free_stack[i] = 0; + } + ugc_handle_count = 0; + ugc_handle_free_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..b742693 --- /dev/null +++ b/ugc/core/ugc_core.h @@ -0,0 +1,506 @@ +/** + * @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 + +/** 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 + * --------------------------------------------------------------------------- + * 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. + * + * 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_free_count <= UGC_HANDLE_COUNT && + (\forall integer k; 0 <= k < ugc_handle_free_count ==> + 0 <= ugc_handle_free_stack[k] < 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; + 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_free_count == 0 && + ugc_handle_count == UGC_HANDLE_COUNT; + ensures \result == \null; + 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; +*/ +void **ugc_handle_create(void *object, int type); + +/*@ + requires ugc_store_consistent; + 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_free_count == 0 && + ugc_handle_count == UGC_HANDLE_COUNT; + ensures \result == \null; + 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; + 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_free_count == 0 && + ugc_handle_count == UGC_HANDLE_COUNT; + ensures \result == \null; + 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_destroy_at(size_t idx); + +/** + * 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_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_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_free_stack[i] == 0; +*/ +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/uGC-riscv64.tar.gz b/ugc/uGC-riscv64.tar.gz new file mode 100644 index 0000000..a0e78f0 Binary files /dev/null and b/ugc/uGC-riscv64.tar.gz differ diff --git a/ugc/uGCHandleManager.cpp b/ugc/uGCHandleManager.cpp index 81ff0d2..3e74150 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() @@ -30,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 @@ -47,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 @@ -77,21 +88,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 +115,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..3871da9 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,78 @@ 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; + return (OBJECTHANDLE)ugc_handle_create_dependent(primary, secondary, + (int)HNDTYPE_DEPENDENT); +} - handles[handlesCount] = primary; - dependentHandles[handlesCount] = secondary; - return (OBJECTHANDLE)&handles[handlesCount++]; +void +uGCHandleStore::uDestroyHandle(OBJECTHANDLE hndl) +{ + if (!ugc_handle_store_contains((const void *)hndl)) + return; + ugc_handle_destroy_at(ugc_handle_index((void **)hndl)); } 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/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); diff --git a/ugc/uGCHeap.cpp b/ugc/uGCHeap.cpp index a89df6c..c238bc9 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 { @@ -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 @@ -361,64 +369,36 @@ 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 */ + /* 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; - return (Object*)(address + 1); + if (acontext != nullptr) + { + alloc_ptr_p = &acontext->alloc_ptr; + alloc_limit_p = &acontext->alloc_limit; } - /* 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) + 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) { - acontext->alloc_ptr = ptr + size; - return (Object*)ptr; + 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; + } } - - /* 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 obj; } void @@ -607,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 */