A handle answers gone, and a pool can enumerate what is live
This commit is contained in:
commit
05e3c643e4
149
BUILT.md
149
BUILT.md
@ -2510,6 +2510,155 @@ there and matching it from a program. `dev.ml`'s inspector still says "union val
|
||||
frame's locals, and `shim.ml`'s "a Flan union has no C layout" is now inaccurate as prose though the refusal it guards
|
||||
is still right: a union has a C layout and still may not cross to C by value, because the shim flattens aggregates.
|
||||
|
||||
## `(Handle T)` and the pool, which is what a stale reference answers with
|
||||
|
||||
A handle is a reference to something that can die, which reports that it died rather than silently resolving to
|
||||
whatever reused its slot. `check.ml` refused `(Handle T)` by name as milestone 6; this is what it stood for, and the
|
||||
pool came with it because the pool is what makes the report possible.
|
||||
|
||||
The problem is concrete and is not about memory safety. Entities live in a pool; something holds a reference to one —
|
||||
a projectile chasing it, the UI showing its health. The entity dies, the slot is reused, and a raw index now names a
|
||||
different entity. Nothing crashes. The projectile chases the wrong thing, at full speed, for the rest of the game.
|
||||
|
||||
It was built for two reasons, both already recorded. On its own terms, for entities referred to across frames. And
|
||||
because **it is the real gate on managed classes**: plan.org's rule is that nothing starts on `defclass` until
|
||||
ordinary `struct`, `Handle` and reload semantics work, and `Handle` was the only one of the three missing. That is not
|
||||
an incidental precondition — `migrate-instances` has to *enumerate* live instances, and a pool behind generational
|
||||
handles gives that by construction where a world arena and an owned region do not. plan.org presents the three storage
|
||||
strategies as a free choice and they are not.
|
||||
|
||||
`PORTING.md` found no customer for handles in the author's real game today, so this is deliberately the smallest
|
||||
correct thing rather than a rich API: eight names, no iteration protocol, no cursor type, no `clone`.
|
||||
|
||||
### A handle is one i64, and the halves are 32 and 32
|
||||
|
||||
Slot index in the low 32 bits, that slot's generation counter in the high 32. One machine word, so it copies, zeroes
|
||||
and compares like the integer it is, and it **owns nothing** — the pool is the single owner. That is what lets a
|
||||
handle sit in a struct field and in a global where a `Vec` may not, and it is the reason the ownership rules needed no
|
||||
new case: `Types.is_move_only` says yes to `Pool` and no to `Handle`, and the three existing refusals (a struct field,
|
||||
a union case, a global) picked the pool up unchanged with the messages they already had.
|
||||
|
||||
The index is 32 bits because a `Vec`'s index is an `i32` here and widening indices is one change across every
|
||||
container, not a pool question.
|
||||
|
||||
### Live is odd, and two things fall out of it
|
||||
|
||||
A slot's generation starts at 0 and is bumped on every allocation *and* on every release, so an odd generation means
|
||||
live and an even one means dead. Both consequences are load-bearing:
|
||||
|
||||
- **A zeroed handle resolves to nothing.** Generation 0 is even, so ZII gives a `(Handle T)` field the right meaning
|
||||
for free instead of pointing it at slot 0. `handles.flan` prints one: `<handle 0:0>`, and resolving it answers `None`.
|
||||
- **Iteration needs no second array and no spare bit.** Asking whether a slot is live is asking whether its generation
|
||||
is odd.
|
||||
|
||||
### The generation wraps by retiring the slot
|
||||
|
||||
32 bits is 2^31 allocate/release pairs on one slot — every frame at 60fps for a year and a bit. "Rare" is not an
|
||||
answer when the failure it produces is the silent wrong one this type exists to prevent, so a release from generation
|
||||
`0xFFFFFFFF` bumps to 0 and does **not** put the slot back on the free list. The slot is retired: dead forever, its
|
||||
payload leaked, and no future handle can collide with an old one. Leaking is defined behaviour here, and one slot is a
|
||||
bounded price for making the collision unrepresentable rather than unlikely.
|
||||
|
||||
### `resolve` answers `(Option (Ptr T))`, and the spec settled that, not this lane
|
||||
|
||||
The task asked whether a lookup should answer `(Option T)`, matching `(get m k)`. It answers `(Option (Ptr T))`, and
|
||||
`spec-memory.md` already writes it out — its worked example under "Mutating something you matched" is annotated
|
||||
`(Option (Ptr Enemy))` — for the reason given one line above it: *pattern bindings bind values, so a matched struct is
|
||||
a copy*. A copy cannot be written back, and writing to the pooled entity in place is what a pool is for. `(Option T)`
|
||||
would answer a question nobody asked.
|
||||
|
||||
The `Option` half is `get`'s shape and for `get`'s reason: absence is an answer, not a failure. A trap would be wrong
|
||||
here — the entity dying is the *expected* case, not a bug.
|
||||
|
||||
**The hole, said plainly.** A `(Ptr T)` from `resolve` is invalidated by any `insert` that grows the pool, exactly as
|
||||
a slice is invalidated by a `push`. The handle survives that and the pointer does not. This is `spec-memory.md`'s
|
||||
explicit Zig/Odin borrowing contract one level down, and it is worth naming rather than implying, because it
|
||||
reintroduces the silent-wrong-answer mode the handle just removed for anyone who keeps a resolved pointer across an
|
||||
insert. Chunked never-moving storage is the fix and it costs code; taking the contract is the smaller correct thing,
|
||||
given `as-slice` already established it.
|
||||
|
||||
### `len` is the slot high-water and `live` is the count, in that direction
|
||||
|
||||
`(len p)` is how many slots have ever been handed out. `(live p)` is how many of them are live now. It had to be that
|
||||
way round: `0..(len p)` are the indices `(pool-handle p i)` accepts, so a loop bounded by `len` visits every live
|
||||
entry. Bounded by the live count instead, it would silently skip entries the moment anything had been released —
|
||||
which is exactly the quiet wrong answer the whole type exists to remove.
|
||||
|
||||
`(pool-handle p i)` answers `(Option (Handle T))`: the handle of slot `i`, or `None` if that slot is dead. That plus
|
||||
`len` is the whole of iteration. An index outside `0..(len p)` **traps**, exactly as `(at v i)` traps: an index is an
|
||||
index here, and answering `None` for one would hide a bug rather than a death.
|
||||
|
||||
### A slot is released through the pool, and that is not a third release point
|
||||
|
||||
`free` consumes its argument as a move, and a handle is a copyable number that owns nothing — consuming one copy would
|
||||
say nothing about the others. So `(free h)` is refused by name and the release operation is on the owner:
|
||||
`(release p h)`. `spec-memory.md`'s two release points are untouched: `(free p)` is release point 1 applied to the
|
||||
pool, and a `free-all` of the region takes the pool with everything else. `release` recycles a slot inside storage the
|
||||
pool still owns, which is not a release of storage at all.
|
||||
|
||||
It answers `bool` rather than `()`: true if this call released it, false if the handle was already gone. The
|
||||
generational scheme makes a double release **detectable**, and that is worth handing to the caller — this is the one
|
||||
place in the language where freeing something twice is an answer instead of a refusal.
|
||||
|
||||
### Growth is transactional, because `retry` re-attempts the same call
|
||||
|
||||
`StorageExhausted`'s restart re-attempts the *same* request, so a failed grow has to leave the pool byte for byte as
|
||||
it was — including a `cap` that still agrees with the real block sizes, since the next attempt passes `cap` as the
|
||||
allocator's `old_size`. A pool grows two blocks together (payloads and slot headers), so resizing the first in place
|
||||
and then failing on the second would leave `cap` describing neither. So the runtime allocates both, copies, and only
|
||||
then releases the old pair: nothing is mutated after the last thing that can fail. An allocator without `can-free`
|
||||
leaks the first block when the second fails, which is the defined outcome and not a new one — the request failed
|
||||
because the region is exhausted, and the region is about to be released whole or its ceiling raised.
|
||||
|
||||
### Two failures, kept apart
|
||||
|
||||
A stale handle is an **answer**: `resolve` says `None` and the program carries on. A pool whose allocator was released
|
||||
**traps**, through the same epoch check a `Vec` gets — the slot array went with the storage and there is nothing left
|
||||
to ask. `test/programs/pool-stale-region.flan` is that case, and keeping the two apart is the same rule that keeps a
|
||||
`Vec`'s generation word and its epoch word apart: they answer different questions and must not be conflated.
|
||||
|
||||
### Two amendments to a frozen spec
|
||||
|
||||
Both are places where `spec-memory.md` describes a handle doing something that cannot answer "gone", which is the one
|
||||
thing the type exists to do. **This amends it: both are deferred, not built.**
|
||||
|
||||
**1. `.field` and `at` do not auto-deref a handle.** The Places table says `x` may be a struct, a `(Ptr S)` or a
|
||||
`(Handle S)`, and that the two forms auto-deref exactly one pointer *or handle* level. They auto-deref one pointer
|
||||
level and nothing else. A `(set (.hp h) ...)` through a handle has two possible meanings when the entity is dead — trap,
|
||||
or do nothing — and both are worse than the third option, which is the spec's own worked example: resolve first, match,
|
||||
and the compiler makes you handle the `None`. The spec contradicts itself here and the example is the half that is
|
||||
right.
|
||||
|
||||
**2. `deref` is not overloaded on `(Handle a)`.** The Generics section says "`deref` yields a value; `resolve` yields a
|
||||
pointer. Both are overloaded on `(Ptr a)` and `(Handle a)`." `deref` is `(Ptr a)` only. Same reason: `deref` returns a
|
||||
value and has nowhere to put "gone".
|
||||
|
||||
### What this does not have, and one of the gaps is not a pool question
|
||||
|
||||
- **No `clone`.** Refused by name. A copied pool would carry the same slot generations, so one handle would resolve in
|
||||
both copies and name two different things — the exact confusion the type removes. A program that wants a second world
|
||||
builds one and inserts into it, and the new handles say they are new.
|
||||
- **No pool of an owning element.** `(Pool (Vec i32))` is refused where `(Vec (Vec i32))` is refused and for the same
|
||||
reason: the type-erased runtime copies and releases slots bytewise. Recursive teardown arrives with `drop`.
|
||||
- **A handle is not a map key.** For the reason a `Ptr` is not: hashing an identity is a different operation from
|
||||
hashing what it names, and a stale handle hashes the same as it always did while naming nothing.
|
||||
- **Handles compare with `=` and not with `<`.** `Types` grew a second predicate, `is_equatable`, beside
|
||||
`is_comparable`. Two handles are equal exactly when they name the same slot at the same generation, so a stale handle
|
||||
is never equal to the live one that replaced it — that is worth one integer compare. Ordering them would order a slot
|
||||
index, which is a free-list artefact and means nothing.
|
||||
- **A pool passed to a helper is consumed**, because a pool is move-only exactly as a `Vec` is and there is no
|
||||
borrowing parameter in the language. `test/programs/handles.flan` is one long function for that reason, and it does
|
||||
not work around it. This is a pre-existing gap and not a pool question: the same sentence is true of every `Vec` in
|
||||
the tree.
|
||||
|
||||
### What classes still need
|
||||
|
||||
The enumeration primitive is the piece migration was blocked on, and it exists now. What is left is `defclass` itself
|
||||
and its runtime shape metadata; `migrate-instances`, which is a walk over `(len p)` and `(pool-handle p i)`; generic
|
||||
functions and method dispatch, whose expensive half is already built and tested (a generic function is an indirection
|
||||
cell whose body is a dispatch table, and a reload extends the table); and the rule that `Enemy@1` stays resolvable for
|
||||
as long as any instance holds it — the same rule as "nothing is ever `dlclose`d".
|
||||
|
||||
## Macros: the compiler dlopens the program
|
||||
|
||||
"Why there is no interpreter" above decided that the compiled path is the only backend. A macro is the first thing
|
||||
|
||||
62
NEXT.md
62
NEXT.md
@ -58,7 +58,8 @@ of a dead session. Note this interacts with the merged one-process build: killin
|
||||
|
||||
**What `PORTING.md` says NOT to build, with evidence:** escaping closures (one capture site, fixed by one parameter),
|
||||
`Handle`/pools, `Result`/`try`, `handler-case`, `loop`/`recur` and tail calls, user allocators, structural typing —
|
||||
**none has a customer in that code**. And **generics is not the blocker** there either: the element-changing maps are
|
||||
**none has a customer in that code**. (`Handle` and the pool were built anyway, and on the other reason: they are the
|
||||
gate on classes. The finding stands and is why they were built small — see [`BUILT.md`](BUILT.md).) And **generics is not the blocker** there either: the element-changing maps are
|
||||
five-line load-time loops. That last one hangs on a design decision the report states flatly — whether the game's
|
||||
state holds fixed arrays or `Vec`s.
|
||||
|
||||
@ -329,9 +330,10 @@ whatever the flag says.
|
||||
|
||||
plan.org grew a `class` facility beside `struct`: identity, runtime shape metadata, an implementation-defined
|
||||
representation, generic-function dispatch, and live schema change with an explicit migration at a frame boundary. Its
|
||||
own last line is the rule — nothing until ordinary `struct`, `Handle` and reload semantics are working. It is here so
|
||||
that a session reading plan.org cold does not take it as the next task. Three things found while reviewing it, none of
|
||||
them in plan.org yet:
|
||||
own last line is the rule — nothing until ordinary `struct`, `Handle` and reload semantics are working. **All three
|
||||
now do**, `Handle` and the pool having landed, so this section is no longer "not yet" but "next, and deliberately not
|
||||
started here". It is here so that a session reading plan.org cold does not take it as the next task. Three things
|
||||
found while reviewing it, none of them in plan.org yet:
|
||||
|
||||
- **A generic function is a cell.** "A later module can add `(defmethod draw ((e Enemy)) ...)` without editing the
|
||||
original" means every compiled call site of `draw` has to find the new method — which is the problem the indirection
|
||||
@ -339,7 +341,8 @@ cells already solve. A generic function is a cell whose body is a dispatch table
|
||||
expensive half of classes is therefore already built and tested.
|
||||
- **The pool is not one storage option among three.** `migrate-instances` has to *enumerate* live instances. A pool
|
||||
behind generational `(Handle T)` gives that by construction; a world arena and an owned region do not obviously.
|
||||
plan.org presents the three as a free choice and they are not.
|
||||
plan.org presents the three as a free choice and they are not. **The pool is built**, and `(len p)` with
|
||||
`(pool-handle p i)` is that enumeration.
|
||||
- **`Enemy@1` has to stay resolvable** for `migrate` to dispatch on it, so the session retains every layout version's
|
||||
metadata for as long as any instance holds it. Same rule as "nothing is ever `dlclose`d", and worth stating as one.
|
||||
|
||||
@ -542,18 +545,16 @@ Three things to settle while building it: whether it takes focus or only display
|
||||
the window, being a deliberate stop rather than a failure; and what it does when the program stops while point is
|
||||
mid-edit in another buffer.
|
||||
|
||||
**`Handle` and the pool are the real gate on classes, and they are buildable now.** plan.org's rule is that nothing
|
||||
starts on managed classes "until ordinary `struct`, `Handle`, and reload semantics are working". Checked against the
|
||||
tree: structs work fully; reload works with one known hole (a changed signature is refused rather than versioned);
|
||||
**`Handle` does not exist at all** — `check.ml:218` still refuses `(Handle T)` by name.
|
||||
**~~`Handle` and the pool are the real gate on classes, and they are buildable now.~~ Built.** plan.org's rule is
|
||||
that nothing starts on managed classes "until ordinary `struct`, `Handle`, and reload semantics are working". All
|
||||
three now hold: structs work fully; reload works with one known hole (a changed signature is refused rather than
|
||||
versioned); and `(Handle T)` and `(Pool T)` exist, with the enumeration primitive `migrate-instances` was blocked on.
|
||||
See [`BUILT.md`](BUILT.md), "`(Handle T)` and the pool, which is what a stale reference answers with".
|
||||
|
||||
It is not an incidental precondition. `migrate-instances` has to *enumerate* live instances, and a pool behind a
|
||||
It was not an incidental precondition. `migrate-instances` has to *enumerate* live instances, and a pool behind a
|
||||
generational `(Handle T)` gives that by construction while a world arena and an owned region do not. plan.org presents
|
||||
the three storage strategies as a free choice and they are not: handles are the one that makes migration possible.
|
||||
|
||||
**The allocator and arena landing today are what unblock it** — a pool is built on them, so `Handle` is buildable now
|
||||
where it was not this morning. Build `Handle` and the pool next and treat *that* as the gate. It earns its place
|
||||
independently of classes: stable references to things that move or die is something any game wants.
|
||||
`(len p)` plus `(pool-handle p i)` is that enumeration, and it is two entry points rather than an iteration protocol.
|
||||
|
||||
Already banked, and it means classes are less work than plan.org implies: **a generic function is an indirection cell**
|
||||
whose body is a dispatch table, which a reload extends. That is the expensive half of method dispatch, and it is built
|
||||
@ -566,7 +567,7 @@ working the case through rather than by preference, so the reasoning is worth ke
|
||||
decided against it. It runs code somewhere the reader is not looking, which is the C++ behaviour the author explicitly
|
||||
does not want. It would not even cover the motivating case — `Image` and `Texture2D` are *raylib's* types, and attaching
|
||||
a hook to a foreign type is its own unsolved design question. And its one real advantage, cascading through a container,
|
||||
is the case `Handle` is about to make rare: entities holding handles hold numbers, not resources.
|
||||
is the case `Handle` makes rare: entities holding handles hold numbers, not resources.
|
||||
|
||||
`with-cleanup` / `unwind-protect` was also put and rejected: awkward with several resources, and it reads worse than
|
||||
what already exists. The raylib begin/end pairs that seemed to motivate it are a macro problem, not a primitive one —
|
||||
@ -876,9 +877,27 @@ run one lane at a time; item 4 is disjoint and runs alongside any of them.
|
||||
`[f32]` would be one copy per ordered pair. A user-written allocator is *not* on this list any more — it wants
|
||||
a C-shaped callback and somewhere to put a `flan_allocator`, neither of which is a type parameter.
|
||||
|
||||
6. **`Handle` and the pool.** A reference to something that can die, that reports that it died rather than silently
|
||||
resolving to whatever reused the slot. Wanted on its own terms for entities referred to across frames, and it is the
|
||||
real gate on classes. Buildable now that the allocator exists.
|
||||
6. ~~**`Handle` and the pool.**~~ **Built.** A reference to something that can die, that reports that it died rather
|
||||
than silently resolving to whatever reused the slot. See [`BUILT.md`](BUILT.md), "`(Handle T)` and the pool, which
|
||||
is what a stale reference answers with". A handle is one `i64` — slot index low, generation high — so it copies,
|
||||
zeroes and compares like an integer and owns nothing; a live slot's generation is odd, which makes a zeroed handle
|
||||
resolve to nothing rather than to slot 0; and a generation that would wrap retires its slot instead, because "rare"
|
||||
is not an answer when the failure is the silent wrong one the type exists to prevent.
|
||||
|
||||
What the spec did not settle and this lane did, beyond those: `resolve` answers `(Option (Ptr T))` and not
|
||||
`(Option T)` — the spec's own worked example is annotated that way, for the reason written a line above it, that a
|
||||
pattern binding binds a value and a copy cannot be written back. `(len p)` is the *slot high-water* and `(live p)`
|
||||
is the live count, in that direction, so a loop bounded by `len` cannot silently skip a live entry. A slot is
|
||||
recycled by `(release p h)` on the owner and never by `free`, because a handle owns nothing and consuming one copy
|
||||
would say nothing about the others — so `spec-memory.md`'s two release points are untouched.
|
||||
|
||||
**Two amendments to the frozen spec, both deferrals**: `.field` and `at` do not auto-deref a handle, and `deref` is
|
||||
not overloaded on one. Neither can answer "gone", which is the whole job; the spec's own example resolves first and
|
||||
matches, and that is the half that is right.
|
||||
|
||||
**Still open**: a `(Ptr T)` from `resolve` dies on any `insert` that grows the pool, the same explicit contract a
|
||||
slice has against `push`. Chunked never-moving storage is the fix and it costs code. And a pool passed to a helper
|
||||
is consumed, because there is no borrowing parameter — a pre-existing `Vec` gap, not a pool one.
|
||||
|
||||
7. ~~**`break` and `continue`, with loop labels.**~~ **Built.** Labels are Odin's in the head position, both blockers
|
||||
are answered, and the refusals name the construct they refuse for. See BUILT.md, "`break` and `continue`, and the
|
||||
@ -1053,7 +1072,7 @@ natural anyway.
|
||||
**Flexible field order waits for classes, deliberately.** A class has an implementation-defined representation, so the
|
||||
compiler owns the layout and field order stops being observable — any order can match. That is the right place to pay
|
||||
for flexibility, because a class already carries identity and metadata, and a `Vector2` should pay for neither. See the
|
||||
`defclass` entry: `Handle` is the gate.
|
||||
`defclass` entry: `Handle` was the gate, and it is built now.
|
||||
|
||||
Note what this settles from the earlier discussion: writability was the question that decided layout, and requiring
|
||||
identical layout answers it — fields are writable on the ordinary terms, by value a copy and through a `(Ptr T)` the
|
||||
@ -1313,8 +1332,9 @@ rest on, and because the escape it describes was tested rather than assumed —
|
||||
The dependency nobody had written down, and the reason it looked worse than it is. `spec-memory.md` defines an
|
||||
allocator as "a procedure plus an opaque data pointer" — a function value. `check.ml` refuses function values four
|
||||
ways, and all four say milestone 5: a written `(Fn ...)` annotation (`Ast.Tfn`), a written `fn` literal (`Ast.Fn`), a
|
||||
`defn`'s name used as a value, and calling anything other than a named function. `(Map K V)`, `(Result T E)` and
|
||||
`(Handle T)` are still refused beside those as milestone 6; `(Vec T)` is not, any more. Read straight off those lines,
|
||||
`defn`'s name used as a value, and calling anything other than a named function. `(Result T E)` was still refused
|
||||
beside those as milestone 6, as `(Map K V)`, `(Handle T)` and `(Vec T)` were when this was written; only `Result` is
|
||||
now. Read straight off those lines,
|
||||
milestone 6's allocators need milestone 5's function values and the work doubles.
|
||||
|
||||
**The escape is real and the work did not double** — this is the claim the built thing confirms. All four refusals are about *surface syntax*, and a value the
|
||||
|
||||
306
lib/check.ml
306
lib/check.ml
@ -429,7 +429,23 @@ let rec resolve env ?(seen = []) (t : Ast.texpr) : Types.t =
|
||||
map_type loc (resolve env ~seen k) (resolve env ~seen v)
|
||||
| "Map", _ -> fail loc "(Map K V) takes exactly two types"
|
||||
| "Result", _ -> unimplemented loc "(Result T E)" 6
|
||||
| "Handle", _ -> unimplemented loc "(Handle T)" 6
|
||||
| "Pool", [ a ] ->
|
||||
let e = resolve env ~seen a in
|
||||
(* The same refusal (Vec T) makes, for the same reason: the pool's
|
||||
runtime is type-erased and copies and releases slots bytewise, so a
|
||||
release would drop what an owning element owns. Recursive teardown
|
||||
arrives with drop. *)
|
||||
if Types.is_move_only e then
|
||||
fail loc
|
||||
"(Pool %s) holds a move-only element, and the type-erased runtime \
|
||||
copies and releases slots bytewise — so releasing a slot would \
|
||||
leak what it owns. Recursive teardown arrives with drop (step 5 \
|
||||
in NEXT.md)"
|
||||
(Types.to_string e);
|
||||
Types.Pool e
|
||||
| "Pool", _ -> fail loc "(Pool T) takes exactly one type"
|
||||
| "Handle", [ a ] -> Types.Handle (resolve env ~seen a)
|
||||
| "Handle", _ -> fail loc "(Handle T) takes exactly one type"
|
||||
| _ ->
|
||||
fail loc
|
||||
"%s takes no type arguments — generics are milestone 5" name)
|
||||
@ -2451,6 +2467,42 @@ and map_new_types ctx ~want loc args =
|
||||
"nothing here says what (map-new) maps — write the key and value \
|
||||
types, as (map-new string i32), or give the binding a type")
|
||||
|
||||
(* The element type for [pool-new]. The same rule [vec-new] uses and for the
|
||||
same reason: a [let] has no type annotation, so a local pool has nowhere
|
||||
else to say what it holds. *)
|
||||
and pool_new_elem ctx ~want loc args =
|
||||
let named =
|
||||
match args with
|
||||
| { Ast.e = Ast.Var n; _ } :: rest
|
||||
when lookup ctx n = None
|
||||
&& (not (Hashtbl.mem ctx.env.globals n))
|
||||
&& type_named ctx n ->
|
||||
Some (resolve_name ctx.env ~seen:[] loc n, rest)
|
||||
| _ -> None
|
||||
in
|
||||
match named with
|
||||
| Some (t, rest) ->
|
||||
if Types.is_move_only t then
|
||||
fail loc
|
||||
"(Pool %s) holds a move-only element, and the type-erased runtime \
|
||||
copies and releases slots bytewise. Recursive teardown arrives with \
|
||||
drop (step 5 in NEXT.md)"
|
||||
(Types.to_string t);
|
||||
t, rest
|
||||
| None ->
|
||||
(match want with
|
||||
| Some (Types.Pool t) -> t, args
|
||||
| _ ->
|
||||
fail loc
|
||||
"nothing here says what (pool-new) is a Pool of — write the element \
|
||||
type, as (pool-new Enemy), or give the binding a type")
|
||||
|
||||
(* The element type, or the reason this is not a Pool. *)
|
||||
and pool_elem loc what (t : Types.t) =
|
||||
match t with
|
||||
| Types.Pool e -> e
|
||||
| other -> fail loc "%s takes a (Pool T), found %s" what (Types.to_string other)
|
||||
|
||||
(* The element type, or the reason this is not a Vec. *)
|
||||
and vec_elem loc what (t : Types.t) =
|
||||
match t with
|
||||
@ -2507,7 +2559,16 @@ and named_call ctx ~want loc name args =
|
||||
in
|
||||
arity loc name 2 args;
|
||||
let a, b = binary ctx name loc ~want:None args in
|
||||
if not (Types.is_comparable a.Tast.ty) then
|
||||
(* [=] and [!=] admit one type [<] does not: a handle, which is a pair of
|
||||
numbers in one word and where "the same entity" is the question the
|
||||
type exists to answer. Ordering handles would order a slot index, which
|
||||
is a free-list artefact and means nothing. *)
|
||||
let ok =
|
||||
match name with
|
||||
| "=" | "!=" -> Types.is_equatable a.Tast.ty
|
||||
| _ -> Types.is_comparable a.Tast.ty
|
||||
in
|
||||
if not ok then
|
||||
fail loc
|
||||
"%s compares machine numbers; %s has no built-in comparison \
|
||||
(plan.org, Types)" name (Types.to_string a.Tast.ty);
|
||||
@ -2912,6 +2973,20 @@ and named_call ctx ~want loc name args =
|
||||
expect loc ~want
|
||||
(rt loc Types.Unit "flan_map_free"
|
||||
[ target; size_of loc k; size_of loc v; here loc ])
|
||||
(* The owner, not a slot. Every handle into it is stale afterwards and
|
||||
answers None, which is a strictly better afterlife than a Vec's
|
||||
binding gets — that one is a compile error and this one is a run-time
|
||||
answer, because handles are copies and the checker cannot see them
|
||||
all. That asymmetry is the reason handles exist. *)
|
||||
| Types.Pool elem ->
|
||||
expect loc ~want
|
||||
(rt loc Types.Unit "flan_pool_free"
|
||||
[ target; size_of loc elem; align_of loc elem; here loc ])
|
||||
| Types.Handle _ ->
|
||||
fail loc
|
||||
"free takes the owner, and a handle owns nothing — it is a copyable \
|
||||
number, so consuming one copy would say nothing about the others. \
|
||||
(release p h) recycles one slot; (free p) releases the pool"
|
||||
| other ->
|
||||
(* A field is never freed on its own: it would leave its owner partly
|
||||
dead with no way to say so. *)
|
||||
@ -2949,6 +3024,18 @@ and named_call ctx ~want loc name args =
|
||||
(Tast.Let ([ (d, mk loc mty (Tast.Zero mty)) ],
|
||||
[ alloc_guard ctx loc attempt;
|
||||
mk loc mty (Tast.Local d) ])))
|
||||
(* Refused by name rather than falling through to "clone takes a
|
||||
(Vec T)". Copying a pool would duplicate every slot *and* every
|
||||
generation counter, so a handle into the original would resolve in
|
||||
the copy too — two live entities behind one identity, which is the
|
||||
exact confusion the type exists to prevent. If a program wants a
|
||||
second world it builds one and inserts into it, and the new handles
|
||||
say they are new. *)
|
||||
| Types.Pool _ ->
|
||||
fail loc
|
||||
"a pool cannot be cloned: the copy would carry the same slot \
|
||||
generations, so one handle would resolve in both and name two \
|
||||
different things. Build a second pool and insert into it"
|
||||
| _ ->
|
||||
let elem = vec_elem loc "clone" target.Tast.ty in
|
||||
let d = fresh_slot ctx (Types.Vec elem) in
|
||||
@ -2965,6 +3052,212 @@ and named_call ctx ~want loc name args =
|
||||
mk loc (Types.Vec elem) (Tast.Local d) ]))))
|
||||
| _ -> fail loc "clone is (clone v) or (clone v allocator)")
|
||||
|
||||
(* ── (Pool T) and (Handle T), spec-memory.md ───────────────────── *)
|
||||
(* The same type-erased shape the Vec has, for the same reason: size_of and
|
||||
align_of are produced here because here is where the concrete element
|
||||
type is known, and nothing below the call site has ever heard of it. *)
|
||||
|
||||
(* (pool-new), (pool-new T), (pool-new a), (pool-new T a). *)
|
||||
| "pool-new" ->
|
||||
let elem, args = pool_new_elem ctx ~want loc args in
|
||||
let a = allocator_arg ctx loc args in
|
||||
let pty = Types.Pool elem in
|
||||
let p = fresh_slot ctx pty in
|
||||
(* [flan_pool_init] cannot fail — a pool with no slots allocates nothing —
|
||||
but it goes under the guard anyway, so that the day it does allocate
|
||||
the site is already the one that signals. *)
|
||||
let attempt =
|
||||
rt loc (Types.Int Types.I8) "flan_pool_init"
|
||||
[ mk loc pty (Tast.Local p); a; size_of loc elem; align_of loc elem;
|
||||
here loc ]
|
||||
in
|
||||
expect loc ~want
|
||||
(mk loc pty
|
||||
(Tast.Let ([ (p, mk loc pty (Tast.Zero pty)) ],
|
||||
[ alloc_guard ctx loc attempt;
|
||||
mk loc pty (Tast.Local p) ])))
|
||||
|
||||
(* (insert p x) -> (Handle T). The handle is the *only* way back to what was
|
||||
inserted: a pool hands out no index and no pointer, because an index does
|
||||
not notice a reuse and that is the entire point. *)
|
||||
| "insert" ->
|
||||
arity loc name 2 args;
|
||||
(match args with
|
||||
| [ target; x ] ->
|
||||
let target = borrowed ctx target (fun () -> check ctx target) in
|
||||
let elem = pool_elem loc "insert" target.Tast.ty in
|
||||
let x = check ctx ~want:elem x in
|
||||
let hty = Types.Handle elem in
|
||||
(* The element is bound before the loop so that a [retry] re-attempts
|
||||
the allocation and not the expression that produced the value —
|
||||
[push]'s rule, and for the same reason. *)
|
||||
let e = fresh_slot ctx elem in
|
||||
let h = fresh_slot ctx hty in
|
||||
let attempt =
|
||||
rt loc (Types.Int Types.I8) "flan_pool_insert"
|
||||
[ target; addr_of loc (mk loc elem (Tast.Local e));
|
||||
addr_of loc (mk loc hty (Tast.Local h));
|
||||
size_of loc elem; align_of loc elem; here loc ]
|
||||
in
|
||||
expect loc ~want
|
||||
(mk loc hty
|
||||
(Tast.Let ([ (e, x); (h, mk loc hty (Tast.Zero hty)) ],
|
||||
[ alloc_guard ctx loc attempt;
|
||||
mk loc hty (Tast.Local h) ])))
|
||||
| _ -> assert false)
|
||||
|
||||
(* (resolve p h) -> (Option (Ptr T)).
|
||||
|
||||
A pointer and not a value, and spec-memory.md settles it rather than this
|
||||
lane guessing: its worked example under "Mutating something you matched"
|
||||
is written out as (Option (Ptr Enemy)), for the reason stated a line
|
||||
above it — "pattern bindings bind values, so a matched struct is a copy",
|
||||
and a copy cannot be written back. Mutating the pooled thing in place is
|
||||
what a pool is for, so (Option T) would answer a question nobody asked.
|
||||
|
||||
An [Option] rather than a trap because the whole thesis is that a stale
|
||||
reference *reports* — the same shape (get m k) has, and for the same
|
||||
reason: absence is an answer, not a failure.
|
||||
|
||||
The hole, said plainly: the (Ptr T) is invalidated by any [insert] that
|
||||
grows the pool, exactly as a slice is invalidated by a [push]. The handle
|
||||
survives that and the pointer does not. It is spec-memory.md's explicit
|
||||
Zig/Odin contract one level down, and it is worth naming because it is
|
||||
the silent-wrong-answer mode the handle just removed, reintroduced for
|
||||
anyone who keeps the pointer across an insert. Chunked never-moving
|
||||
storage is the fix and it costs code; taking the contract is the smaller
|
||||
correct thing, given [as-slice] already established it. *)
|
||||
| "resolve" ->
|
||||
arity loc name 2 args;
|
||||
(match args with
|
||||
| [ target; h ] ->
|
||||
let target = borrowed ctx target (fun () -> check ctx target) in
|
||||
let elem = pool_elem loc "resolve" target.Tast.ty in
|
||||
let h = check ctx ~want:(Types.Handle elem) h in
|
||||
(match h.Tast.ty with
|
||||
| Types.Handle e when Types.equal e elem -> ()
|
||||
| other ->
|
||||
fail loc "resolve takes a (Handle %s), found %s"
|
||||
(Types.to_string elem) (Types.to_string other));
|
||||
let pty = Types.Ptr elem in
|
||||
let oty = Types.Option pty in
|
||||
let out = fresh_slot ctx pty in
|
||||
let got =
|
||||
rt loc pty "flan_pool_resolve"
|
||||
[ target; h; size_of loc elem; here loc ]
|
||||
in
|
||||
(* The runtime answers a pointer or NULL and the Option is built here,
|
||||
which is [get]'s arrangement: the runtime has no idea what an
|
||||
Option's layout is, and keeping it that way is what lets one entry
|
||||
point serve every element type. *)
|
||||
let cond =
|
||||
mk loc Types.Bool
|
||||
(Tast.Prim (Tast.Ne,
|
||||
[ mk loc (Types.Int Types.I64)
|
||||
(Tast.Prim (Tast.Cast (Types.Int Types.I64),
|
||||
[ mk loc pty (Tast.Local out) ]));
|
||||
mk loc (Types.Int Types.I64) (Tast.Int (0L, Types.I64)) ]))
|
||||
in
|
||||
let some = mk loc oty (Tast.Some_ (mk loc pty (Tast.Local out))) in
|
||||
let none = mk loc oty Tast.None_ in
|
||||
expect loc ~want
|
||||
(mk loc oty
|
||||
(Tast.Let ([ (out, got) ],
|
||||
[ mk loc oty (Tast.If (cond, some, none)) ])))
|
||||
| _ -> assert false)
|
||||
|
||||
(* (release p h) -> bool: true if this call released it, false if the handle
|
||||
was already gone.
|
||||
|
||||
This is how a pooled value dies, and it is not [free]. [free] consumes
|
||||
its argument as a move, and a handle is a copyable number that owns
|
||||
nothing — consuming one copy would say nothing about the others. The pool
|
||||
is the owner, so the release operation is on the pool and takes the
|
||||
handle as an ordinary argument. spec-memory.md's two release points are
|
||||
untouched: (free p) is release point 1 applied to the owner, and a
|
||||
free-all of the region takes the pool with everything else. This is a
|
||||
third thing and it is not a release point — it recycles a slot inside
|
||||
storage the pool still owns.
|
||||
|
||||
It answers a bool rather than () because the generational scheme makes a
|
||||
double release *detectable*, which is worth handing to the caller: this
|
||||
is the one place in the language where freeing something twice is an
|
||||
answer instead of a refusal. *)
|
||||
| "release" ->
|
||||
arity loc name 2 args;
|
||||
(match args with
|
||||
| [ target; h ] ->
|
||||
let target = borrowed ctx target (fun () -> check ctx target) in
|
||||
let elem = pool_elem loc "release" target.Tast.ty in
|
||||
let h = check ctx ~want:(Types.Handle elem) h in
|
||||
(match h.Tast.ty with
|
||||
| Types.Handle e when Types.equal e elem -> ()
|
||||
| other ->
|
||||
fail loc "release takes a (Handle %s), found %s"
|
||||
(Types.to_string elem) (Types.to_string other));
|
||||
let got = rt loc (Types.Int Types.I8) "flan_pool_release"
|
||||
[ target; h; here loc ] in
|
||||
expect loc ~want
|
||||
(mk loc Types.Bool
|
||||
(Tast.Prim (Tast.Ne,
|
||||
[ got;
|
||||
mk loc (Types.Int Types.I8) (Tast.Int (0L, Types.I8)) ])))
|
||||
| _ -> assert false)
|
||||
|
||||
(* (live p) — how many slots are live now. (len p) is the *slot high-water*,
|
||||
which is deliberately the other number: 0..(len p) are the indices
|
||||
(pool-handle p i) accepts, so a loop bounded by [len] visits every live
|
||||
entry. Bounding it by the live count instead would silently skip entries
|
||||
the moment anything had been released, which is precisely the kind of
|
||||
quiet wrong answer this whole type exists to remove. *)
|
||||
| "live" ->
|
||||
arity loc name 1 args;
|
||||
let target = borrowed ctx (List.hd args) (fun () -> check ctx (List.hd args)) in
|
||||
ignore (pool_elem loc "live" target.Tast.ty);
|
||||
let n = rt loc (Types.Int Types.I64) "flan_pool_live" [ target; here loc ] in
|
||||
expect loc ~want (mk loc index_ty (Tast.Prim (Tast.Cast index_ty, [ n ])))
|
||||
|
||||
(* (pool-handle p i) -> (Option (Handle T)): the handle of slot [i], or None
|
||||
if that slot is dead. This plus (len p) is the whole of iteration, and
|
||||
iteration is not a convenience — migrate-instances has to *enumerate*
|
||||
live instances, and a pool behind generational handles gives that by
|
||||
construction where a world arena and an owned region do not. It is the
|
||||
reason plan.org's three storage strategies are not a free choice.
|
||||
|
||||
An index out of 0..(len p) traps, exactly as (at v i) traps: an index is
|
||||
an index here, and answering None for one would hide a bug rather than a
|
||||
death. *)
|
||||
| "pool-handle" ->
|
||||
arity loc name 2 args;
|
||||
(match args with
|
||||
| [ target; i ] ->
|
||||
let target = borrowed ctx target (fun () -> check ctx target) in
|
||||
let elem = pool_elem loc "pool-handle" target.Tast.ty in
|
||||
let i = check ctx ~want:index_ty i in
|
||||
let hty = Types.Handle elem in
|
||||
let oty = Types.Option hty in
|
||||
let out = fresh_slot ctx hty in
|
||||
let got = rt loc hty "flan_pool_handle" [ target; i; here loc ] in
|
||||
(* 0 is the never-valid handle — generation 0 is even, and a live slot's
|
||||
generation is odd — so the runtime says "dead" with it and needs no
|
||||
second return value. *)
|
||||
let cond =
|
||||
mk loc Types.Bool
|
||||
(Tast.Prim (Tast.Ne,
|
||||
[ mk loc (Types.Int Types.I64)
|
||||
(Tast.Prim (Tast.Cast (Types.Int Types.I64),
|
||||
[ mk loc hty (Tast.Local out) ]));
|
||||
mk loc (Types.Int Types.I64) (Tast.Int (0L, Types.I64)) ]))
|
||||
in
|
||||
expect loc ~want
|
||||
(mk loc oty
|
||||
(Tast.Let ([ (out, got) ],
|
||||
[ mk loc oty
|
||||
(Tast.If (cond,
|
||||
mk loc oty (Tast.Some_ (mk loc hty (Tast.Local out))),
|
||||
mk loc oty Tast.None_)) ])))
|
||||
| _ -> assert false)
|
||||
|
||||
(* ── (Map K V), spec-memory.md ─────────────────────────────────── *)
|
||||
(* Every one of these is a named call over the same type-erased runtime the
|
||||
Vec uses, with the two sizes and the key's hash and equality pair produced
|
||||
@ -3322,9 +3615,16 @@ and named_call ctx ~want loc name args =
|
||||
| Types.Map _ ->
|
||||
let n = rt loc (Types.Int Types.I64) "flan_map_len" [ a; here loc ] in
|
||||
expect loc ~want (mk loc index_ty (Tast.Prim (Tast.Cast index_ty, [ n ])))
|
||||
(* A pool's [len] is its slot high-water, not its live count, so that
|
||||
0..(len p) stays the range of valid indices the way it is for every
|
||||
other container here. (live p) is the other number. *)
|
||||
| Types.Pool _ ->
|
||||
let n = rt loc (Types.Int Types.I64) "flan_pool_len" [ a; here loc ] in
|
||||
expect loc ~want (mk loc index_ty (Tast.Prim (Tast.Cast index_ty, [ n ])))
|
||||
| other ->
|
||||
fail loc
|
||||
"len takes an array, a slice, a string, a Vec or a Map, found %s"
|
||||
"len takes an array, a slice, a string, a Vec, a Map or a Pool, \
|
||||
found %s"
|
||||
(Types.to_string other))
|
||||
| "at" ->
|
||||
(match args with
|
||||
|
||||
60
lib/emit.ml
60
lib/emit.ml
@ -113,6 +113,15 @@ let rec ll (t : Types.t) =
|
||||
map's address — so the shape exists only so that a slot, a struct field
|
||||
and a copy in the IR are the right number of bytes. *)
|
||||
| Types.Map _ -> "%map"
|
||||
(* items + slots + len + cap + live + free + allocator + epoch. Nothing here
|
||||
reads a field of one either — every operation is a runtime call taking
|
||||
the pool's address. *)
|
||||
| Types.Pool _ -> "%pool"
|
||||
(* A handle is one 64-bit number: the slot index in the low half and that
|
||||
slot's generation in the high half. Packed rather than a two-field struct
|
||||
so that copying, zeroing and [=] are what they are for an integer, with no
|
||||
backend arm anywhere except the one comparison below. *)
|
||||
| Types.Handle _ -> "i64"
|
||||
| Types.Option e -> Printf.sprintf "{ i8, %s }" (ll e)
|
||||
| Types.Var _ ->
|
||||
(* The checker rejects it by name — nothing reaches here. *)
|
||||
@ -267,6 +276,8 @@ let rec lay m (t : Types.t) : int * int =
|
||||
| Types.Alloc -> 8, 8
|
||||
| Types.Fn _ -> 8, 8
|
||||
| Types.Vec _ | Types.Map _ -> 48, 8
|
||||
| Types.Pool _ -> 64, 8
|
||||
| Types.Handle _ -> 8, 8
|
||||
(* [n x T] adds no padding of its own: T's size already carries its tail. *)
|
||||
| Types.Array (n, e) -> let s, a = lay m e in Int64.to_int n * s, a
|
||||
| Types.Option e -> let s, a, _ = lay_fields m [ Types.Int Types.I8; e ] in s, a
|
||||
@ -460,6 +471,19 @@ let rec dty m d (t : Types.t) : int =
|
||||
("allocator", Types.Alloc); ("gen", Types.Int Types.I64);
|
||||
("epoch", Types.Int Types.I64) ]
|
||||
|> fun n -> ignore k; ignore v; n
|
||||
(* Eight fields, shown as eight, for the reason the two above are. *)
|
||||
| Types.Pool e ->
|
||||
composite (Types.to_string t)
|
||||
[ ("items", Types.Ptr e);
|
||||
("slots", Types.Ptr (Types.Int Types.U8));
|
||||
("len", Types.Int Types.I64); ("cap", Types.Int Types.I64);
|
||||
("live", Types.Int Types.I64); ("free", Types.Int Types.I64);
|
||||
("allocator", Types.Alloc); ("epoch", Types.Int Types.I64) ]
|
||||
(* An i64 under lldb, which is what it is. Splitting it into a two-field
|
||||
composite would be describing a struct that is not there: the packing
|
||||
is the runtime's, and [p h] answering with the number is honest. *)
|
||||
| Types.Handle _ ->
|
||||
basic (Types.to_string t) 64 "DW_ATE_unsigned"
|
||||
(* A pointer to code, and lldb is told exactly that and no more. DWARF
|
||||
has DW_TAG_subroutine_type for the signature behind it, and spelling
|
||||
one out here would buy a reader nothing they cannot get from the
|
||||
@ -1684,6 +1708,11 @@ and prim f (e : Tast.expr) (p : Tast.prim) (args : Tast.expr list) =
|
||||
location. Signed, because a member may be declared negative. *)
|
||||
| Types.Enum _ ->
|
||||
ins f "%s = icmp %s %s %s, %s" t (icmp_op true p) (ll x.Tast.ty) a b
|
||||
(* [Types.is_equatable] admits a handle and [is_comparable] does not, so
|
||||
only [Eq]/[Ne] arrive here — one unsigned integer compare over the
|
||||
packed (index, generation) pair. *)
|
||||
| Types.Handle _ ->
|
||||
ins f "%s = icmp %s i64 %s, %s" t (icmp_op false p) a b
|
||||
| t' -> failwith ("comparison on " ^ Types.to_string t'));
|
||||
t
|
||||
| (Tast.BitAnd | Tast.BitOr | Tast.BitXor | Tast.Shl | Tast.Shr), [ x; y ] ->
|
||||
@ -1822,7 +1851,7 @@ and prim f (e : Tast.expr) (p : Tast.prim) (args : Tast.expr list) =
|
||||
lets an operation mutate the caller's container in place.
|
||||
Passing the header by value here would hand the runtime a
|
||||
copy to grow and leave the caller's untouched. *)
|
||||
| Types.Vec _ | Types.Map _ -> [ "ptr " ^ addr f a ]
|
||||
| Types.Vec _ | Types.Map _ | Types.Pool _ -> [ "ptr " ^ addr f a ]
|
||||
| t -> [ ll t ^ " " ^ value f a ])
|
||||
args)
|
||||
in
|
||||
@ -1878,7 +1907,14 @@ and cast f (x : Tast.expr) target =
|
||||
the REPL's renderer needs an enum's number when it falls outside the
|
||||
declared members. *)
|
||||
let concrete (t : Types.t) =
|
||||
match t with Types.Enum _ -> Types.Int Types.I32 | t -> t
|
||||
match t with
|
||||
| Types.Enum _ -> Types.Int Types.I32
|
||||
(* A handle already *is* an i64 — see [ll] — so a cast involving one
|
||||
changes the reading and never the bits. [pool-handle] tests one against
|
||||
the never-valid zero, and the renderer splits one into its index and
|
||||
its generation. Unsigned, because both halves are. *)
|
||||
| Types.Handle _ -> Types.Int Types.U64
|
||||
| t -> t
|
||||
in
|
||||
let src = concrete x.Tast.ty and target = concrete target in
|
||||
if Types.equal src target then v
|
||||
@ -1899,6 +1935,10 @@ and cast f (x : Tast.expr) target =
|
||||
holds — and under opaque pointers there is no instruction to emit for
|
||||
it, both sides being [ptr]. *)
|
||||
| Types.Ptr _, Types.Ptr _ -> "bitcast"
|
||||
(* Also not written in the surface language. [resolve] needs it: the
|
||||
pool answers a pointer or NULL and the Option is built in the
|
||||
checker, so the null test is one integer compare on the address. *)
|
||||
| Types.Ptr _, Types.Int Types.I64 -> "ptrtoint"
|
||||
| _ -> failwith "unsupported cast"
|
||||
in
|
||||
if op = "bitcast" then v
|
||||
@ -2242,6 +2282,10 @@ let header = {|; Generated by flan. The layout is C's: no object headers anywher
|
||||
; nor value type appears in it, for the same reason: one type-erased runtime,
|
||||
; handed the two sizes and a hash/equality pair at each call site.
|
||||
%map = type { ptr, i64, i64, ptr, i64, i64 }
|
||||
; (Pool T) — slab storage handed out behind (Handle T). Type-erased in exactly
|
||||
; the same way; the element type is nowhere in it. items and slots are grown
|
||||
; together and share one cap, so a slot index is an index into both.
|
||||
%pool = type { ptr, ptr, i64, i64, i64, i64, ptr, i64 }
|
||||
; A handler frame: the one it displaced, the condition type it matches, and
|
||||
; the lifted function that runs. Allocated on the establishing frame's stack.
|
||||
%handler = type { ptr, i32, ptr }
|
||||
@ -2314,6 +2358,18 @@ declare i64 @flan_vec_len(ptr, ptr, i64)
|
||||
declare ptr @flan_vec_at(ptr, i32, i64, ptr, i64)
|
||||
declare void @flan_vec_as_slice(ptr, ptr, i32, i32, i64, ptr, i64)
|
||||
declare void @flan_vec_free(ptr, i64, i64, ptr, i64)
|
||||
; (Pool T) and (Handle T). A handle crosses as the i64 it is; the pool, like
|
||||
; every other owning container, crosses as its address. [resolve] answers a
|
||||
; pointer or null and [pool-handle] answers a packed handle or the never-valid
|
||||
; zero, so neither needs a second return value.
|
||||
declare i8 @flan_pool_init(ptr, ptr, i64, i64, ptr, i64)
|
||||
declare i8 @flan_pool_insert(ptr, ptr, ptr, i64, i64, ptr, i64)
|
||||
declare ptr @flan_pool_resolve(ptr, i64, i64, ptr, i64)
|
||||
declare i8 @flan_pool_release(ptr, i64, ptr, i64)
|
||||
declare i64 @flan_pool_len(ptr, ptr, i64)
|
||||
declare i64 @flan_pool_live(ptr, ptr, i64)
|
||||
declare i64 @flan_pool_handle(ptr, i32, ptr, i64)
|
||||
declare void @flan_pool_free(ptr, i64, i64, ptr, i64)
|
||||
; (Map K V). The two ptr arguments before the location on put/get/clone are the
|
||||
; hash and equality pair, which the checker emits per key type and passes here
|
||||
; the way Odin hangs them off Map_Info.
|
||||
|
||||
@ -122,6 +122,28 @@ let rec render c depth (e : Tast.expr) : Tast.expr list =
|
||||
does not own, and the walk is what [as-slice] is for: (print (as-slice
|
||||
v)) prints the elements and says at the call site that it borrowed. *)
|
||||
| Types.Vec _ -> [ lit "<vec>" ]
|
||||
(* Opaque for the reason a Vec is: the slots are storage this function does
|
||||
not own, and a walk over them would print the dead ones too — there is
|
||||
no way to say "dead" inside a rendered element. (pool-handle p i) and
|
||||
(resolve p h) are how a program looks, and they say it. *)
|
||||
| Types.Pool _ -> [ lit "<pool>" ]
|
||||
(* Its identity, which is what spec-memory.md says a handle prints —
|
||||
"Ptr and Handle print their address or identity rather than recursively
|
||||
dereferencing". Shown as index:generation rather than as the packed
|
||||
number, because those are the two things a reader is trying to tell
|
||||
apart when two handles disagree. *)
|
||||
| Types.Handle _ ->
|
||||
let h = cast (Types.Int Types.U64) e in
|
||||
let u64 v = { Tast.e = v; ty = Types.Int Types.U64; loc } in
|
||||
let idx =
|
||||
u64 (Tast.Prim (Tast.BitAnd,
|
||||
[ h; u64 (Tast.Int (0xFFFFFFFFL, Types.U64)) ]))
|
||||
in
|
||||
let gen =
|
||||
u64 (Tast.Prim (Tast.Shr, [ h; u64 (Tast.Int (32L, Types.U64)) ]))
|
||||
in
|
||||
[ do_ [ lit "<handle "; c.emit.eu64 idx; lit ":"; c.emit.eu64 gen;
|
||||
lit ">" ] ]
|
||||
(* A function value is a code address, and printing the address would make
|
||||
an inspection depend on where the image loaded. The signature is what a
|
||||
reader can act on, so that is what is shown — and the inspector reaches
|
||||
|
||||
42
lib/types.ml
42
lib/types.ml
@ -44,6 +44,25 @@ type t =
|
||||
so this is a container without generics — the concrete type is known only
|
||||
at the call site, which is exactly where the two numbers are produced. *)
|
||||
| Vec of t
|
||||
(* [(Pool T)]: slab storage handed out behind [(Handle T)]. Owning and
|
||||
move-only exactly as a [Vec] is, and built on the same type-erased
|
||||
runtime over (size, align). It is not a second [Vec]: a [Vec]'s indices
|
||||
shift when something is removed and a [Pool]'s slot index never moves,
|
||||
which is the whole reason a handle into one stays meaningful. *)
|
||||
| Pool of t
|
||||
(* [(Handle T)]: a reference to something that can die, which reports that
|
||||
it died rather than silently resolving to whatever reused its slot
|
||||
(spec-memory.md, "Borrowing" — "Cross-referencing long-lived objects uses
|
||||
(Handle a) into a pool, never a raw pointer or slice. A stale handle is
|
||||
detectable").
|
||||
|
||||
It is a plain 64-bit number — a slot index in the low 32 bits and that
|
||||
slot's generation counter in the high 32 — so it copies, compares and
|
||||
zeroes like an integer and owns nothing. A zeroed handle is generation 0,
|
||||
and a live slot's generation is always odd, so [Zero] of a handle is a
|
||||
handle that resolves to nothing rather than one that resolves to slot 0.
|
||||
See runtime/flan_rt.c's pool section for the packing. *)
|
||||
| Handle of t
|
||||
| Option of t (* (Option T) *)
|
||||
| Fn of t list * t (* (Fn [T ...] R) *)
|
||||
| Var of string (* a type variable — milestone 5 *)
|
||||
@ -94,6 +113,8 @@ let rec equal a b =
|
||||
| Ptr x, Ptr y -> equal x y
|
||||
| Alloc, Alloc -> true
|
||||
| Vec x, Vec y -> equal x y
|
||||
| Pool x, Pool y -> equal x y
|
||||
| Handle x, Handle y -> equal x y
|
||||
| Option x, Option y -> equal x y
|
||||
| Fn (ps, r), Fn (ps', r') ->
|
||||
List.length ps = List.length ps'
|
||||
@ -116,6 +137,8 @@ let rec to_string = function
|
||||
| Ptr t -> "(Ptr " ^ to_string t ^ ")"
|
||||
| Alloc -> "Allocator"
|
||||
| Vec t -> "(Vec " ^ to_string t ^ ")"
|
||||
| Pool t -> "(Pool " ^ to_string t ^ ")"
|
||||
| Handle t -> "(Handle " ^ to_string t ^ ")"
|
||||
| Option t -> "(Option " ^ to_string t ^ ")"
|
||||
| Fn (ps, r) ->
|
||||
Printf.sprintf "(Fn [%s] %s)"
|
||||
@ -130,7 +153,10 @@ let is_numeric = function Int _ | Float _ -> true | _ -> false
|
||||
[free] needs no analysis of its own. A struct that owns one is move-only
|
||||
too; that arrives with [drop], which is the step after this one. *)
|
||||
let rec is_move_only = function
|
||||
| Vec _ | Map _ -> true
|
||||
(* A [Pool] owns its storage; a [Handle] into one owns nothing, which is the
|
||||
point of it — handles are copied freely, and the pool is the single
|
||||
owner that [free] applies to. *)
|
||||
| Vec _ | Map _ | Pool _ -> true
|
||||
| Option t -> is_move_only t
|
||||
| Array (_, t) -> is_move_only t
|
||||
| _ -> false
|
||||
@ -153,6 +179,11 @@ let rec keyable = function
|
||||
| Float _ -> false (* NaN /= NaN, and 0.0 and -0.0 differ bytewise *)
|
||||
| Array (_, t) -> keyable t
|
||||
| Named _ -> true (* [Check] decides, by walking the fields *)
|
||||
(* A [Handle] is not a map key, for the reason a [Ptr] is not: hashing an
|
||||
identity is a different operation from hashing what it names, and a
|
||||
handle whose slot has been reused hashes the same as it always did while
|
||||
naming nothing. The type exists to make that difference visible, so
|
||||
burying it under a key is the one thing it must not do. *)
|
||||
| _ -> false
|
||||
|
||||
(* Ordering and equality are defined on machine types and on nothing else at
|
||||
@ -160,6 +191,15 @@ let rec keyable = function
|
||||
unconstrained type supports only what every type supports (plan.org, Types). *)
|
||||
let is_comparable = function Enum _ -> true | t -> is_numeric t
|
||||
|
||||
(* [=] and [!=] admit one more type than [<] does. A [Handle] is a pair of
|
||||
numbers in a 64-bit word, so "is this the same entity" is one integer
|
||||
compare and is worth having — two handles are equal exactly when they name
|
||||
the same slot at the same generation, so a stale handle is never equal to
|
||||
the live one that replaced it. Ordering handles would compare a slot index,
|
||||
which means nothing: allocation order is a free-list artefact. Hence two
|
||||
predicates rather than one. *)
|
||||
let is_equatable = function Handle _ -> true | t -> is_comparable t
|
||||
|
||||
(* [Never] is the type of an expression that does not produce a value: return,
|
||||
an early-returning `some`, exit. It fits anywhere, and that is the only
|
||||
place anything resembling subtyping exists. *)
|
||||
|
||||
@ -1007,6 +1007,265 @@ int8_t flan_vec_clone(flan_vec *dst, flan_vec *src, flan_allocator *a,
|
||||
return 1;
|
||||
}
|
||||
|
||||
/* ── (Pool T) and (Handle T), spec-memory.md ─────────────────────────
|
||||
*
|
||||
* A handle is a reference to something that can die, which reports that it
|
||||
* died rather than silently resolving to whatever reused its slot. That is
|
||||
* the whole design, and every decision below follows from it.
|
||||
*
|
||||
* THE PACKING. A handle is one int64_t: the slot index in the low 32 bits and
|
||||
* that slot's generation counter in the high 32. One word, so it copies,
|
||||
* zeroes and compares like the integer it is, and owns nothing — the pool is
|
||||
* the single owner. 32 bits of index because a Vec's index is an i32 here and
|
||||
* widening indices is one change across every container, not a pool question.
|
||||
*
|
||||
* LIVE IS ODD. A slot's generation starts at 0 and is bumped on every
|
||||
* allocation and on every release, so an odd generation means live and an
|
||||
* even one means dead. Two things fall out of that and both are load-bearing:
|
||||
* a zeroed handle is generation 0, which is even, so it resolves to nothing
|
||||
* rather than to slot 0 — ZII gives a handle field the right meaning for
|
||||
* free; and iteration can ask a slot whether it is live without a second
|
||||
* array or a spare bit.
|
||||
*
|
||||
* WRAPPING RETIRES THE SLOT. 32 bits is 2^31 allocate/release pairs on one
|
||||
* slot — every frame at 60fps for a year and a bit — but "rare" is not an
|
||||
* answer when the failure is the silent wrong one this type exists to
|
||||
* prevent. So a release from generation 0xFFFFFFFF bumps to 0 and does *not*
|
||||
* put the slot back on the free list. The slot is retired: dead forever, its
|
||||
* payload leaked, and no future handle can ever collide with an old one.
|
||||
* Leaking is defined behaviour here (spec-memory.md, "Leaking is defined
|
||||
* behaviour") and one slot is a bounded price for making the collision
|
||||
* unrepresentable rather than unlikely.
|
||||
*
|
||||
* TWO FAILURES, KEPT APART. A stale handle answers "gone" — it is an answer,
|
||||
* not an error. A pool whose allocator was released traps, through the same
|
||||
* epoch check a Vec gets. They answer different questions and must not be
|
||||
* conflated, exactly as the Vec's generation and epoch words must not be.
|
||||
*
|
||||
* GROWTH IS TRANSACTIONAL, and that is not tidiness. spec-memory.md's
|
||||
* StorageExhausted restart re-attempts *the same call*, so a failed grow has
|
||||
* to leave the pool byte for byte as it was — including a cap that still
|
||||
* agrees with the real block sizes, since the next attempt passes cap as the
|
||||
* allocator's old_size. Two blocks grow together, so a resize-in-place of the
|
||||
* first followed by a failure on the second would leave cap describing
|
||||
* neither. Allocate both, copy, then release the old pair: the only state
|
||||
* mutated after the last thing that can fail.
|
||||
*/
|
||||
|
||||
typedef struct flan_pool_slot {
|
||||
uint32_t gen; /* odd: live. even: dead. 0: never allocated, or retired. */
|
||||
int32_t next; /* free-list link, -1 for the end. Meaningless while live. */
|
||||
} flan_pool_slot;
|
||||
|
||||
typedef struct flan_pool {
|
||||
void *items; /* cap payloads, size bytes each */
|
||||
flan_pool_slot *slots; /* cap slot headers, index-parallel with items */
|
||||
int64_t len; /* slot high-water: 0..len have ever been handed out */
|
||||
int64_t cap;
|
||||
int64_t live; /* how many of those are live now */
|
||||
int64_t free; /* head of the free list, -1 when empty */
|
||||
flan_allocator *alloc;
|
||||
int64_t epoch;
|
||||
} flan_pool;
|
||||
|
||||
static int64_t flan_handle_pack(int64_t i, uint32_t gen) {
|
||||
return (int64_t)(((uint64_t)gen << 32) | (uint64_t)(uint32_t)i);
|
||||
}
|
||||
|
||||
static int64_t flan_handle_index(int64_t h) {
|
||||
return (int64_t)(uint32_t)(uint64_t)h;
|
||||
}
|
||||
|
||||
static uint32_t flan_handle_gen(int64_t h) {
|
||||
return (uint32_t)((uint64_t)h >> 32);
|
||||
}
|
||||
|
||||
/* The same epoch check a Vec gets, and for the same reason. A pool that never
|
||||
* allocated has no allocator and nothing to check. */
|
||||
static void flan_pool_check(flan_pool *p, const uint8_t *loc, int64_t loclen) {
|
||||
if (p->alloc) {
|
||||
int64_t now = (int64_t)p->alloc->epoch;
|
||||
if (now != p->epoch) flan_vec_stale_fail(loc, loclen, p->epoch, now);
|
||||
}
|
||||
}
|
||||
|
||||
static flan_allocator *flan_pool_adopt(flan_pool *p) {
|
||||
if (!p->alloc) {
|
||||
p->alloc = flan_context_allocator();
|
||||
p->epoch = (int64_t)p->alloc->epoch;
|
||||
}
|
||||
return p->alloc;
|
||||
}
|
||||
|
||||
static int8_t flan_pool_grow(flan_pool *p, int64_t want, int64_t size,
|
||||
int64_t align) {
|
||||
flan_allocator *a = flan_pool_adopt(p);
|
||||
int64_t cap = p->cap, sslot = (int64_t)sizeof(flan_pool_slot);
|
||||
void *ni, *ns;
|
||||
if (want <= cap) return 1;
|
||||
/* Doubling from four, exactly as the Vec grows. */
|
||||
if (cap < 4) cap = 4;
|
||||
while (cap < want) {
|
||||
if (cap > (int64_t)1 << 40) { cap = want; break; }
|
||||
cap *= 2;
|
||||
}
|
||||
flan_fail_bytes = cap * size + cap * sslot;
|
||||
flan_fail_align = align;
|
||||
flan_fail_id = (int64_t)(intptr_t)a;
|
||||
ni = a->proc(a, FLAN_ALLOC_ALLOC, NULL, 0, cap * size, align);
|
||||
if (!ni) return 0;
|
||||
ns = a->proc(a, FLAN_ALLOC_ALLOC, NULL, 0, cap * sslot, 8);
|
||||
if (!ns) {
|
||||
/* An allocator without can-free leaks the first block here. That is the
|
||||
* defined outcome and not a new one: the request failed because the
|
||||
* region is exhausted, and the region is about to be released whole or
|
||||
* the ceiling raised and the call re-attempted. */
|
||||
if (a->caps & FLAN_CAN_FREE)
|
||||
a->proc(a, FLAN_ALLOC_FREE, ni, cap * size, 0, align);
|
||||
return 0;
|
||||
}
|
||||
if (p->len > 0) {
|
||||
memcpy(ni, p->items, (size_t)(p->len * size));
|
||||
memcpy(ns, p->slots, (size_t)(p->len * sslot));
|
||||
}
|
||||
if (p->items && (a->caps & FLAN_CAN_FREE)) {
|
||||
a->proc(a, FLAN_ALLOC_FREE, p->items, p->cap * size, 0, align);
|
||||
a->proc(a, FLAN_ALLOC_FREE, p->slots, p->cap * sslot, 0, 8);
|
||||
}
|
||||
p->items = ni;
|
||||
p->slots = ns;
|
||||
p->cap = cap;
|
||||
return 1;
|
||||
}
|
||||
|
||||
int8_t flan_pool_init(flan_pool *p, flan_allocator *a, int64_t size,
|
||||
int64_t align, const uint8_t *loc, int64_t loclen) {
|
||||
(void)size; (void)align;
|
||||
/* Null for the same reason and with the same answer flan_vec_init gives:
|
||||
* the no-allocator-named case never arrives here as NULL. */
|
||||
if (!a) flan_null_alloc_fail(loc, loclen);
|
||||
p->items = NULL;
|
||||
p->slots = NULL;
|
||||
p->len = 0;
|
||||
p->cap = 0;
|
||||
p->live = 0;
|
||||
p->free = -1;
|
||||
p->alloc = a;
|
||||
p->epoch = (int64_t)a->epoch;
|
||||
return 1;
|
||||
}
|
||||
|
||||
/* 1/0 for "did it fit", like every other allocating entry point. The handle
|
||||
* goes out through [out] rather than being returned, so that the compiler's
|
||||
* alloc_guard reads the answer and the handle separately. */
|
||||
int8_t flan_pool_insert(flan_pool *p, const void *elem, int64_t *out,
|
||||
int64_t size, int64_t align, const uint8_t *loc,
|
||||
int64_t loclen) {
|
||||
int64_t i;
|
||||
flan_pool_check(p, loc, loclen);
|
||||
if (p->free >= 0) {
|
||||
i = p->free;
|
||||
p->free = p->slots[i].next;
|
||||
} else {
|
||||
if (p->len + 1 > p->cap && !flan_pool_grow(p, p->len + 1, size, align))
|
||||
return 0;
|
||||
i = p->len++;
|
||||
p->slots[i].gen = 0;
|
||||
p->slots[i].next = -1;
|
||||
}
|
||||
p->slots[i].gen++; /* even -> odd: this slot is live */
|
||||
p->live++;
|
||||
memcpy((uint8_t *)p->items + i * size, elem, (size_t)size);
|
||||
*out = flan_handle_pack(i, p->slots[i].gen);
|
||||
return 1;
|
||||
}
|
||||
|
||||
/* NULL when the handle names nothing, which the compiler turns into None. The
|
||||
* index is bounded with the unsigned comparison flan_vec_at uses, because the
|
||||
* low half of a handle can be any 32 bits at all. */
|
||||
void *flan_pool_resolve(flan_pool *p, int64_t h, int64_t size,
|
||||
const uint8_t *loc, int64_t loclen) {
|
||||
int64_t i = flan_handle_index(h);
|
||||
uint32_t g = flan_handle_gen(h);
|
||||
flan_pool_check(p, loc, loclen);
|
||||
if (!(g & 1u)) return NULL; /* a zeroed or dead handle */
|
||||
if ((uint64_t)i >= (uint64_t)p->len) return NULL;
|
||||
if (p->slots[i].gen != g) return NULL; /* the slot was reused */
|
||||
return (uint8_t *)p->items + i * size;
|
||||
}
|
||||
|
||||
/* 1 if this call released it, 0 if the handle was already gone. Releasing
|
||||
* twice is therefore an answer rather than undefined behaviour — which is the
|
||||
* generational scheme paying for itself a second time, since a pool is the
|
||||
* one place a double free is *detectable* rather than merely refused. */
|
||||
int8_t flan_pool_release(flan_pool *p, int64_t h, const uint8_t *loc,
|
||||
int64_t loclen) {
|
||||
int64_t i = flan_handle_index(h);
|
||||
uint32_t g = flan_handle_gen(h), was;
|
||||
flan_pool_check(p, loc, loclen);
|
||||
if (!(g & 1u)) return 0;
|
||||
if ((uint64_t)i >= (uint64_t)p->len) return 0;
|
||||
if (p->slots[i].gen != g) return 0;
|
||||
was = p->slots[i].gen;
|
||||
p->slots[i].gen = was + 1; /* odd -> even: dead, and every old handle with it */
|
||||
p->live--;
|
||||
/* The wrap. See the header: the slot is retired rather than reissued. */
|
||||
if (was != 0xFFFFFFFFu) {
|
||||
p->slots[i].next = (int32_t)p->free;
|
||||
p->free = i;
|
||||
}
|
||||
return 1;
|
||||
}
|
||||
|
||||
int64_t flan_pool_len(flan_pool *p, const uint8_t *loc, int64_t loclen) {
|
||||
flan_pool_check(p, loc, loclen);
|
||||
return p->len;
|
||||
}
|
||||
|
||||
int64_t flan_pool_live(flan_pool *p, const uint8_t *loc, int64_t loclen) {
|
||||
flan_pool_check(p, loc, loclen);
|
||||
return p->live;
|
||||
}
|
||||
|
||||
/* The handle of slot [i], or 0 — the never-valid handle — if that slot is
|
||||
* dead. This plus (len p) is the whole of enumeration, which is what
|
||||
* migrate-instances needs and what a Vec behind an index cannot give: a Vec's
|
||||
* indices shift under a removal and a pool's never do. Out of range traps
|
||||
* rather than answering 0, because an index is an index here and 0..len are
|
||||
* the valid ones. */
|
||||
int64_t flan_pool_handle(flan_pool *p, int32_t i, const uint8_t *loc,
|
||||
int64_t loclen) {
|
||||
uint32_t g;
|
||||
flan_pool_check(p, loc, loclen);
|
||||
if ((uint64_t)(int64_t)i >= (uint64_t)p->len)
|
||||
flan_vec_bounds_fail(loc, loclen, (int64_t)i, p->len);
|
||||
g = p->slots[i].gen;
|
||||
if (!(g & 1u)) return 0;
|
||||
return flan_handle_pack((int64_t)i, g);
|
||||
}
|
||||
|
||||
/* spec-memory.md's first release point, applied to the owner. Zeroed rather
|
||||
* than left dangling, for the reason flan_vec_free zeroes. Every handle into
|
||||
* it is stale afterwards and says so: len goes to 0, so the bound check
|
||||
* answers "gone" for all of them. */
|
||||
void flan_pool_free(flan_pool *p, int64_t size, int64_t align,
|
||||
const uint8_t *loc, int64_t loclen) {
|
||||
flan_pool_check(p, loc, loclen);
|
||||
if (p->items && p->alloc && (p->alloc->caps & FLAN_CAN_FREE)) {
|
||||
p->alloc->proc(p->alloc, FLAN_ALLOC_FREE, p->items, p->cap * size, 0, align);
|
||||
p->alloc->proc(p->alloc, FLAN_ALLOC_FREE, p->slots,
|
||||
p->cap * (int64_t)sizeof(flan_pool_slot), 0, 8);
|
||||
}
|
||||
p->items = NULL;
|
||||
p->slots = NULL;
|
||||
p->len = 0;
|
||||
p->cap = 0;
|
||||
p->live = 0;
|
||||
p->free = -1;
|
||||
p->alloc = NULL;
|
||||
p->epoch = 0;
|
||||
}
|
||||
|
||||
/* ── (Map K V), spec-memory.md ──────────────────────────────────────────
|
||||
*
|
||||
* Odin's map, followed deliberately: open-addressed Robin Hood hashing at a
|
||||
|
||||
103
test/programs/handles.flan
Normal file
103
test/programs/handles.flan
Normal file
@ -0,0 +1,103 @@
|
||||
;;;; (Handle T) and (Pool T), spec-memory.md — "Cross-referencing long-lived
|
||||
;;;; objects uses (Handle a) into a pool, never a raw pointer or slice. A
|
||||
;;;; stale handle is detectable."
|
||||
;;;;
|
||||
;;;; The thesis, in one program: something holds a reference to an entity; the
|
||||
;;;; entity dies; the slot is reused by a different entity; and the old
|
||||
;;;; reference answers "gone" instead of answering wrong. Every other case
|
||||
;;;; here is secondary to that one.
|
||||
;;;;
|
||||
;;;; It is all one function because a Pool is move-only exactly as a Vec is,
|
||||
;;;; so passing one to a helper *consumes* it — there is no borrowing
|
||||
;;;; parameter in the language yet. That is not a pool question and this
|
||||
;;;; program does not work around it; see BUILT.md.
|
||||
|
||||
(defstruct Enemy [hp i32 kind i32])
|
||||
|
||||
;; The projectile does not hold an Enemy and does not hold an index. It holds
|
||||
;; a handle, which is a number that owns nothing and copies freely — which is
|
||||
;; why a struct may contain one where it may not contain a Vec.
|
||||
(defstruct Projectile [target (Handle Enemy) damage i32])
|
||||
|
||||
(defn main [] i32
|
||||
(let [pool (pool-new Enemy)]
|
||||
(let [a (insert pool (Enemy {.hp 10 .kind 1}))
|
||||
b (insert pool (Enemy {.hp 20 .kind 2}))
|
||||
c (insert pool (Enemy {.hp 30 .kind 3}))
|
||||
sum 0]
|
||||
(println (len pool)) ; 3 slots handed out
|
||||
(println (live pool)) ; 3 of them live
|
||||
|
||||
;; Enumeration, which is what a world arena and an owned region do not
|
||||
;; give and which migrate-instances will need. (len p) is the slot
|
||||
;; high-water, so 0..(len p) visits every slot ever handed out, and
|
||||
;; (pool-handle p i) says which of them are still live.
|
||||
(dotimes [i (len pool)]
|
||||
(match (pool-handle pool i)
|
||||
(Some h) (match (resolve pool h)
|
||||
;; resolve yields a *pointer*, not a copy: mutating the
|
||||
;; pooled thing in place is what a pool is for, and a
|
||||
;; pattern binding binds a value.
|
||||
(Some e) (set sum (+ sum (.hp e)))
|
||||
None (do))
|
||||
None (do)))
|
||||
(println sum) ; 60
|
||||
|
||||
;; A write through a resolved pointer is a write to the pooled entity.
|
||||
(match (resolve pool b)
|
||||
(Some e) (set (.hp e) 21)
|
||||
None (do))
|
||||
(match (resolve pool b)
|
||||
(Some e) (println (.hp e)) ; 21
|
||||
None (println -1))
|
||||
|
||||
;; ── The thesis ────────────────────────────────────────────────
|
||||
;; A projectile chasing b. b dies. The slot is reused by a fourth
|
||||
;; enemy, which lands in exactly that slot — and the projectile's
|
||||
;; handle says so rather than chasing the newcomer.
|
||||
(let [shot (Projectile {.target b .damage 5})]
|
||||
(println (release pool b)) ; true — this call released it
|
||||
(println (release pool b)) ; false — it was already gone
|
||||
(println (live pool)) ; 2
|
||||
(let [d (insert pool (Enemy {.hp 99 .kind 4}))]
|
||||
;; Printed as index:generation. Same slot, later generation — the
|
||||
;; two halves of the answer, visible.
|
||||
(println b)
|
||||
(println d)
|
||||
(println (= d b)) ; false
|
||||
(println (= d d)) ; true
|
||||
(match (resolve pool (.target shot))
|
||||
(Some e) (println (.hp e))
|
||||
None (println -1)) ; -1, not 99
|
||||
(match (resolve pool d)
|
||||
(Some e) (println (.hp e)) ; 99
|
||||
None (println -1))
|
||||
(println (len pool)) ; still 3 slots
|
||||
(println (live pool)) ; 3 live
|
||||
|
||||
;; A zeroed handle is generation 0, which is even, and a live slot's
|
||||
;; generation is always odd — so ZII gives a handle field the right
|
||||
;; meaning for free rather than pointing it at slot 0.
|
||||
(let [z (Projectile {.damage 1})]
|
||||
(println (.target z))
|
||||
(match (resolve pool (.target z))
|
||||
(Some e) (println (.hp e))
|
||||
None (println -1))) ; -1
|
||||
|
||||
;; a and c are untouched by any of it.
|
||||
(match (resolve pool a)
|
||||
(Some e) (println (.hp e)) ; 10
|
||||
None (println -1))
|
||||
(match (resolve pool c)
|
||||
(Some e) (println (.hp e)) ; 30
|
||||
None (println -1))
|
||||
|
||||
;; spec-memory.md's first release point, applied to the owner. The
|
||||
;; runtime leaves the pool empty, so a handle into it would resolve
|
||||
;; to None rather than into released storage — but that is not
|
||||
;; demonstrable from here and this program does not pretend it is:
|
||||
;; free consumes pool, so a resolve on the next line is a compile
|
||||
;; error. The runtime property is real and the checker makes it
|
||||
;; unreachable.
|
||||
(free pool)
|
||||
0)))))
|
||||
25
test/programs/pool-stale-region.flan
Normal file
25
test/programs/pool-stale-region.flan
Normal 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)
|
||||
@ -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
|
||||
|
||||
@ -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
|
||||
|
||||
@ -126,6 +126,7 @@ let corpus =
|
||||
"programs/edn.flan", [];
|
||||
"programs/enum-compare.flan", [];
|
||||
"programs/error.flan", [];
|
||||
"programs/handles.flan", [];
|
||||
"programs/machine.flan", [];
|
||||
"programs/math.flan", [];
|
||||
"programs/pkg-diamond.flan", [];
|
||||
|
||||
@ -190,8 +190,9 @@ 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 six programs here that abort by design — error, exhausted-unhandled,
|
||||
free-all-refused, map-stale-region, slurp-unhandled, stale-region — are
|
||||
The seven programs here that abort by design — error, exhausted-unhandled,
|
||||
free-all-refused, map-stale-region, pool-stale-region, slurp-unhandled,
|
||||
stale-region — are
|
||||
kept. A trap is a controlled abort after an fprintf, and "the trap still
|
||||
fires, in the same place, with the same message, under memcheck" is worth
|
||||
asserting: the region and epoch traps are the runtime's own answer to the
|
||||
@ -214,11 +215,13 @@ let corpus =
|
||||
"programs/exhausted.flan", [];
|
||||
"programs/exhausted-unhandled.flan", [];
|
||||
"programs/free-all-refused.flan", [];
|
||||
"programs/handles.flan", [];
|
||||
"programs/machine.flan", [];
|
||||
"programs/map-exhausted.flan", [];
|
||||
"programs/map-stale-region.flan", [];
|
||||
"programs/maps.flan", [];
|
||||
"programs/math.flan", [];
|
||||
"programs/pool-stale-region.flan", [];
|
||||
"programs/pkg-diamond.flan", [];
|
||||
"programs/pkg-return.flan", [];
|
||||
"programs/pkg-shadow.flan", [];
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user