The marker, written up: what it refuses and what it deliberately does not
This commit is contained in:
parent
fa83056708
commit
1f30d9a067
@ -6,19 +6,140 @@ dies with SIGSEGV at the first call into a redefined function that takes or retu
|
||||
it, and `flan build game.flan --x86 --dev` followed by `flan reload game.flan changed.flan` builds exactly that
|
||||
pair.
|
||||
|
||||
## The plan
|
||||
**It is refused now, by the loader, before any of the new code runs, with a sentence that says why.** Both
|
||||
directions are in `dune test`.
|
||||
|
||||
A marker symbol, as that handoff recommended.
|
||||
## What was built
|
||||
|
||||
- `X86.program` defines `flan.abi.x86`; `X86.redefinition` emits a data relocation against it.
|
||||
- `Emit.program` defines `flan.abi.llvm`; `Emit.redefinition` emits one against that.
|
||||
- Both sides gated on `dev`, so a release build's output is byte-for-byte what it was.
|
||||
- The two `dlopen` sites — `test/reload_host.c` and `vendor/agent/flan_agent.c` — recognise a `flan.abi.`
|
||||
failure and say, in a sentence, that the module and the host were built by different backends.
|
||||
- `test/test_reload.ml` gains the crossed pair, both directions, asserting the refusal.
|
||||
| file | what |
|
||||
|---|---|
|
||||
| `lib/x86.ml` | `abi_marker = "flan.abi.x86"`. `program` defines it in `.data`, in a dev build only; `redefinition` emits a `.quad` against it |
|
||||
| `lib/emit.ml` | `abi_marker = "flan.abi.llvm"`, the same two halves — a definition inside `program`'s existing `if dev` block, and an `external` plus a hidden pointer to it in `redefinition`'s |
|
||||
| `vendor/agent/flan_agent.c` | `abi_mismatch`, which turns a `flan.abi.` `dlopen` failure into a sentence; the reload handler uses it |
|
||||
| `test/reload_host.c` | the same function, duplicated rather than shared, and the same use at its `dlopen` |
|
||||
| `test/test_reload.ml` | `agg_cross`, run both ways, asserting a nonzero exit *and* the sentence *and* which marker was missing |
|
||||
|
||||
`flan reload --x86` is judged out of scope; see below.
|
||||
`lib/build.ml` was not touched. Its option-record guard is the other half of this answer and is unchanged; the
|
||||
comment there already says what it cannot catch, which is what the marker is for.
|
||||
|
||||
## Status
|
||||
## The mechanism, and why it is a datum and not a call
|
||||
|
||||
In progress. This file is written early and updated as the work lands.
|
||||
A dev build defines a marker symbol naming the backend that built it. A redefinition module emits a
|
||||
pointer-sized datum holding the address of the marker it was itself built for.
|
||||
|
||||
That datum is the whole of it. A pointer in `.data` is a relocation the dynamic loader has to resolve while it
|
||||
maps the object, whatever it does about lazy binding of calls, so a host that does not define the marker fails
|
||||
the `dlopen` outright. A call into an absent function would do as well under `RTLD_NOW`, which is what both
|
||||
loaders in this repo pass, but the datum does not depend on that and costs eight bytes.
|
||||
|
||||
Both sides are gated on `dev`, for two reasons that happen to agree. A release build has no cells and nothing
|
||||
to load into one, so the marker would be dead weight; and `Build.executable` passes `-rdynamic` only for a dev
|
||||
build, so a release build could not export the symbol even if it emitted it. Gating also keeps a release
|
||||
build's output byte-for-byte what it was, which `x86.ml`'s `.Ldwtext` comment says the repo cares about.
|
||||
Measured on `test/programs/cleanup.flan`:
|
||||
|
||||
```
|
||||
x86 --dev : 00000000004280f0 D flan.abi.x86
|
||||
llvm --dev : 000000000041d3f0 B flan.abi.llvm
|
||||
x86 release : (nothing)
|
||||
```
|
||||
|
||||
Macro modules are unaffected and were checked: `Build.macro_module` calls `Emit.program` without `~dev`, so a
|
||||
macro module neither defines a marker nor requires one, and the OCaml-side `dlopen` in `lib/dynload_stubs.c` —
|
||||
which is the *only* other `dlopen` of a Flan-built object anywhere — never sees one. It therefore got no arm,
|
||||
deliberately.
|
||||
|
||||
`lib/dev.ml` got no arm either, and this is worth stating because it looks like an omission. The daemon builds
|
||||
the host itself and sends every module to the agent in the game process; it has no `dlopen` of a redefinition
|
||||
module of its own, and `--x86` has no spelling anywhere in `dev.ml` or `session.ml`, so a `flan dev` session
|
||||
builds host and modules both through LLVM and is matched by construction. The mismatch is only reachable
|
||||
through `flan build --x86 --dev` plus a separately built module, and that module is loaded by the agent, which
|
||||
is where the sentence lives.
|
||||
|
||||
## What the crossed pair does now
|
||||
|
||||
Verbatim, from the two new cases in `test/test_reload.ml`, captured from the host's stderr:
|
||||
|
||||
```
|
||||
flan: the module and this host were built by different backends: the module came from LLVM and needs
|
||||
flan.abi.llvm, which an --x86 host does not define. The two backends pass every struct differently. Rebuild
|
||||
the host without --x86.
|
||||
```
|
||||
|
||||
```
|
||||
flan: the module and this host were built by different backends: the module came from the x86 dev backend and
|
||||
needs flan.abi.x86, which this host does not define. The two backends pass every struct differently. Rebuild
|
||||
the host with --x86.
|
||||
```
|
||||
|
||||
Exit 1 in both cases, from the host refusing to install. Before this it was exit 139 — SIGSEGV, at a call site,
|
||||
after `a1` and `host 54063108` had already been printed.
|
||||
|
||||
The agent's wording is longer than the test host's, because its reader is a person in an editor rather than a
|
||||
test: it names the running program rather than "this host", says the pair would die at the first call into a
|
||||
redefined function taking or returning a struct, and — in the LLVM-module direction — says why the program is
|
||||
the half that has to move.
|
||||
|
||||
Two things about the matching that are deliberate. It matches on the *marker's name*, not on `"undefined
|
||||
symbol"`, which is glibc's phrasing and glibc's to change. And `dlerror` is one-shot with a buffer the next
|
||||
`dl` call may clobber, so the pointer is taken once and used for both the test and the reply; the agent's
|
||||
existing code called it once and still does.
|
||||
|
||||
## Why it is in `dune test` now, when the segfault was not
|
||||
|
||||
The aggregate lane measured the crossed pair and deliberately left it out: it was undefined behaviour, what it
|
||||
printed was a property of whichever LLVM was installed, and a test pinning it would have been pinning the shape
|
||||
of a crash. That is no longer true. The refusal happens in the loader, at a fixed point, before a single
|
||||
instruction of the new body runs, so it is deterministic and is asserted the way the retyped-global and
|
||||
registry-overflow cases already were: on the exit status *and* on the message.
|
||||
|
||||
Both directions, because a marker only one backend emitted would refuse in one direction and say nothing in the
|
||||
other — and the direction with no test is the direction that quietly stops working.
|
||||
|
||||
The matched pairs are unchanged and still print the transcript the aggregate lane derived:
|
||||
|
||||
```
|
||||
a1 / host 54063108 / a1 / after1 54063108 / a2 / after2 104337044 / counter 12
|
||||
```
|
||||
|
||||
from `Emit.redefinition` + `Build.shared` and from `X86.redefinition` + `Build.shared_x86` alike.
|
||||
|
||||
## `flan reload --x86` did not land, and should not have
|
||||
|
||||
The brief left this to judgement. It is item 3 of `HANDOFF-x86-redef.md`, not a flag.
|
||||
|
||||
`flan reload` does not build a module directly; it runs a `Session` over the program and asks
|
||||
`Session.eval` for one, and `Session.change` holds a single `ir : string` field filled by
|
||||
`Emit.redefinition ~consts`. Three things would have to move together:
|
||||
|
||||
- `Session.change` would need a backend-tagged payload rather than an `ir` string, and every one of the six
|
||||
`Emit.redefinition` call sites in `session.ml` would have to choose.
|
||||
- `X86.redefinition` raises `Unsupported` on `~consts`, on `~call`, and on any name the host was not built
|
||||
with. `Session.eval` passes `~consts` as a matter of course and the expression path passes `~call`. So the
|
||||
x86 path would refuse most of what a session legitimately sends, and the refusals would surface as "this
|
||||
works in LLVM and not in x86" rather than as anything a user could act on.
|
||||
- The daemon is the real caller of all of this. Giving `flan reload` a flag the daemon does not have would
|
||||
leave the two commands disagreeing about what a session can do.
|
||||
|
||||
So the deliverable here is the refusal, which is the part that matters: a silent segfault is the bug. The
|
||||
remedy the messages name is the one that actually exists today — rebuild the host to match the module — rather
|
||||
than a flag that does not. When item 3 does land, the marker is what makes the choice checkable rather than
|
||||
merely intended, and these two crossed tests are what will catch a half-done version of it.
|
||||
|
||||
## Baseline
|
||||
|
||||
| | before | after |
|
||||
|---|---|---|
|
||||
| `spike/x86/survey.sh` | 103 MATCH / 0 DIFFER / 0 REFUSED | see below |
|
||||
| skip breakdown | 28 does-not-compile / 8 no-main / 2 runs-forever | see below |
|
||||
| `spike/x86/cells.sh` | 4/4 ok | **4/4 ok** |
|
||||
| `dune test --root .` | exit 0, 232 checks, 0 failures | **exit 0, 232 checks, 0 failures** |
|
||||
|
||||
## What remains
|
||||
|
||||
- Item 3 of `HANDOFF-x86-redef.md`: `flan dev` and `flan reload` choosing host and module backend together.
|
||||
The marker is now the thing that makes that checkable.
|
||||
- A per-shape crossed measurement, still unmeasured and still depended on by nothing. It is *harder* to get
|
||||
now, not easier: the marker refuses the pair before any of the four `step` functions runs, so anyone who
|
||||
wants the answer has to build the crossed module with the marker suppressed on purpose.
|
||||
- Items 1, 2 and 5 of `HANDOFF-x86-redef.md`, untouched.
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user