The x86 backend and dyn finally meet, which is where the dev loop is
x86 is what flan dev takes by default and dyn is the iteration feature, so a backend that refused dyn meant the two halves of the dev loop could not be in the same program. The refusal was one arm of is_agg, and it said the true thing: it was never the representation that was missing. A dyn is uint64_t, a scalar in both calling conventions, classified by every rule this file already had; every operation on one is a Tast.Rt primitive and call_rt has always known how to make one of those. What the lane actually cost was the collector's root discipline. Which is emit.ml's, reused rather than rewritten: Emit.dyn_roots counts the roots for both backends now, so the pushes and the pops balance because one counter decides both ends, and the two backends root the same nodes because there is one counter and not two. A zeroed frame slot per dyn slot and per dyn-producing call, minted beside the channel and outside every scoped -- the bump allocator reclaims at the end of a statement and a slot minted in the body would be handed out again while the collector still held its address. Pushed from the body buffer, not the prologue's, because a call clobbers the registers the prologue is still spilling from. And one pop in the epilogue, which is the whole of why this backend needed no landing-pad work for it: there is exactly one epilogue, and the return, the fall-through and the transfer exit all arrive at it. emit.ml needs the same pop at five separate rets. The ABI point the dyn handoff left open for the integrator is settled by reading the other side rather than by agreeing: flan_dyn.c's mark follows a value only when the quiet-NaN prefix is set, and the zero word does not have it, so a zeroed root decodes as the double 0.0 and is never an address anything dereferences. Zero is safe for a reason. The header says so now. And one line in dev.ml that was never x86's: the merged dev host resets the condition stacks and the frame chain between runs, because main is re-entered by longjmp and pops no frame -- and it never reset the root stack, so every root a finished run pushed still named stack the next run was about to write over. That gap was an LLVM dev build's too. Verification, and one of the numbers is new. @x86: MATCH 129 -> 135, DIFFER 0, REFUSED 0 -- the five dyn programs off survey.sh's llvmonly list, which is gone rather than empty, plus p13. dune test --force green, with --x86 acceptance rows beside the LLVM ones for all five dyn programs, dyn-boundary asserted on the same exit 134 and the same sentence on both. p13-dyn-collect.flan is the one that is not a formality. Nothing else in this repository allocates past flan_dyn.c's one-megabyte floor, so nothing else collects even once, so a program whose roots are entirely wrong passes every output test there is -- the handoff wrote that about the stub and it outlived the stub. p13 allocates several megabytes of garbage while holding live values across it: at forty times the corpus size it peaks at 4MB of RSS, which is the collector running many times over, and both backends still print the same four lines.
This commit is contained in:
parent
2ec12c064d
commit
c2d378957e
@ -84,6 +84,17 @@ encoding.
|
||||
If the real runtime NaN-boxes and integer zero is the zero word, this is wrong
|
||||
and the two sides need a different sentinel. Do not fix it on one side.
|
||||
|
||||
**Settled, by reading the other side.** The real runtime does NaN-box, and the
|
||||
zero word is *not* the zero integer: an integer is boxed, and boxed means the
|
||||
quiet-NaN prefix is set. `mark_value` in `runtime/flan_dyn.c` follows a value
|
||||
only when `dyn_boxed` holds, which tests `(v & 0xFFF8000000000000) ==
|
||||
0xFFF8000000000000`, and the zero word fails it. So a rooted slot holding 0
|
||||
decodes as the double `0.0` — an ordinary value rather than a marker, and
|
||||
crucially never an address the collector dereferences. Zero is safe, and the
|
||||
header's sentence is true for a reason both sides can check rather than by the
|
||||
two of them having guessed alike. No sentinel is needed and neither side
|
||||
changes.
|
||||
|
||||
## Not in milestone 1, each refused by name with a location
|
||||
|
||||
- a typed container boxing into dyn (`(Vec i64)` → dyn): "not yet"; the
|
||||
@ -99,7 +110,15 @@ and the two sides need a different sentinel. Do not fix it on one side.
|
||||
the ABI carries one of each, and a `need_i64` plus a truncation would put an
|
||||
implicit narrowing at the one boundary where the value's type was already
|
||||
uncertain
|
||||
- the x86 dev backend, and the JS dialect, refuse dyn entirely
|
||||
- ~~the x86 dev backend, and~~ the JS dialect, refuse dyn entirely. The x86
|
||||
backend does not any more: a dyn is one machine word in both calling
|
||||
conventions and every operation on one is an ordinary `Tast.Rt` call, so what
|
||||
the lane cost was the root discipline and not the arithmetic — a zeroed frame
|
||||
slot per dyn local and per dyn-producing call, pushed in the body buffer at
|
||||
entry, and one `flan_dyn_root_pop` in the epilogue that every return and
|
||||
every transfer out of the frame already went through. `Emit.dyn_roots` is
|
||||
called by both backends, which is what makes the counts agree rather than
|
||||
merely both being written down
|
||||
|
||||
## Roots: what is and is not verified
|
||||
|
||||
|
||||
@ -3480,6 +3480,14 @@ extern void (*flan_exit_hook)(int32_t status);
|
||||
extern void flan_condition_stacks_reset(void);
|
||||
extern void flan_dev_frames_reset(void) __attribute__((weak));
|
||||
|
||||
/* And the collector's roots, which are the third stack threaded through stack
|
||||
* the finished run no longer owns. main is re-entered by longjmp, which pops
|
||||
* no frame, so every root the last run pushed still names an address the next
|
||||
* run is about to write over — and the next mark would follow whatever it put
|
||||
* there. Weak for the reason the frames reset is weak; runtime/flan_dyn.h
|
||||
* exports this for this one caller. */
|
||||
extern void flan_dyn_root_reset(void) __attribute__((weak));
|
||||
|
||||
/* The agent's ring, drained on whatever thread calls this. Weak for the reason
|
||||
* the reset above is weak, and it is the same class of fact: a merged binary
|
||||
* links the agent by construction, which is exactly the kind of guarantee that
|
||||
@ -3628,6 +3636,7 @@ static void flan_merged_exit(int32_t status) {
|
||||
static void flan_merged_park(void) {
|
||||
flan_condition_stacks_reset();
|
||||
if (flan_dev_frames_reset) flan_dev_frames_reset();
|
||||
if (flan_dyn_root_reset) flan_dyn_root_reset();
|
||||
pthread_mutex_lock(&program_lock);
|
||||
program_state = PROGRAM_PARKED;
|
||||
pthread_mutex_unlock(&program_lock);
|
||||
|
||||
236
lib/x86.ml
236
lib/x86.ml
@ -475,23 +475,16 @@ let is_agg (t : Types.t) =
|
||||
| Types.Unit | Types.Never -> false
|
||||
| Types.String | Types.Slice _ | Types.Array _ | Types.Map _ | Types.Vec _
|
||||
| Types.Option _ | Types.Named _ -> true
|
||||
(* Refused by name rather than classified. A dyn word is one machine word and
|
||||
would classify trivially — it is not the representation that is missing,
|
||||
it is every operation on it, which is a call into runtime/flan_dyn.h that
|
||||
this backend does not emit. Saying "a dyn value" here rather than letting
|
||||
it through to fail at the first [+] means the reader is told the one true
|
||||
thing about their program instead of something about an opcode.
|
||||
|
||||
The sentence naming [--llvm] is not written here on purpose: both callers
|
||||
add it, and each says it differently for a good reason — Session because
|
||||
the daemon takes this backend by default and the reader chose a program
|
||||
rather than a code generator, and main.ml only when [--x86] was not typed
|
||||
out. Repeating it here would say it twice to the one reader and to the
|
||||
wrong one. *)
|
||||
| Types.Dyn ->
|
||||
unsupported
|
||||
"a dyn value. Every operation on one is a call into the dynamic runtime, \
|
||||
and this backend emits none of them"
|
||||
(* A scalar, and trivially one: runtime/flan_dyn.h says [typedef uint64_t
|
||||
flan_dyn], so a dyn is a machine word in both calling conventions and
|
||||
nothing about it is ever passed by address. This arm used to refuse — not
|
||||
because the representation was missing but because every *operation* on
|
||||
one is a call into the dynamic runtime, and for a while this backend
|
||||
emitted none of them. It emits them now: they are [Tast.Rt] primitives
|
||||
like every other runtime call, and [call_rt] has always known how to make
|
||||
one. What the lane actually cost was the collector's root discipline, not
|
||||
the arithmetic. *)
|
||||
| Types.Dyn -> false
|
||||
| Types.Var v -> unsupported "type variable %s" v
|
||||
|
||||
let is_void (t : Types.t) = match t with Types.Unit | Types.Never -> true | _ -> false
|
||||
@ -656,6 +649,23 @@ type fnctx = {
|
||||
anyway is what makes the two backends' frames answer identically, which is
|
||||
the only thing the break loop can check. *)
|
||||
mutable dslotv : int option;
|
||||
(* The collector's shadow stack — runtime/flan_dyn.h's [flan_dyn_root_push]
|
||||
and [flan_dyn_root_pop]. [droots] is how many this function pushed at
|
||||
entry and so how many the one pop in the epilogue takes off; [droot_ns]
|
||||
is the frame offsets of the *temporaries* among them, in push order,
|
||||
handed out one at a time by [dyn_tmp] as the body is lowered. Both are
|
||||
zero and empty for every function with no dyn in it, and then not an
|
||||
instruction is emitted — which is what keeps every other program in the
|
||||
survey byte for byte what it was.
|
||||
|
||||
A count rather than a running tally for [emit.ml]'s reason: the epilogue
|
||||
is emitted after the body, but the pushes are decided before it, by
|
||||
[Emit.dyn_roots], which is deliberately the *same* function both backends
|
||||
call. The pushes and the pops balance because one counter decides both
|
||||
ends, and the two backends root the same nodes because there is one
|
||||
counter and not two. *)
|
||||
mutable droots : int;
|
||||
mutable droot_ns : int list;
|
||||
(* [fn.snames], carried so [bind_slot] can ask whether a slot has a name to
|
||||
show without the whole [Tast.fn] being threaded to every binding site. *)
|
||||
snames : string option array;
|
||||
@ -1361,6 +1371,24 @@ let with_pad f tag g =
|
||||
f.pads <- List.tl f.pads;
|
||||
(pad, used, r)
|
||||
|
||||
(* The next pre-made root slot for a dyn temporary — [emit.ml]'s [dyn_tmp],
|
||||
in frame offsets rather than alloca names. Every one of them was minted,
|
||||
zeroed and pushed before a line of the body was emitted, and this only
|
||||
hands them out, which is what makes the pushes and the pops balance by
|
||||
construction rather than by the body being walked the same way twice.
|
||||
|
||||
[Emit.dyn_roots] counts the same nodes this emission visits, so the supply
|
||||
runs out only if those two disagree — and since both backends call that one
|
||||
function, disagreeing would be one of them visiting a node the other does
|
||||
not. The fallback is an ordinary unrooted temporary, for [emit.ml]'s
|
||||
reason and it is the same trade here: one dyn value the collector cannot
|
||||
see is a bug to go and find, where a root stack that pops more than it
|
||||
pushed is memory corruption. *)
|
||||
let dyn_tmp f =
|
||||
match f.droot_ns with
|
||||
| n :: rest -> f.droot_ns <- rest; n
|
||||
| [] -> alloc f 8 8
|
||||
|
||||
(* ── The runtime's two dynamic stacks ────────────────────────────────── *)
|
||||
|
||||
(* [emit.ml]'s [%handler] and [%restart] types, laid out by the C rules — the
|
||||
@ -2589,7 +2617,23 @@ and rt_signals sym =
|
||||
String.equal sym "flan_vec_at" || String.equal sym "flan_vec_as_slice"
|
||||
|
||||
and call_rt f ~sym ~args ~rty dst =
|
||||
call_native f ~sym ~chan:(rt_signals sym) ~args ~rty dst
|
||||
call_native f ~sym ~chan:(rt_signals sym) ~args ~rty dst;
|
||||
(* A dyn word is spilled into a rooted slot the instant it exists, because
|
||||
the next allocation may be the one that collects what it is holding and
|
||||
the collector finds its roots by address. [dst] is not enough: it is
|
||||
often a temporary inside a [scoped] that the bump allocator is about to
|
||||
hand out again, and it is never a slot anything was pushed for.
|
||||
[Emit.dyn_roots] counted this call, so the slot below is one the entry
|
||||
block has already zeroed and pushed.
|
||||
|
||||
Here rather than in [call_native], which is [call_c]'s as well: a dyn
|
||||
crossing to C is refused in the checker and there would be nothing to
|
||||
root. rax still holds the answer — [store_loc] above takes r11 for its
|
||||
scratch and nothing else. *)
|
||||
if rty = Types.Dyn then begin
|
||||
let slot = dyn_tmp f in
|
||||
store_int f.b ~src:rax ~mm:(Frame slot) ~size:8
|
||||
end
|
||||
|
||||
and call_native f ~sym ?(chan = false) ~(args : Tast.expr list) ~rty dst =
|
||||
(* A Vec and a Map cross to the runtime as their
|
||||
@ -3193,7 +3237,8 @@ let emit_fn (md : Emit.m) ~externs ~fns ?(ext = fun _ -> false)
|
||||
{ b; md; fnname = fn.Tast.name; retlbl = "";
|
||||
fret = fn.Tast.ret; slots = Array.make nslots 0;
|
||||
xfer_off = 0; sret_off = 0; retval = 0;
|
||||
dframe = None; dslotv = None; snames = fn.Tast.snames;
|
||||
dframe = None; dslotv = None; droots = 0; droot_ns = [];
|
||||
snames = fn.Tast.snames;
|
||||
frame = 0; maxframe = 0; outgoing = 0;
|
||||
loops = []; pads = []; xfer_lbl = ""; unwound = false;
|
||||
rodata = Buffer.create 64; externs; fns; ext; slot; dw;
|
||||
@ -3236,6 +3281,63 @@ let emit_fn (md : Emit.m) ~externs ~fns ?(ext = fun _ -> false)
|
||||
f.xfer_off <- ptmp f;
|
||||
if sret then f.sret_off <- ptmp f;
|
||||
if (not sret) && not (is_void fn.Tast.ret) then f.retval <- tmp f fn.Tast.ret;
|
||||
(* The collector's roots — runtime/flan_dyn.h. Not gated on [md.dev], unlike
|
||||
everything below it: the shadow stack is a debugging convenience a release
|
||||
build does without, while a collector that cannot find its roots is a
|
||||
collector that frees live values. Only a function with a dyn in it pays
|
||||
anything, because [Emit.dyn_roots] is zero otherwise and not an
|
||||
instruction is emitted — which is what keeps every dyn-free program in the
|
||||
survey byte for byte what it was before this lane.
|
||||
|
||||
The *slots* are already frame temporaries from the loop above, so they are
|
||||
pushed where they are; the temporaries need slots of their own, and they
|
||||
are minted here, beside the channel and the return temporary and outside
|
||||
every [scoped], because the bump allocator reclaims at the end of each
|
||||
statement and a slot minted inside the body would be handed out again to
|
||||
the next one while the collector still held its address.
|
||||
|
||||
The pushes themselves go into the *body* buffer below, not this one: this
|
||||
runs before the prologue is built, and it is the prologue that still has
|
||||
the incoming arguments in registers. *)
|
||||
let nroots = Emit.dyn_roots fn in
|
||||
(* The slots to zero and the offsets to push, worked out here and emitted
|
||||
into the body buffer further down. In push order, which is [emit.ml]'s:
|
||||
every dyn slot in slot order, and then the temporaries. The order has to
|
||||
be *an* order and this is the one both backends use, so an asm listing
|
||||
and an IR listing put the same value at the same depth.
|
||||
|
||||
A parameter's slot is filled from its incoming register in the prologue
|
||||
and must not be zeroed over the top of it; every other slot holds
|
||||
whatever the stack held until its binding runs, and the binding may be in
|
||||
a branch that does not.
|
||||
|
||||
Zero rather than a call to [flan_dyn_nil], and this is the ABI point the
|
||||
dyn handoff left open for the integrator while the collector was a stub.
|
||||
It is not a stub now, and the answer is in runtime/flan_dyn.c:
|
||||
[mark_value] follows a value only when [dyn_boxed] holds, which tests
|
||||
[(v & 0xFFF8...) == 0xFFF8...], and the zero word fails it. So a rooted
|
||||
slot holding 0 decodes as the double 0.0 — an ordinary value, not a
|
||||
marker, and crucially never a pointer the collector will follow. Zero is
|
||||
safe, and it is safe for a reason rather than by the two sides having
|
||||
guessed the same thing. *)
|
||||
let droot_zero = ref [] and droot_push = ref [] in
|
||||
if nroots > 0 then begin
|
||||
let nparams = List.length fn.Tast.params in
|
||||
let slots = ref [] and zeros = ref [] in
|
||||
Array.iteri
|
||||
(fun i t ->
|
||||
if t = Types.Dyn then begin
|
||||
slots := f.slots.(i) :: !slots;
|
||||
if i >= nparams then zeros := f.slots.(i) :: !zeros
|
||||
end)
|
||||
fn.Tast.slots;
|
||||
let slots = List.rev !slots and zeros = List.rev !zeros in
|
||||
let temps = List.init (nroots - List.length slots) (fun _ -> ptmp f) in
|
||||
droot_push := slots @ temps;
|
||||
droot_zero := zeros @ temps;
|
||||
f.droots <- nroots;
|
||||
f.droot_ns <- temps
|
||||
end;
|
||||
(* The shadow stack's storage, in a dev build and nowhere else: three words
|
||||
for the record and one per slot for the table. Allocated here, beside the
|
||||
channel and the return temporary, so that they sit above [fixed] and the
|
||||
@ -3275,6 +3377,35 @@ let emit_fn (md : Emit.m) ~externs ~fns ?(ext = fun _ -> false)
|
||||
| _ -> None)
|
||||
fn.Tast.params param_at
|
||||
in
|
||||
(* The collector's roots, zeroed and pushed. Into the *body* buffer for the
|
||||
same reason the shadow stack's push below is, and more sharply: this is a
|
||||
run of calls, and a call clobbers every scratch register the prologue is
|
||||
still using to hand the arguments to their slots. The body buffer's first
|
||||
byte is the first point at which they are all safely in the frame.
|
||||
|
||||
Before the shadow stack's push and not after, so that a stopped frame's
|
||||
record is the last thing established and the first thing taken down —
|
||||
the two stacks are independent, but keeping them strictly nested is
|
||||
one less thing to reason about at a break. *)
|
||||
if f.droots > 0 then begin
|
||||
if ann then set_ind f.b "";
|
||||
note f
|
||||
"The collector's roots — runtime/flan_dyn.h. Every dyn slot and every dyn-producing \
|
||||
runtime call gets a frame slot the collector is told the address of, zeroed first \
|
||||
because the push happens here and the code that fills one may be in a branch that \
|
||||
never runs. The single pop is in the epilogue, which every return and every \
|
||||
transfer out of this frame goes through.";
|
||||
xor_rr f.b ~dst:rax ~src:rax;
|
||||
List.iter
|
||||
(fun off -> store_int f.b ~src:rax ~mm:(Frame off) ~size:8)
|
||||
!droot_zero;
|
||||
List.iter
|
||||
(fun off ->
|
||||
lea f.b ~dst:rdi ~mm:(Frame off);
|
||||
xor_rr f.b ~dst:rax ~src:rax;
|
||||
call_sym f.b "flan_dyn_root_push")
|
||||
!droot_push
|
||||
end;
|
||||
(* The shadow stack's push, and the pop is in the epilogue. plan.org has had
|
||||
*Frames: shadow stack* in the dev column since the beginning; [emit.ml]
|
||||
builds the same four words on the LLVM side and this is the x86 one, down
|
||||
@ -3499,6 +3630,26 @@ let emit_fn (md : Emit.m) ~externs ~fns ?(ext = fun _ -> false)
|
||||
load_int f.b ~dst:rax ~mm:(Frame fr) ~size:8 ~signed:false;
|
||||
store_int f.b ~src:rax
|
||||
~mm:(lmem f (sym_loc f "flan_frame_head") ~scratch:r11) ~size:8);
|
||||
(* The collector's pop, and it is one call because this backend has one
|
||||
epilogue: a [return], the fall through the body's tail and the transfer
|
||||
exit all arrive at this label, so the roots come off on the unwinding
|
||||
path as well as on the normal one. [emit.ml] needs the same pop at five
|
||||
separate [ret]s and routes them through its own [ret] for exactly that
|
||||
reason — roots left on the stack after a handled condition point into a
|
||||
frame that has gone, and the next mark reads whatever the next call put
|
||||
there.
|
||||
|
||||
Here, between the shadow stack's restore and the return value's load,
|
||||
because a call clobbers both rax and xmm0 and the return value is about
|
||||
to go into one of them. Bare — one immediate into rdi and the call —
|
||||
because [frame_bytes] was read to build the prologue's [sub] before this
|
||||
line was reached: a frame temporary or a stack argument allocated here
|
||||
would be a frame this function never subtracted for. *)
|
||||
if f.droots > 0 then begin
|
||||
imm_into f ~reg:rdi (Int64.of_int f.droots);
|
||||
xor_rr f.b ~dst:rax ~src:rax;
|
||||
call_sym f.b "flan_dyn_root_pop"
|
||||
end;
|
||||
if sret then load_int f.b ~dst:rax ~mm:(Frame f.sret_off) ~size:8 ~signed:false
|
||||
else if not (is_void fn.Tast.ret) then
|
||||
load_scalar f ~reg:(if is_float fn.Tast.ret then xmm0 else rax)
|
||||
@ -3574,8 +3725,8 @@ let init_sym = "\"flan..init-globals\""
|
||||
the loader put them in, the program's own end of the transfer channel is a
|
||||
null cell on this frame, and the exit goes through [flan_exit] because
|
||||
stdout is a FILE* and something has to flush it. *)
|
||||
let emit_main ?(cfi = false) ?(ann = false) ?(startup = false) (md : Emit.m)
|
||||
(fn : Tast.fn) =
|
||||
let emit_main ?(cfi = false) ?(ann = false) ?(startup = false) ?(gc = false)
|
||||
?(dyn_globals = []) (md : Emit.m) (fn : Tast.fn) =
|
||||
let b = create () in
|
||||
bnote ann b
|
||||
"C's main, which is the whole of the adapter between the loader and a Flan program. \
|
||||
@ -3595,6 +3746,34 @@ let emit_main ?(cfi = false) ?(ann = false) ?(startup = false) (md : Emit.m)
|
||||
without an exception, which is worth more than the two bytes. *)
|
||||
xor_rr b ~dst:rax ~src:rax;
|
||||
call_sym b "flan_rt_init";
|
||||
(* Immediately after the host runtime and before anything that could box: a
|
||||
dyn global's initialiser runs in the startup function below, and the very
|
||||
first thing it does is allocate. Asked of the whole program rather than
|
||||
assumed, so a program with no dyn in it emits no call and its [main] is
|
||||
byte for byte the [main] it was. *)
|
||||
if gc then begin
|
||||
xor_rr b ~dst:rax ~src:rax;
|
||||
call_sym b "flan_gc_init"
|
||||
end;
|
||||
(* The dyn globals, rooted here and never popped, which is the whole of what
|
||||
a global's extent means. They go on the root stack *before* the startup
|
||||
function runs, because that function is what fills them and its first
|
||||
allocation may be the one that collects — and before any function of the
|
||||
program pushes a root of its own, because every pop takes the top of the
|
||||
stack and these are the ones that must never be at the top.
|
||||
|
||||
Zero is what a global holds until its initialiser has run: [.bss] gives
|
||||
that for free, and a zero word is not a pointer the collector will
|
||||
follow — see the entry-block roots in [emit_fn] for why that is a fact
|
||||
about runtime/flan_dyn.c and not a convention. *)
|
||||
List.iter
|
||||
(fun g ->
|
||||
(* Pc-relative and not through the GOT: [emit_main] is only ever a
|
||||
whole program's, and a whole program defines every global it names. *)
|
||||
lea b ~dst:rdi ~mm:(Sym (gsym g, 0));
|
||||
xor_rr b ~dst:rax ~src:rax;
|
||||
call_sym b "flan_dyn_root_push")
|
||||
dyn_globals;
|
||||
(* The computed globals, after the runtime is up and before a line of the
|
||||
program's own code — [emit.ml]'s [emit_startup] says why this is a call
|
||||
from here rather than a second constructor. It takes no channel: no caller
|
||||
@ -3662,7 +3841,8 @@ let emit_globals_init ?(cfi = false) ?(ann = false) ~sym (md : Emit.m) ~externs
|
||||
let f =
|
||||
{ b; md; fnname = "<globals>"; retlbl = new_label () "ginit";
|
||||
fret = Types.Unit; slots = [||]; xfer_off = 0; sret_off = 0; retval = 0;
|
||||
dframe = None; dslotv = None; snames = [||];
|
||||
dframe = None; dslotv = None; droots = 0; droot_ns = [];
|
||||
snames = [||];
|
||||
frame = 0; maxframe = 0; outgoing = 0; loops = []; pads = [];
|
||||
xfer_lbl = ""; unwound = false;
|
||||
rodata = Buffer.create 64; externs; fns; ext = (fun _ -> false);
|
||||
@ -4085,7 +4265,14 @@ let program ~checks ?(dev = false) ?(debug = false) ?(annotate = false)
|
||||
end;
|
||||
(match List.find_opt (fun (f : Tast.fn) -> f.Tast.name = "main") p.Tast.fns with
|
||||
| Some fn ->
|
||||
Buffer.add_string text (emit_main ~cfi:debug ~ann:annotate ~startup md fn)
|
||||
Buffer.add_string text
|
||||
(emit_main ~cfi:debug ~ann:annotate ~startup ~gc:(Emit.uses_dyn p)
|
||||
~dyn_globals:
|
||||
(List.filter_map
|
||||
(fun (g : Tast.global) ->
|
||||
if g.Tast.gty = Types.Dyn then Some g.Tast.gname else None)
|
||||
p.Tast.globals)
|
||||
md fn)
|
||||
(* No [main] is not an error, and [emit.ml] treats it the same way: a
|
||||
program can be linked against a C host that brings its own entry point,
|
||||
which is what [reload_host.c] is. Refusing here made a --x86 host for the
|
||||
@ -4305,7 +4492,8 @@ let redefinition ~checks ?(dev = true) ?(known = fun _ -> true)
|
||||
let f =
|
||||
{ b = ib; md; fnname = "<install>"; retlbl = new_label () "install";
|
||||
fret = Types.Unit; slots = [||]; xfer_off = 0; sret_off = 0; retval = 0;
|
||||
dframe = None; dslotv = None; snames = [||];
|
||||
dframe = None; dslotv = None; droots = 0; droot_ns = [];
|
||||
snames = [||];
|
||||
frame = 0; maxframe = 0; outgoing = 0; loops = []; pads = [];
|
||||
xfer_lbl = ""; unwound = false;
|
||||
rodata = Buffer.create 256; externs; fns = fnstbl; ext; slot; dw = None;
|
||||
|
||||
@ -124,6 +124,13 @@ int64_t flan_gc_live_bytes(void);
|
||||
* is the whole of the contract; the compiler lane zeroes a slot at its
|
||||
* declaration anyway.
|
||||
*
|
||||
* A zeroed slot satisfies it, and this used to be the one thing in this header
|
||||
* decided by one side alone. It is checkable now that both sides exist:
|
||||
* flan_dyn.c's mark walks a value only when it is boxed, and boxed means the
|
||||
* quiet-NaN prefix is set, which the zero word does not have. So zero decodes
|
||||
* as the double 0.0 — an ordinary value, and never an address anything
|
||||
* follows. Both backends zero, and they are right to.
|
||||
*
|
||||
* Globals go through the same pair, pushed once at startup and never popped.
|
||||
*
|
||||
* [flan_dyn_root_pop] takes a count rather than an address because that is
|
||||
|
||||
55
spike/x86/p13-dyn-collect.flan
Normal file
55
spike/x86/p13-dyn-collect.flan
Normal file
@ -0,0 +1,55 @@
|
||||
;;;; Enough allocation that the collector actually runs, with live dyn values
|
||||
;;;; held across it.
|
||||
;;;;
|
||||
;;;; Every other dyn program in this repository allocates a handful of objects
|
||||
;;;; and stops. runtime/flan_dyn.c's trigger has a one-megabyte floor, so none
|
||||
;;;; of them ever crosses it and none of them collects even once — which means
|
||||
;;;; that until this file existed, a program whose root discipline was entirely
|
||||
;;;; wrong printed the right answer on both backends. The dyn handoff said that
|
||||
;;;; about the stub that never collected; the stub is gone and the observation
|
||||
;;;; outlived it, because a heap that never fills is a collector that never
|
||||
;;;; runs.
|
||||
;;;;
|
||||
;;;; So this one allocates well past the floor while holding values the
|
||||
;;;; collector must not free: a vector that grows for the whole run, a text
|
||||
;;;; allocated before the loop and read after it, and a running total. The
|
||||
;;;; garbage is the per-iteration vector that nothing keeps, and there is a lot
|
||||
;;;; of it.
|
||||
;;;;
|
||||
;;;; What a lost root looks like here is not a wrong number. It is a use of
|
||||
;;;; freed memory — a crash, or a word that decodes as some other tag and traps
|
||||
;;;; with a sentence about the wrong type. Either way the two backends stop
|
||||
;;;; saying the same thing, which is what the sweep asks.
|
||||
|
||||
;;; Held in locals across every allocation the loop makes, which are the slots
|
||||
;;; the entry block roots. Returned, so the vector is live to the last line.
|
||||
(defn build [n dyn] dyn
|
||||
(let [xs (vec-new dyn)
|
||||
i 0]
|
||||
(while (< i n)
|
||||
;; Fresh and unreferenced: this is the garbage. Four pushes each, so the
|
||||
;; items array is allocated too and the heap moves quickly.
|
||||
(let [junk (vec-new dyn)]
|
||||
(push junk i)
|
||||
(push junk "row")
|
||||
(push junk 2.5)
|
||||
(push junk true))
|
||||
;; Every sixteenth iteration keeps one, so the live vector grows *through*
|
||||
;; the collections rather than only between them.
|
||||
(if (= 0 (% i 16)) (push xs i))
|
||||
(set i (+ i 1)))
|
||||
xs))
|
||||
|
||||
(defn main [] ()
|
||||
;; Allocated before the loop runs and read after it, which is the check that
|
||||
;; main's own root outlived every collection build triggered.
|
||||
(let [keep "kept"
|
||||
xs (build 40000)]
|
||||
(print (len xs))
|
||||
(print "\n")
|
||||
(print (at xs 0))
|
||||
(print "\n")
|
||||
(print (at xs (- (len xs) 1)))
|
||||
(print "\n")
|
||||
(print keep)
|
||||
(print "\n")))
|
||||
@ -78,14 +78,15 @@ out=$(mktemp -d); trap 'rm -rf "$out"' EXIT
|
||||
# truncations are both empty.
|
||||
forever="dev-loop dev-watch dev-chatty"
|
||||
|
||||
# The dyn programs, which this backend refuses by name and is meant to: every
|
||||
# operation on a dyn value is a call into the dynamic runtime and x86.ml emits
|
||||
# none of them. They are listed rather than left to be counted as refusals
|
||||
# because a REFUSED here means "a node this backend has stopped lowering",
|
||||
# which is a regression, and this is the opposite -- a lane that has not
|
||||
# started. Take a name off this list when the backend grows the lowering, and
|
||||
# the survey will say whether it works.
|
||||
llvmonly="dyn-basic dyn-vec dyn-global dyn-boundary dyn-defer"
|
||||
# There used to be a second exclusion list here, holding the five dyn
|
||||
# programs, and its note said to take a name off it when the backend grew the
|
||||
# lowering and the sweep would then say whether it works. The backend grew it,
|
||||
# so the list is gone rather than empty: a dyn is one machine word in both
|
||||
# calling conventions and every operation on one is an ordinary runtime call.
|
||||
# What the lane cost was the collector's root discipline -- a zeroed frame
|
||||
# slot per dyn local and per dyn-producing call, pushed at entry, and one pop
|
||||
# in the epilogue that every exit already went through. The five are in the
|
||||
# sweep now and they are five of the MATCHes.
|
||||
|
||||
TIMEOUT=${TIMEOUT:-20}
|
||||
|
||||
@ -110,7 +111,6 @@ for src in "$corpus"/test/programs/*.flan "$corpus"/spike/x86/*.flan \
|
||||
[ $want = 1 ] || continue
|
||||
fi
|
||||
case " $forever " in *" $name "*) skip+=("$name:runs-forever"); continue;; esac
|
||||
case " $llvmonly " in *" $name "*) skip+=("$name:dyn-is-llvm-only"); continue;; esac
|
||||
|
||||
# LLVM first. A program that does not compile at all, or has no main, is not
|
||||
# this backend's business -- the frontend refused it either way.
|
||||
|
||||
@ -27,10 +27,13 @@ let run exe arg =
|
||||
Sys.remove out;
|
||||
(code, text)
|
||||
|
||||
let compile ?(opt = "-O2") ?(checks = true) ?(dev = false) path =
|
||||
let compile ?(opt = "-O2") ?(checks = true) ?(dev = false) ?(x86 = false) path =
|
||||
let exe =
|
||||
Filename.concat scratch
|
||||
("flan-t-" ^ Filename.remove_extension (Filename.basename path))
|
||||
("flan-t-" ^ Filename.remove_extension (Filename.basename path)
|
||||
(* A name of its own, so an x86 row and an LLVM row over the same
|
||||
program are two files and not one built twice over the other. *)
|
||||
^ if x86 then "-x86" else "")
|
||||
in
|
||||
(* Through [Load], so a program with an (import ...) is buildable here: it
|
||||
brings back the package's C shim and linker arguments as well. *)
|
||||
@ -40,7 +43,7 @@ let compile ?(opt = "-O2") ?(checks = true) ?(dev = false) path =
|
||||
reachable calls into hands over no C and no linker argument, and its
|
||||
functions are not emitted. *)
|
||||
let p, csrcs, lflags = Reach.link ~dev l p in
|
||||
ignore (Build.executable ~opts:{ Build.default with opt; checks; dev }
|
||||
ignore (Build.executable ~opts:{ Build.default with opt; checks; dev; x86 }
|
||||
~csrcs ~lflags p ~out:exe);
|
||||
exe
|
||||
|
||||
@ -101,8 +104,8 @@ let () =
|
||||
surface calc-me does not reach — globals, 2-D arrays, places through a
|
||||
pointer, casts, match with either arm taken, and the value semantics of
|
||||
spec-memory.md. *)
|
||||
let outputs ?opt ?dev name path expected =
|
||||
let exe = compile ?opt ?dev path in
|
||||
let outputs ?opt ?dev ?x86 name path expected =
|
||||
let exe = compile ?opt ?dev ?x86 path in
|
||||
let code, text = run exe None in
|
||||
if text <> expected || code <> 0 then begin
|
||||
incr failures;
|
||||
@ -2990,35 +2993,50 @@ level "1"
|
||||
call whose result feeds a machine instruction and that is exactly the
|
||||
shape the optimiser could launder away.
|
||||
|
||||
They are LLVM-only, and the [@x86] survey skips them by name — see
|
||||
[llvmonly] in spike/x86/survey.sh. Not compiled by the dev backend, so
|
||||
not run as dev builds either. *)
|
||||
They used to be LLVM-only, and this paragraph used to say so. The x86
|
||||
backend compiles them now, and each gets a row of its own here beside
|
||||
its LLVM rows — which is not the same question the [@x86] sweep asks.
|
||||
That one asks whether the two backends agree with *each other*, and
|
||||
two backends can agree on the wrong answer; these rows are the
|
||||
expected text, written out, and a backend that is wrong on its own is
|
||||
wrong against them. The dev daemon takes x86 by default and dyn is the
|
||||
iteration feature, so this is the pairing the whole lane was about. *)
|
||||
let dyn_basic_out = "5\n3.75\n" in
|
||||
outputs "dyn: an unannotated defn at two types"
|
||||
"programs/dyn-basic.flan" dyn_basic_out;
|
||||
outputs ~opt:"-O0" "dyn: an unannotated defn at two types, -O0"
|
||||
"programs/dyn-basic.flan" dyn_basic_out;
|
||||
outputs ~x86:true "dyn: an unannotated defn at two types, --x86"
|
||||
"programs/dyn-basic.flan" dyn_basic_out;
|
||||
let dyn_vec_out = "4\n[1 2.5 three true]\n1 2.5 three true \n" in
|
||||
outputs "dyn: a heterogeneous vector"
|
||||
"programs/dyn-vec.flan" dyn_vec_out;
|
||||
outputs ~opt:"-O0" "dyn: a heterogeneous vector, -O0"
|
||||
"programs/dyn-vec.flan" dyn_vec_out;
|
||||
outputs ~x86:true "dyn: a heterogeneous vector, --x86"
|
||||
"programs/dyn-vec.flan" dyn_vec_out;
|
||||
let dyn_global_out = "0 start\n2 done\n" in
|
||||
outputs "dyn: a global" "programs/dyn-global.flan" dyn_global_out;
|
||||
outputs ~opt:"-O0" "dyn: a global, -O0"
|
||||
"programs/dyn-global.flan" dyn_global_out;
|
||||
(* The one that needed [main] to push a root before the startup function
|
||||
ran, on this backend as on the other: the initialiser is what fills the
|
||||
global and its first allocation may be the one that collects. *)
|
||||
outputs ~x86:true "dyn: a global, --x86"
|
||||
"programs/dyn-global.flan" dyn_global_out;
|
||||
|
||||
(* The boundary, both directions, and then the claim that is wrong. The
|
||||
first four lines are the conversions; the trap is the fifth, and the
|
||||
runtime owns its wording — the compiler could only have said that two
|
||||
dyns did not agree, which is what they are for. *)
|
||||
let dyn_boundary ?opt () =
|
||||
let exe = compile ?opt "programs/dyn-boundary.flan" in
|
||||
let dyn_boundary ?opt ?x86 () =
|
||||
let exe = compile ?opt ?x86 "programs/dyn-boundary.flan" in
|
||||
let code, text = run exe None in
|
||||
let want = "107\n42\n21\n5\n" in
|
||||
let name =
|
||||
"dyn: the boundary both ways, and the trap"
|
||||
^ (match opt with Some o -> ", " ^ o | None -> "")
|
||||
^ (match x86 with Some true -> ", --x86" | _ -> "")
|
||||
in
|
||||
if code <> 134
|
||||
|| not (contains text want)
|
||||
@ -3034,10 +3052,21 @@ level "1"
|
||||
in
|
||||
dyn_boundary ();
|
||||
dyn_boundary ~opt:"-O0" ();
|
||||
(* The trap path, on the backend the dev daemon takes by default. The same
|
||||
exit status and the same sentence: the runtime owns the wording, so a
|
||||
backend can only get this wrong by not reaching the runtime with the
|
||||
right two words in the right two registers — which is exactly what the
|
||||
exit status alone would not have shown. *)
|
||||
dyn_boundary ~x86:true ();
|
||||
|
||||
(* The root count, which is the one part of this feature no run can check:
|
||||
the stub never collects, so a program whose roots are entirely wrong
|
||||
passes every test above. What can be checked is the IR, and this is the
|
||||
(* The root count, which is the part of this feature the runs above cannot
|
||||
check — and the reason has outlived the stub it was first written
|
||||
about. flan_dyn.c's trigger has a one-megabyte floor, and not one
|
||||
program in this list allocates enough to cross it, so none of them
|
||||
collects even once and a program whose roots are entirely wrong passes
|
||||
every row above. spike/x86/p13-dyn-collect.flan is the one that does
|
||||
cross it, on both backends, and it is the sweep's business rather than
|
||||
this file's. What can be checked here is the IR, and this is the
|
||||
assertion that found a real hole — a defer appears twice in the typed IR,
|
||||
spliced into the body for the normal path and again in [fdefers] for the
|
||||
path a transfer leaves through, so a dyn temporary inside one is emitted
|
||||
@ -3071,6 +3100,15 @@ level "1"
|
||||
"1005\n6\n";
|
||||
outputs ~opt:"-O0" "dyn: a defer on the transfer path, -O0"
|
||||
"programs/dyn-defer.flan" "1005\n6\n";
|
||||
(* And through the other backend, where the defer and the roots meet in a
|
||||
sharper place: this backend has *one* epilogue, so the single
|
||||
[flan_dyn_root_pop] sits on the path a transfer leaves through as well
|
||||
as on the path a return does, and there is no second copy to forget.
|
||||
The [%dx] check above cannot be asked of it — that assertion reads LLVM
|
||||
text and there is no asm spelling of it that means the same thing — so
|
||||
what stands behind the roots here is this row and the sweep. *)
|
||||
outputs ~x86:true "dyn: a defer on the transfer path, --x86"
|
||||
"programs/dyn-defer.flan" "1005\n6\n";
|
||||
|
||||
(* ── --no-gc ─────────────────────────────────────────────────────
|
||||
The flag is a pass between checking and emission that answers unit or
|
||||
|
||||
@ -897,21 +897,42 @@ let () =
|
||||
"(declare c-take [d dyn] () \"c_take\")"
|
||||
~needle:"does not cross to C";
|
||||
|
||||
(* The x86 backend refuses dyn by name, and the sentence has to be good: the
|
||||
dev daemon takes that backend by default, so this is the first thing a
|
||||
user of dyn sees. Neither half of the message names [--llvm] — Session and
|
||||
main.ml each add that, differently and for their own reasons — so what is
|
||||
pinned here is the half this file owns. *)
|
||||
(match
|
||||
X86.program ~checks:true
|
||||
(Check.program_all
|
||||
(program "(defn add [x y] dyn (+ x y))\n\
|
||||
(defn main [] () (print (add 1 2)))"))
|
||||
with
|
||||
| _ -> check "the x86 backend refuses dyn" false
|
||||
| exception X86.Unsupported m ->
|
||||
check "the x86 backend refuses dyn by name"
|
||||
(contains m "a dyn value" && contains m "dynamic runtime"));
|
||||
(* The x86 backend used to refuse dyn by name, and what was pinned here was
|
||||
the sentence it refused with. It compiles it now, which is the thing this
|
||||
row is for: that backend is the dev daemon's default and dyn is the
|
||||
iteration feature, so a refusal there was the two of them never meeting.
|
||||
The assertion is the same shape inverted — it lowers, and it emits the
|
||||
root discipline while it does. The roots are asserted rather than only
|
||||
the absence of an exception, because a build that emits the calls and
|
||||
forgets the roots is exactly the failure that passes every output test:
|
||||
the collector simply never hears about a value.
|
||||
|
||||
Which programs *agree* between the backends is the @x86 sweep's question
|
||||
and all five dyn programs are in it; this one only has to know that the
|
||||
lowering exists. *)
|
||||
let dyn_asm =
|
||||
X86.program ~checks:true
|
||||
(Check.program_all
|
||||
(program "(defn add [x y] dyn (+ x y))\n\
|
||||
(defn main [] () (print (add 1 2)))"))
|
||||
in
|
||||
check "the x86 backend lowers dyn"
|
||||
(contains dyn_asm "flan_dyn_add");
|
||||
check "the x86 backend roots its dyn values"
|
||||
(contains dyn_asm "flan_dyn_root_push"
|
||||
&& contains dyn_asm "flan_dyn_root_pop");
|
||||
(* And a program with no dyn in it emits not one byte of any of it, which is
|
||||
what lets the sweep's other MATCHes stand as a regression check on this
|
||||
lane rather than being re-measured by it. *)
|
||||
check "a dyn-free program pays nothing for the collector"
|
||||
(let plain =
|
||||
X86.program ~checks:true
|
||||
(Check.program_all
|
||||
(program "(defn add [x i32 y i32] i32 (+ x y))\n\
|
||||
(defn main [] () (print (add 1 2)))"))
|
||||
in
|
||||
(not (contains plain "flan_dyn_root_push"))
|
||||
&& not (contains plain "flan_gc_init"));
|
||||
|
||||
(* ── Static bounds ─────────────────────────────────────────────── *)
|
||||
(* A literal index into a fixed array is known now, so it is an error now
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user