Joseph Ferano
87b5dad486
BUILT.md gets the section: the 32/32 split, live-is-odd and the two things that fall out of it, wrapping retiring the slot, why resolve answers (Option (Ptr T)) and where the spec already said so, why len is the slot high-water and not the live count, and why a slot is released through the pool rather than through free. Two amendments to a 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, and the spec's own worked example resolves first and matches. The pointer hole is written down rather than implied: a (Ptr T) from resolve dies on any insert that grows, which is the slice contract one level down. NEXT.md swept, not just struck — five places beyond item 6 were still asserting that Handle did not exist.
104 lines
4.8 KiB
Plaintext
104 lines
4.8 KiB
Plaintext
;;;; (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)))))
|