Joseph Ferano
74c6489020
spec-memory.md defines an allocator as a procedure plus an opaque data pointer, which reads as a function value, which check.ml refuses four ways. None of the four is anywhere near this: `Allocator` is a `Types.t` case with no user-writable constructor, the way `string` is a builtin ptr+len, its procedure is a C symbol the emitter names, and every operation is an ordinary named call that `check_call` already routes through `named_call`. The one thing that really does need milestone 5 is a *user-written* allocator — it wants a defn's name in value position — and that is refused by name with that reason rather than left to come back as an unknown function. An `Allocator` value is a pointer to the runtime's struct and never a copy of one. That is forced, not chosen: the capability set has to be readable from wherever a container landed, and `free-all` bumps an epoch every container made from the allocator has to observe. A copy would give each its own epoch and the dev trap would never fire. Two decisions the spec left to be made here, both announced in BUILT.md: `free-all` is retain-capacity — offset = 0, the pages stay — and handing the pages back is `arena-destroy`, a separate operation. Zig's reset takes a mode; Odin's arena_free_all is already retain-capacity in effect. Taking the mode would have grown the operation table the spec froze at four. The epoch is bumped either way, because the pages being the same does not make a container made before the reset valid. `context/allocator` and `context/temp` are dynamic variables with save and restore, not extra parameters. The spec calls the allocator part of the calling convention; the literal reading touches every signature, the FFI shim, the dev trampolines and the reload ABI for the same observable behaviour. `with-allocator` is its own IR node rather than a let and two calls, because the restore has to happen on the transfer path too. A body that errors leaves through the landing pad, and a context allocator left pointing into a region nobody outside the body has heard of would be wrong in the break loop, which is exactly where something is about to allocate to render a condition. The acceptance program asserts that path by taking a restart out of a body. The backend grew one prim, `Rt of string`: a call into the runtime's C named by symbol, with argument and result types read off the expression nodes. The container runtime is type-erased and therefore *is* a list of C entry points, so one arm covers all of them rather than one arm each.
69 lines
3.1 KiB
Plaintext
69 lines
3.1 KiB
Plaintext
;;;; Allocators — spec-memory.md, "Allocators". No container here: this is the
|
|
;;;; tier on its own, so that a failure in it is not read as a Vec bug.
|
|
;;;;
|
|
;;;; What is asserted: the capability set is readable at run time and differs
|
|
;;;; per allocator; with-allocator rebinds for its dynamic extent and restores
|
|
;;;; afterwards, including out of a call and out of a transfer; free-all is
|
|
;;;; retain-capacity and bumps the epoch anyway; and nothing is released at
|
|
;;;; scope exit, which is the point the spec is most emphatic about.
|
|
|
|
;; A zeroed Allocator. A global rather than a local because the arena has to
|
|
;; outlive the frame that makes it, and because a handler cannot see a local
|
|
;; (check.ml's `captured` says so by name).
|
|
(defvar frame Allocator)
|
|
|
|
;;; The context is a dynamic variable, so a function called from inside a
|
|
;;; with-allocator body sees the rebinding without anything being passed.
|
|
(defn who-am-i [] bool
|
|
(can-free? context/allocator))
|
|
|
|
(defn main [] i32
|
|
;; The heap allocator frees one block; an arena does not. That is Odin's
|
|
;; answer too — its arena returns Mode_Not_Implemented for .Free — and it is
|
|
;; the capability spec-memory.md calls load-bearing.
|
|
(set frame (arena-new 1024))
|
|
(println (can-free? (heap-allocator))) ; true
|
|
(println (can-free? frame)) ; false
|
|
(println (can-free-all? (heap-allocator))) ; false
|
|
(println (can-free-all? frame)) ; true
|
|
|
|
;; The default context is the heap allocator, and context/temp is its own
|
|
;; arena — the per-frame tier, distinct from it.
|
|
(println (can-free? context/allocator)) ; true
|
|
(println (can-free? context/temp)) ; false
|
|
|
|
;; with-allocator rebinds for the dynamic extent, so a call made from inside
|
|
;; the body sees the arena, and the binding is gone after the body.
|
|
(println (with-allocator frame (who-am-i))) ; false
|
|
(println (who-am-i)) ; true
|
|
|
|
;; ... and it is an expression: the body's last value is the form's value.
|
|
(println (with-allocator frame 41)) ; 41
|
|
|
|
;; free-all is retain-capacity: the pages stay, the epoch moves. Both halves
|
|
;; matter — the first is what makes a per-frame reset free, and the second is
|
|
;; what a container's dev trap reads.
|
|
(println (alloc-epoch frame)) ; 0
|
|
(free-all frame)
|
|
(println (alloc-epoch frame)) ; 1
|
|
(free-all frame)
|
|
(println (alloc-epoch frame)) ; 2
|
|
|
|
;; Nothing is released at scope exit — not at the end of a let, not at the
|
|
;; end of a with-allocator body. The epoch is the observable proof: leaving
|
|
;; the body did not release the region it named.
|
|
(let [before (alloc-epoch frame)]
|
|
(with-allocator frame (println (alloc-epoch frame))) ; 2
|
|
(println (= before (alloc-epoch frame)))) ; true
|
|
|
|
;; And out of a transfer. The restart-case's clause runs after the body has
|
|
;; left through the pad, so the context allocator here is the one the
|
|
;; with-allocator displaced, not the arena.
|
|
(println
|
|
(restart-case
|
|
(with-allocator frame (invoke-restart 'resync))
|
|
(resync [] (can-free? context/allocator)))) ; true
|
|
|
|
(arena-destroy frame)
|
|
0)
|