carlos / platform Public

ACCEPT WITH FIXES

Reviewed a6ba2a09..ef71d55d, the rebase onto 412ca787, and the supplied reports against spec rev 17. Read-only: no builds, tests, or mutants run. The worktree remains clean.

The original failing sequences are addressed. Two cleanup regressions introduced by the fixes still need correction before merge.

| Item | Verdict | Evidence | |---|---|---| | F1 | ADDRESSED | Publication now precedes the ownership/context check in workerbuild.go:89; installation rechecks ownership in activator.go:2504. Preparation-time lease loss no longer executes or installs a replacement. See regression R2-1 below. | | F2 | ADDRESSED | swapsimtest.go:432 holds w.mu across publishing death and removing the process. A lease-release observer cannot see the inconsistent model state. | | F3 | ADDRESSED | mutate.sh:180 checks execution integrity before accepting a kill. Panic and missing execution remain failures despite another assertion kill. | | F4 | ADDRESSED | mutate.sh:60 allocates unique scratch with mktemp; cleanup targets that invocation’s tree and work directory. | | F5 | ADDRESSED | logsink.go:51 maps both unproven-start sentinels to existing fence wording. activator.go:2511 corrects the proof diagnosis and preserves the ownership refusal reason. | | F7 | ADDRESSED | swaphold.go:269 checks the locally acquired lease and attempt; swaphold.go:352 repeats the gate immediately before StartStaged, after verification and tier lookup. | | F8 | ADDRESSED | schedfence.go:43 admits writes against a persistent retirement latch. swap.go:504 excludes writes across the switch. Body parsing happens outside the fence. | | F9 | ADDRESSED | claimgen.go:28 refuses every production claims-backed swap, including both capabilities enabled. claimgen_test.go:370 covers all combinations and absence of stop/raise/With side effects. The unexported claimSpawn exception is assigned only by tests. | | F10 | ADDRESSED | swaphold.go:283 records execution from a returned process or unproven-start sentinel. Ordinary pre-exec errors now abandon; post-exec health failures remain down. | | F11 | ADDRESSED — original sequences | swap.go:418 marks the possible raise before calling the backend. opset.go:315 clears it only after successful repair. The new retry has regression R2-2 below. | | F12 | ADDRESSED | maintenance.go:294 transfers failed-wake identity; activator.go:2531 transfers shed-member identity. generations_file.go:108 includes both retained owners through the existing serialized writer. | | T2 | ADDRESSED | opset_test.go:128 waits for the barrier signal or observable barrier bypass. | | T5 | ADDRESSED | settle_test.go:15 controls exit/cancellation through observation polls; the intentional-stop test waits for the settle’s first poll. | | T6 | ADDRESSED | swapholdtest.go:37 observes request entry into its wait before opening the stop gate. | | T7 | ADDRESSED | swapsidecartest.go:341 uses the sidecar-start join signal and checks that neither instance stop nor lease release passed it. | | T8 | ADDRESSED | swapscheduletest.go:232 exercises a real nested control listener and verifies generation 7 reaches the fence. | | T9 | ADDRESSED | backend_exec.go:1638 removes the generation launch file after definite staged-executable refusal. The nested refusal test asserts removal. | | T11 | ADDRESSED | workergentest.go:204 checks proof calls and successful recovery after healing. workerretainedpin_test.go:107 covers retained shed-process pins with generations enabled. | | T13 | ADDRESSED | activator.go:3738 now documents bounded flag-off Shutdown waiting and the remaining leader-only limitation. |

1. R2-1 — High: the new flag-off installation refusal can forget its spawned worker. Fix before merge.

Evidence: activator.go:2504, activator.go:2535, activator.go:2748.

Failing sequence: with generations off, the old worker exits and its replacement executes. Lease renewal fails before installation. The new ownership check correctly refuses installation, but m == nil, so cleanup ignores proc.Stop’s result, drops the pending build pin, and leaves e.proc pointing at the old, exited worker. If Stop returns without proving exit, the replacement is forgotten. The next lease-loss stop checks the old process and closes replication/deletes the entry.

A blocked shed Stop also fails: terminal stop eventually exceeds its bounded respawnDone wait, then proceeds against that same old process while the replacement remains alive.

This broadens the pre-existing shed-cleanup weakness to the newly added lease-loss refusal. The new test checks only a replacement whose Stop succeeds.

Smallest fix: retain the replacement’s process handle and staged identity in terminal-cleanup ownership even with generations off. Neither cleanup completion nor the pin may be released before termination is proven. Add a controlled failed/blocked shed-stop case to the flag-off ownership test, asserting retained process, pin, and replication state.

1. R2-2 — High: a parent-limit retry can outlive its entry and lower a later overlap’s parent. Fix before merge.

Evidence: opset.go:362, swaphold.go:124, activator.go:3051.

Failing sequence: restoration fails after an overlap. The sweep launches a retry carrying the old entry’s route and tier; pause it before the backend write. A hold or terminal stop proceeds because the retry is absent from the operation set. The entry disappears, the host wakes again, and a new overlap raises its parent and starts a successor. Resume the old retry: RestoreGenParent writes the old single-generation tier to that host’s parent while the new overlap still has two children.

Blocking overlaps on e.ops.raised protects only the original entry. The replacement has a fresh operation set. The backend parent write is keyed by host, without an entry/generation condition.

Smallest fix: make an in-flight restore a joined lifecycle operation. Terminal stop must join it before releasing/deleting the entry or installing a pinned replacement; stopping entries must not launch further retries. Keep the backend call outside a.mu. An identity check immediately before the call alone would leave another check/use race.

Add a gated retry test covering stop/hold, replacement entry, and a subsequent overlap.

The F8 lock order is sound: the switch waits for writes before acquiring a.mu; write callbacks do not acquire a.mu; the fence’s internal mutex is not held while callbacks run. Retirement remains latched after member removal. Process-wide generation numbers prevent a later entry from inheriting an old retirement. The generation-zero claims-listener limitation remains unreachable for production overlaps because F9 closes claims-backed admission; carry that requirement into the eventual launcher implementation.

Flag-off changes to ownership checking, sentinel wording, and retained failed-wake pins are justified. R2-1 prevents accepting the claim that every newly refused replacement is safely stopped.

The rebase preserves main’s changes. Neither new main commit changes internal/activator, internal/instancectl, or internal/schedule. The digest-ratchet additions remain in materialization/adoption, including agent.go:949, alongside the new schedule wiring. Digest-bound staging retains the generations-file pin machinery. Moves still enter through the existing FenceAndStop/Quiesced wiring; claims-backed swaps remain closed. I found no additional rebase-specific failing sequence.

I agree with the M5 ruling as a manually reviewed kill. Removing the awake check permits a hold to call beginStopLocked on an already-stopping entry; two stop goroutines can then close the same e.stopped. The designated witness independently fails on the intended admission property. That supports the kill without treating the panic as a harness failure.

The automated mutation gate nevertheless returned 8 CAUGHT, 1 BROKEN, exit 1. Preserve that result and the explicit controller exception. Neither a narrower mutant nor a defensive beginStopLocked guard is required solely to validate this recorded kill; do not weaken F3’s general integrity rule.

R2-1 worsens the deferred T11 respawn-join limitation by exposing it through the new post-exec ownership refusal. F6 remains the separately deferred descendant-proof limitation; it does not excuse forgetting a live replacement leader. I found no other worsening of the round-one deferred triage.