Six refusals and a trap, each one a way of losing the property

The refusals: the arities, a pool of an owning element, ordering handles,
free of a handle, and clone of a pool. Each names what it would cost — a
cloned pool duplicates the generation counters with the slots, so one handle
would resolve in both copies and name two different things.

pool-stale-region.flan is the other failure, and the point of it is that it
is not the first. A stale handle is an answer and resolve says None; a pool
whose region was released has no slot array left to ask, so it traps. Same
rule that keeps a Vec's generation word and its epoch word apart.
This commit is contained in:
Joseph Ferano 2026-09-13 07:59:04 +07:00
parent e933f5a84c
commit 0837959140
3 changed files with 87 additions and 0 deletions

View File

@ -0,0 +1,25 @@
;;;; The epoch trap on the pool's side. spec-memory.md, "Dev builds detect a
;;;; released region".
;;;;
;;;; This is deliberately the *other* failure from a stale handle, and the two
;;;; must not be conflated — the same rule that keeps a Vec's generation word
;;;; and its epoch word apart. A stale handle is an answer: the entity died,
;;;; resolve says None, the program carries on. A released region is not an
;;;; answer at all: the storage the pool sits in is gone, the slot array with
;;;; it, and there is nothing left to ask. So one returns None and the other
;;;; traps naming the site.
(defn main [] i32
(let [a (arena-new 4096)]
(let [p (pool-new i32 a)]
(let [h (insert p 7)]
(match (resolve p h)
(Some x) (println (deref x))
None (println -1))
;; The region goes. p is still in scope, still looks fine, and h is
;; still a perfectly well-formed handle — which is exactly the case a
;; static rule cannot see.
(free-all a)
(match (resolve p h)
(Some x) (println (deref x))
None (println -1)))))
0)

View File

@ -691,6 +691,41 @@ let () =
end;
(try Sys.remove exe with Sys_error _ -> ());
(* (Handle T) and (Pool T), spec-memory.md. The thesis is one line of this
output and the rest is scaffolding for it: the same slot prints as
<handle 1:1> before a death and <handle 1:3> after the reuse, and the
projectile still holding the first is told -1 rather than the
newcomer's 99. At -O0 as well, because the null test resolve is built
out of is exactly the kind of control flow an optimiser launders, and
as a dev build, because a pool then lives in a frame the reload path
has to agree with on 64 bytes. *)
let handles_out =
"3\n3\n60\n21\ntrue\nfalse\n2\n<handle 1:1>\n<handle 1:3>\nfalse\ntrue\n-1\n99\n3\n3\n<handle 0:0>\n-1\n10\n30\n"
in
outputs "handles" "programs/handles.flan" handles_out;
outputs ~opt:"-O0" "handles, -O0" "programs/handles.flan" handles_out;
outputs ~dev:true "handles, dev" "programs/handles.flan" handles_out;
(* The epoch trap on the pool's side, and it is deliberately the *other*
failure from a stale handle. A stale handle is an answer and resolve
returns None; a released region is not an answer at all, because the
slot array went with the storage, so it traps. The two must not be
conflated, which is the same rule that keeps a Vec's generation word
and its epoch word apart. *)
let exe = compile "programs/pool-stale-region.flan" in
let code, text = run exe None in
if code <> 134 || not (contains text "programs/pool-stale-region.flan:")
|| not (contains text "allocator was released")
|| not (contains text "7")
then begin
incr failures;
Printf.printf
"FAIL a pool used after its region was released\n\
\ got: %S (exit %d)\n wanted: exit 134, naming the site\n"
text code
end;
(try Sys.remove exe with Sys_error _ -> ());
(* The same trap on the Map's side, and it is not the same code path: a
Vec's operations check on the way in and stop there, while a map's get
goes on to call a hash and an equality function through pointers into

View File

@ -835,6 +835,33 @@ let () =
~needle:"exactly two types";
rejects_check "Result is milestone 6" "(defn f [] (Result i32 i32) None)"
~needle:"milestone 6";
(* (Handle T) and (Pool T) are built. What stays refused is the arity, for
the reason Vec's and Map's arities are, and the four shapes below each
of which is a way of losing the one property the type exists to have. *)
rejects_check "Handle takes one type" "(defn f [x (Handle i32 i32)] ())"
~needle:"exactly one type";
rejects_check "Pool takes one type" "(defn f [x (Pool i32 i32)] ())"
~needle:"exactly one type";
(* A pool of an owning element, refused where a Vec of a Vec is refused and
for the same reason: the runtime copies and releases slots bytewise. *)
rejects_check "a pool of a Vec"
"(defn f [x (Pool (Vec i32))] ())" ~needle:"move-only element";
(* Ordering handles would order a slot index, which is a free-list artefact.
Equality is admitted and ordering is not, which is why there are two
predicates in Types rather than one. *)
rejects_check "handles do not order"
"(defn f [a (Handle i32) b (Handle i32)] bool (< a b))"
~needle:"no built-in comparison";
(* free takes the owner. A handle is a copyable number that owns nothing, so
consuming one copy would say nothing about the others which is why a
slot is recycled by (release p h) and not by free. *)
rejects_check "free of a handle"
"(defn f [h (Handle i32)] () (free h))" ~needle:"a handle owns nothing";
(* Cloning a pool would duplicate the generation counters with the slots, so
one handle would resolve in both copies and name two different things. *)
rejects_check "a pool cannot be cloned"
"(defn f [p (Pool i32)] () (let [q (clone p)] (do)))"
~needle:"cannot be cloned";
rejects_check "try is milestone 6" "(defn f [] i32 (try 1))"
~needle:"milestone 6";
(* dotimes and defer are implemented, and a defer in a [let] is now one of