Joseph Ferano
69f5d8a05a
A program that wants to load its data once and keep it could not say so. Every move-only global was refused where it was declared, on an argument about the dead set being per function: two functions each freeing the same global would be a double free nothing could see. The argument was sound and the conclusion was too strong. It assumed a global has an owner. It does not. Reading a move-only global is now always a borrow. Nothing may take ownership of one, so nothing may free one, and with no owner to hand over there is no double free left to catch. This is not a general ownership model for globals and is not meant to grow into one: it is sound precisely because the lifetime question that model would exist to answer has a constant answer here, the process's. The refusal lands at the read, which is where a move would have been recorded for a local -- passing the global to something that owns its parameter, binding it to a local, returning it and freeing it all reach the same place, and each is told to borrow instead, or to clone if it really wants something of its own. Such a global is mutable where it stands. push, put, reserve and set already take their target through the borrow path, so a global (Vec u8) is filled and grown in place, and the aliasing that raises is the one every Vec has: spec-memory.md's explicit Zig/Odin contract, where a push that reallocates invalidates a slice taken before it and the dev build's generation word traps on the stale one. Globals get no borrow rule locals do not have, because the hazard is not new and the trap lives on the Vec rather than on the binding. What a move-only global may not do is carry a computed initialiser. A global's initialiser is a link-time constant -- there is no init-at-startup path in the LLVM backend by design, and the x86 backend that has one deliberately leaves it out of a reload module, because re-running an initialiser wipes the live state reloading exists to preserve. So the global starts zeroed, which for a Vec is an empty Vec and therefore a value rather than a placeholder, and the load is an ordinary assignment in whichever function loads it. That is also what makes the data survive: nothing runs between one entry to main and the next, so a re-entered main finds the global as it left it. A defconst cannot be one at all, since a constant is not an assignable place and nothing could ever load it; both refusals name the (defvar g (Vec u8)) that works. The reload fixture gains a global Vec in the host and another that arrives at run time, because that is where declaring instead of defining has teeth: a module that defined the host's Vec would take a zeroed header of its own and strand the block the process is still using, which a re-zeroed i64 cannot demonstrate.
59 lines
2.2 KiB
Plaintext
59 lines
2.2 KiB
Plaintext
;;;; A global of move-only type, which is allowed, and the one rule that makes
|
|
;;;; it allowed: reading a global Vec is always a borrow and never a move. The
|
|
;;;; lifetime question ownership tracking exists to answer has a constant
|
|
;;;; answer here — the process's — so nothing may take the global and nothing
|
|
;;;; may free it, and with no owner to hand over there is no double free to
|
|
;;;; catch. The refusals that enforce that are in test_flan.ml.
|
|
;;;;
|
|
;;;; A zeroed Vec is a real empty Vec, so the global starts as one and is
|
|
;;;; loaded by whoever loads it. What this program pins is that the loading
|
|
;;;; happens once and survives: [entry] is called twice, the way a re-entered
|
|
;;;; main would be, and the second call finds the data the first one left.
|
|
(defvar the-data (Vec u8))
|
|
(defvar counts (Map u8 i64))
|
|
|
|
;; Reading it here is a borrow. So is reading it in [total] below, which is the
|
|
;; case the old rule could not express: two functions holding the same global
|
|
;; at once is fine exactly because neither of them can free it.
|
|
(defn loaded? [] bool (> (len the-data) 0))
|
|
|
|
(defn load [] ()
|
|
(when (not (loaded?))
|
|
(set the-data (vec-new u8))
|
|
(dotimes [i 5] (push the-data (u8 (* i 3))))))
|
|
|
|
(defn total [] i64
|
|
(let [s (i64 0)]
|
|
(dotimes [i (len the-data)] (set s (+ s (i64 (at the-data i)))))
|
|
s))
|
|
|
|
;; Mutating in place, through the global rather than through a copy of it. The
|
|
;; aliasing contract is the one every Vec has (spec-memory.md, "Borrowing"): a
|
|
;; push may reallocate and invalidate a slice taken before it, and that is the
|
|
;; programmer's, here as much as for a local.
|
|
(defn bump [] ()
|
|
(set (at the-data 0) (+ (at the-data 0) 1))
|
|
(push the-data 100))
|
|
|
|
(defn entry [] ()
|
|
(load)
|
|
(bump)
|
|
(put counts 1 (total))
|
|
(println (len the-data))
|
|
(println (total))
|
|
(match (get counts 1) (Some v) (println v) None (println "?")))
|
|
|
|
(defn main [] i32
|
|
(entry)
|
|
;; The second run. Nothing re-initialises the global between them, so the
|
|
;; length keeps climbing and the loaded data is the same block it was.
|
|
(entry)
|
|
(println (len (as-slice the-data)))
|
|
;; A copy is the one thing something else may own, and freeing that copy
|
|
;; leaves the global untouched.
|
|
(let [c (clone the-data)]
|
|
(println (len c))
|
|
(free c))
|
|
(println (len the-data))
|
|
0)
|