Strike four fixed defects, and say why the dlclose rule has two exceptions
NEXT.md: the ring, the seqlock, the break loop's exit and the leaked handle are struck with what each was fixed to rather than only that it was. The snapshot generation stays open — it wants a hook a test can drive, which is a design decision and not a fix. The four-buffer paragraph is now two and two. BUILT.md carries the reasoning that outlives the change. "Nothing is ever dlclosed" is restated as "nothing that published anything is ever dlclosed", because that is what the rule was always about — being pointed into — and the two modules that are closed are the ones nothing can point into. Stating it the weaker way is what made a dropped handle look like obedience. The agent section gains why a full ring refuses rather than drops or blocks, and why the break loop leaves with _exit. The renderer section gains why the result counter had to become a real seqlock and why marking it odd needs a release fence rather than a release store — a release store orders what precedes it, so the buffer writes could still be hoisted over it, which is the original bug with more ceremony. One correction: the release-build story named flan_dev_result_get as the symbol that came up undefined. That symbol no longer exists. dune test green; dune build @sanitize clean.
This commit is contained in:
parent
e22a8dba82
commit
66dcf30c8a
38
BUILT.md
38
BUILT.md
@ -382,7 +382,7 @@ slice parameter.
|
||||
**`flan_dev.c` is compiled into every build, not only a dev one.** Nothing in a release build calls into it — the
|
||||
compiler only emits a registry lookup for a name the host was not built with, which cannot arise without cells — but the
|
||||
agent package's C refers to it, and a package's C sources are collected whatever `main` does. Leaving it out of release
|
||||
builds made `flan build sand.flan` fail at the link with an undefined `flan_dev_result_get`, which reads as a compiler
|
||||
builds made `flan build sand.flan` fail at the link with an undefined `flan_dev_result_read`, which reads as a compiler
|
||||
bug rather than as a missing flag. The table is BSS, so the cost is address space and not binary size; `-rdynamic` and
|
||||
the cells are still what `--dev` means. `test_agent.ml` links the agent program both ways for this reason.
|
||||
|
||||
@ -467,8 +467,13 @@ still null. Not race-testable, so it is asserted on the emitted `flan_reload_ins
|
||||
- **`flan_dev_global` refuses a size change.** The running process has already laid that memory out; handing back the
|
||||
old allocation for a differently shaped type means the new body reads fields at the wrong offsets and nothing says so.
|
||||
This is the layout-drift rule's first enforcement point. Retyping a var needs a restart.
|
||||
- **Nothing is ever `dlclose`d.** A cell holds an address inside a module's text; unloading it leaves every call site
|
||||
pointing at unmapped memory. That is a constraint on the agent too.
|
||||
- **Nothing that published anything is ever `dlclose`d.** A cell holds an address inside a module's text; unloading it
|
||||
leaves every call site pointing at unmapped memory. That is a constraint on the agent too. The rule is about being
|
||||
*pointed into*, which is why it has exactly two exceptions and they are not exceptions to the reasoning: a transient
|
||||
thunk, which takes no registry slot and has returned; and a module the agent refuses before queueing it — no installer,
|
||||
or no room in the ring — which published nothing and which nothing can name. What was leaked in the second case was the
|
||||
handle *value* rather than the mapping: `dlopen` refcounts by path, so re-sending the same bad file raised a count
|
||||
nothing could lower, and the one reference that could was dropped on the floor.
|
||||
- **The registry never moves.** A module holds a cell's address for as long as it is loaded, so the table is fixed
|
||||
capacity with a loud failure rather than growable.
|
||||
|
||||
@ -497,6 +502,19 @@ redefined function is on the stack, so it happens on the game thread, at the top
|
||||
The two are connected by a single-producer/single-consumer ring and two atomics; the game thread never blocks on the
|
||||
loader.
|
||||
|
||||
**A full ring is refused, at the sender, before the `dlopen`.** Of the three honest answers this is the only one that
|
||||
reaches the person who asked: dropping loses a reload the sender was told was `ok`, which is the same lie more quietly,
|
||||
and blocking stalls the accept loop — it serves connections inline, so a program that had stopped polling would also
|
||||
stop answering `status` and `abort`, leaving the dev loop with no way to reach a program that had stopped listening to
|
||||
it. The check is separate from the store because there is exactly one producer: room, once seen, cannot be taken away,
|
||||
since the consumer only ever makes more of it. Sixty-four is a lot of reloads between two frames and the refusal says
|
||||
what to do about it — call `agent/poll`.
|
||||
|
||||
**The way out of the break loop is `_exit`, not `exit`.** `exit` runs the atexit chain and the ELF destructors, which
|
||||
want the loader lock the listener thread may be holding inside `dlopen`; a program asked to abort would hang instead of
|
||||
dying, which is the failure the break loop exists to replace. The streams are flushed by hand at each call site, and 134
|
||||
stays because that is what a trap exits with.
|
||||
|
||||
`wait` exists for tests. A test that races the frame rate fails on a loaded machine, so `test/programs/agent.flan` waits
|
||||
for the reload instead of sleeping past it. It takes **two** reloads, which is the daemon's actual loop: the first
|
||||
introduces a global the process was never built with, the second only reads it, and the second can only answer 1007 if
|
||||
@ -763,8 +781,18 @@ decision's bill, and it is why the printer set is small rather than universal.
|
||||
|
||||
It does not go through stdout. Stdout belongs to the program, it is in the hot path for anything that prints, and a
|
||||
dev-only feature must not put a branch in it — so `flan_rt.c` is untouched and the value is read back over the agent's
|
||||
socket. The read is safe without a handshake because `flan_dev_result` bumps a generation counter last; the daemon waits
|
||||
for it to move rather than assuming the program has reached a frame boundary.
|
||||
socket. The read is safe without a handshake because the counter is a **seqlock**, and it had to be made into a real
|
||||
one: the first version bumped the generation last and handed back the buffer itself, which says a new value has arrived
|
||||
and says nothing about whether the bytes the agent then wrote to a socket were that value — the game thread is free to
|
||||
be a hundred bytes into the next one by then. A seqlock cannot validate a read that finishes after it returns, so the
|
||||
bare pointer was the bug rather than the ordering. `flan_dev_result_read` copies into the caller's buffer and checks
|
||||
the counter either side of the copy; the counter is odd for exactly as long as a value is being written, and a reader
|
||||
that loses the race reports the last *complete* generation and no bytes, so a daemon polling for a new value keeps
|
||||
polling rather than being shown half of one. The count handed out is the number of complete values, so the daemon's
|
||||
"has it moved" still means what it meant. Marking the counter odd needs a release *fence* and not a release store — a
|
||||
release store orders what precedes it, so the writes to the buffer would be free to become visible ahead of it, which
|
||||
is the original bug with more ceremony. The daemon waits for the count to move rather than assuming the program has
|
||||
reached a frame boundary.
|
||||
|
||||
**This renderer is most of `println`**, which is worth knowing before anyone schedules it. plan.org describes a
|
||||
compiler-provided, type-directed intrinsic that selects or emits a structural printer per concrete instantiation, prints
|
||||
|
||||
43
NEXT.md
43
NEXT.md
@ -82,11 +82,13 @@ it *would* have written.
|
||||
which is a compiler feature of the same shape the bounds checks already have, or they belong to the checker. Not
|
||||
decided. `test_sanitize` pins the current answer with a control that must *not* report, so a future clang changing
|
||||
this is a test failure rather than a discovery.
|
||||
2. **Four named buffers got no evidence at all.** The 4K result cap, the dev registry overflow guard,
|
||||
`SNAP_MAX`/`SNAP_NAMES` and `condition_name[128]` are on the daemon and agent paths, which need a socket and are not
|
||||
in the corpus. Their guards were read and are correct; that is reading, not testing. `escaped[ESCAPE_MAX]` is the one
|
||||
that *is* covered, because `println.flan` drives a 1100-character string through it on purpose — 1019 bytes out
|
||||
against a worst case of 1021 into 1024. `scratch[SCRATCH]` never sees more than 20 characters of 64.
|
||||
2. **Two of the four named buffers now have evidence; two still do not.** The 4K result cap and `condition_name[128]`
|
||||
are driven over the agent's socket from `test_agent.ml` — a 5000-byte value comes back as 4096 ending in the
|
||||
ellipsis, a 198-character condition class comes back from `status` as 127. The **dev registry overflow guard** and
|
||||
`SNAP_MAX`/`SNAP_NAMES` are still read rather than tested: four thousand interned names and sixty-five nested
|
||||
`restart-case`s are a lot of program for a clamp each. `escaped[ESCAPE_MAX]` is covered because `println.flan`
|
||||
drives a 1100-character string through it on purpose — 1019 bytes out against a worst case of 1021 into 1024.
|
||||
`scratch[SCRATCH]` never sees more than 20 characters of 64.
|
||||
3. **Valgrind over the headless corpus, not done.** ASan does not see uninitialised reads, which is where `zeroed` and
|
||||
struct padding live. MSan is out: it needs every dependency instrumented and raylib settles that.
|
||||
|
||||
@ -383,7 +385,7 @@ plan.org's single line on it (831) names a `for` the language does not have and
|
||||
no evidence of what it meant. The agent copies the list on entering `break_loop` — names into its own buffer, frames
|
||||
as the addresses a transfer carries — one snapshot per nested break, and every verb answers from it. Caps are
|
||||
`SNAP_MAX` 64 restarts and `SNAP_NAMES` 4096 bytes; past either, the listing says how many it did not show. Neither
|
||||
cap has a test, same blind spot as the 4K result cap below.
|
||||
cap has a test; the 4K result cap that shared that blind spot now does.
|
||||
|
||||
- **A snapshot generation has no test, and the window is a race.** A choice is validated against the snapshot on top
|
||||
when the request arrives and resolved against the snapshot on top when the game thread next looks. Between those,
|
||||
@ -395,13 +397,25 @@ plan.org's single line on it (831) names a `for` the language does not have and
|
||||
window means landing a request inside a two-millisecond poll from outside the process. It wants a hook the test can
|
||||
drive, not a sleep.
|
||||
|
||||
- **The job ring has no fullness check**, and the comment describing its overflow is wrong. `publish` never consults
|
||||
`tail`; past `QUEUE` entries it overwrites the slot the consumer is reading, and `job` is 24 non-atomic bytes.
|
||||
Reachable from a program that goes a long time between `agent/poll` calls.
|
||||
- **`flan_dev_result_get` is not the seqlock its comment claims** — it reads the generation first, then a non-atomic
|
||||
length, then returns a bare pointer the caller sends later.
|
||||
- Smaller: `exit(134)` from the break loop with the listener inside `dlopen`; a `dlopen` handle leaked when a module
|
||||
has no installer.
|
||||
- ~~The job ring has no fullness check.~~ **Fixed by refusing, at the sender.** Dropping loses a reload the sender was
|
||||
told was ok; blocking stalls the accept loop, which serves connections inline, so a program that had stopped polling
|
||||
would also stop answering `status` and `abort`. The refusal happens before the `dlopen`, so a module there is no room
|
||||
for is never relocated and no handle is taken for it. `programs/agent-queue.flan` blocks on stdin so the window is
|
||||
held open by the test rather than by a timer: 64 queued, the 65th refused with a reason, 64 installed when it finally
|
||||
polls.
|
||||
|
||||
- ~~`flan_dev_result_get` is not the seqlock its comment claims.~~ **Fixed by making it one**, rather than by writing
|
||||
the honest comment — what it guaranteed was nothing, and the daemon has no other way to read a result. The counter is
|
||||
odd while a value is being written, `flan_dev_result_read` copies into the caller's buffer and checks the counter
|
||||
either side of the copy, and a reader that loses the race reports the last complete generation and no bytes. The
|
||||
count handed out is the number of complete values, so `lib/dev.ml`'s "has it moved" still means what it meant. The
|
||||
race itself has no test, for the same reason the snapshot generation above has none.
|
||||
|
||||
- ~~Smaller: `exit(134)` from the break loop with the listener inside `dlopen`; a `dlopen` handle leaked when a module
|
||||
has no installer.~~ **Both fixed.** `exit` runs the atexit chain and the ELF destructors, which want the loader lock
|
||||
the listener may be holding — a program asked to abort would hang instead of dying; `_exit`, with the streams flushed
|
||||
by hand. The leak was the handle *value* and not the mapping: a module with no installer published nothing, so
|
||||
nothing can point into it, and it is closed. The deadlock is read rather than tested; the exit status is tested.
|
||||
- **`(A {:x 1})` on a union variant says "unknown struct A"** rather than the union refusal `check_struct` plainly
|
||||
intends — `env` has no table of variant names. A diagnostics bug, not a backend death.
|
||||
|
||||
@ -414,7 +428,8 @@ Sixty mutations, nineteen left the whole suite green. The severe cluster is clos
|
||||
function a valid program calls, so the build fails to link.
|
||||
- `flan_dev_global`'s size-change guard — the layout-drift check, with no test that retypes a global across a reload.
|
||||
- A local shadowing an imported name is qualified anyway.
|
||||
- The 4K result cap and the registry overflow guard have **no coverage at all**, rather than a missing assertion.
|
||||
- The registry overflow guard has **no coverage at all**, rather than a missing assertion. The 4K result cap that used
|
||||
to sit beside it here is driven over the agent's socket now.
|
||||
- The reader accepts an unknown string escape; `+5` stops being a number.
|
||||
- And a warning: a reader mutation makes the suite **hang** rather than fail. A green run is not the only outcome to
|
||||
plan for in CI.
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user