The proof the first commit's numbers could not give
Green runs of a load-only flake, taken on an idle machine, are worth nothing, and a count alone cannot tell you which kind you have. So the load for the 55-run test_reload proof was a build of flan_dev.c from the commit before this fix, churning beside it: a positive control as well as a load. It refused 4151 of the 50478 runs it managed in that window — 8% — while test_reload went 55 for 55. Paired on the direct binary too, eight copies at a time: 13 of 80 before, 0 of 160 after. Also here: the bound BUILT.md used to quote went from two milliseconds to about sixty-six, and the doc says so rather than dropping the number; the note that flan_dev_reg_at shared the spin and could answer "never heard of this address" under load; and the verdict on the two neighbouring dev flakes, which are three causes and not one.
This commit is contained in:
parent
8f05ece441
commit
a29424a7b6
58
FIX.org
58
FIX.org
@ -5575,7 +5575,8 @@ one, so the dead count sits at zero for the whole run and no rearrangement is
|
||||
possible. The table under the reader was stationary. The reader refused it
|
||||
anyway.
|
||||
|
||||
runtime/flan_dev.c:1140, [flan_reg_snap], read the slot's counter sixty-four
|
||||
[flan_reg_snap] — runtime/flan_dev.c:1140 before this commit, :1187 after, since
|
||||
the fix put a block of reasoning above it — read the slot's counter sixty-four
|
||||
times with nothing between the tries. Two different things leave that counter
|
||||
odd and they are minutes apart in scale. A writer that is running holds it odd
|
||||
for seven stores; a bare re-read wins almost at once, and that is the case the
|
||||
@ -5602,11 +5603,56 @@ being rearranged. A stationary table earning a refusal was the reader lying
|
||||
about the writer.
|
||||
|
||||
** Proof
|
||||
The same 24-at-a-time harness, twice: 480 runs of [regfull], zero refusals,
|
||||
zero wrong, zero zero-row. [regchurn] unchanged at 120 runs. [regrace], whose
|
||||
Three levels, because the cheap one alone proves the least.
|
||||
|
||||
The direct binary, paired against a build of the same file from the commit
|
||||
before. Eight copies at a time on sixteen cores: before, 13 of 80 runs
|
||||
refused; after, 0 of 160. [regchurn] unchanged at 120 runs. [regrace], whose
|
||||
answered/refused split is the machine's business and is printed rather than
|
||||
pinned, still never produced a zero-row or a wrong count in 120 contended runs.
|
||||
|
||||
** Not the dev-pause flake
|
||||
test_dev's "rerun: the program is already running" at high load is a different
|
||||
mechanism — nothing in that path reads the registry. Left where it was.
|
||||
Then test_reload.exe itself, 55 runs, sequential. Sequential is not caution
|
||||
about load — [tmp] in test_reload.ml is a fixed /tmp/flan-reload-* path, so two
|
||||
copies would fight over the same host and .so files and invent failures that
|
||||
look like a regression.
|
||||
|
||||
Fifty-five green runs of a one-in-five flake would be worth having; fifty-five
|
||||
green runs of a flake that only appears under load, taken on an idle machine,
|
||||
would be worth nothing, and there is no way to tell the two apart from the
|
||||
count. So the load for that run was the *pre-fix* binary churning beside it,
|
||||
which makes it a positive control as well as a load: if it stops refusing, the
|
||||
window had no race in it and the run proved nothing. It did not stop. In the
|
||||
same window it managed 50478 runs and 4151 of them refused — 8% — while
|
||||
test_reload went 55 for 55.
|
||||
|
||||
Machine: 16 cores, load average 15-18 through the run.
|
||||
|
||||
** It also hardens the address root, which was the same spin
|
||||
[flan_dev_reg_at] — the inspector's "what block is this address in" — calls
|
||||
the same [flan_reg_snap] and, unlike the listing, steps *past* a slot it could
|
||||
not read rather than counting it. That is deliberate and documented: a slot it
|
||||
could not read either did not hold the block, in which case skipping costs
|
||||
nothing, or did, in which case the whole call answers "never heard of this
|
||||
address". With the naked spin, the second branch was reachable under load, so
|
||||
test_dev's address-root cases could be told an address it had just been given
|
||||
was not in the table. Nothing was seen failing that way; it is named because
|
||||
the fix closes it and the next person should not have to rediscover that this
|
||||
verb shared the defect.
|
||||
|
||||
** Not the dev-pause flake, and not the initialiser one either
|
||||
Two other dev flakes were on the table while this was chased. Neither is this.
|
||||
|
||||
test_dev's "rerun: the program is already running" at high load: nothing in
|
||||
that path reads the registry. A reviewer has since put a name to it —
|
||||
[flan_merged_rerun] (lib/dev.ml:4514) answers ok with [program_state] still
|
||||
PROGRAM_PARKED, so an [await parked] straight after a re-run is satisfied by
|
||||
the stale park. Its own lane.
|
||||
|
||||
test_dev's edited-initialiser case, which failed once in a full run and passed
|
||||
the two after: also not this. The race fixed here lives entirely in the
|
||||
allocation registry's *reading* side, and the only symptoms it can produce are
|
||||
a listing that refuses and an address root that answers "never heard of it".
|
||||
It cannot make a global hold a wrong value or an install go missing. Those run
|
||||
through the by-name table ([flan_dev_cell]) and the install path, which the
|
||||
program touches from one thread and which share no state with the allocation
|
||||
table. Three flakes, three causes; one of them is fixed here.
|
||||
|
||||
@ -5341,7 +5341,10 @@ looking is what keeps the core busy. So the reader burned its whole budget insid
|
||||
perfectly readable slot unreadable, and the listing above it refused a table that never moved at all. It showed up
|
||||
only under load, which is exactly when a writer gets descheduled: no refusals at all on an idle machine, and one run in
|
||||
five when the cores were oversubscribed. The retry is now eight bare looks and then the same quarter-millisecond step,
|
||||
so a refusal means the table really would not hold still. See FIX.org, 2026-09-21.
|
||||
forty tries in all, so a refusal means the table really would not hold still. That moves the bound on a refusal from
|
||||
two milliseconds to about sixty-six -- eight milliseconds of patience per contended slot, once per walk because there
|
||||
is one writer, across eight walks -- which is still far under what a person waiting for a keypress to be answered
|
||||
notices, and is only ever paid by a listing that is about to refuse anyway. See FIX.org, 2026-09-21.
|
||||
|
||||
**"At exit" is not a hook, and the honest reason is that a game is killed.** A program stopped by a signal runs no
|
||||
`atexit` handler, no destructor, nothing — so no code written inside the program could report anything about the run
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user