From 1f30d9a06778d967f0cf6665bf2587ab7d9422db Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Mon, 14 Sep 2026 07:19:27 +0700 Subject: [PATCH] The marker, written up: what it refuses and what it deliberately does not --- HANDOFF-x86-abi-marker.md | 143 +++++++++++++++++++++++++++++++++++--- 1 file changed, 132 insertions(+), 11 deletions(-) diff --git a/HANDOFF-x86-abi-marker.md b/HANDOFF-x86-abi-marker.md index c026b59..9538664 100644 --- a/HANDOFF-x86-abi-marker.md +++ b/HANDOFF-x86-abi-marker.md @@ -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.