11 KiB
Row 52, CHAT-01 engine-exit stop, round 1 review (Darkwing)
Issue #1538, request comment 27085, notes comment 27086, queue revs
310-312. Base cc83ee4f (CHAT-01, local, not pushed). Candidate manifest
sha256
deac74341448e8e4560b2cc6418b55fbdcf3e68aa6963211ac7040af49d33d73,
6 files. Filbert reviewed in parallel (27087, rev 313); I wrote this
before reading theirs.
Verdict: approve, on these four CHAT-01 files at cc83ee4f:
a41fc4e2edb11371c275e3167774c162254e1457fd737121630dedd665431889 docs/plans/chat-01/README.md
ccceaf2653b279f5890748b40d16fae7493f199a33cecee035f82b92e80243af docs/plans/chat-01/check.mjs
941675de949c52c7fe7c4b7bcce3aff48bb26ccc1120e090574c5d25f9d9e22e docs/plans/chat-01/contracts.schema.json
c75c2b9f731bb70d0e033e8aa56f2c28accfa09384ec964fd3ecbd45974b2a7d docs/plans/chat-01/fixtures.json
All four points from my brief hold in the model and in the controller, and a test fails when each one is taken away. Two of Dewey's five "equivalent" survivors I'd call untested guards rather than equivalents, and I found three more guards no test reaches. None of that blocks the row. Notes below.
Method
- I checked the four CHAT-01 hashes in the canonical tree against Dewey's
list (all match) and read the
cc83ee4fdiff in full. - Detached worktree at
cc83ee4f, the six candidate files copied from a snapshot of the canonical tree, thensha256sum -c: 6 OK. A second worktree for the mutants; its files still check OK after all runs (r1/mut/manifest-after.txt). - I read the candidate diff in full (
cohort.mjs,controller.mjs,shim.mjs, E1-E6, the README), plus the parts of the controller it touches:#transport,#uncertain, the force-stop branch and itsescalatingslot,#serveOrphan, and the claim chain. - 13 conversation mutants (
r1/mut/mutate.py,run.sh): a base run, Dewey's five survivors rewritten from the packet's descriptions, and seven of mine. Whole conversation suite each, own TMPDIR each, one at a time after the gate. No mutant left a shim, and nomosaic-chat-*unit was listed at the end. - Two model mutants of my own on scratch copies of
check.mjs.
Node v26.8.1, TMPDIR=~/darkwing-scratch/r52a/tmp, gate.sh with
DOCKER_HOST=unix:///nonexistent.sock, 08:04:09Z to 08:07:47Z, then
control-board, queue (node) and the CHAT-01 check. Mutants 08:08:23Z to
08:21:31Z. test-release with Docker after that.
Suites
| Suite | Result |
|---|---|
node docs/plans/chat-01/check.mjs |
PASS: 100 shape, 76 reference, 22 lifecycle |
| conversation | 182/0 |
| webui | 22/0 |
| control-board | 124/0 |
| queue (node) | 148/0 |
| test-auth | 15/0 |
| test-conductor | 17/0 |
| test-config | 24/0 |
| test-discord | 66/0 |
| test-extension-package | 18/0 |
| test-foundation | 44/0 |
| test-queue | 27/0 |
| test-release | 4/0 without Docker, 14/0 with it (test-release-docker.txt) |
| test-task | 26/2 |
The two test-task failures are "user recall run succeeds" and "recalled
user name", the live worker check that needs Docker and a model call, as in
row 51. Dewey's 98/0 ran them. The gate's last line counts two
mosaic-chat-* units at 08:07:47Z. Both counts right after the
conversation and webui suites were zero, so they weren't from those runs; I
think they were another seat's test run, but I can't show that. None was
listed at 08:21:31Z. Filbert saw two scopes from my run directory at about
08:15Z: that's the noinv mutant's suite, which ran 08:15:40Z to 08:16:38Z
and left no shim.
The four points
- Never supersede an unfinished force stop. Model:
engine-exitrefusesstop-ownedwhen the current stop's mode isforce-stoporengine-exit, in any state, and theengine-exit-refused-during-force-stopsequence walks the four force-stop states. Controller:#engineExit(controller.mjs:1550) returns before#startStopwhileescalatingis held or the current stop is ending. E3's second half (a force stop held atforce-stop-recorded) and E5 (a force stop that endeduncertainbefore it closed the execution) pin it; Dewey'snoowncheckandnostopcheckdie there. My model mutantsecond(refuse only under a force stop, so a second engine exit goes through) dies inengine-exit-empty-cohort-stopped, which sends a second engine exit after the first is proven. - The binding follows the stop. The model uses
endingatstartStop,advance-stopandconfirm-stopped, andengine-exit-binding-follows-stopchecks each. The controller uses the sameendingin#startStopand#advanceStop, and#endStopUncertainand#stopProvenset the binding themselves. That double path is whybindadvancesurvives alone. Mybindboth(bindadvanceplus#endStopUncertainnot setting the binding) dies on E2 and E4, so theuncertainhalf is pinned. E3 pinsstoppingat the fence. - The proof names the engine. The shim reads the engine's start ticks
right after spawn and records
{ code, signal, at, pid, startTicks, boot }in its exit handler (shim.mjs:77).engineExitCohort(cohort.mjs:219) refuses a reaped process whose PID, start ticks or boot differ, then proves with one member: the engine, with the reap time asterminatedAt. E1 compares the member list exactly. The model'sstopped()and the controller's#stoppedboth refuse anengine-exitproof with no member.nopidcmpandnostartcmpeach die on E6, so both halves of the identity check are pinned, not just the pair. - A deadline that frees the slot. The observation runs under
within(..., this.T.exitProof)andfinallyfreesescalating(controller.mjs:1567). E4 SIGSTOPs the shim, sees the stop enduncertainwith the deadline's reason andescalatingnull, then proves a force stop after SIGCONT. Note 1 is about what E4 can and can't tell apart.
The claim: an engine exit writes no stopping claim, so a restart finds an
uncertain orphan and #serveOrphan resumes no stop (resumeStop needs
claim state stopping). #transport's uncertain claim write and
#stopProven's stopped write both go through claimChain, so the
stopped write can't land first.
Mutants
| Mutant | Change | Conversation | Result |
|---|---|---|---|
| base | none | 182/0 | |
| noslotcheck | EOF ignores a held slot | 182/0 | survives: equivalent, agreed |
| bindadvance | #advanceStop moves the binding only for a force stop |
182/0 | survives: equivalent, agreed |
| emptyguard | #stopped accepts an engine-exit proof with no member |
182/0 | survives: equivalent alone, agreed |
| nopopulated | a populated engine cgroup proves |
182/0 | survives: see note 2 |
| nomembers | a listed member proves | 182/0 | survives: see note 2 |
| bindboth | bindadvance plus #endStopUncertain not setting the binding |
180/2 | killed: E2, E4 |
| noinv | the engine-exit observation skips the invocation ID check | 182/0 | survives: note 3 |
| noscope | it skips the hello's scope check | 182/0 | survives: note 3 |
| nopidcmp | the identity check skips the PID | 181/1 | killed: E6 |
| nostartcmp | it skips the start ticks | 181/1 | killed: E6 |
| noboot | it skips the boot (Dewey's follow-up) | 182/0 | survives: note 3 |
| noadvance | the engine-exit stop never moves fenced to stopping |
182/0 | survives: note 4 |
Model mutants (r1/model/): second (an engine exit refused only under a
force stop) fails engine-exit-empty-cohort-stopped; working
(working input moved to delivery-unknown too) fails
engine-exit-stale-confirmation-dispatched-receipt. Both killed.
On the three equivalents I agree with: escalating is set only for the
current force stop (controller.mjs:726, #forceStop) or the engine-exit
stop itself, and the resumed force stop in #serveOrphan has no engine
pipe, so #onEnd can't run beside it. The binding is stopping from the
fence on, and interrupt (controller.mjs:742) and revocation
(controller.mjs:1758) need it active. emptyguard is
reachable only through a second fault.
Notes (not blocking)
- E4 tells the deadline apart from
shimRequest's own 3000 ms timeout only by the reason text. A SIGSTOPped shim also failshelloafter 3 s withoutwithin, so the slot would still come free;nodeadlinedies on E4's/deadline/match, not on a held slot. That's fine: the match shows the deadline fired first.withinis what caps the loop. One pass can spend three 3 s requests, and the settle check runs only between passes.systemctlShowis aspawnSyncwith a 5 s timeout that the deadline can't preempt.forceStopCohortdoes the same, so this isn't new. nopopulatedandnomembers: I accept the race argument as far as it goes. The shim'smemberswalks theenginecgroup thatpopulatedreports on, so the two reads disagree only if a process starts or exits between them. I'd call them untested guards rather than equivalents, though:noliveshows a test needs both gone. A fakemembersanswer (the K15 shapes, Dewey's second follow-up) would pin each one.- Three checks in
engineExitCohortthat no test reaches: the invocation ID againstsystemctl show, the hello'sscopeagainst the unit's control group, and the boot (Dewey already lists the boot). All three fail closed when they fire. The first two guard against a scope of the same name from another invocation.forceStopCohorthas the same checks; I didn't look at whether its tests reach them. I'd fold these into Dewey's K15 follow-up. noadvancesurvives. Without the advance, an engine-exit stop goesfencedtostoppedorfencedtouncertain. The model'sconfirm-stoppedandadvance-stopallow both, so it isn't a model violation; a client just never sees the stop instopping. The force stop makes the same advance, and keeping the two paths alike is reason enough to keep it. No test needed.- At EOF the binding goes
uncertainfirst (#transport), thenstoppingwhen#startStopruns. Clients see anuncertainevent, thenstopping. The model has no EOF step beforeengine-exit, so there's nothing to compare it to. I'd mention the order in the README if it ever confuses a client. - Dewey's follow-ups (the pgroup fallback's untested natural exit, the K15 shapes on this path) stand. I'd file them with notes 2 and 3 as one issue.
Files
r1/candidate-manifest.sha256: copy of Dewey's.r1/gate.sh,r1/out/: suite runs, the CHAT-01 check andsummary.txt.r1/mut/: mutant definitions, runner, per-mutant output and shims-left lists,summary.txt, and the manifest check after the runs.r1/model/: the two model mutants' outputs.