docs: GC soundness proof — ref counting is complete for IC#42
Open
gavlooth wants to merge 6 commits intoHigherOrderCO:mainfrom
Open
docs: GC soundness proof — ref counting is complete for IC#42gavlooth wants to merge 6 commits intoHigherOrderCO:mainfrom
gavlooth wants to merge 6 commits intoHigherOrderCO:mainfrom
Conversation
Introduces two features that enable iterative HVM4 programs (like Bellman-Ford with early termination) to run without exhausting heap: 1. @compact(term): Normalizes term to SNF, then deep-copies the result tree to fresh heap positions. Safe to call from any evaluation context (inside WNF, nested in expressions) because it never modifies existing heap data. Enables iterative algorithms to shed accumulated evaluation intermediates between rounds. 2. Per-thread, size-segregated free lists (sizes 1-16): Freed heap blocks are recycled via LIFO free lists, checked first by heap_alloc before bump-allocating. heap_free calls added to all interaction handlers (APP-LAM, DUP-NOD, DUP-SUP, MAT-CTR, MAT-NUM, OP2, EQL, etc.). Disabled in multi-threaded mode to avoid cross-thread races. Also includes OP2-NUM fast path (skip frame push when both operands are already NUM) and dup_nod split allocation (3 separate allocs instead of one block, enabling free-list reuse of smaller sizes). Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Analyze BOOK terms after parsing to compute program hints (node count, SUP/DUP presence, max depth, arity stats). Use hints to right-size all runtime buffers instead of hardcoded compile-time capacities — reducing memory footprint from GBs to KBs for small programs while still handling large ones via dynamic growth. Key changes: - analyze/hints.c: O(N) post-parse analysis producing HvmHints - data/wsq.c: resizable Chase-Lev deque (WsqArray indirection, 2x growth) - data/wspq.c: dynamic bracket count and per-bucket capacity - data/uset.c: sized initialization from hints instead of HEAP_CAP - data/elastic_ring.c: ouroboros double-map ring buffer with elastic growth/shrink via memfd_create (Linux) / shm_open (macOS) - eval/normalize.c, eval/collapse.c, cnf/_.c: hint-based buffer sizing - main.c: -v flag for hints output, --test-ring for ring self-test Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Standalone data structure for future Hybrid SIV + Ring work queues. Dense swap-compacted array with stable IDs, separate data/ID capacity growth, and O(1) push/erase/valid/get operations. Self-test via --test-siv flag. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Leverage fd data persistence across ftruncate+remap: on growth, existing data at fd offsets [0, old_cap) survives the extend. Only the wrapped prefix (if any) needs a memcpy within the mapping. On shrink, compact live data to offset 0 with a single memmove before truncating. Removes the malloc/free allocation overhead from the resize hot path. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
elastic_ring.c: - Update header comment to reflect zero-copy growth (was stale) - Add thread-safety notes for future MT integration - Document byte-level alignment contract - Enforce cap/4 threshold in ring_shrink (was documented but not checked) - Add tests: shrink with wrapped data, cap/4 threshold rejection, grow when empty, direct double-map mirror verification siv.c: - Document u32 ID space exhaustion (4B push limit) - Add thread-safety contract for SIV+Ring thief pattern (release/acquire barriers, erase-during-read race) - Add tests: garbage ID rejection (SIV_INVALID, near-max, beyond next_id, erased), independent id_cap vs data_cap growth across 3 push-erase rounds, erase-last-element (no-swap path) Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
This PR adds a formal argument proving that reference counting alone is sufficient for complete garbage collection in HVM4, without cycle detection or tracing GC.
Key Points
DAG Invariant: The heap is always a DAG because nodes can only reference previously-allocated nodes (monotonic allocation order)
No Cycles Possible: A cycle
A₁ → A₂ → ... → A₁would requiret(A₁) > t(A₁), a contradictionRecursion is Unfolding: Recursive definitions like
@Ycreate infinite chains, not circular referencesDUP/SUP is Acyclic: Superposition nodes reference the original (older) computation
Implications
Files Changed
docs/GC_SOUNDNESS.md: Full proof with lemmas, theorem, and discussion of edge cases (recursion, DUP/SUP, FFI)