flan/docs/handoffs/HANDOFF-x86-abi-marker.md

Handoff — the ABI marker symbol, so a crossed pair is refused at dlopen

Branch dev-loop, from 682cb74. This closes the serious finding of HANDOFF-x86-aggregates.md: a redefinition module built by one backend, dlopened into a host built by the other, links and loads and then dies with SIGSEGV at the first call into a redefined function that takes or returns a struct. Nothing refused it, and flan build game.flan --x86 --dev followed by flan reload game.flan changed.flan builds exactly that pair.

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.

What was built

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

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.

The mechanism, and why it is a datum and not a call

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.

The agent's two sentences have no unit test of their own, so they were checked the one way that matters: that they are in a binary a user would actually run. vendor/agent/flan_agent.c reaches a program through the vendor package's C sources rather than through an embedded-as-a-string module like Runtime_src, so an edit to it lands without regenerating anything — but that had to be confirmed rather than assumed, because a repo that embeds one C file that way can embed another.

flan build test/programs/agent.flan --dev       -o ahost ; strings ahost | grep -c "built by different backends"  → 2
flan build test/programs/agent.flan --x86 --dev -o ahost ; strings ahost | grep -c "built by different backends"  → 2

Two, in both configurations: one sentence per direction.

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.

And "a matched pair is unaffected" is checked through the agent as well as through reload_host.c, which is worth saying because the two are different code paths and only one of them is what a user meets. The daemon tests in dune test — dev-globals, dev-repl, dev-watch, dev-pause, dev-loop — start a real flan dev session, build a real host, and send real redefinition modules to the agent in it over the socket. Every one of those dlopens now has to resolve flan.abi.llvm, and every one of those tests passes.

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 / 0 NOX86	103 / 0 / 0 / 0
skip breakdown	28 does-not-compile / 8 no-main / 2 runs-forever	28 / 8 / 2
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

The survey is the measurement that could have moved and did not, which is the point of running it: both backends now emit a symbol into every --dev build, and the survey's default is a release build on both sides, so an unguarded marker would have shown up as 103 identical-but-different objects rather than as a wrong answer. It agrees byte-for-byte on what the programs print.

Run it detached — setsid timeout 2400 spike/x86/survey.sh > log 2>&1 </dev/null — or a signal to this harness's process group comes back as SURVEY_EXIT=143, which is not a result. The log is block-buffered through the redirect and stays empty until the end; that is not a hang.

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.
• A seam worth knowing about before anyone renames a marker. The two strings live in OCaml — X86.abi_marker and Emit.abi_marker — and the two abi_mismatch functions match the same literals in C, with nothing linking the four. Rename one and the refusal still fires, because the symbol is still missing; it just stops being a sentence and reverts to the loader's bare "undefined symbol", which is the failure this lane was about. The crossed tests would catch it — they assert on the marker's name — so the seam is guarded, but it is a seam.