From 4d10f3c3276e7b6050fe21b83af019e94eef52a2 Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Fri, 25 Sep 2026 10:18:31 +0700 Subject: [PATCH] An allocator outlives the arena arena-destroy hands back, so a container made from it traps on a read of live memory --- TODO.org | 13 ++++++++----- docs/BUILT.md | 7 +++++++ runtime/flan_rt.c | 28 +++++++++++++++++++++++++++- test/programs/destroy-region.flan | 26 ++++++++++++++++++++++++++ test/test_acceptance.ml | 27 +++++++++++++++++++++++++++ test/test_valgrind.ml | 6 +++++- 6 files changed, 100 insertions(+), 7 deletions(-) create mode 100644 test/programs/destroy-region.flan diff --git a/TODO.org b/TODO.org index f9ea5c11..04ccd719 100644 --- a/TODO.org +++ b/TODO.org @@ -1260,11 +1260,14 @@ redefinition module is built separately from its host and nothing makes the two agree on a struct size. Give the reload path a way to carry the build flags and this falls out. -** TODO arena-destroy under a live view reads freed memory -The epoch check that makes free-all safe under a live view does not survive -=arena-destroy=, which frees the block holding the epoch. It happens to trap in -practice because the freed block still holds the bumped value. A question about -=arena-destroy='s ordering, not about views, and the typed side has the same shape. +** DONE arena-destroy under a live view reads freed memory +CLOSED: [2026-09-25] +No ordering of the frees fixes it: the container holds a pointer to the header. +=arena-destroy= now frees the pages and the arena record and retires the +allocator header — epoch bumped, procedure trapping as =DestroyedAllocator=, +never freed — so the stale check reads live memory on every side that makes it. +Rules out freeing the header while any container may hold it. See +docs/BUILT.md, "Three amendments to a frozen spec". ** DONE Map removal costs a backward-shift loop Removal landed, with the loop the spec predicted as its cost. Deferring it was diff --git a/docs/BUILT.md b/docs/BUILT.md index 930c83da..eada520f 100644 --- a/docs/BUILT.md +++ b/docs/BUILT.md @@ -2829,6 +2829,13 @@ handing the pages back only to ask for them again is the unusual one. Taking the the table the spec froze at four names; a second operation does not. The epoch is bumped either way — the pages being the same does not make a container built before the reset valid, which is the whole point of the trap. +`arena-destroy` hands back the pages and the arena record but not the allocator header. A container made from the +arena still holds a pointer to that header and reads the epoch through it on its next operation, so freeing the header +turned the trap into a read of freed memory that happened to see the bumped value (memcheck reported it). The header is +retired instead — epoch bumped, procedure swapped for one that traps as `DestroyedAllocator`, never freed — which costs +one small block per destroyed arena for the life of the process. A second `arena-destroy` of the same allocator does +nothing. + **2. `context/allocator` and `context/temp` are dynamic variables with save and restore, not extra parameters.** The spec says the allocator is "part of the calling convention". The literal reading touches every function signature, the FFI shim, the dev trampolines and the reload ABI, for the same observable behaviour, and it collides with every other diff --git a/runtime/flan_rt.c b/runtime/flan_rt.c index 1332d9f6..d63a5fc1 100644 --- a/runtime/flan_rt.c +++ b/runtime/flan_rt.c @@ -1448,6 +1448,29 @@ flan_allocator *flan_arena_new(int64_t cap) { return a; } +/* What an allocator's procedure becomes once [flan_arena_destroy] has handed + * its arena back. Every request traps, because there is nothing left to serve + * it from and answering NULL would read as exhaustion — which a retry handler + * that raises the budget would then retry for ever. */ +static void *flan_destroyed_proc(flan_allocator *a, int32_t mode, void *p, + int64_t old_size, int64_t size, int64_t align) { + (void)a; (void)mode; (void)p; (void)old_size; (void)size; (void)align; + rt_flush_out(); + fprintf(stderr, + "this allocator was destroyed by arena-destroy, so nothing can be " + "allocated from it or released through it\n"); + rt_trap((const uint8_t *)"DestroyedAllocator", 18); +} + +/* The pages and the arena record go; the allocator itself does not. Every + * container made from it holds this pointer and reads [epoch] through it on + * its next operation — that read is the whole of the stale-region trap — so + * freeing the header would turn the trap into a read of freed memory that + * happens to see the bumped value. The header is retired instead: epoch + * bumped, procedure swapped for one that refuses, never freed. That is one + * small block per destroyed arena, kept for the life of the process. + * + * A second destroy finds the retired procedure and does nothing. */ void flan_arena_destroy(flan_allocator *a) { flan_arena *ar; if (!a || a->proc != flan_arena_proc) return; @@ -1458,7 +1481,10 @@ void flan_arena_destroy(flan_allocator *a) { flan_dev_reg_dead_range(ar->base, ar->cap); free(ar->base); free(ar); - free(a); + a->proc = flan_destroyed_proc; + a->data = NULL; + a->live_blocks = 0; + a->live_bytes = 0; } flan_allocator *flan_heap_allocator(void) { return &flan_heap; } diff --git a/test/programs/destroy-region.flan b/test/programs/destroy-region.flan new file mode 100644 index 00000000..6c2f0f49 --- /dev/null +++ b/test/programs/destroy-region.flan @@ -0,0 +1,26 @@ +;;;; stale-region.flan's trap, reached through arena-destroy rather than +;;;; free-all. The difference is what the check reads: free-all keeps the +;;;; allocator and bumps its epoch, while arena-destroy hands the arena back, +;;;; and a container made from it still points at the allocator to read the +;;;; epoch from. The allocator therefore outlives its arena, so that read is of +;;;; memory that is still there and the trap names the site. +;;;; +;;;; Argument 1 is the other use of a destroyed arena: a new container made +;;;; from it, which has no stale epoch to catch and reaches the allocator +;;;; itself. +(defn main [args [string]] i32 + (let [a (arena-new 4096) + which (if (> (length args) 1) (i32 (bytes->i64 (bytes-view (at args 1)))) 0)] + (if (= which 1) + (do + (arena-destroy a) + (let [w (vec-new i32 a)] + (push w 1) + (println (length w)))) + (let [v (vec-new i32 a)] + (push v 1) + (push v 2) + (println (at v 1)) + (arena-destroy a) + (println (at v 1))))) + 0) diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml index eb357e3b..b67de969 100644 --- a/test/test_acceptance.ml +++ b/test/test_acceptance.ml @@ -1876,6 +1876,33 @@ let () = end; (try Sys.remove exe with Sys_error _ -> ()); + (* The same trap after arena-destroy, which hands the arena back: the + container's allocator pointer has to still be readable for the epoch + check to run at all, so the allocator outlives its arena. A new + container made from the destroyed arena has no stale epoch, and what + stops it is the allocator itself. Both are also clean under memcheck, + which is where reading a freed allocator showed up. *) + let exe = compile "programs/destroy-region.flan" in + let code, text = run exe None in + if code <> 134 || not (contains text "programs/destroy-region.flan:") + || not (contains text "allocator was released") + then begin + incr failures; + Printf.printf + "FAIL a container used after its arena was destroyed\n\ + \ got: %S (exit %d)\n wanted: exit 134, naming the site\n" + text code + end; + let code, text = run exe (Some "1") in + if code <> 134 || not (contains text "destroyed by arena-destroy") then begin + incr failures; + Printf.printf + "FAIL allocating from a destroyed arena\n\ + \ got: %S (exit %d)\n wanted: exit 134, naming arena-destroy\n" + text code + end; + (try Sys.remove exe with Sys_error _ -> ()); + (try Sys.remove exe with Sys_error _ -> ()); diff --git a/test/test_valgrind.ml b/test/test_valgrind.ml index e881581a..d9c882d2 100644 --- a/test/test_valgrind.ml +++ b/test/test_valgrind.ml @@ -186,7 +186,7 @@ let check label path args ~checks = - shadow-pkg.flan, which is a package fragment with no main and does not link on its own. - The seven programs here that abort by design — error, exhausted-unhandled, + The programs here that abort by design — destroy-region, error, exhausted-unhandled, free-all-refused, map-stale-region, slurp-unhandled, stale-region — are kept. A trap is a controlled abort after an fprintf, and "the trap still @@ -246,6 +246,10 @@ let corpus = "programs/slurp.flan", []; "programs/slurp-unhandled.flan", []; "programs/stale-region.flan", []; + (* The same trap after arena-destroy, which read the freed allocator for + its epoch until the allocator was made to outlive its arena. *) + "programs/destroy-region.flan", []; + "programs/destroy-region.flan", [ "1" ]; "programs/string-of-bytes.flan", []; "programs/text.flan", []; "programs/time.flan", [];