diff --git a/lib/check.ml b/lib/check.ml index a9895d6..9253654 100644 --- a/lib/check.ml +++ b/lib/check.ml @@ -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 diff --git a/spec-memory.md b/spec-memory.md index c10fac4..5eb17f6 100644 --- a/spec-memory.md +++ b/spec-memory.md @@ -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 diff --git a/test/programs/reload-v2.flan b/test/programs/reload-v2.flan index d4a7bb0..ad80dee 100644 --- a/test/programs/reload-v2.flan +++ b/test/programs/reload-v2.flan @@ -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)) diff --git a/test/programs/reload-v3.flan b/test/programs/reload-v3.flan index f2c33c1..78665cb 100644 --- a/test/programs/reload-v3.flan +++ b/test/programs/reload-v3.flan @@ -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)) diff --git a/test/programs/reload.flan b/test/programs/reload.flan index 910f304..5693798 100644 --- a/test/programs/reload.flan +++ b/test/programs/reload.flan @@ -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 diff --git a/test/programs/vec-global.flan b/test/programs/vec-global.flan index b1be5f6..4647a21 100644 --- a/test/programs/vec-global.flan +++ b/test/programs/vec-global.flan @@ -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) diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml index a5d59bf..10d12f4 100644 --- a/test/test_acceptance.ml +++ b/test/test_acceptance.ml @@ -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 diff --git a/test/test_flan.ml b/test/test_flan.ml index b5c9524..bbf2c74 100644 --- a/test/test_flan.ml +++ b/test/test_flan.ml @@ -956,6 +956,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. *) diff --git a/test/test_reload.ml b/test/test_reload.ml index ff23ce7..39c68c8 100644 --- a/test/test_reload.ml +++ b/test/test_reload.ml @@ -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. *)