JosephFerano/flan
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

A global Vec is borrowed, never moved, and outlives every entry to main

Browse Source 
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.
This commit is contained in:
Joseph Ferano 2026-09-17 18:42:01 +07:00
parent 0251cf4aaa
commit 69f5d8a05a
9 changed files with 285 additions and 33 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

119
lib/check.ml
View File

@ -1758,7 +1758,9 @@ and var ctx loc ~want name =
expect loc ~want (mk loc b.bty (Tast.Local b.slot))
| None ->
match Hashtbl.find_opt ctx.env.globals name with
| Some (ty, _) -> expect loc ~want (mk loc ty (Tast.Global name))
| Some (ty, _) ->
if Types.is_move_only ty then global_borrow ctx loc name ty;
expect loc ~want (mk loc ty (Tast.Global name))
| None ->
match Hashtbl.find_opt ctx.env.cases name with
(* A case with no fields is a whole value on its own, so it is written
@ -1820,6 +1822,46 @@ and moved ?ty ctx loc name slot =
| None -> ());
if not ctx.borrow then ctx.dead <- (slot, loc) :: ctx.dead
(* Reading a move-only *global*, which is the same fork as [moved] with the
other answer: a global is never moved out of, so a site that would have
taken ownership is refused rather than recorded.
The rule this enforces is one sentence — reading a move-only global is
always a borrow. It is sound for a reason that does not generalise to
locals: the lifetime question, which ownership tracking exists to answer,
has a constant answer here. A global lives as long as the process, so
nothing may free it and nothing needs to; there is no frame whose exit it
could outlive and no second owner to disagree with. What would break the
argument is exactly one thing — someone taking ownership — and that is a
move, and every move reaches this function because [ctx.borrow] is false
everywhere except the operations that said they only look.
So the dead set is not consulted and not extended. A global cannot be dead:
two functions reading the same one are both borrowing it, which is why the
per-function dead set that the declaration site used to argue from was
never the obstacle it looked like. It could not track a global's ownership;
with this rule there is no ownership to track.
Mutation is not a move and is not refused. [push], [put] and [set] all take
their target through [borrowed], so a global (Vec u8) is filled and grown in
place, and the aliasing that raises — a push that reallocates invalidating a
slice into the same Vec — is the programmer's, exactly as it is for a local
(spec-memory.md, "Borrowing", and the note on [as-slice] below). Globals get
no rule locals do not have: the dev build's generation word lives on the Vec
and traps on a stale slice whether the Vec is a global or not. *)
and global_borrow ctx loc name (ty : Types.t) =
if not ctx.borrow then
fail loc
"%s is %s, which is move-only, and a global of one is only ever \
borrowed: its lifetime is the process's, so nothing may take ownership \
of it, and this site would. A free through the new owner would leave \
every other reader of %s pointing at released memory. Read and mutate \
it where it is — (len %s), (at %s i), (push %s x), (set (at %s i) x) \
— or take a view with (as-slice %s), a pointer with (addr %s), or an \
independent copy with (clone %s), which is the one of these that \
something else may own"
name (Types.to_string ty) name name name name name name name name
(* The target of an operation that reads a container without consuming it. Only
a syntactically simple target is treated as a borrow: in [(len (f v))] the
call still moves [v], and setting the flag over the whole subexpression
@ -5548,22 +5590,63 @@ and check_generic env (fn : Ast.fn) =
checking a function. *)
let () = check_fn_ref := check_fn
(* A global of move-only type is refused. The dead set is per function, so two
functions each freeing the same global is a double free nothing here could
see; and within one function a global read does not go through [var]'s move
path at all, so even the local case would be accepted. Rather than half a
rule, the type is refused where it is declared. A global *Allocator* is not
this — an allocator is a copyable opaque handle — which is what makes the
handler-owns-the-arena shape in exhausted.flan expressible. *)
let no_move_only_global loc n (ty : Types.t) =
no_zeroed_fn loc (Printf.sprintf "the global %s" n) ty;
(* A global of move-only type is legal, and what makes it legal is [var]'s
refusal rather than anything here: reading one is always a borrow, so no
function can take it, and none can free it. See [global_borrow] for why that
one sentence is enough where a general ownership model would not be.
What this pass still decides is how such a global may be *started*, and the
answer is zeroed and nothing else. A zeroed Vec is a real empty Vec — null
block, zero length, zero capacity — so the ZII value is the value a program
would have written anyway, and filling it is an ordinary (set g (slurp
"...")) in whichever function loads it. The alternative, a computed
initialiser, does not exist to be relaxed into: [Emit.const] says so in as
many words ("there is no init-at-startup path, by design"), and the backend
that does run initialisers at startup, [x86.ml], runs them from .init_array
before main and deliberately omits them from a reload module, because
re-running one would wipe the live state reloading exists to preserve. A
rule that held on one backend and not the other would not be a rule.
That fits what a runtime-loaded global is for. The data is loaded by
whoever loads it, once, and it outlives main: a main that returns and is
entered again finds the global exactly as it left it, because nothing
between the two runs touches it. Assigning a second time overwrites the
first block and leaks it — there is no [drop] and no cross-function flow
analysis that could see the second assignment, so that is the manual-memory
answer and the language's own: free is a thing you write.
A global *Allocator* is not any of this — an allocator is a copyable opaque
handle — which is what makes the handler-owns-the-arena shape in
exhausted.flan expressible. *)
let move_only_global_init loc n (ty : Types.t) (init : Ast.init) =
if Types.is_move_only ty then
match init with
| Ast.Zeroed -> ()
| _ ->
fail loc
"the global %s is %s, which is move-only, and a move-only global \
starts zeroed: a global's initialiser is a compile-time constant and \
%s is not one. Write (defvar %s %s) with no initialiser — a zeroed \
%s is an empty one, and that is a value, not a placeholder — then \
load it with (set %s ...) in the function that loads it, which runs \
once and whose result outlives every call to main"
n (Types.to_string ty)
(match init with Ast.Uninit -> "uninit" | _ -> "this initialiser")
n (Types.to_string ty) (Types.to_string ty) n
(* A move-only global has to be a [defvar]. A [defconst] is not an assignable
place — [check_place] refuses one by name — so a constant Vec could only
ever hold the zeroed value it was declared with, and nothing could ever put
the file's bytes in it. Refused here, where the fix is one keyword, rather
than at the (set ...) that discovers it three forms later. *)
let no_move_only_defconst loc n (ty : Types.t) =
if Types.is_move_only ty then
fail loc
"the global %s is %s, which is move-only, and ownership of a global \
cannot be tracked: the dead set is per function, so two functions each \
freeing it is a double free nothing would catch. Hold it in a local and \
pass it, or hold the allocator globally instead"
n (Types.to_string ty)
"the global %s is %s, which is move-only, and a move-only global is a \
defvar and not a defconst: a constant is not an assignable place, so \
nothing could ever load this one — it would stay the empty %s it was \
declared as. Write (defvar %s %s) and fill it in a function"
n (Types.to_string ty) (Types.to_string ty) n (Types.to_string ty)
let check_global env (d : Ast.decl) : Tast.global option =
let ctx () = { env; ret = Types.Unit; slots = 0; slot_tys = []; slot_names = []; scope = []; defers = [];
@ -5571,7 +5654,8 @@ let check_global env (d : Ast.decl) : Tast.global option =
match d.Ast.d with
| Ast.Defvar (n, _, init) ->
let ty, _ = Hashtbl.find env.globals n in
no_move_only_global d.Ast.dloc n ty;
no_zeroed_fn d.Ast.dloc (Printf.sprintf "the global %s" n) ty;
move_only_global_init d.Ast.dloc n ty init;
let ginit =
match init with
| Ast.Zeroed -> { Tast.e = Tast.Zero ty; ty; loc = d.Ast.dloc }
@ -5601,7 +5685,8 @@ let check_global env (d : Ast.decl) : Tast.global option =
Some { Tast.gname = n; gty = ty; ginit; gconst = false; gfolded = false }
| Ast.Defconst (n, _, v) ->
let ty, _ = Hashtbl.find env.globals n in
no_move_only_global d.Ast.dloc n ty;
no_zeroed_fn d.Ast.dloc (Printf.sprintf "the global %s" n) ty;
no_move_only_defconst d.Ast.dloc n ty;
(* [collect] already folded the integer constants, because an array length
has to be known before any type resolves. Use that value here rather
than the expression it came from: a global's initialiser has to be a

40
spec-memory.md
View File

@ -42,8 +42,9 @@ Equality and hashing for those keys are compiler-provided structural operations
and not type classes. They are not available to an unconstrained type variable
either; a variable that means to key a map declares `hashable?` in the signature
that binds it, and the refusal then lands at the call site that names an
unhashable key. An empty map names its key and value types, because a global
cannot hold one and there is therefore no declaration for it to take a type from:
unhashable key. An empty map names its key and value types, because the position
it is usually written in — a `let` binding — has no type slot for it to take
them from:
```
(let [enemies (map-new string Enemy)]
@ -88,6 +89,41 @@ once — and a type with one cannot be `clone`d.
- Cross-referencing long-lived objects uses `(Handle a)` into a pool, never a
raw pointer or slice. A stale handle is detectable.
## Globals of move-only type
A global may be a `Vec` or a `Map`, and **reading one is always a borrow, never
a move**. Nothing can take ownership of it, so nothing can `free` it; its
lifetime is the process's and it is never released. That is one rule rather than
a general ownership model for globals, and it is sound for the reason a general
model would be needed and is not: the lifetime question has a constant answer.
Passing a global to a function that owns its parameter, binding it to a local,
returning it and freeing it are all refused at the read, which is exactly where
a move would have been recorded for a local. `(clone g)` is the one of these
that yields something another owner may have.
Such a global is **mutable in place**: `push`, `put`, `reserve` and `set` all
take their target as a borrow, so a global `(Vec u8)` is filled and grown where
it stands. The aliasing contract is the one above and nothing more — a push that
reallocates invalidates a slice taken before it, and that is the programmer's
whether the owner is a local or a global. Globals get no borrow rule locals do
not have; the dev build's generation word lives on the `Vec`, so the stale-slice
trap works the same either way.
A move-only global **starts zeroed** — a zeroed `Vec` is an empty `Vec` — and is
loaded by whichever function loads it, with an ordinary assignment:
```
(defvar the-data (Vec u8))
(defn load [] () (set the-data (slurp "game-data.edn")))
```
A computed initialiser on the declaration is refused: a global's initialiser is
a link-time constant, and the load has to be something the program does rather
than something that happens before `main`. That is also what makes the data
outlive `main` — nothing re-runs between one entry and the next, so a re-entered
`main` finds the global as it left it. Assigning a second time overwrites the
first block and leaks it; there is no `drop`, and freeing is a thing you write.
## Taking an address
`(addr x)` yields `(Ptr T)` for any assignable place `x` — a local, a global, a

1
test/programs/reload-v2.flan
View File

@ -15,6 +15,7 @@
;;;; host's [* x 2]; with the two bodies identical nothing at run time would
;;;; notice a module that grew its own copy.
(defvar counter i64)
(defvar tally (Vec u8))
(defn helper [x i64] i64 (* x 3))

6
test/programs/reload-v3.flan
View File

@ -9,6 +9,12 @@
;;;; is a module referring to storage that does not exist yet.
(defvar counter i64)
(defvar extra i64)
;;; And a run-time-new one of move-only type: no symbol to bind to, so it goes
;;; through the by-name registry like [extra], with its declared initial value
;;; travelling along as a constant. A zeroed Vec is an empty Vec, so that
;;; constant is a zeroinitializer and the allocation the registry makes is a
;;; usable Vec rather than a placeholder.
(defvar fresh (Vec u8))
(defn helper [x i64] i64 (* x 2))

9
test/programs/reload.flan
View File

@ -12,6 +12,15 @@
;;;; its own constants, and a one-function module usually has none.
(defvar counter i64)
;;; A move-only global, which is allowed because reading one is always a borrow
;;; (spec-memory.md, "Globals of move-only type"). It is here for the reload
;;; question rather than the ownership one: a redefinition module declares it
;;; [external] like any other host global, so a load must not hand the module
;;; its own zeroed header -- that would drop the storage the running process is
;;; still using, which is the failure a plain i64 counter cannot exhibit
;;; because a re-zeroed i64 merely looks wrong.
(defvar tally (Vec u8))
;;; Unused, and that is the point: the session's compatibility rules only get a
;;; chance to speak about a change the *checker* accepts, and retyping a var
;;; something else reads is an ordinary type error long before it is a layout

65
test/programs/vec-global.flan
View File

@ -1,9 +1,58 @@
;;;; A global of move-only type. The dead set is per function, so two functions
;;;; each freeing this is a double free nothing here could see — and a global
;;;; read does not go through the move path at all, so even the one-function
;;;; case would be accepted. Half a rule is worse than none, so the type is
;;;; refused where it is declared. A global *Allocator* is a different thing
;;;; and is allowed: an allocator is a copyable opaque handle.
(defvar everything (Vec i32))
;;;; 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))
(defn main [] i32 0)
;; 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)

21
test/test_acceptance.ml
View File

@ -117,6 +117,15 @@ let () =
outputs "value semantics" "programs/values.flan" values_out;
outputs "machine surface" "programs/machine.flan" machine_out;
outputs "unit main exits 0" "programs/unit-main.flan" "ok\n";
(* A global of move-only type, which this compiler used to refuse outright.
What the numbers assert is the half of the rule no checker test can: the
global is loaded once and *stays* loaded across a second entry, which is
what a re-entered main needs, and the mutations land on the global
itself rather than on a copy of its header — the second run's length is
the first run's plus one, and the count after cloning and freeing the
clone is still the global's. *)
outputs "a global Vec" "programs/vec-global.flan"
"6\n131\n131\n7\n232\n232\n7\n7\n7\n";
(* (array COUNT TYPE). Every line of it is a [let] binding, which is the
one position with no type slot and the whole reason the form exists. *)
outputs "array constructor" "programs/array-ctor.flan" "4\n0\n7\n9\n4\n";
@ -1755,14 +1764,14 @@ let () =
there is nothing to infer from — and guessing is the alternative. *)
refuses "vec-new with nothing saying what of" "programs/vec-untyped.flan"
"write the element type";
(* The three shapes ownership is not transitive through yet. Each is
refused where it is declared, naming drop as what it waits on, rather
than accepted into a path that would copy a header and hand out a
second owner. *)
(* The two shapes ownership is not transitive through yet. Each is refused
where it is declared, naming drop as what it waits on, rather than
accepted into a path that would copy a header and hand out a second
owner. A global used to be the third; it is not any more, and the
program that was this row is now an accepted one — see "a global Vec"
above, and [Check.global_borrow] for the rule that replaced it. *)
refuses "a struct field that owns a Vec" "programs/vec-in-struct.flan"
"a struct that owns one is move-only too";
refuses "a global Vec" "programs/vec-global.flan"
"the dead set is per function";
refuses "a Vec of a Vec" "programs/vec-of-vec.flan"
"copies and releases elements bytewise";
(* And it does not cross to C: the shim would flatten a header that owns

41
test/test_flan.ml
View File

@ -901,6 +901,47 @@ let () =
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";
(* ── A move-only global ─────────────────────────────────────────────
Legal now, and legal because of one rule: reading one is always a borrow.
The accepted side is programs/vec-global.flan, which has to run to say
anything; these are the four things the rule refuses, and between them
they are the whole of it.
The first two are the rule itself. Ownership is what may not be taken, and
the two ways to take it — hand the global to something that owns its
parameter, or bind it to a local that owns it — are the same refusal at
the read, because that is where a move would have been recorded for a
local. [free] is the third of them and reaches it the same way: it does
not borrow its target, so nothing special had to be written for it. *)
rejects_check "passing a global Vec to a function"
"(defvar g (Vec u8)) (defn eat [v (Vec u8)] () (free v)) (defn f [] () (eat g))"
~needle:"only ever borrowed";
rejects_check "freeing a global Vec"
"(defvar g (Vec u8)) (defn f [] () (free g))"
~needle:"only ever borrowed";
rejects_check "binding a global Vec to a local"
"(defvar g (Vec u8)) (defn f [] () (let [v g] (free v)))"
~needle:"only ever borrowed";
(* And the two declaration shapes. A computed initialiser would have to run
before main, which is a path [Emit.const] does not have and which
[x86.ml] deliberately leaves out of a reload module; a defconst could
never be assigned, so nothing could ever load it. Both name the (defvar g
(Vec u8)) that works, which is the point of refusing them here rather
than letting the backend say "this one is computed" three passes later. *)
rejects_check "a global Vec with a computed initialiser"
"(defvar g (Vec u8) (slurp \"game-data.edn\")) (defn f [] ())"
~needle:"starts zeroed";
rejects_check "a move-only global as a defconst"
"(defconst g (Vec u8) (slurp \"game-data.edn\")) (defn f [] ())"
~needle:"a defvar and not a defconst";
(* The borrows, which are what is left once ownership is off the table: a
global Vec is read, mutated in place, viewed and copied, and the copy is
the one thing something else may own. *)
accepts "a global Vec is borrowed, mutated and cloned"
"(defvar g (Vec u8)) \
(defn f [] () (set g (vec-new u8)) (push g 1) (set (at g 0) 2) \
(println (len (as-slice g))) (let [c (clone g)] (free c)))";
(* 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. *)

16
test/test_reload.ml
View File

@ -111,6 +111,13 @@ let () =
in
if not (has ir2 "@\"flan.counter\" = external global i64") then
fail "redefinition defines the global instead of declaring it";
(* The same rule for a global of move-only type, where it has teeth the
scalar case cannot show. A module that defined [tally] would get a
zeroed Vec header of its own, and the block the running process had
already filled would be storage nothing points at any more — a leak the
reload caused, not the program. A re-zeroed i64 only looks wrong. *)
if not (has ir2 "@\"flan.tally\" = external global %vec") then
fail "redefinition defines a move-only global instead of declaring it";
(* In a dev module a sibling is reached only through its cell, so there is
nothing to declare and a [define] would be a private copy. *)
if has ir2 "declare i64 @\"flan.helper\"" then
@ -133,6 +140,15 @@ let () =
fail "a run-time-new global did not get a slot";
if has ir3 "@\"flan.extra\" = " then
fail "a run-time-new global was given storage in the module";
(* And a run-time-new global of move-only type, which takes the same path
and is the case where the initial value that travels with it has to be
a real value rather than a placeholder: a zeroed Vec is an empty Vec,
so the registry's allocation is usable the moment it exists. This runs
as well as being read — the host loads v3 below. *)
if not (has ir3 "@\"flan.gp.fresh\" = internal global ptr null") then
fail "a run-time-new move-only global did not get a slot";
if has ir3 "@\"flan.fresh\" = " then
fail "a run-time-new move-only global was given storage in the module";
(* Every lookup is resolved before any body is published: publishing first
exposes a function whose module-local slots are still null to anything
that calls it. Not race-testable, so it is asserted on the text. *)