docs(process): framing revision 4 — record what implementing found
Not a new design round. Every bet resolved, and one acceptance turned out to be satisfiable vacuously. Acceptance 2's in-drain clause said "the live descendant's named late output absent" without saying how the descendant stays live. It does not, by default: `poll_one` TERMs the whole group on leader exit. The first fixture's marker was therefore absent on both paths, and the pin would have stayed green with the collapse fixed. Bets 1 and 2 hold — every site took a directed outcome without restructuring, and every consequence is reachable, so the lane does not shrink. Bet 3 resolves the shutdown coupling as real and measured. Bet 4 is falsified exactly as its own clause anticipated: `ProcessEvent` is keyed by `ProcessId` while the ledger is keyed by pgid and is deliberately independent of managed records, every production consumer polls per known id, and `take_all_events` has no production consumer at all. Q#RL3 is answered accordingly and reporting is parked as its own lane. Also records the four sites and the two reusable lessons in `docs/agent-handoff.md` — that a seam for a background loop has to be directed, and that an absence assertion is only as good as its fixture's ability to produce the thing. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Lv428Fth9LRtffwJSsqH7T
This commit is contained in:
parent
2f8a39463d
commit
2a1cf9be2e
|
|
@ -333,14 +333,32 @@ compatible.
|
||||||
githubsucks/test-ambient-config-isolation
|
githubsucks/test-ambient-config-isolation
|
||||||
```
|
```
|
||||||
|
|
||||||
## Reap-ledger silent failures — FRAMING OPEN, revision 3
|
## Reap-ledger silent failures — IMPLEMENTED, PR OPEN
|
||||||
|
|
||||||
- **Branch `reap-ledger-silent-failures`**, worktree
|
- **Branch `reap-ledger-silent-failures`**, worktree
|
||||||
`../pmacs-reap-ledger`, based on `githubsucks/main` @ `22df6ab`.
|
`../pmacs-reap-ledger`, based on `githubsucks/main` @ `22df6ab`.
|
||||||
**Framing only; no code, no PR yet.**
|
`docs/reap-ledger-silent-failures-framing.md`, **revision 4**;
|
||||||
`docs/reap-ledger-silent-failures-framing.md`, revision 3; two review
|
approved at revision 3 after two review rounds (round 1: three
|
||||||
rounds closed (round 1: three blocking, two major; round 2: two
|
blocking, two major; round 2: two blocking, two major; all accepted).
|
||||||
blocking, two major; all accepted).
|
Revision 4 records implementation findings, not a new design round.
|
||||||
|
- **All four bets resolved.** Bet 1 (every site takes a directed
|
||||||
|
outcome) and Bet 2 (every consequence is reachable) hold. **Bet 3
|
||||||
|
resolves the shutdown coupling as real and measured** — under 500ms
|
||||||
|
with a failed force-kill plus an errored probe, versus the full 2s
|
||||||
|
bound with only the force-kill failing. **Bet 4 is falsified: no
|
||||||
|
reporting channel exists**, so reporting becomes its own lane.
|
||||||
|
- **The in-drain pin's first fixture was vacuous, and the bite caught
|
||||||
|
it.** `poll_one` TERMs the group on leader exit, so an untrapped
|
||||||
|
descendant died before writing its late marker — absent on *both*
|
||||||
|
paths. With the seam reverted the pin failed only the consumed-plan
|
||||||
|
check, never the content assertion. Fixed with `trap '' TERM` behind
|
||||||
|
the readiness gate.
|
||||||
|
- **Gates: 10/10 green** on the pushed tree, all five bootstrap-storage
|
||||||
|
variables controlled — fmt, diff-check, clippy, `--lib` (1888),
|
||||||
|
`--lib --features crdt` (2073), compile-mode (67), copy-mode in both
|
||||||
|
feature configurations (18/19), M4 with the basedpyright skip (149),
|
||||||
|
required GPU (221). The five new process pins ran **15/15** as a
|
||||||
|
repetition set, since supervisor tests are load-sensitive.
|
||||||
- **Unparked from PR #200's §5.** #200 retired the premise that
|
- **Unparked from PR #200's §5.** #200 retired the premise that
|
||||||
justified the ledger's leniency and deliberately changed no
|
justified the ledger's leniency and deliberately changed no
|
||||||
disposition; this lane owns what it refused.
|
disposition; this lane owns what it refused.
|
||||||
|
|
|
||||||
|
|
@ -257,6 +257,61 @@ commands, read `docs/active-work.md` immediately after this file.
|
||||||
disagree — and it still establishes no identity, because it is read
|
disagree — and it still establishes no identity, because it is read
|
||||||
inside the same read-then-act window and no portable mechanism closes
|
inside the same read-then-act window and no portable mechanism closes
|
||||||
that for a *group* (`pidfd` covers a process; macOS has neither).
|
that for a *group* (`pidfd` covers a process; macOS has neither).
|
||||||
|
- **Reap-ledger silent failures — DIAGNOSTIC, in flight**
|
||||||
|
(`docs/reap-ledger-silent-failures-framing.md`). The lane #200's
|
||||||
|
framing §5 parked and its evidence unparked. **Four `kill(2)` results
|
||||||
|
are discarded in the group reap ledger**, and each discard has its own
|
||||||
|
consequence — three in the persistent ledger, one in the in-drain
|
||||||
|
twin:
|
||||||
|
- `tick_reap_ledger`'s probe cannot tell `ESRCH` (the group is gone —
|
||||||
|
correct) from any other errno (we could not ask — not correct), and
|
||||||
|
`retain` deletes the entry either way, cancelling escalation.
|
||||||
|
- The deadline escalation sets `killed = true` whether or not the
|
||||||
|
`SIGKILL` landed, so a failed one is **never retried by anything**.
|
||||||
|
- `shutdown()`'s force-kill does the same, on the path written
|
||||||
|
specifically to stop a leak at editor exit.
|
||||||
|
- `final_drain_runtime`'s twin collapses every errno into "dead",
|
||||||
|
which quiesces the drain and **cancels the readers** — truncated
|
||||||
|
output rather than a leaked process, and terminal for that drain
|
||||||
|
where a later tick could revisit the ledger.
|
||||||
|
- **None of the four has been observed to fire.** #200's evidence is an
|
||||||
|
explicit `SIGTERM` failing in `signal()`, not any ledger call. What
|
||||||
|
it retires is the *reason* ("EPERM cannot happen for our own
|
||||||
|
children"), not the behaviour.
|
||||||
|
- **`shutdown()`'s loop exit depends on the silent drop, and this is
|
||||||
|
now measured.** It runs while `any_running() || !reap_ledger.is_empty()`,
|
||||||
|
so an early exit needs the ledger empty **and** no live managed
|
||||||
|
record — the leader-exited-survivor case the ledger exists to serve.
|
||||||
|
With a failed force-kill followed by an errored probe it exits in
|
||||||
|
under 500ms instead of holding its 2s bound, having concluded
|
||||||
|
cleanup finished because the probe failed. Making the probe strict
|
||||||
|
without touching the loop converts that silent early exit into a
|
||||||
|
guaranteed 2s stall at every editor exit that hits it: **the two
|
||||||
|
cannot be changed independently.**
|
||||||
|
- **There is no channel for a background tick to report on.**
|
||||||
|
`ProcessEvent` is keyed by `ProcessId`, while the ledger is keyed by
|
||||||
|
pgid and is deliberately independent of managed records, so in the
|
||||||
|
case that matters there is no id to attribute to. Every production
|
||||||
|
consumer polls `take_events(id)` per known id; `take_all_events`
|
||||||
|
would sidestep the keying but **has no production consumer at all**
|
||||||
|
(two test call sites only). `pmacs.error` is dead. Reporting is
|
||||||
|
therefore its own lane, as the framing's Bet 4 anticipated.
|
||||||
|
- **A test seam for a background loop has to be directed.**
|
||||||
|
`shutdown()` signals every managed process before it reaches its
|
||||||
|
ledger force-kill, so one undirected "next kill fails" slot is eaten
|
||||||
|
by the wrong call and the test passes while proving nothing. The
|
||||||
|
persistent sites take a FIFO each (the coupling pin needs two
|
||||||
|
outcomes pending at once); the in-drain site needs one outcome that
|
||||||
|
**repeats for a whole drain**, because a one-shot is consumed by the
|
||||||
|
next 1ms probe and can never survive the 50ms window `quiesced`
|
||||||
|
requires.
|
||||||
|
- **An absence assertion needs a fixture that could have produced the
|
||||||
|
thing.** The in-drain pin's first fixture had no `trap '' TERM`, so
|
||||||
|
`poll_one`'s leader-exit group TERM killed the descendant before it
|
||||||
|
wrote its late marker: the marker was absent on *both* paths and the
|
||||||
|
pin would have stayed green with the collapse fixed. The bite caught
|
||||||
|
it — the reverted seam failed only the consumed-plan check, not the
|
||||||
|
content assertion. That is what the consumed-plan check is for.
|
||||||
- **Lean 4 arc (Arc 8) — stages 1, 2, 3a, 3b, 4a, 4b ALL LANDED**
|
- **Lean 4 arc (Arc 8) — stages 1, 2, 3a, 3b, 4a, 4b ALL LANDED**
|
||||||
(`docs/lean4-mode-framing.md`; #160, #161, #167, #170, #179, #181). pmacs edits Lean 4: `arborium-lean` highlighting, a
|
(`docs/lean4-mode-framing.md`; #160, #161, #167, #170, #179, #181). pmacs edits Lean 4: `arborium-lean` highlighting, a
|
||||||
`lean4` major mode, `⟨⟩ ⦃⦄ ⟮⟯` pairs, and a `lake serve` language
|
`lean4` major mode, `⟨⟩ ⦃⦄ ⟮⟯` pairs, and a `lake serve` language
|
||||||
|
|
|
||||||
|
|
@ -1,8 +1,9 @@
|
||||||
# Framing — group cleanup fails silently at four sites
|
# Framing — group cleanup fails silently at four sites
|
||||||
|
|
||||||
**Revision 3.** Status: awaiting review round 3. Proposed lane:
|
**Revision 4.** Status: **APPROVED at revision 3; implemented.** Lane
|
||||||
`reap-ledger-silent-failures`, worktree `../pmacs-reap-ledger`, based on
|
`reap-ledger-silent-failures`, worktree `../pmacs-reap-ledger`, based on
|
||||||
`githubsucks/main` @ `22df6ab` (a reading; re-measure at branch time).
|
`githubsucks/main` @ `22df6ab`. Revision 4 records what implementation
|
||||||
|
found; it is not a new design round.
|
||||||
|
|
||||||
**Parked by PR #200's framing §5 and unparked by its evidence.** #200
|
**Parked by PR #200's framing §5 and unparked by its evidence.** #200
|
||||||
retired the premise that justified the ledger's leniency; it deliberately
|
retired the premise that justified the ledger's leniency; it deliberately
|
||||||
|
|
@ -10,6 +11,53 @@ changed no disposition, and said so. This lane owns what it refused.
|
||||||
|
|
||||||
## Revision history
|
## Revision history
|
||||||
|
|
||||||
|
**Revision 3 → 4**, found **while implementing**, not a new design
|
||||||
|
round. Every bet resolved; one acceptance turned out to be satisfiable
|
||||||
|
vacuously.
|
||||||
|
|
||||||
|
- **Acceptance 2's in-drain clause could be met by a vacuous fixture,
|
||||||
|
and was.** "The live descendant's named late output absent" says
|
||||||
|
nothing about how the descendant stays live — and `poll_one` sends
|
||||||
|
`SIGTERM` to the whole group on leader exit, so an untrapped
|
||||||
|
descendant dies before it can write. The marker was then absent on
|
||||||
|
*both* paths and the pin would have stayed green with the collapse
|
||||||
|
fixed. The bite is what caught it: with the seam reverted, the pin
|
||||||
|
failed only the consumed-plan check, never the content assertion. The
|
||||||
|
fixture now uses `trap '' TERM` behind `survivor_script`'s readiness
|
||||||
|
gate. **The lesson generalises past this pin: an absence assertion is
|
||||||
|
only as good as the fixture's ability to produce the thing.**
|
||||||
|
- **Bet 1 holds.** All four sites took a directed outcome with no
|
||||||
|
restructuring. `final_drain_runtime` — the one §3 named as at risk,
|
||||||
|
being a free function — needed only a shared handle on the context it
|
||||||
|
already receives.
|
||||||
|
- **Bet 2 holds, in the direction that keeps the lane.** All four
|
||||||
|
consequences are reachable; none was already foreclosed by an earlier
|
||||||
|
guard. The lane does not shrink.
|
||||||
|
- **Bet 3 resolves: the coupling is real and measured.** With a failed
|
||||||
|
force-kill and an errored probe, `shutdown()` returns in **under
|
||||||
|
500ms** instead of holding its 2s bound, with the survivor alive. With
|
||||||
|
only the failed force-kill it burns the full bound. §1.3's warning
|
||||||
|
stands: making the probe strict without touching the loop converts a
|
||||||
|
silent early exit into a guaranteed 2s stall.
|
||||||
|
- **Bet 4 is falsified, exactly as its own clause anticipated: no
|
||||||
|
channel exists.** `ProcessEvent` is keyed by `ProcessId` while the
|
||||||
|
ledger is keyed by pgid and is deliberately independent of managed
|
||||||
|
records, so in the leader-exited-survivor case there is no id to
|
||||||
|
attribute to. Every production consumer polls `take_events(id)` per
|
||||||
|
known id (`lua_bindings/mod.rs:8933`, `:10731`, `mcp.rs:361`).
|
||||||
|
`take_all_events` would sidestep the keying but **has no production
|
||||||
|
consumer at all** — its only two call sites are tests, despite a doc
|
||||||
|
comment naming a `*processes*` buffer. `pmacs.error` was already
|
||||||
|
known dead. **Reporting becomes its own lane** (§5), and this PR ships
|
||||||
|
instrumentation plus tests without it, which is what §7 said it would
|
||||||
|
do in this case.
|
||||||
|
- **The in-drain `SIGKILL` is still unpinned**, as §1.2a promised. Its
|
||||||
|
`group_killed` flag stays local and the persistent ledger retries in
|
||||||
|
the same outer tick, so pinning the local non-retry still needs a
|
||||||
|
call-count assertion or a direct free-function test. Unchanged, and
|
||||||
|
restated here so a later reader does not mistake the shipped seam for
|
||||||
|
covering it.
|
||||||
|
|
||||||
**Revision 2 → 3**, after review round 2 (two blocking, two major).
|
**Revision 2 → 3**, after review round 2 (two blocking, two major).
|
||||||
All four accepted; all four verified in the code first.
|
All four accepted; all four verified in the code first.
|
||||||
|
|
||||||
|
|
@ -271,10 +319,17 @@ noted so a red run on it is not mistaken for this lane's doing.*
|
||||||
*Unknown. `killed = true` on a failed `SIGKILL` is clearly wrong as
|
*Unknown. `killed = true` on a failed `SIGKILL` is clearly wrong as
|
||||||
bookkeeping; what should replace it is a policy question, not an
|
bookkeeping; what should replace it is a policy question, not an
|
||||||
obvious fix.*
|
obvious fix.*
|
||||||
- **Q#RL3** — How does a background tick report anything? *The ledger
|
- **Q#RL3** — How does a background tick report anything? **ANSWERED at
|
||||||
emits no events and has no status channel. `pmacs.error` is defined
|
revision 4: it cannot, today.** `ProcessEvent` is keyed by
|
||||||
only by a test stub and is dead at 15 call sites, so it is not the
|
`ProcessId`; the ledger is keyed by pgid and is deliberately
|
||||||
answer. This is the lane's real design question.*
|
independent of managed records, so in the leader-exited-survivor case
|
||||||
|
— the one the mechanism exists for — there is no id to attribute to.
|
||||||
|
All three production consumers poll `take_events(id)` per known id
|
||||||
|
(`lua_bindings/mod.rs:8933`, `:10731`, `mcp.rs:361`).
|
||||||
|
`take_all_events` would sidestep the keying but has **no production
|
||||||
|
consumer**; its only call sites are two tests, notwithstanding a doc
|
||||||
|
comment naming a `*processes*` buffer. `pmacs.error` was already dead
|
||||||
|
at 15 sites. Reporting is therefore parked as its own lane (§5).
|
||||||
- **Q#RL4** — Does the `shutdown()` loop need its own termination
|
- **Q#RL4** — Does the `shutdown()` loop need its own termination
|
||||||
condition if (a) becomes strict? *Almost certainly (§1.3), and that
|
condition if (a) becomes strict? *Almost certainly (§1.3), and that
|
||||||
coupling is why the two cannot be changed independently.*
|
coupling is why the two cannot be changed independently.*
|
||||||
|
|
|
||||||
Loading…
Reference in New Issue