Isolated exec spec: revision 9 after codex round 8
Round 8 findings committed unedited. Accepted: the wake re-reads the registry row before Acquire and runs on the committed row, and the layout pass reloads routing before releasing the fence, so a stale flat route can never restore a second database or start childProc for a migrated host.
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YZ1ZvWj7naf73GjTX8MBv5
2 files changed,
+70
−9
docs/superpowers/specs/2026-09-11-isolated-exec-design.md+42 −9docs/superpowers/specs/CODEX-FINDINGS-ISOLATED-EXEC-R8.md+28 −0
CI passed — run details
diff --git a/docs/superpowers/specs/2026-09-11-isolated-exec-design.md b/docs/superpowers/specs/2026-09-11-isolated-exec-design.md| index bde92df89..def5d1cc0 100644 |
| --- a/docs/superpowers/specs/2026-09-11-isolated-exec-design.md |
| +++ b/docs/superpowers/specs/2026-09-11-isolated-exec-design.md |
| @@ -1,7 +1,7 @@ |
| # Isolated exec — every exec-backed instance in its own namespace |
| -**Date:** 2026-09-11 · **Status:** revision 8, after codex rounds 1 to 7 |
| -(19 + 14 + 7 + 4 + 3 + 1 + 1 findings, all accepted; §13) · **Requested by:** discussion |
| +**Date:** 2026-09-11 · **Status:** revision 9, after codex rounds 1 to 8 |
| +(19 + 14 + 7 + 4 + 3 + 1 + 1 + 1 findings, all accepted; §13) · **Requested by:** discussion |
| #126 (Tito, with box evidence), approved in direction by Paul on |
| 2026-09-11 |
| @@ -951,10 +951,11 @@ which a symlink could otherwise still perform during this release. |
| ## 6. The activator on units |
| -`internal/activator/activator.go` changes in exactly two places: the |
| -sidecar restart in `sweepOnce` (§6.7, codex R2-6) and the lease release |
| -in `stop` (§6.3, codex R2-5). `doWake` (`activator.go:772`), `Bounce` |
| -(`:946-956`) and the `Proc`/`Rep` seams (`:194-207`) keep their contracts. |
| +`internal/activator/activator.go` changes in exactly three places: the |
| +sidecar restart in `sweepOnce` (§6.7, codex R2-6), the lease release |
| +in `stop` (§6.3, codex R2-5), and the route the wake runs on (§6.8, |
| +codex R8-1). `doWake` (`activator.go:772`), `Bounce` (`:946-956`) and |
| +the `Proc`/`Rep` seams (`:194-207`) keep their contracts. |
| `Exited()` stays a non-blocking read of a flag (R1-4); everything that |
| talks to systemd runs in the proc's own goroutine or in the |
| sidecar-start goroutine. The rest of the change is inside `ExecBackend`, |
| @@ -1276,7 +1277,33 @@ arrives during the start finds `sidecarStarting` and waits for the |
| install step to see it. One test drives a stalled sidecar start while |
| another host wakes and stops. |
| -### 6.8 What does not change |
| +### 6.8 The wake runs on the committed row, not on a copy (codex R8-1) |
| + |
| +The edge hands the activator the route it proxied for, and the |
| +activator copies it into the entry (`activator.go:481`); `doWake` then |
| +restores, seeds, spawns and replicates on that copy (`:806, :870`). The |
| +copy can be older than the registry: for the interval between a layout |
| +pass's row CAS and the edge's reload, the edge still holds the flat |
| +paths, and a request in that interval would carry a flat route to a |
| +host the registry already calls `nested`. On that copy the exec backend |
| +would classify the host `flat`, restore a second database at the |
| +vacated flat path, and run `childProc`, and `RetireExcept` |
| +(`activator.go:1260`) would keep the entry because its host name did |
| +not change. |
| + |
| +**The third `activator.go` change**: at the top of `doWake`, before |
| +`Acquire`, the activator **re-reads the row** (`reg.Get(host)`, one |
| +indexed read) and uses that row for the whole wake, restore through |
| +replication, storing it back into the entry. If the row's `DBPath` or |
| +`Socket` differ from the copy the edge supplied, the wake logs |
| +`route refreshed: <old> → <new>` and proceeds on the fresh one; if the |
| +host has no row, or the row is `fenced` or `conflict`, the wake refuses |
| +as §8.1 says. The exec backend's classification (§8.1) therefore always |
| +sees the committed row. One test delivers a saved flat route for a |
| +migrated host and asserts no flat artifact is created and no |
| +`childProc` starts. |
| + |
| +### 6.9 What does not change |
| `Acquire`, `Restore` (including the `.corrupt` quarantine and |
| `PurgeLocalDBArtifacts`, all keyed off `dbPath`), `lease.Replicate` (the |
| @@ -1447,8 +1474,11 @@ needed) and, per host in scope, in this order: |
| a new sibling of `SetDBPath` (`registry.go:1057-1075`). Then journal |
| `phase: "done"`. |
| 9. Remove the journal; log `layout: <host>: flat → nested` (or the |
| - reverse); release the host to the activator. The edge picks the new |
| - `Socket` up on its next registry poll (`edge.go:449-451`, ~2s). |
| + reverse); **reload routing synchronously** (the agent owns the edge |
| + and calls its `Reload()`, `edge.go:449-451`, and the activator's |
| + `RetireExcept`/route refresh, rather than waiting for the 2s poll); |
| + only then release the host to the activator. A request that copied |
| + the old route before that reload is caught by §6.8 (codex R8-1). |
| **Recovery is the journal, and it is exact, and it is checked** (R2-7, |
| R3-1, R4 disposition). On agent start and at the top of every layout |
| @@ -2000,3 +2030,6 @@ rollback runs the old binary). |
| R7-1 the startup sweep is `POST /sweep`, performed by the control service on the unit names systemd reports, so a hashed identifier without a row is still stopped (§5.3, §6.7); |
| R5-2 the downgrade guard checks every row's path shape regardless of flags; unflagging a nested row is refused (§8.2); |
| §10 aligned with the `conflict` rule. |
| +- **Round 8** (codex, `CODEX-FINDINGS-ISOLATED-EXEC-R8.md`, 1 new |
| + finding, every prior item resolved, verdict request changes). Accepted: |
| + R8-1 the wake re-reads the row before `Acquire` and runs on it; the layout pass reloads routing before releasing the fence (§6.8, §8.2). |
diff --git a/docs/superpowers/specs/CODEX-FINDINGS-ISOLATED-EXEC-R8.md b/docs/superpowers/specs/CODEX-FINDINGS-ISOLATED-EXEC-R8.md| new file mode 100644 |
| index 000000000..dfc39e165 |
| --- /dev/null |
| +++ b/docs/superpowers/specs/CODEX-FINDINGS-ISOLATED-EXEC-R8.md |
| @@ -0,0 +1,28 @@ |
| +| Prior finding | Disposition at `81f25b6c` | |
| +|---|---| |
| +| R7-1 | **Resolved.** `/sweep` enumerates and stops the three templates by unit name, including orphaned hashed identifiers and pending jobs (§§5.3, 6.7). Retain §5.4’s process authentication. | |
| +| R6-1 | **Resolved.** Identifier domains remain separate; collisions refuse execution as `conflict`. §10 now agrees. | |
| +| R5-2 | **Resolved at spec level.** The downgrade guard checks every row’s paths regardless of flags, and unflagging nested rows is refused (§8.2). | |
| +| R5-3 | **Resolved.** Directory, socket, unit and slice names consistently use `InstanceID(host)`. | |
| +| R2-4 | **Resolved.** Blocking seed execution and `RemainAfterExit=yes` retain identity and results through capture (§§4.2, 5.3, 6.5). [systemd service semantics](https://raw.githubusercontent.com/systemd/systemd/v257/man/systemd.service.xml). | |
| +| R2-5 | **Resolved.** Completion requires terminal state and cgroup emptiness; uncertain stops retain replication and the lease. | |
| +| R2-7 | **Resolved.** Recovery derives both endpoints from the journal’s direction, completes that transaction, then converges to current intent. | |
| +| R2-9 | **Resolved for the reported downgrade defects.** Flat minting, explicit reversal and the expanded downgrade guard cover them. | |
| +| R2-14 | **Resolved at spec level.** The IPv6 exception is explicit, bounded, rechecked and reported. | |
| +| R1-4 | **Resolved.** Completion is independent of log EOF; blocking observations remain outside the activator mutex. | |
| +| R1-5 | **Resolved.** Preparation, execution budget, cancellation, result retention and termination-before-cleanup are specified. | |
| +| R1-8 | **Resolved under the recorded decision.** Shared tier limits remain; per-service OOM families are an explicit difference. | |
| +| R1-12 | **Resolved for the reported partial-migration failure.** Consumer fences and bidirectional recovery cover interrupted transactions. R8-1 concerns admission after completion. | |
| +| R1-13 | **Resolved for the reported rollback defects.** Reverse recovery and the expanded downgrade guard address them. | |
| +| R1-15 | **Resolved at spec level.** No unsafe PID-namespace fallback; the behavioural gate and bounded IPv6 exception remain. | |
| +| R1-18 | **Resolved under the recorded ruling.** Remote reporting and layout operations are specified; the `foreign` repair residual remains explicitly accepted. | |
| + |
| +**R8-1 — P1 — §§6, 8.1–8.2: A completed migration can admit a stale flat-layout wake.** |
| + |
| +[Step 9 releases the migration fence before the edge’s next registry poll](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/isolated-exec-spec/docs/superpowers/specs/2026-09-11-isolated-exec-design.md:1449). During that interval, the edge still supplies the old route. The activator [copies that route into its new entry](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/isolated-exec-spec/internal/activator/activator.go:481); the unchanged `doWake` then [restores using that copy](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/isolated-exec-spec/internal/activator/activator.go:806) and [replicates its `DBPath`](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/isolated-exec-spec/internal/activator/activator.go:870). The existing admission check [tests only whether the host is fenced](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/isolated-exec-spec/internal/activator/maintenance.go:148). |
| + |
| +Consequently, immediately after flat→nested migration, a request can restore a second database at the vacated flat path and select §8.1’s unisolated `childProc` path. The registry already reports `nested`. Reloading subsequently does not retire this process: [`RetireExcept` retains entries by hostname](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/isolated-exec-spec/internal/activator/activator.go:1260), which did not change. Writes can advance the flat copy while the next correctly routed wake trusts the older nested copy. |
| + |
| +**Correction:** assign a route-freshness check to wake admission, coordinated with the layout fence. Before restore, seed, spawn or replication, reject or refresh a supplied route whose paths differ from the committed row; use one consistent route throughout the wake. Refresh routing before releasing the fence, while also rejecting requests that retained an older route before that refresh. Pin the case by delivering a saved flat route after migration completes and asserting that it neither recreates flat artifacts nor starts `childProc`. |
| + |
| +**Verdict: request changes.** |
| \ No newline at end of file |