diff --git a/deno.json b/deno.json index 7b0e6ff0..00ece21a 100644 --- a/deno.json +++ b/deno.json @@ -63,6 +63,7 @@ "gen:publish-workflow": "deno run --allow-all packages/cli/src/deno.ts run scripts/gen-publish-workflow.md", "bump": "deno run -A scripts/bump-version.ts", "weights:measure": "deno run --allow-all scripts/measure-test-weights.ts", + "proof:tmux-pane-workers": "deno run --allow-all --frozen scripts/proofs/tmux-pane-workers/proof.ts", "test": "deno test --allow-all --frozen", "verify": "deno run --allow-all --node-modules-dir=none --cached-only --frozen scripts/preflight.ts scripts/verify.ts", "vendor:verify": "deno run --allow-read --allow-write=/tmp --allow-env --allow-run --cached-only --frozen scripts/verify-cloudflare-dofs.ts", diff --git a/plans/tmux-pane-workers-evidence.json b/plans/tmux-pane-workers-evidence.json new file mode 100644 index 00000000..4363b1ab --- /dev/null +++ b/plans/tmux-pane-workers-evidence.json @@ -0,0 +1,2807 @@ +{ + "environment": { + "commit": "650510b553111c9a46a8205f09fbe0ff2c797a9f", + "os": "darwin 25.5.0", + "arch": "arm64", + "tmux": "tmux 3.6a", + "deno": "deno 2.9.5 (stable, release, aarch64-apple-darwin)", + "date": "2026-09-02T14:34:03.667Z", + "command": "deno task proof:tmux-pane-workers --inner --out /tmp/xmd-proof-ev2 --runs 20" + }, + "checks": [ + { + "name": "layout-geometry", + "ok": true, + "claims": [ + { + "claim": "4@2 80x24: row-major placement", + "ok": true, + "observed": [] + }, + { + "claim": "4@2 80x24: 2 rows", + "ok": true, + "observed": 2 + }, + { + "claim": "4@2 200x60: row-major placement", + "ok": true, + "observed": [] + }, + { + "claim": "4@2 200x60: 2 rows", + "ok": true, + "observed": 2 + }, + { + "claim": "5@2 80x24: row-major placement", + "ok": true, + "observed": [] + }, + { + "claim": "5@2 80x24: 3 rows", + "ok": true, + "observed": 3 + }, + { + "claim": "5@2 200x60: row-major placement", + "ok": true, + "observed": [] + }, + { + "claim": "5@2 200x60: 3 rows", + "ok": true, + "observed": 3 + }, + { + "claim": "8@3 80x24: row-major placement", + "ok": true, + "observed": [] + }, + { + "claim": "8@3 80x24: 3 rows", + "ok": true, + "observed": 3 + }, + { + "claim": "8@3 200x60: row-major placement", + "ok": true, + "observed": [] + }, + { + "claim": "8@3 200x60: 3 rows", + "ok": true, + "observed": 3 + } + ], + "facts": { + "observations": { + "4@2 80x24": { + "cells": [ + { + "ordinal": 0, + "left": 0, + "top": 1, + "width": 40, + "height": 11 + }, + { + "ordinal": 1, + "left": 41, + "top": 1, + "width": 39, + "height": 11 + }, + { + "ordinal": 2, + "left": 0, + "top": 13, + "width": 40, + "height": 11 + }, + { + "ordinal": 3, + "left": 41, + "top": 13, + "width": 39, + "height": 11 + } + ], + "problems": [] + }, + "4@2 80x24 tiled": { + "columns": 2, + "problems": [] + }, + "4@2 200x60": { + "cells": [ + { + "ordinal": 0, + "left": 0, + "top": 1, + "width": 100, + "height": 29 + }, + { + "ordinal": 1, + "left": 101, + "top": 1, + "width": 99, + "height": 29 + }, + { + "ordinal": 2, + "left": 0, + "top": 31, + "width": 100, + "height": 29 + }, + { + "ordinal": 3, + "left": 101, + "top": 31, + "width": 99, + "height": 29 + } + ], + "problems": [] + }, + "4@2 200x60 tiled": { + "columns": 2, + "problems": [] + }, + "5@2 80x24": { + "cells": [ + { + "ordinal": 0, + "left": 0, + "top": 1, + "width": 40, + "height": 7 + }, + { + "ordinal": 1, + "left": 41, + "top": 1, + "width": 39, + "height": 7 + }, + { + "ordinal": 2, + "left": 0, + "top": 9, + "width": 40, + "height": 7 + }, + { + "ordinal": 3, + "left": 41, + "top": 9, + "width": 39, + "height": 7 + }, + { + "ordinal": 4, + "left": 0, + "top": 17, + "width": 80, + "height": 7 + } + ], + "problems": [] + }, + "5@2 80x24 tiled": { + "columns": 2, + "problems": [] + }, + "5@2 200x60": { + "cells": [ + { + "ordinal": 0, + "left": 0, + "top": 1, + "width": 100, + "height": 19 + }, + { + "ordinal": 1, + "left": 101, + "top": 1, + "width": 99, + "height": 19 + }, + { + "ordinal": 2, + "left": 0, + "top": 21, + "width": 100, + "height": 19 + }, + { + "ordinal": 3, + "left": 101, + "top": 21, + "width": 99, + "height": 19 + }, + { + "ordinal": 4, + "left": 0, + "top": 41, + "width": 200, + "height": 19 + } + ], + "problems": [] + }, + "5@2 200x60 tiled": { + "columns": 2, + "problems": [] + }, + "8@3 80x24": { + "cells": [ + { + "ordinal": 0, + "left": 0, + "top": 1, + "width": 26, + "height": 7 + }, + { + "ordinal": 1, + "left": 27, + "top": 1, + "width": 26, + "height": 7 + }, + { + "ordinal": 2, + "left": 54, + "top": 1, + "width": 26, + "height": 7 + }, + { + "ordinal": 3, + "left": 0, + "top": 9, + "width": 26, + "height": 7 + }, + { + "ordinal": 4, + "left": 27, + "top": 9, + "width": 26, + "height": 7 + }, + { + "ordinal": 5, + "left": 54, + "top": 9, + "width": 26, + "height": 7 + }, + { + "ordinal": 6, + "left": 0, + "top": 17, + "width": 40, + "height": 7 + }, + { + "ordinal": 7, + "left": 41, + "top": 17, + "width": 39, + "height": 7 + } + ], + "problems": [] + }, + "8@3 80x24 tiled": { + "columns": 3, + "problems": [] + }, + "8@3 200x60": { + "cells": [ + { + "ordinal": 0, + "left": 0, + "top": 1, + "width": 66, + "height": 19 + }, + { + "ordinal": 1, + "left": 67, + "top": 1, + "width": 66, + "height": 19 + }, + { + "ordinal": 2, + "left": 134, + "top": 1, + "width": 66, + "height": 19 + }, + { + "ordinal": 3, + "left": 0, + "top": 21, + "width": 66, + "height": 19 + }, + { + "ordinal": 4, + "left": 67, + "top": 21, + "width": 66, + "height": 19 + }, + { + "ordinal": 5, + "left": 134, + "top": 21, + "width": 66, + "height": 19 + }, + { + "ordinal": 6, + "left": 0, + "top": 41, + "width": 100, + "height": 19 + }, + { + "ordinal": 7, + "left": 101, + "top": 41, + "width": 99, + "height": 19 + } + ], + "problems": [] + }, + "8@3 200x60 tiled": { + "columns": 3, + "problems": [] + } + } + }, + "notes": [ + "tiled column counts are recorded beside each shape; they are tmux's choice, not the author's" + ], + "durationMs": 5336 + }, + { + "name": "readiness-boundary", + "ok": true, + "claims": [ + { + "claim": "tmux alone: a missing executable still yields a pane pid", + "ok": true, + "observed": "2 pid=16425 dead=1 status=1 cmd=/definitely/missing x" + }, + { + "claim": "missing executable: startup-failed", + "ok": true, + "observed": { + "type": "startup-failed", + "id": "missing", + "reason": "the interactive child could not be started (ENOENT)" + } + }, + { + "claim": "missing executable: never ready", + "ok": true + }, + { + "claim": "exit 1: ready acknowledged", + "ok": true, + "observed": { + "type": "ready", + "id": "exit1", + "pid": 16786 + } + }, + { + "claim": "exit 1: then exit code 1", + "ok": true, + "observed": { + "type": "exited", + "id": "exit1", + "exitCode": 1, + "proof": { + "method": "exited", + "childPid": 16786, + "childGone": true, + "descendants": [], + "survivors": [], + "terminalHolders": [] + } + } + }, + { + "claim": "exit 1: ready precedes exited", + "ok": true, + "observed": [ + "startup-failed", + "ready", + "exited" + ] + }, + { + "claim": "the pane and its worker survived both launches", + "ok": true, + "observed": "%0 16582 0" + }, + { + "claim": "server stopped", + "ok": true, + "observed": { + "serverGone": true, + "unreachable": true, + "socketFileRemains": true + } + } + ], + "facts": { + "tmuxAlone": [ + "0 pid=16398 dead=0 status= cmd=sleep 60", + "1 pid=16444 dead=1 status=1 cmd=/bin/sh -c \"exit 1\"", + "2 pid=16425 dead=1 status=1 cmd=/definitely/missing x" + ] + }, + "notes": [], + "durationMs": 2276 + }, + { + "name": "journey", + "ok": true, + "claims": [ + { + "claim": "pane 0: worker on the pane terminal", + "ok": true, + "observed": { + "hello": { + "type": "hello", + "ordinal": 0, + "token": "", + "pid": 17190, + "ppid": 17188, + "pgid": 17190, + "tty": "ttys009", + "isatty": [ + true, + true, + true + ] + }, + "pane": { + "ordinal": 0, + "id": "%0", + "tty": "/dev/ttys009", + "pid": 17190, + "cell": { + "ordinal": 0, + "left": 0, + "top": 1, + "width": 80, + "height": 23 + } + } + } + }, + { + "claim": "pane 0: worker stdin/stdout/stderr are terminals", + "ok": true + }, + { + "claim": "pane 1: worker on the pane terminal", + "ok": true, + "observed": { + "hello": { + "type": "hello", + "ordinal": 1, + "token": "", + "pid": 17262, + "ppid": 17188, + "pgid": 17262, + "tty": "ttys012", + "isatty": [ + true, + true, + true + ] + }, + "pane": { + "ordinal": 1, + "id": "%1", + "tty": "/dev/ttys012", + "pid": 17262, + "cell": { + "ordinal": 1, + "left": 81, + "top": 1, + "width": 79, + "height": 23 + } + } + } + }, + { + "claim": "pane 1: worker stdin/stdout/stderr are terminals", + "ok": true + }, + { + "claim": "pane 2: worker on the pane terminal", + "ok": true, + "observed": { + "hello": { + "type": "hello", + "ordinal": 2, + "token": "", + "pid": 17271, + "ppid": 17188, + "pgid": 17271, + "tty": "ttys020", + "isatty": [ + true, + true, + true + ] + }, + "pane": { + "ordinal": 2, + "id": "%2", + "tty": "/dev/ttys020", + "pid": 17271, + "cell": { + "ordinal": 2, + "left": 0, + "top": 25, + "width": 80, + "height": 23 + } + } + } + }, + { + "claim": "pane 2: worker stdin/stdout/stderr are terminals", + "ok": true + }, + { + "claim": "pane 3: worker on the pane terminal", + "ok": true, + "observed": { + "hello": { + "type": "hello", + "ordinal": 3, + "token": "", + "pid": 17293, + "ppid": 17188, + "pgid": 17293, + "tty": "ttys021", + "isatty": [ + true, + true, + true + ] + }, + "pane": { + "ordinal": 3, + "id": "%3", + "tty": "/dev/ttys021", + "pid": 17293, + "cell": { + "ordinal": 3, + "left": 81, + "top": 25, + "width": 79, + "height": 23 + } + } + } + }, + { + "claim": "pane 3: worker stdin/stdout/stderr are terminals", + "ok": true + }, + { + "claim": "prelude displayed before any child", + "ok": true + }, + { + "claim": "all four panes ready before attach", + "ok": true + }, + { + "claim": "visible client attached after readiness", + "ok": true, + "observed": [ + { + "kind": "other", + "line": "%begin 1788359651 330 0" + }, + { + "kind": "other", + "line": "%end 1788359651 330 0" + }, + { + "kind": "other", + "line": "%session-changed $0 grid" + }, + { + "kind": "client-attached", + "client": "/dev/ttys005" + } + ] + }, + { + "claim": "two children received input concurrently", + "ok": true + }, + { + "claim": "argv bytes unchanged through IPC", + "ok": true, + "observed": [ + "a b", + "\"quoted\"", + "$HOME", + "x;y", + "`z`", + "new\nline", + "it's", + "#{pane_id}" + ] + }, + { + "claim": "child A on pane 0's terminal, in the worker's process group", + "ok": true, + "observed": { + "tty": "ttys009", + "pgid": 17190, + "isatty": [ + true, + true, + true + ] + } + }, + { + "claim": "prelude text was not fed to the child as input", + "ok": true, + "observed": [ + "hello from zero" + ] + }, + { + "claim": "pane 0 shows prelude, banner and echo", + "ok": true, + "observed": "Prelude: this pane belongs to the Implementor.\nhello from zero\nchild[plain] pid=17409 pgid=17190 tty=ttys009 isatty=true,true,true argv=[\"a b\",\"\\\"quoted\\\"\",\"$HOME\",\"x;y\",\"`z`\",\"new\\nline\",\"it's\",\"#{pane_id}\"]\n> hello from zero" + }, + { + "claim": "a second concurrent launch on pane 0 is refused", + "ok": true, + "observed": { + "type": "refused", + "id": "A-dup", + "reason": "busy" + } + }, + { + "claim": "shell took the foreground in a process group of its own", + "ok": true, + "observed": { + "shellRow": { + "pid": 17411, + "ppid": 17293, + "pgid": 17411, + "tty": "ttys021", + "tpgid": 17411, + "command": "/bin/zsh" + }, + "workerRow": { + "pid": 17293, + "ppid": 17188, + "pgid": 17293, + "tty": "ttys021", + "tpgid": 17411, + "command": "deno run --allow-all /private/tmp/xmd-726-pane-workers/scripts/proofs/tmux-pane-workers/worker.ts 3 /var/folders/6_/pc0hwbg54xsgfstv9nwq5qpc0000gn/T/xtg-BXg4aN" + } + } + }, + { + "claim": "shell put its background job in a process group of its own", + "ok": true, + "observed": { + "sleeper": { + "pid": 18202, + "ppid": 17411, + "pgid": 18202, + "tty": "ttys021", + "tpgid": 17411, + "command": "sleep 300" + }, + "shellRow": { + "pid": 17411, + "ppid": 17293, + "pgid": 17411, + "tty": "ttys021", + "tpgid": 17411, + "command": "/bin/zsh" + } + } + }, + { + "claim": "fg made the job the terminal's foreground process group", + "ok": true, + "observed": { + "pid": 18202, + "ppid": 17411, + "pgid": 18202, + "tty": "ttys021", + "tpgid": 18202, + "command": "sleep 300" + } + }, + { + "claim": "^Z suspended the foreground job", + "ok": true, + "observed": [ + "[1] + 18202 running sleep 300", + "^Z", + "[1] + 18202 suspended sleep 300" + ] + }, + { + "claim": "^C interrupted child B", + "ok": true, + "observed": { + "type": "exited", + "id": "B", + "signal": "SIGINT", + "proof": { + "method": "exited", + "childPid": 17408, + "childGone": true, + "descendants": [], + "survivors": [], + "terminalHolders": [] + } + } + }, + { + "claim": "worker 1 survived the ^C that ended its child", + "ok": true + }, + { + "claim": "child A exited 3 on request", + "ok": true, + "observed": { + "type": "exited", + "id": "A", + "exitCode": 3, + "proof": { + "method": "exited", + "childPid": 17409, + "childGone": true, + "descendants": [], + "survivors": [], + "terminalHolders": [] + } + } + }, + { + "claim": "child C still runs while A exited", + "ok": true + }, + { + "claim": "second child in pane 0 on the same pane and worker", + "ok": true, + "observed": { + "a2": { + "type": "ready", + "id": "A2", + "pid": 18696 + }, + "paneNow": "%0 17190" + } + }, + { + "claim": "second child received input", + "ok": true + }, + { + "claim": "reader close observed as %client-detached", + "ok": true, + "observed": [ + { + "kind": "layout-change" + }, + { + "kind": "client-detached", + "client": "/dev/ttys005" + } + ] + }, + { + "claim": "attach client exited 0 after detach", + "ok": true, + "observed": { + "exitCode": 0 + } + }, + { + "claim": "after reader close, children still run until cancelled", + "ok": true + }, + { + "claim": "every cancelled child is gone", + "ok": true, + "observed": [ + { + "method": "interrupted", + "childPid": 18696, + "childGone": true, + "descendants": [ + { + "pid": 18826, + "command": "/bin/ps -axo pid=,ppid=,pgid=,tty=,tpgid=,command=", + "inGroup": true, + "delivery": "absent", + "gone": true + } + ], + "survivors": [], + "terminalHolders": [] + }, + { + "method": "killed", + "childPid": 17410, + "childGone": true, + "descendants": [ + { + "pid": 17602, + "command": "sleep 600", + "inGroup": true, + "delivery": "delivered", + "gone": true + }, + { + "pid": 18827, + "command": "/bin/ps -axo pid=,ppid=,pgid=,tty=,tpgid=,command=", + "inGroup": true, + "delivery": "absent", + "gone": true + } + ], + "survivors": [], + "terminalHolders": [] + }, + { + "method": "killed", + "childPid": 17411, + "childGone": true, + "descendants": [], + "survivors": [], + "terminalHolders": [] + } + ] + }, + { + "claim": "C ignored SIGINT and was killed, with its in-group descendant", + "ok": true, + "observed": { + "method": "killed", + "cDescendant": 17602, + "descendants": [ + { + "pid": 17602, + "command": "sleep 600", + "inGroup": true, + "delivery": "delivered", + "gone": true + }, + { + "pid": 18827, + "command": "/bin/ps -axo pid=,ppid=,pgid=,tty=,tpgid=,command=", + "inGroup": true, + "delivery": "absent", + "gone": true + } + ], + "signals": [ + "SIGINT" + ] + } + }, + { + "claim": "every worker acknowledged shutdown with nothing left on its terminal", + "ok": true, + "observed": [ + [], + [], + [], + [] + ] + }, + { + "claim": "workers gone", + "ok": true + }, + { + "claim": "tmux server gone", + "ok": true, + "observed": { + "serverGone": true, + "unreachable": true, + "socketFileRemains": true + } + }, + { + "claim": "all child pids gone", + "ok": true + }, + { + "claim": "nothing holds a pane terminal open", + "ok": true, + "observed": { + "/dev/ttys009": [], + "/dev/ttys012": [], + "/dev/ttys020": [], + "/dev/ttys021": [] + } + }, + { + "claim": "control client never received pane output", + "ok": true, + "observed": 8 + }, + { + "claim": "terminal settings restored", + "ok": true, + "observed": { + "sttyBefore": "gfmt1:cflag=4b00:iflag=6b02:lflag=5cb:oflag=3:discard=f:dsusp=19:eof=4:eol=ff:eol2=ff:erase=7f:intr=3:kill=15:lnext=16:min=1:quit=1c:reprint=12:start=11:status=14:stop=13:susp=1a:time=0:werase=17:ispeed=9600:ospeed=9600", + "sttyAfter": "gfmt1:cflag=4b00:iflag=6b02:lflag=5cb:oflag=3:discard=f:dsusp=19:eof=4:eol=ff:eol2=ff:erase=7f:intr=3:kill=15:lnext=16:min=1:quit=1c:reprint=12:start=11:status=14:stop=13:susp=1a:time=0:werase=17:ispeed=9600:ospeed=9600" + } + } + ], + "facts": { + "panes": [ + { + "ordinal": 0, + "id": "%0", + "tty": "/dev/ttys009", + "pid": 17190, + "cell": { + "ordinal": 0, + "left": 0, + "top": 1, + "width": 80, + "height": 23 + } + }, + { + "ordinal": 1, + "id": "%1", + "tty": "/dev/ttys012", + "pid": 17262, + "cell": { + "ordinal": 1, + "left": 81, + "top": 1, + "width": 79, + "height": 23 + } + }, + { + "ordinal": 2, + "id": "%2", + "tty": "/dev/ttys020", + "pid": 17271, + "cell": { + "ordinal": 2, + "left": 0, + "top": 25, + "width": 80, + "height": 23 + } + }, + { + "ordinal": 3, + "id": "%3", + "tty": "/dev/ttys021", + "pid": 17293, + "cell": { + "ordinal": 3, + "left": 81, + "top": 25, + "width": 79, + "height": 23 + } + } + ], + "hellos": [ + { + "type": "hello", + "ordinal": 0, + "token": "", + "pid": 17190, + "ppid": 17188, + "pgid": 17190, + "tty": "ttys009", + "isatty": [ + true, + true, + true + ] + }, + { + "type": "hello", + "ordinal": 1, + "token": "", + "pid": 17262, + "ppid": 17188, + "pgid": 17262, + "tty": "ttys012", + "isatty": [ + true, + true, + true + ] + }, + { + "type": "hello", + "ordinal": 2, + "token": "", + "pid": 17271, + "ppid": 17188, + "pgid": 17271, + "tty": "ttys020", + "isatty": [ + true, + true, + true + ] + }, + { + "type": "hello", + "ordinal": 3, + "token": "", + "pid": 17293, + "ppid": 17188, + "pgid": 17293, + "tty": "ttys021", + "isatty": [ + true, + true, + true + ] + } + ], + "visibleClient": "/dev/ttys005", + "closeDetectMs": 48, + "quiescence": [ + { + "method": "interrupted", + "childPid": 18696, + "childGone": true, + "descendants": [ + { + "pid": 18826, + "command": "/bin/ps -axo pid=,ppid=,pgid=,tty=,tpgid=,command=", + "inGroup": true, + "delivery": "absent", + "gone": true + } + ], + "survivors": [], + "terminalHolders": [] + }, + { + "method": "killed", + "childPid": 17410, + "childGone": true, + "descendants": [ + { + "pid": 17602, + "command": "sleep 600", + "inGroup": true, + "delivery": "delivered", + "gone": true + }, + { + "pid": 18827, + "command": "/bin/ps -axo pid=,ppid=,pgid=,tty=,tpgid=,command=", + "inGroup": true, + "delivery": "absent", + "gone": true + } + ], + "survivors": [], + "terminalHolders": [] + }, + { + "method": "killed", + "childPid": 17411, + "childGone": true, + "descendants": [], + "survivors": [], + "terminalHolders": [] + } + ], + "controlLog": [ + "%begin 1788359651 330 0", + "%end 1788359651 330 0", + "%session-changed $0 grid", + "%client-session-changed /dev/ttys005 $0 grid", + "%layout-change @0 b1a4,200x56,0,0[200x28,0,0{100x28,0,0,0,99x28,101,0,1},200x27,0,29{100x27,0,29,2,99x27,101,29,3}] b1a4,200x56,0,0[200x28,0,0{100x28,0,0,0,99x28,101,0,1},200x27,0,29{100x27,0,29,2,99x27,101,29,3}] *", + "%client-detached /dev/ttys005", + "%sessions-changed", + "%exit" + ] + }, + "notes": [], + "durationMs": 8083 + }, + { + "name": "startup-failure-atomic", + "ok": true, + "claims": [ + { + "claim": "pane 2 reported startup-failed", + "ok": true, + "observed": { + "type": "startup-failed", + "id": "c", + "reason": "the interactive child could not be started (ENOENT)" + } + }, + { + "claim": "three siblings had already started", + "ok": true + }, + { + "claim": "the grid failed instead of attaching", + "ok": true, + "observed": "grid startup failed: pane 2" + }, + { + "claim": "started siblings torn down", + "ok": true, + "observed": [ + 20545, + 20546, + 20547 + ] + }, + { + "claim": "workers torn down", + "ok": true, + "observed": [ + 20311, + 20370, + 20392, + 20415 + ] + }, + { + "claim": "server torn down", + "ok": true, + "observed": 20310 + } + ], + "facts": { + "outcomes": [ + { + "type": "ready", + "id": "a", + "pid": 20545 + }, + { + "type": "ready", + "id": "b", + "pid": 20546 + }, + { + "type": "startup-failed", + "id": "c", + "reason": "the interactive child could not be started (ENOENT)" + }, + { + "type": "ready", + "id": "s", + "pid": 20547 + } + ] + }, + "notes": [], + "durationMs": 756 + }, + { + "name": "signals-distinct", + "ok": true, + "claims": [ + { + "claim": "detach: %client-detached names the visible client", + "ok": true, + "observed": [ + { + "kind": "layout-change" + }, + { + "kind": "client-detached", + "client": "/dev/ttys005" + } + ] + }, + { + "claim": "detach: children keep running", + "ok": true + }, + { + "claim": "control loss: the stream ends with %exit, not %client-detached for the reader", + "ok": true, + "observed": [ + { + "kind": "exit" + }, + { + "kind": "closed" + } + ] + }, + { + "claim": "control loss: server still answers", + "ok": true + }, + { + "claim": "control loss: children keep running", + "ok": true + }, + { + "claim": "control loss: workers still connected", + "ok": true + }, + { + "claim": "server stop: every worker link closed", + "ok": true + }, + { + "claim": "server stop: children ended with their terminal (SIGHUP)", + "ok": true, + "observed": [ + false, + false + ] + }, + { + "claim": "server stop: workers ended with their terminal", + "ok": true + } + ], + "facts": { + "controlClient": "client-20751" + }, + "notes": [ + "the three signals were classified from different sources: attach exit + %client-detached, control EOF/%exit, has-session failure + link EOF" + ], + "durationMs": 746 + }, + { + "name": "negative-children", + "ok": true, + "claims": [ + { + "claim": "negative child and its in-group descendant survived the first interrupt", + "ok": true + }, + { + "claim": "escaped descendant left the session and process group", + "ok": true, + "observed": { + "pid": 21500, + "ppid": 21237, + "pgid": 21500, + "tty": "??", + "tpgid": 0, + "command": "/bin/sleep 600" + } + }, + { + "claim": "orphan-escape: the descendant left the session and process group while its parent lived", + "ok": true, + "observed": { + "pid": 21774, + "ppid": 21682, + "pgid": 21774, + "tty": "??", + "tpgid": 0, + "command": "/bin/sleep 600" + } + }, + { + "claim": "orphan-escape: outside the settlement's ancestry once the parent exited", + "ok": true, + "observed": [] + }, + { + "claim": "orphan-escape-closed: the descendant left the session and process group while its parent lived", + "ok": true, + "observed": { + "pid": 22180, + "ppid": 22088, + "pgid": 22180, + "tty": "??", + "tpgid": 0, + "command": "/bin/sleep 600" + } + }, + { + "claim": "orphan-escape-closed: outside the settlement's ancestry once the parent exited", + "ok": true, + "observed": [] + }, + { + "claim": "ignore-sigint-fork: child stopped (killed)", + "ok": true + }, + { + "claim": "ignore-sigint-fork: descendant 21511 was found in the pre-kill snapshot and stopped", + "ok": true, + "observed": { + "pid": 21511, + "command": "sleep 600", + "inGroup": true, + "delivery": "delivered", + "gone": true + } + }, + { + "claim": "escape: child stopped (interrupted)", + "ok": true + }, + { + "claim": "escape: descendant 21500 was found in the pre-kill snapshot and stopped", + "ok": true, + "observed": { + "pid": 21500, + "command": "/bin/sleep 600", + "inGroup": false, + "delivery": "delivered", + "gone": true + } + }, + { + "claim": "escape-closed: child stopped (interrupted)", + "ok": true + }, + { + "claim": "escape-closed: descendant 21526 was found in the pre-kill snapshot and stopped", + "ok": true, + "observed": { + "pid": 21526, + "command": "/bin/sleep 600", + "inGroup": false, + "delivery": "delivered", + "gone": true + } + }, + { + "claim": "orphans: outside the pane sweep's ancestry once their parent exited", + "ok": true, + "observed": [ + { + "method": "exited", + "childGone": true, + "descendants": [], + "survivors": [], + "terminalHolders": [] + }, + { + "method": "exited", + "childGone": true, + "descendants": [], + "survivors": [], + "terminalHolders": [] + }, + { + "method": "exited", + "childGone": true, + "descendants": [], + "survivors": [], + "terminalHolders": [] + }, + { + "method": "exited", + "childGone": true, + "descendants": [], + "survivors": [], + "terminalHolders": [] + }, + { + "method": "exited", + "childGone": true, + "descendants": [], + "survivors": [], + "terminalHolders": [] + } + ] + }, + { + "claim": "server stopped", + "ok": true + }, + { + "claim": "orphan holding the terminal: named by its parent's settlement sweep and stopped before `exited`", + "ok": true, + "observed": { + "holdingOrphan": 21774, + "foundHolding": { + "pid": 21774, + "gone": true + } + } + }, + { + "claim": "orphan that closed the terminal: outlived its parent, reparented, still running", + "ok": true, + "observed": { + "pid": 22180, + "ppid": 1, + "pgid": 22180, + "tty": "??", + "tpgid": 0, + "command": "/bin/sleep 600" + } + }, + { + "claim": "orphan that closed the terminal: recorded as unprovable by this topology", + "ok": true, + "observed": { + "closedFound": false, + "closedAlive": true + } + }, + { + "claim": "after the server stopped, `lsof` names no holder of any pane terminal", + "ok": true, + "observed": { + "/dev/ttys009": [], + "/dev/ttys012": [], + "/dev/ttys020": [], + "/dev/ttys021": [], + "/dev/ttys022": [] + } + } + ], + "facts": { + "children": { + "ignore-sigint-fork": { + "mode": "ignore-sigint-fork", + "argv": [], + "pid": 21236, + "ppid": 20883, + "pgid": 20883, + "tty": "ttys009", + "tpgid": 20883, + "isatty": [ + true, + true, + true + ], + "stdin": [], + "signals": [ + "SIGINT" + ], + "descendants": [ + { + "pid": 21511, + "kind": "in-group" + } + ] + }, + "escape": { + "mode": "escape", + "argv": [], + "pid": 21237, + "ppid": 20940, + "pgid": 20940, + "tty": "ttys012", + "tpgid": 20940, + "isatty": [ + true, + true, + true + ], + "stdin": [], + "signals": [], + "descendants": [ + { + "pid": 21500, + "kind": "escape" + } + ] + }, + "escape-closed": { + "mode": "escape-closed", + "argv": [], + "pid": 21238, + "ppid": 20950, + "pgid": 20950, + "tty": "ttys020", + "tpgid": 20950, + "isatty": [ + true, + true, + true + ], + "stdin": [], + "signals": [], + "descendants": [ + { + "pid": 21526, + "kind": "escape-closed" + } + ] + } + }, + "orphan-escape": { + "pid": 21774, + "before": { + "pid": 21774, + "ppid": 21682, + "pgid": 21774, + "tty": "??", + "tpgid": 0, + "command": "/bin/sleep 600" + }, + "settlement": { + "method": "exited", + "childPid": 21682, + "childGone": true, + "descendants": [], + "survivors": [], + "terminalHolders": [ + { + "pid": 21774, + "gone": true + } + ] + } + }, + "orphan-escape-closed": { + "pid": 22180, + "before": { + "pid": 22180, + "ppid": 22088, + "pgid": 22180, + "tty": "??", + "tpgid": 0, + "command": "/bin/sleep 600" + }, + "afterParentExit": { + "pid": 22180, + "ppid": 1, + "pgid": 22180, + "tty": "??", + "tpgid": 0, + "command": "/bin/sleep 600" + }, + "settlement": { + "method": "exited", + "childPid": 22088, + "childGone": true, + "descendants": [], + "survivors": [], + "terminalHolders": [] + } + }, + "ignore-sigint-fork.proof": { + "method": "killed", + "childPid": 21236, + "childGone": true, + "descendants": [ + { + "pid": 21511, + "command": "sleep 600", + "inGroup": true, + "delivery": "delivered", + "gone": true + }, + { + "pid": 22494, + "command": "/bin/ps -axo pid=,ppid=,pgid=,tty=,tpgid=,command=", + "inGroup": true, + "delivery": "absent", + "gone": true + } + ], + "survivors": [], + "terminalHolders": [] + }, + "escape.proof": { + "method": "interrupted", + "childPid": 21237, + "childGone": true, + "descendants": [ + { + "pid": 21500, + "command": "/bin/sleep 600", + "inGroup": false, + "delivery": "delivered", + "gone": true + }, + { + "pid": 22495, + "command": "/bin/ps -axo pid=,ppid=,pgid=,tty=,tpgid=,command=", + "inGroup": true, + "delivery": "absent", + "gone": true + } + ], + "survivors": [], + "terminalHolders": [] + }, + "escape-closed.proof": { + "method": "interrupted", + "childPid": 21238, + "childGone": true, + "descendants": [ + { + "pid": 21526, + "command": "/bin/sleep 600", + "inGroup": false, + "delivery": "delivered", + "gone": true + }, + { + "pid": 22493, + "command": "/bin/ps -axo pid=,ppid=,pgid=,tty=,tpgid=,command=", + "inGroup": true, + "delivery": "absent", + "gone": true + } + ], + "survivors": [], + "terminalHolders": [] + }, + "ttyHolders": [ + [], + [], + [], + [], + [] + ], + "orphanClosed": { + "pid": 22180, + "foundByAnySweep": false, + "stillRunning": true + } + }, + "notes": [ + "orphan 22180 (escaped the group, lost its parent, closed the terminal) is invisible to ancestry, process-group and terminal-holder sweeps; the check killed it afterwards using the child's own record of its pid", + "once the worker exits, tmux closes the pane's pty master and macOS revokes the slave, so a holder can only be named by the worker before it leaves" + ], + "durationMs": 9995 + }, + { + "name": "sequential-handoff", + "ok": true, + "claims": [ + { + "claim": "the descendant left the session and process group and still holds the pane terminal", + "ok": true, + "observed": { + "escaped": { + "pid": 24236, + "ppid": 24157, + "pgid": 24236, + "tty": "??", + "tpgid": 0, + "command": "/bin/sleep 600" + }, + "holdersBefore": [ + 24055, + 24157, + 24236 + ] + } + }, + { + "claim": "a launch sent while the first child was settling was refused, before `exited`", + "ok": true, + "observed": { + "early": { + "type": "refused", + "id": "early", + "reason": "busy" + }, + "order": [ + "ready", + "refused", + "exited" + ] + } + }, + { + "claim": "the orphaned descendant was outside ancestry but named by the settlement's terminal sweep", + "ok": true, + "observed": { + "descendants": [], + "terminalHolders": [ + { + "pid": 24236, + "gone": true + } + ] + } + }, + { + "claim": "the descendant was stopped before `exited` was reported", + "ok": true, + "observed": { + "swept": { + "pid": 24236, + "gone": true + }, + "reachable": false + } + }, + { + "claim": "after admission, only the worker and the second child hold the pane terminal", + "ok": true, + "observed": { + "holdersAfter": [ + 24055, + 24548 + ], + "worker": 24055, + "second": 24548 + } + }, + { + "claim": "the second child runs on the same pane and worker", + "ok": true + }, + { + "claim": "nothing held the terminal at shutdown", + "ok": true, + "observed": [] + }, + { + "claim": "server stopped", + "ok": true + }, + { + "claim": "first child, descendant, second child gone", + "ok": true + } + ], + "facts": { + "first": { + "child": 24157, + "descendant": 24236, + "escaped": { + "pid": 24236, + "ppid": 24157, + "pgid": 24236, + "tty": "??", + "tpgid": 0, + "command": "/bin/sleep 600" + }, + "holdersBefore": [ + 24055, + 24157, + 24236 + ] + }, + "exited": { + "exitCode": 0, + "proof": { + "method": "exited", + "childPid": 24157, + "childGone": true, + "descendants": [], + "survivors": [], + "terminalHolders": [ + { + "pid": 24236, + "gone": true + } + ] + }, + "handoffMs": 443, + "order": [ + "ready", + "refused", + "exited" + ] + }, + "second": { + "child": 24548, + "holdersAfter": [ + 24055, + 24548 + ], + "relaunchMs": 1 + } + }, + "notes": [ + "handoff (exit requested → exited) 443 ms; relaunch (launch → ready) 1 ms" + ], + "durationMs": 2520 + }, + { + "name": "cancellation-points", + "ok": true, + "claims": [ + { + "claim": "prepared: phase reached", + "ok": true + }, + { + "claim": "prepared: server gone", + "ok": true + }, + { + "claim": "prepared: workers gone", + "ok": true + }, + { + "claim": "prepared: children gone", + "ok": true + }, + { + "claim": "prepared: private directory removed", + "ok": true + }, + { + "claim": "workers: phase reached", + "ok": true + }, + { + "claim": "workers: server gone", + "ok": true + }, + { + "claim": "workers: workers gone", + "ok": true + }, + { + "claim": "workers: children gone", + "ok": true + }, + { + "claim": "workers: private directory removed", + "ok": true + }, + { + "claim": "ready: phase reached", + "ok": true + }, + { + "claim": "ready: server gone", + "ok": true + }, + { + "claim": "ready: workers gone", + "ok": true + }, + { + "claim": "ready: children gone", + "ok": true + }, + { + "claim": "ready: private directory removed", + "ok": true + }, + { + "claim": "attached: phase reached", + "ok": true + }, + { + "claim": "attached: server gone", + "ok": true + }, + { + "claim": "attached: workers gone", + "ok": true + }, + { + "claim": "attached: children gone", + "ok": true + }, + { + "claim": "attached: private directory removed", + "ok": true + }, + { + "claim": "active: phase reached", + "ok": true + }, + { + "claim": "active: server gone", + "ok": true + }, + { + "claim": "active: workers gone", + "ok": true + }, + { + "claim": "active: children gone", + "ok": true + }, + { + "claim": "active: private directory removed", + "ok": true + } + ], + "facts": { + "prepared": { + "serverPid": 25020, + "workerPids": [], + "childPids": [], + "teardownMs": 81 + }, + "workers": { + "serverPid": 25172, + "workerPids": [ + 25180, + 25236 + ], + "childPids": [ + 25323, + 25324 + ], + "teardownMs": 88 + }, + "ready": { + "serverPid": 25378, + "workerPids": [ + 25379, + 25432 + ], + "childPids": [ + 25528, + 25527 + ], + "teardownMs": 72 + }, + "attached": { + "serverPid": 25574, + "workerPids": [ + 25578, + 25637 + ], + "childPids": [ + 25739, + 25740 + ], + "teardownMs": 330 + }, + "active": { + "serverPid": 25912, + "workerPids": [ + 25914, + 25970 + ], + "childPids": [ + 26086, + 26085 + ], + "teardownMs": 426 + } + }, + "notes": [], + "durationMs": 3568 + }, + { + "name": "measurements", + "ok": true, + "claims": [ + { + "claim": "60 runs completed with complete teardown", + "ok": true + } + ], + "facts": { + "runs": [ + { + "panes": 2, + "layoutMs": 348, + "workersMs": 497, + "readyMs": 504, + "attachMs": 31, + "closeDetectMs": 35, + "handoffMs": 732, + "relaunchMs": 1, + "teardownMs": 1662 + }, + { + "panes": 2, + "layoutMs": 1461, + "workersMs": 1922, + "readyMs": 1927, + "attachMs": 117, + "closeDetectMs": 94, + "handoffMs": 614, + "relaunchMs": 1, + "teardownMs": 1265 + }, + { + "panes": 2, + "layoutMs": 338, + "workersMs": 506, + "readyMs": 509, + "attachMs": 58, + "closeDetectMs": 32, + "handoffMs": 648, + "relaunchMs": 2, + "teardownMs": 1170 + }, + { + "panes": 2, + "layoutMs": 280, + "workersMs": 401, + "readyMs": 404, + "attachMs": 38, + "closeDetectMs": 29, + "handoffMs": 561, + "relaunchMs": 3, + "teardownMs": 1184 + }, + { + "panes": 2, + "layoutMs": 282, + "workersMs": 405, + "readyMs": 409, + "attachMs": 57, + "closeDetectMs": 29, + "handoffMs": 559, + "relaunchMs": 2, + "teardownMs": 1185 + }, + { + "panes": 2, + "layoutMs": 248, + "workersMs": 365, + "readyMs": 368, + "attachMs": 33, + "closeDetectMs": 28, + "handoffMs": 568, + "relaunchMs": 2, + "teardownMs": 1160 + }, + { + "panes": 2, + "layoutMs": 249, + "workersMs": 361, + "readyMs": 364, + "attachMs": 43, + "closeDetectMs": 29, + "handoffMs": 611, + "relaunchMs": 4, + "teardownMs": 1212 + }, + { + "panes": 2, + "layoutMs": 316, + "workersMs": 450, + "readyMs": 453, + "attachMs": 66, + "closeDetectMs": 49, + "handoffMs": 598, + "relaunchMs": 1, + "teardownMs": 1249 + }, + { + "panes": 2, + "layoutMs": 659, + "workersMs": 765, + "readyMs": 770, + "attachMs": 48, + "closeDetectMs": 28, + "handoffMs": 608, + "relaunchMs": 3, + "teardownMs": 1232 + }, + { + "panes": 2, + "layoutMs": 628, + "workersMs": 709, + "readyMs": 715, + "attachMs": 145, + "closeDetectMs": 36, + "handoffMs": 591, + "relaunchMs": 1, + "teardownMs": 1209 + }, + { + "panes": 2, + "layoutMs": 307, + "workersMs": 434, + "readyMs": 438, + "attachMs": 45, + "closeDetectMs": 31, + "handoffMs": 657, + "relaunchMs": 2, + "teardownMs": 1452 + }, + { + "panes": 2, + "layoutMs": 806, + "workersMs": 949, + "readyMs": 959, + "attachMs": 78, + "closeDetectMs": 35, + "handoffMs": 648, + "relaunchMs": 1, + "teardownMs": 1238 + }, + { + "panes": 2, + "layoutMs": 598, + "workersMs": 674, + "readyMs": 678, + "attachMs": 77, + "closeDetectMs": 40, + "handoffMs": 639, + "relaunchMs": 1, + "teardownMs": 1214 + }, + { + "panes": 2, + "layoutMs": 393, + "workersMs": 465, + "readyMs": 468, + "attachMs": 181, + "closeDetectMs": 71, + "handoffMs": 652, + "relaunchMs": 2, + "teardownMs": 1285 + }, + { + "panes": 2, + "layoutMs": 297, + "workersMs": 403, + "readyMs": 406, + "attachMs": 49, + "closeDetectMs": 35, + "handoffMs": 569, + "relaunchMs": 2, + "teardownMs": 1069 + }, + { + "panes": 2, + "layoutMs": 286, + "workersMs": 389, + "readyMs": 393, + "attachMs": 39, + "closeDetectMs": 27, + "handoffMs": 616, + "relaunchMs": 5, + "teardownMs": 1299 + }, + { + "panes": 2, + "layoutMs": 268, + "workersMs": 377, + "readyMs": 380, + "attachMs": 30, + "closeDetectMs": 29, + "handoffMs": 668, + "relaunchMs": 2, + "teardownMs": 1301 + }, + { + "panes": 2, + "layoutMs": 363, + "workersMs": 473, + "readyMs": 476, + "attachMs": 287, + "closeDetectMs": 96, + "handoffMs": 686, + "relaunchMs": 1, + "teardownMs": 1173 + }, + { + "panes": 2, + "layoutMs": 365, + "workersMs": 526, + "readyMs": 531, + "attachMs": 147, + "closeDetectMs": 145, + "handoffMs": 954, + "relaunchMs": 1, + "teardownMs": 1241 + }, + { + "panes": 2, + "layoutMs": 314, + "workersMs": 414, + "readyMs": 427, + "attachMs": 57, + "closeDetectMs": 39, + "handoffMs": 565, + "relaunchMs": 1, + "teardownMs": 1156 + }, + { + "panes": 4, + "layoutMs": 543, + "workersMs": 633, + "readyMs": 637, + "attachMs": 54, + "closeDetectMs": 26, + "handoffMs": 780, + "relaunchMs": 2, + "teardownMs": 1976 + }, + { + "panes": 4, + "layoutMs": 436, + "workersMs": 567, + "readyMs": 574, + "attachMs": 91, + "closeDetectMs": 31, + "handoffMs": 855, + "relaunchMs": 1, + "teardownMs": 1964 + }, + { + "panes": 4, + "layoutMs": 591, + "workersMs": 711, + "readyMs": 717, + "attachMs": 51, + "closeDetectMs": 31, + "handoffMs": 801, + "relaunchMs": 2, + "teardownMs": 2042 + }, + { + "panes": 4, + "layoutMs": 565, + "workersMs": 764, + "readyMs": 769, + "attachMs": 68, + "closeDetectMs": 33, + "handoffMs": 789, + "relaunchMs": 2, + "teardownMs": 1979 + }, + { + "panes": 4, + "layoutMs": 705, + "workersMs": 728, + "readyMs": 733, + "attachMs": 59, + "closeDetectMs": 43, + "handoffMs": 825, + "relaunchMs": 2, + "teardownMs": 2024 + }, + { + "panes": 4, + "layoutMs": 493, + "workersMs": 558, + "readyMs": 562, + "attachMs": 49, + "closeDetectMs": 35, + "handoffMs": 831, + "relaunchMs": 1, + "teardownMs": 1878 + }, + { + "panes": 4, + "layoutMs": 549, + "workersMs": 620, + "readyMs": 624, + "attachMs": 68, + "closeDetectMs": 70, + "handoffMs": 888, + "relaunchMs": 1, + "teardownMs": 1830 + }, + { + "panes": 4, + "layoutMs": 521, + "workersMs": 544, + "readyMs": 548, + "attachMs": 46, + "closeDetectMs": 34, + "handoffMs": 803, + "relaunchMs": 1, + "teardownMs": 2000 + }, + { + "panes": 4, + "layoutMs": 1587, + "workersMs": 1587, + "readyMs": 1693, + "attachMs": 700, + "closeDetectMs": 46, + "handoffMs": 1169, + "relaunchMs": 2, + "teardownMs": 2066 + }, + { + "panes": 4, + "layoutMs": 653, + "workersMs": 711, + "readyMs": 718, + "attachMs": 73, + "closeDetectMs": 32, + "handoffMs": 814, + "relaunchMs": 1, + "teardownMs": 1980 + }, + { + "panes": 4, + "layoutMs": 548, + "workersMs": 637, + "readyMs": 640, + "attachMs": 82, + "closeDetectMs": 37, + "handoffMs": 699, + "relaunchMs": 2, + "teardownMs": 1990 + }, + { + "panes": 4, + "layoutMs": 1224, + "workersMs": 1224, + "readyMs": 1261, + "attachMs": 250, + "closeDetectMs": 34, + "handoffMs": 725, + "relaunchMs": 2, + "teardownMs": 2181 + }, + { + "panes": 4, + "layoutMs": 607, + "workersMs": 631, + "readyMs": 635, + "attachMs": 47, + "closeDetectMs": 28, + "handoffMs": 989, + "relaunchMs": 1, + "teardownMs": 2068 + }, + { + "panes": 4, + "layoutMs": 616, + "workersMs": 655, + "readyMs": 659, + "attachMs": 39, + "closeDetectMs": 65, + "handoffMs": 790, + "relaunchMs": 1, + "teardownMs": 1975 + }, + { + "panes": 4, + "layoutMs": 523, + "workersMs": 592, + "readyMs": 599, + "attachMs": 95, + "closeDetectMs": 45, + "handoffMs": 901, + "relaunchMs": 2, + "teardownMs": 2166 + }, + { + "panes": 4, + "layoutMs": 545, + "workersMs": 597, + "readyMs": 601, + "attachMs": 72, + "closeDetectMs": 28, + "handoffMs": 872, + "relaunchMs": 2, + "teardownMs": 2062 + }, + { + "panes": 4, + "layoutMs": 797, + "workersMs": 797, + "readyMs": 818, + "attachMs": 101, + "closeDetectMs": 39, + "handoffMs": 731, + "relaunchMs": 2, + "teardownMs": 1980 + }, + { + "panes": 4, + "layoutMs": 946, + "workersMs": 984, + "readyMs": 990, + "attachMs": 155, + "closeDetectMs": 30, + "handoffMs": 746, + "relaunchMs": 1, + "teardownMs": 2409 + }, + { + "panes": 4, + "layoutMs": 869, + "workersMs": 954, + "readyMs": 961, + "attachMs": 103, + "closeDetectMs": 69, + "handoffMs": 1115, + "relaunchMs": 1, + "teardownMs": 2096 + }, + { + "panes": 4, + "layoutMs": 553, + "workersMs": 610, + "readyMs": 614, + "attachMs": 35, + "closeDetectMs": 32, + "handoffMs": 800, + "relaunchMs": 1, + "teardownMs": 1912 + }, + { + "panes": 8, + "layoutMs": 936, + "workersMs": 1093, + "readyMs": 1101, + "attachMs": 78, + "closeDetectMs": 32, + "handoffMs": 1354, + "relaunchMs": 2, + "teardownMs": 4392 + }, + { + "panes": 8, + "layoutMs": 1030, + "workersMs": 1095, + "readyMs": 1103, + "attachMs": 105, + "closeDetectMs": 34, + "handoffMs": 1714, + "relaunchMs": 1, + "teardownMs": 4405 + }, + { + "panes": 8, + "layoutMs": 1266, + "workersMs": 1266, + "readyMs": 1300, + "attachMs": 369, + "closeDetectMs": 167, + "handoffMs": 1855, + "relaunchMs": 2, + "teardownMs": 5068 + }, + { + "panes": 8, + "layoutMs": 2176, + "workersMs": 2176, + "readyMs": 2353, + "attachMs": 182, + "closeDetectMs": 98, + "handoffMs": 1465, + "relaunchMs": 2, + "teardownMs": 4497 + }, + { + "panes": 8, + "layoutMs": 1281, + "workersMs": 1281, + "readyMs": 1299, + "attachMs": 92, + "closeDetectMs": 73, + "handoffMs": 1227, + "relaunchMs": 1, + "teardownMs": 4105 + }, + { + "panes": 8, + "layoutMs": 980, + "workersMs": 1082, + "readyMs": 1092, + "attachMs": 79, + "closeDetectMs": 30, + "handoffMs": 1939, + "relaunchMs": 3, + "teardownMs": 4374 + }, + { + "panes": 8, + "layoutMs": 1885, + "workersMs": 1885, + "readyMs": 1944, + "attachMs": 669, + "closeDetectMs": 273, + "handoffMs": 1432, + "relaunchMs": 1, + "teardownMs": 4483 + }, + { + "panes": 8, + "layoutMs": 993, + "workersMs": 1179, + "readyMs": 1217, + "attachMs": 84, + "closeDetectMs": 35, + "handoffMs": 1556, + "relaunchMs": 2, + "teardownMs": 4839 + }, + { + "panes": 8, + "layoutMs": 1249, + "workersMs": 1249, + "readyMs": 1326, + "attachMs": 384, + "closeDetectMs": 99, + "handoffMs": 2106, + "relaunchMs": 2, + "teardownMs": 4549 + }, + { + "panes": 8, + "layoutMs": 1973, + "workersMs": 1973, + "readyMs": 1990, + "attachMs": 153, + "closeDetectMs": 143, + "handoffMs": 1500, + "relaunchMs": 2, + "teardownMs": 4108 + }, + { + "panes": 8, + "layoutMs": 1032, + "workersMs": 1169, + "readyMs": 1194, + "attachMs": 145, + "closeDetectMs": 52, + "handoffMs": 1368, + "relaunchMs": 1, + "teardownMs": 4387 + }, + { + "panes": 8, + "layoutMs": 1094, + "workersMs": 1212, + "readyMs": 1218, + "attachMs": 142, + "closeDetectMs": 31, + "handoffMs": 1540, + "relaunchMs": 1, + "teardownMs": 4524 + }, + { + "panes": 8, + "layoutMs": 1080, + "workersMs": 1224, + "readyMs": 1230, + "attachMs": 100, + "closeDetectMs": 76, + "handoffMs": 1309, + "relaunchMs": 3, + "teardownMs": 4371 + }, + { + "panes": 8, + "layoutMs": 1724, + "workersMs": 1724, + "readyMs": 1756, + "attachMs": 126, + "closeDetectMs": 63, + "handoffMs": 1735, + "relaunchMs": 2, + "teardownMs": 4821 + }, + { + "panes": 8, + "layoutMs": 1449, + "workersMs": 1486, + "readyMs": 1494, + "attachMs": 264, + "closeDetectMs": 68, + "handoffMs": 1388, + "relaunchMs": 2, + "teardownMs": 4230 + }, + { + "panes": 8, + "layoutMs": 890, + "workersMs": 984, + "readyMs": 992, + "attachMs": 89, + "closeDetectMs": 29, + "handoffMs": 1233, + "relaunchMs": 13, + "teardownMs": 4515 + }, + { + "panes": 8, + "layoutMs": 2634, + "workersMs": 2634, + "readyMs": 2654, + "attachMs": 99, + "closeDetectMs": 31, + "handoffMs": 1368, + "relaunchMs": 2, + "teardownMs": 4445 + }, + { + "panes": 8, + "layoutMs": 1945, + "workersMs": 1945, + "readyMs": 2008, + "attachMs": 221, + "closeDetectMs": 87, + "handoffMs": 1399, + "relaunchMs": 2, + "teardownMs": 4214 + }, + { + "panes": 8, + "layoutMs": 805, + "workersMs": 968, + "readyMs": 984, + "attachMs": 95, + "closeDetectMs": 61, + "handoffMs": 1513, + "relaunchMs": 2, + "teardownMs": 4340 + }, + { + "panes": 8, + "layoutMs": 1061, + "workersMs": 1165, + "readyMs": 1176, + "attachMs": 118, + "closeDetectMs": 163, + "handoffMs": 1710, + "relaunchMs": 2, + "teardownMs": 4314 + } + ], + "summary": { + "2": { + "layoutMs": { + "median": 338, + "min": 248, + "max": 1461 + }, + "workersMs": { + "median": 465, + "min": 361, + "max": 1922 + }, + "readyMs": { + "median": 468, + "min": 364, + "max": 1927 + }, + "attachMs": { + "median": 57, + "min": 30, + "max": 287 + }, + "closeDetectMs": { + "median": 35, + "min": 27, + "max": 145 + }, + "handoffMs": { + "median": 616, + "min": 559, + "max": 954 + }, + "relaunchMs": { + "median": 2, + "min": 1, + "max": 5 + }, + "teardownMs": { + "median": 1232, + "min": 1069, + "max": 1662 + } + }, + "4": { + "layoutMs": { + "median": 591, + "min": 436, + "max": 1587 + }, + "workersMs": { + "median": 655, + "min": 544, + "max": 1587 + }, + "readyMs": { + "median": 659, + "min": 548, + "max": 1693 + }, + "attachMs": { + "median": 72, + "min": 35, + "max": 700 + }, + "closeDetectMs": { + "median": 34, + "min": 26, + "max": 70 + }, + "handoffMs": { + "median": 814, + "min": 699, + "max": 1169 + }, + "relaunchMs": { + "median": 2, + "min": 1, + "max": 2 + }, + "teardownMs": { + "median": 2000, + "min": 1830, + "max": 2409 + } + }, + "8": { + "layoutMs": { + "median": 1249, + "min": 805, + "max": 2634 + }, + "workersMs": { + "median": 1249, + "min": 968, + "max": 2634 + }, + "readyMs": { + "median": 1299, + "min": 984, + "max": 2654 + }, + "attachMs": { + "median": 126, + "min": 78, + "max": 669 + }, + "closeDetectMs": { + "median": 68, + "min": 29, + "max": 273 + }, + "handoffMs": { + "median": 1500, + "min": 1227, + "max": 2106 + }, + "relaunchMs": { + "median": 2, + "min": 1, + "max": 13 + }, + "teardownMs": { + "median": 4405, + "min": 4105, + "max": 5068 + } + } + } + }, + "notes": [], + "durationMs": 282203 + } + ] +} diff --git a/plans/tmux-pane-workers-proof.md b/plans/tmux-pane-workers-proof.md new file mode 100644 index 00000000..0e058599 --- /dev/null +++ b/plans/tmux-pane-workers-proof.md @@ -0,0 +1,267 @@ +# Persistent tmux pane workers for `` — proof report (#726) + +**Decision recommended for #717: adopt the persistent pane-worker topology, +with the lifecycle contract narrowed as stated under _What teardown can and +cannot prove_.** Readiness, pane display, sequential reuse, job control, +reader-close detection and ordered teardown all hold; complete teardown is +provable for everything except a descendant that has left the pane's session +_and_ closed the pane's terminal _and_ outlived its parent, which no parent +process can name without operating-system containment. + +## The run + +| | | +|---|---| +| evidence commit | `650510b5` (this branch, `spike/tmux-pane-workers`, base `a7f60c02` on `main`) | +| host | macOS `darwin 25.5.0`, `arm64` | +| tmux | 3.6a | +| Deno | 2.9.5 (stable, release, aarch64-apple-darwin) | +| command | `deno task proof:tmux-pane-workers --out ` from a prepared checkout | +| result | 9/9 checks, 127 claims, `plans/tmux-pane-workers-evidence.json` (IPC tokens redacted; the pane ids, tty names, pids and socket paths in it belong to that one run and to nothing durable) | + +The proof is `scripts/proofs/tmux-pane-workers/`. It ships nothing in the +binary. Run it unattended (it starts a throwaway outer tmux session of its own +so the visible attachment has a terminal), or run `deno task +proof:tmux-pane-workers -- --attach` to watch the journey on your own terminal +and close the grid yourself. `--only ` runs one check; `--runs N` sets +the measurement runs per pane count. + +## The topology, as proven + +``` +xmd (parent) private dir, mode 0700, short path + ├─ pane sockets: one Unix socket + one 0600 token file per pane + ├─ tmux server (-S /s -f /dev/null), hidden until attach + │ └─ window: explicit row-major layout from `columns` + │ └─ pane N: worker.ts N ← session leader on the pane pty + │ └─ interactive child ← inherits the pty, same pgrp + ├─ control client (tmux -C attach -f no-output) %client-detached / %exit + └─ visible client (tmux attach, stdio inherited) the reader's view +``` + +Each pane's initial process is a persistent worker that tmux starts and that +owns the pane's terminal until shutdown. The worker connects to its pane's +socket, proves which pane it is with the token it read and removed, and then +serves: `display` (write bytes to the pane), `launch` (start one child that +inherits the terminal), `cancel`, `shutdown`. It never reads the terminal. +Command vectors, working directories and environments travel only over that +socket; tmux's command parser sees `deno run --allow-all worker.ts +` and nothing else. + +Observed relationships (journey check, `hellos` and child evidence files): + +- every worker: `pid == pgid`, `ppid == tmux server`, tty == `#{pane_tty}` + for its pane, stdin/stdout/stderr all terminals; +- every interactive child: same tty as its worker, `pgid == worker pid`, + all three streams terminals; +- the default shell (`/bin/zsh`): moved itself into a process group of its own + and took the foreground (`tpgid == shell pgid`), put `sleep 300 &` in yet + another group, `fg` made that group the terminal's foreground group, `^Z` + suspended it — ordinary job control, observed through `ps -o tpgid`, not + inferred from what the shell printed. + +## Acceptance items + +| acceptance item | check | result | how it was observed | +|---|---|---|---| +| workers and children on the expected pane terminal; shell has job control | journey | holds | `isatty` ×3 and tty name vs `#{pane_tty}` for 4 workers and 5 children; `ps -o pgid,tpgid` before/after `sleep &`, `fg`, `^Z` | +| missing executable never acknowledges readiness; `exit 1` acknowledges then reports 1 | readiness-boundary | holds | `/definitely/missing` → `startup-failed`, no `ready` in the pane's event log; `--mode exit1` → `ready` then `exited {exitCode: 1}`, in that order; the pane and worker pid unchanged across both | +| argv bytes unchanged | journey | holds | `["a b", "\"quoted\"", "$HOME", "x;y", "`z`", "new\nline", "it's", "#{pane_id}"]` sent over IPC, read back byte-identical from the child's evidence file | +| pane text before and after a child, not as its input; child bytes never through the parent | journey | holds | prelude/epilogue `displayed` acks; child's recorded stdin holds only the typed lines; the control client received no `%output` line (it attaches `-f no-output`); the parent reads pane content only through `capture-pane`, as evidence | +| two sequential children in one pane; concurrent second refused; distinct panes concurrent | journey, sequential-handoff | holds | child A exits 3, epilogue, child A2 `ready` on the same `#{pane_id}` and worker pid; `A-dup` → `refused busy`; A and B typed into concurrently; the handoff regression below | +| 2×2 and 5-pane `columns={2}` row-major at different sizes; no `tiled` | layout-geometry | holds | 4@2, 5@2, 8@3 at 80×24 and 200×60; `list-panes` geometry checked pairwise (below / right-of); the last short row spans its width; `tiled` recorded beside each for contrast | +| attach only after every pane is ready; startup failure exposes no grid and tears everything down | journey, startup-failure-atomic | holds | attach issued after all four `ready`; with pane 2 launching a missing executable, no attach, and the three started children, four workers and the server are all unreachable afterwards | +| detach ≠ control loss ≠ server stop; none ends pane work | signals-distinct | holds | `%client-detached ` names the visible client, children keep running; detaching the control client ends its stream with `%exit` while `has-session` still answers and workers stay connected; `kill-server` closes every worker link and SIGHUPs workers and children | +| reader close and parent cancellation: stop launches, cancel children, await quiescence, stop the server, remove private paths, restore the terminal | journey, cancellation-points | holds | ordered teardown; every pid unreachable; `stty -g` identical before and after; halts at prepared / workers / ready / attached / active each leave server, workers, children gone and the private directory removed | +| negative children: ignore the interrupt and fork; escape the group | negative-children | holds, with a recorded limit | see _What teardown can and cannot prove_ | +| timings for 2, 4, 8 panes over 20 runs | measurements | measured | table below | +| cancellation at preparation, readiness, attachment, active child; one named scope and finalizer per resource | cancellation-points | holds | the ownership diagram below is the code's resource structure | + +## What teardown can and cannot prove + +A child's **settlement** is two sweeps in order, run by its worker after every +exit — natural, cancelled or at shutdown — and `exited` is reported only after +both, because `exited` is what frees the pane. First the interactive-process +resource escalates SIGINT → 2 s → SIGKILL on the child, then reaches what the +child left behind from a snapshot taken _before_ the first signal: the child's +descendants by parent links, plus every member of the pane's process group +other than the worker. Then the worker lists every process still holding the +pane's terminal (`lsof -t /dev/ttysN`) and kills it. Outcomes, with ground +truth from the children's own records of the pids they forked: + +| descendant | found by | stopped | +|---|---|---| +| in the inherited process group, parent ignoring SIGINT (`sh -c "trap '' INT; exec sleep 600"`) | ancestry and group snapshot | yes (`method: killed`) | +| `setsid()` away, terminal still open, parent alive at cancel | ancestry snapshot | yes | +| `setsid()` away, terminal closed, parent alive at cancel | ancestry snapshot | yes | +| `setsid()` away, terminal still open, **parent already exited** (reparented to launchd) | the parent's settlement terminal sweep, before `exited` | yes | +| `setsid()` away, terminal closed, **parent already exited** | nothing | **no** — recorded, then killed by the check from the child's own record | + +Two facts fix where each sweep has to live: + +- once the worker exits, tmux marks the pane dead and closes the pty master, + and macOS revokes the slave; after that `lsof` names nobody. A provider-level + sweep before `kill-server` found nothing. The terminal sweep is the + worker's, while it still holds the pane open — at every settlement, so an + orphan left by one child never meets the next, and once more at shutdown; +- a descendant's parent link is gone the moment the parent exits, so the + ancestry snapshot must precede the first signal, and a child that exits on + its own is swept then, before `exited` is reported — `exited` is what makes + the pane free, and a sweep running beside a new child would reach that child + too (they share the group). + +The `sequential-handoff` regression is the case those facts protect: the first +child forks a descendant that `setsid()`s, keeps the pane terminal open and +outlives its parent; a second launch is sent the instant the parent is told +to exit. Observed: the launch is `refused busy` before `exited`; `exited` +arrives with the descendant absent from the ancestry snapshot but named and +gone in `terminalHolders`; the descendant is unreachable; a third launch is +admitted, and `lsof` then names only the worker and the new child on that +terminal. Removing the settlement sweep fails exactly those claims. + +So the contract #717 can carry is: **teardown proves that nothing remains in +any pane's process group, nothing is a descendant of any child that was alive +when teardown began, and nothing holds any pane's terminal.** A process that +has left the session, closed the terminal and lost its parent is outside every +fact a parent process can observe on this platform; the contract should say +that boundary rather than claim more. A PID, a timeout or the visible client +leaving is not treated as any of it. + +Cancellation during provider preparation has one unprovable window of its own: +between `tmux new-session` forking the server and that server listening, a +`kill-server` finds nothing to kill. The proof's "prepared" cancellation lands +after the first pane exists (the server is up), which is the earliest point a +halt can be proven complete; the window before it is recorded here rather than +tested. + +## Measurements + +Medians with (min–max) over 20 runs per pane count, milliseconds, on the host above. Each run is one complete lifecycle: hidden server and layout, workers connected, every child's `spawn` event, visible attach, `detach-client` issued and `%client-detached` observed, one sequential handoff on pane 0, then cancel, shutdown, `kill-server`, and every pid proven unreachable. + +| panes | server + layout | workers connected | all children ready | attach | reader-close detected | handoff | relaunch | teardown | +|---|---|---|---|---|---|---|---|---| +| 2 | 338 (248–1461) | 465 (361–1922) | 468 (364–1927) | 57 (30–287) | 35 (27–145) | 616 (559–954) | 2 (1–5) | 1232 (1069–1662) | +| 4 | 591 (436–1587) | 655 (544–1587) | 659 (548–1693) | 72 (35–700) | 34 (26–70) | 814 (699–1169) | 2 (1–2) | 2000 (1830–2409) | +| 8 | 1249 (805–2634) | 1249 (968–2634) | 1299 (984–2654) | 126 (78–669) | 68 (29–273) | 1500 (1227–2106) | 2 (1–13) | 4405 (4105–5068) | + +The first three columns are cumulative from the start of the run; the others are each measured from their own trigger. Startup is Deno starting one worker per pane (the child `spawn` event follows the workers by tens of milliseconds, because readiness is the spawn, not the child's own startup). + +**Handoff** is the sequential-reuse latency the settlement sweep introduces: from `exit 0` typed into pane 0's child to the worker's `exited`, which follows the escalation's process-table snapshot (~0.1 s) and the terminal-holder sweep — `lsof -t` costs ~0.4 s on this host and grows with the number of processes holding files, hence 0.6 s at 2 panes and 1.5 s at 8. **Relaunch**, from the next `launch` to its `ready`, is a couple of milliseconds: the pane is already free. Teardown is the same sweep once per pane, run concurrently and contending, plus the 500 ms settle window after SIGKILL. No pass threshold is proposed; these are the numbers. + +## Findings a Planner should not have to rediscover + +1. **tmux hands panes to layout leaves in window-list order and ignores the + pane ids written in a layout string.** Authored order is imposed afterwards + with `swap-pane`; the explicit layout string sets the cells. The first + attempt came out column-major. +2. **A missing executable is a live pane to tmux.** Multi-argument pane + commands run without a shell and leave `pane_dead_status=1`; a single + argument goes through `sh -c` and leaves 127. Both have a `pane_pid`. The + `spawn`/`error` events of `node:child_process` are the readiness boundary, + and `exited` is separate from it. +3. **Attach-client exit codes do not classify a close**: 0 after + `detach-client`, 0 after `kill-session`, 1 after `kill-server`. The + control-mode client does (`%client-detached `, `%sessions-changed`, + `%exit`, EOF), and `-f no-output` keeps pane bytes out of it. +4. **Effection's `main()` binds SIGINT to its own shutdown (exit 130).** A + pane worker, and any child that must survive `^C`, has to be started with + `run()`; the first journey run lost its worker to the first `^C`. +5. **The worker must ignore SIGINT, SIGQUIT and SIGTSTP with handlers**, since + it shares the pane's foreground process group with the child; handlers are + reset across `exec`, so the child still gets defaults. `detached: true` + would break job control and is not an option. +6. **Unix socket paths are limited to 104 bytes on macOS.** The private + directory lives directly under `$TMPDIR` (49 characters here). +7. **The tmux socket file outlives the server**; "gone" is the server pid + unreachable and `has-session` refusing, not the file's absence. +8. **The visible client must be asked to detach before it is signalled.** A + SIGKILLed `tmux attach` cannot restore the terminal; the attach resource + registers `detach-client` ahead of the process escalation, which took + attached-phase teardown from ~2.3 s to under 0.5 s. +9. **A parent that dies of SIGHUP orphans the hidden servers.** The proof turns + SIGHUP into SIGTERM so `main()` tears down; the same applies to `xmd run` + losing its terminal while a grid is up. +10. The default shell needs ~1.5 s to read its rc files; readiness is the + shell process, not its prompt. +11. **`lsof` is the cost of the terminal sweep**: ~0.4 s per call here, + scaling with the processes on the host, paid once per settlement and once + more per pane at shutdown. It is what a sequential handoff waits for; a + cheaper way to name a pty's holders would take that latency out. + +## Resource ownership + +``` +proof scope +└─ workspace (resource) + ├─ private directory ─────────── ensure: rm -rf + ├─ pane sockets (resource) ───── ensure: destroy connections, close servers + │ └─ admission task per connection (halted with the scope) + ├─ tmux grid (resource) ──────── ensure: kill-server, wait for pid + has-session + │ ├─ control client (exec in a spawned task; SIGTERM on halt) + │ └─ visible client (interactive-process resource) + │ ├─ ensure: detach-client, wait for the client to leave + │ └─ ensure: SIGINT → SIGKILL → descendant sweep + └─ reader task per pane (halted with the scope) + +worker (tmux pane process, own program) +└─ run() + └─ per launch: spawned task + └─ interactive-process resource ── ensure: SIGINT → SIGKILL → snapshot sweep + per settlement (exit, cancel, shutdown): escalation → terminal-holder sweep → `exited` + shutdown: settle → one more terminal-holder sweep → bye → exit +``` + +## The smallest interfaces the evidence supports + +```ts +// The pane worker protocol (over an invocation-private Unix socket). +type ToWorker = + | { type: "display"; seq: number; text: string } + | { type: "launch"; id: string; argv: string[]; cwd: string; env: Record } + | { type: "cancel"; id: string } + | { type: "shutdown" }; +type FromWorker = + | { type: "hello"; ordinal: number; token: string; pid: number; pgid: number; tty: string; isatty: [boolean, boolean, boolean] } + | { type: "displayed"; seq: number } + | { type: "ready"; id: string; pid: number } // the spawn event, nothing earlier + | { type: "startup-failed"; id: string; reason: string } // the error event; never after ready + | { type: "refused"; id: string; reason: "busy" } + | { type: "exited"; id: string; exitCode?: number; signal?: string; proof: QuiescenceProof } // after settlement + | { type: "quiescent"; id?: string; proof: QuiescenceProof } + | { type: "bye"; ttyHolders: { pid: number; gone: boolean }[] }; + +// The interactive child, derived from packages/runtime/launcher.ts. +interface InteractiveProcess { + ready: Operation>; // Ok(pid) on spawn, Err on error + exited: Operation<{ exitCode?: number; signal?: string }>; + stop(): Operation; // idempotent; also the scope's ensure +} +interface QuiescenceProof { + method: "exited" | "interrupted" | "killed"; + childGone: boolean; + descendants: { pid: number; inGroup: boolean; delivery: "delivered" | "absent" | "refused"; gone: boolean }[]; + survivors: number[]; + terminalHolders: { pid: number; gone: boolean }[]; // the worker's sweep, after the escalation +} + +// The provider seam core would own. +interface TerminalGridProvider { + prepare(layout: { columns: number; panes: number }): Operation; // hidden; workers connected + attach(grid: PreparedGrid): Operation; // after every pane is ready + close: ControlEvents; // client-detached | control-lost | server-stopped, kept distinct + stop(grid: PreparedGrid): Operation; // server pid gone, socket unreachable +} +``` + +Nothing tmux-specific crosses those boundaries: socket paths, session and +pane ids, client names and the server pid stay inside the provider, and appear +in this report's evidence only because a proof records them. + +## Decision for #717 + +Adopt the persistent pane-worker topology. The Planner can take the measured +lifecycle boundary above and the interfaces as the shape of the work. The +Architect should narrow the lifecycle contract's teardown claim to what the +table under _What teardown can and cannot prove_ supports — group, ancestry +at teardown start, and terminal holders — and state the SIGHUP and +`run()`-not-`main()` obligations for the worker and the host. diff --git a/scripts/proofs/tmux-pane-workers/checks.ts b/scripts/proofs/tmux-pane-workers/checks.ts new file mode 100644 index 00000000..e57312b2 --- /dev/null +++ b/scripts/proofs/tmux-pane-workers/checks.ts @@ -0,0 +1,1195 @@ +/** + * The checks, one per acceptance item of #726. Each runs a topology of its + * own and records what it observed; `proof.ts` sequences them. + */ + +import { execFile } from "node:child_process"; +import { join } from "node:path"; +import { readTextFile, exists } from "@effectionx/fs"; +import { all, scoped, sleep, spawn, suspend, until } from "effection"; +import type { Operation, Task } from "effection"; +import type { Check, Logger } from "./evidence.ts"; +import { placementMatches } from "./layout.ts"; +import { deliver, holdersOf, isReachable, processFacts, processTable } from "./processes.ts"; +import type { ProcessRow } from "./processes.ts"; +import { tmuxAt, useTmuxGrid } from "./provider.ts"; +import type { ControlEvent, TmuxGrid, VisibleClient } from "./provider.ts"; +import { + childCommand, + filteredEnvironment, + isLaunchEvent, + isType, + usePrivateDirectory, + useWorkspace, +} from "./workspace.ts"; +import type { PaneEvent } from "./workspace.ts"; + +export interface CheckContext { + evidenceDirectory: string; + log: Logger; + /** Whether this process has a terminal to attach the grid on. */ + attachable: boolean; + /** Wait for a person to detach instead of issuing `detach-client`. */ + manualClose: boolean; +} + +interface ChildEvidenceFile { + argv: string[]; + pid: number; + pgid: number; + tty: string; + tpgid: number; + isatty: boolean[]; + stdin: string[]; + signals: string[]; + descendants: { pid: number; kind: string }[]; +} + +function* readChildEvidence(path: string): Operation { + if (!(yield* exists(path))) { + return undefined; + } + try { + return JSON.parse(yield* readTextFile(path)); + } catch { + return undefined; + } +} + +function* eventually(condition: () => Operation, limitMs: number): Operation { + const deadline = Date.now() + limitMs; + while (Date.now() < deadline) { + if (yield* condition()) { + return true; + } + yield* sleep(50); + } + return yield* condition(); +} + +function* allGone(pids: number[], limitMs = 5_000): Operation { + return yield* eventually(function* () { + return pids.every((pid) => !isReachable(pid)); + }, limitMs); +} + +function* childEvidenceHas( + path: string, + test: (file: ChildEvidenceFile) => boolean, +): Operation { + return yield* eventually(function* () { + const file = yield* readChildEvidence(path); + return file !== undefined && test(file); + }, 10_000); +} + +/** The controlling terminal's settings, or `undefined` without one. */ +function* sttyState(): Operation { + return yield* until( + new Promise((resolve) => { + execFile("sh", ["-c", "stty -g < /dev/tty"], (error, stdout) => { + resolve(error ? undefined : stdout.trim()); + }); + }), + ); +} + +const TTY_DEVICE = (tty: string) => (tty.startsWith("/dev/") ? tty : `/dev/${tty}`); + +/** + * Control events from `from` onwards until one satisfies `test` or time runs + * out. Returns the events seen and where the next read starts. + */ +function* controlUntil( + grid: TmuxGrid, + from: number, + test: (event: ControlEvent) => boolean, + limitMs = 5_000, +): Operation<{ seen: ControlEvent[]; next: number }> { + const deadline = Date.now() + limitMs; + let cursor = from; + const seen: ControlEvent[] = []; + while (true) { + while (cursor < grid.events.length) { + const event = grid.events[cursor++]; + seen.push(event); + if (test(event) || event.kind === "closed") { + return { seen, next: cursor }; + } + } + if (Date.now() >= deadline) { + return { seen, next: cursor }; + } + yield* sleep(10); + } +} + +export function* checkLayoutGeometry(check: Check, context: CheckContext): Operation { + const env = filteredEnvironment(); + const shapes = [ + { columns: 2, panes: 4 }, + { columns: 2, panes: 5 }, + { columns: 3, panes: 8 }, + ]; + const sizes = [ + { width: 80, height: 24 }, + { width: 200, height: 60 }, + ]; + const observations: Record = {}; + for (const shape of shapes) { + for (const size of sizes) { + const directory = yield* usePrivateDirectory(); + const grid = yield* useTmuxGrid(directory, { + session: "layout", + columns: shape.columns, + panes: shape.panes, + width: size.width, + height: size.height, + titles: [], + workerCommand: () => ["sleep", "300"], + cwd: "/", + env, + }); + const cells = yield* grid.geometry(); + const key = `${shape.panes}@${shape.columns} ${size.width}x${size.height}`; + const problems = placementMatches(cells, shape.columns); + const rows = new Set(cells.map((cell) => cell.top)).size; + observations[key] = { cells, problems }; + check.expect(`${key}: row-major placement`, problems.length === 0, problems); + check.expect( + `${key}: ${Math.ceil(shape.panes / shape.columns)} rows`, + rows === Math.ceil(shape.panes / shape.columns), + rows, + ); + // What `select-layout tiled` would have done with the same panes. + yield* grid.tmux.run(["select-layout", "-t", "layout:0", "tiled"]); + const tiled = yield* grid.geometry(); + const tiledColumns = new Set( + tiled.filter((cell) => cell.top === tiled[0].top).map((cell) => cell.left), + ).size; + observations[`${key} tiled`] = { + columns: tiledColumns, + problems: placementMatches(tiled, shape.columns), + }; + yield* grid.stop(); + } + } + check.fact("observations", observations); + check.note( + "tiled column counts are recorded beside each shape; they are tmux's choice, not the author's", + ); + yield* context.log("layout shapes recorded"); +} + +export function* checkReadinessBoundary(check: Check, context: CheckContext): Operation { + const env = filteredEnvironment(); + // First, tmux by itself: both a missing executable and a real `exit 1` + // produce a pane with a pid. + { + const directory = yield* usePrivateDirectory(); + const tmux = tmuxAt(join(directory, "s"), env); + yield* tmux.run(["new-session", "-d", "-s", "bare", "-x", "80", "-y", "24", "sleep", "60"]); + yield* tmux.run(["set", "-g", "remain-on-exit", "on"]); + yield* tmux.run(["split-window", "-d", "-t", "bare:0", "/definitely/missing", "x"]); + yield* tmux.run(["split-window", "-d", "-t", "bare:0", "/bin/sh", "-c", "exit 1"]); + yield* sleep(300); + const listed = yield* tmux.run([ + "list-panes", + "-t", + "bare:0", + "-F", + "#{pane_index} pid=#{pane_pid} dead=#{pane_dead} status=#{pane_dead_status} cmd=#{pane_start_command}", + ]); + check.fact("tmuxAlone", listed.split("\n")); + const missing = listed.split("\n").find((line) => line.includes("missing")); + check.expect( + "tmux alone: a missing executable still yields a pane pid", + missing !== undefined && /pid=\d+/.test(missing) && !/pid=0\b/.test(missing), + missing, + ); + yield* tmux.tryRun(["kill-server"]); + } + + const workspace = yield* useWorkspace({ + columns: 1, + panes: 1, + evidenceDirectory: context.evidenceDirectory, + titles: ["readiness"], + }); + const before = workspace.pane(0); + yield* workspace.launch(0, { id: "missing", argv: ["/definitely/missing", "x"] }); + const failed = yield* workspace.waitFor(0, isLaunchEvent("startup-failed", "missing")); + check.expect("missing executable: startup-failed", failed.type === "startup-failed", failed); + check.expect( + "missing executable: never ready", + !workspace.events(0).some((event) => event.type === "ready"), + ); + + const evidence = join(context.evidenceDirectory, "exit1.json"); + yield* workspace.launch(0, { id: "exit1", argv: childCommand(evidence, "exit1") }); + const ready = yield* workspace.waitFor(0, isLaunchEvent("ready", "exit1")); + const exited = yield* workspace.waitFor(0, isLaunchEvent("exited", "exit1")); + check.expect("exit 1: ready acknowledged", ready.type === "ready", ready); + check.expect("exit 1: then exit code 1", exited.exitCode === 1, exited); + const order = workspace.events(0).map((event) => event.type); + check.expect( + "exit 1: ready precedes exited", + order.indexOf("ready") < order.indexOf("exited"), + order, + ); + + const after = (yield* workspace.grid.geometry()).length; + const facts = yield* workspace.grid.tmux.run([ + "list-panes", + "-t", + "grid:0", + "-F", + "#{pane_id} #{pane_pid} #{pane_dead}", + ]); + check.expect( + "the pane and its worker survived both launches", + facts === `${before.id} ${before.pid} 0` && after === 1, + facts, + ); + yield* workspace.shutdown(0); + const stopped = yield* workspace.grid.stop(); + check.expect("server stopped", stopped.serverGone && stopped.unreachable, stopped); +} + +const TRICKY_ARGS = ["a b", '"quoted"', "$HOME", "x;y", "`z`", "new\nline", "it's", "#{pane_id}"]; + +export function* checkJourney(check: Check, context: CheckContext): Operation { + const sttyBefore = yield* sttyState(); + const evidenceOf = (name: string) => join(context.evidenceDirectory, `journey-${name}.json`); + const workspace = yield* useWorkspace({ + columns: 2, + panes: 4, + titles: ["Implementor", "Planner", "Architect", "Shell"], + evidenceDirectory: context.evidenceDirectory, + }); + const { grid } = workspace; + + for (const [ordinal, link] of workspace.links.entries()) { + const pane = workspace.pane(ordinal); + check.expect( + `pane ${ordinal}: worker on the pane terminal`, + TTY_DEVICE(link.hello.tty) === pane.tty && + link.hello.pid === pane.pid && + link.hello.pgid === link.hello.pid, + { hello: link.hello, pane }, + ); + check.expect( + `pane ${ordinal}: worker stdin/stdout/stderr are terminals`, + link.hello.isatty.every(Boolean), + ); + } + check.fact("panes", grid.panes); + check.fact( + "hellos", + workspace.links.map((link) => link.hello), + ); + + yield* workspace.display(0, "Prelude: this pane belongs to the Implementor.\n"); + yield* workspace.display(1, "Prelude: this pane belongs to the Planner.\n"); + check.expect("prelude displayed before any child", true); + + yield* workspace.launch(0, { + id: "A", + argv: childCommand(evidenceOf("A"), "plain", ...TRICKY_ARGS), + }); + yield* workspace.launch(1, { id: "B", argv: childCommand(evidenceOf("B"), "plain", "planner") }); + yield* workspace.launch(2, { + id: "C", + argv: childCommand(evidenceOf("C"), "ignore-sigint-fork"), + }); + yield* workspace.launch(3, { id: "S", argv: [workspace.env.SHELL ?? "/bin/sh"] }); + const readies = yield* all([ + workspace.waitFor(0, isLaunchEvent("ready", "A")), + workspace.waitFor(1, isLaunchEvent("ready", "B")), + workspace.waitFor(2, isLaunchEvent("ready", "C")), + workspace.waitFor(3, isLaunchEvent("ready", "S")), + ]); + check.expect( + "all four panes ready before attach", + readies.every((event) => event.type === "ready"), + ); + const childPids = readies.map((event) => event.pid); + + let client: VisibleClient | undefined; + let cursor = 0; + if (context.attachable) { + client = yield* grid.attach(); + const attached = yield* controlUntil(grid, cursor, (event) => event.kind === "client-attached"); + cursor = attached.next; + check.expect( + "visible client attached after readiness", + attached.seen.some((event) => event.kind === "client-attached"), + attached.seen, + ); + check.fact("visibleClient", client.name); + } else { + check.note("no terminal: the visible attach was skipped"); + } + + // Interact with two children at once. + yield* workspace.keys(0, "hello from zero", "Enter"); + yield* workspace.keys(1, "hello from one", "Enter"); + const aSaw = yield* childEvidenceHas(evidenceOf("A"), (file) => + file.stdin.includes("hello from zero"), + ); + const bSaw = yield* childEvidenceHas(evidenceOf("B"), (file) => + file.stdin.includes("hello from one"), + ); + check.expect("two children received input concurrently", aSaw && bSaw); + const aFile = yield* readChildEvidence(evidenceOf("A")); + check.expect( + "argv bytes unchanged through IPC", + JSON.stringify(aFile?.argv) === JSON.stringify(TRICKY_ARGS), + aFile?.argv, + ); + check.expect( + "child A on pane 0's terminal, in the worker's process group", + aFile !== undefined && + TTY_DEVICE(aFile.tty) === workspace.pane(0).tty && + aFile.pgid === workspace.links[0].hello.pid && + aFile.isatty.every(Boolean), + aFile && { tty: aFile.tty, pgid: aFile.pgid, isatty: aFile.isatty }, + ); + check.expect( + "prelude text was not fed to the child as input", + aFile !== undefined && !aFile.stdin.some((line) => line.includes("Prelude")), + aFile?.stdin, + ); + const captured = yield* workspace.capture(0); + check.expect( + "pane 0 shows prelude, banner and echo", + captured.includes("Prelude") && captured.includes("> hello from zero"), + captured, + ); + + yield* workspace.launch(0, { id: "A-dup", argv: ["true"] }); + const refused = yield* workspace.waitFor(0, isLaunchEvent("refused", "A-dup")); + check.expect( + "a second concurrent launch on pane 0 is refused", + refused.reason === "busy", + refused, + ); + + // Job control in the shell pane. The shell reads its rc files first, so + // each observation waits for the shell rather than for a fixed delay. + yield* workspace.keys(3, "sleep 300 &", "Enter"); + yield* workspace.keys(3, "jobs", "Enter"); + const shellPid = childPids[3]; + let sleeper: ProcessRow | undefined; + let shellRow: ProcessRow | undefined; + yield* eventually(function* () { + const table = yield* processTable(); + sleeper = table.find((row) => row.ppid === shellPid && row.command.startsWith("sleep 300")); + shellRow = table.find((row) => row.pid === shellPid); + return sleeper !== undefined; + }, 10_000); + const workerRow = yield* processFacts(workspace.links[3].hello.pid); + check.expect( + "shell took the foreground in a process group of its own", + shellRow !== undefined && + workerRow !== undefined && + shellRow.pgid === shellRow.pid && + shellRow.pgid !== workerRow.pgid, + { shellRow, workerRow }, + ); + check.expect( + "shell put its background job in a process group of its own", + sleeper !== undefined && + shellRow !== undefined && + sleeper.pgid !== shellRow.pgid && + sleeper.pgid === sleeper.pid, + { sleeper, shellRow }, + ); + yield* workspace.keys(3, "fg", "Enter"); + let foreground: ProcessRow | undefined; + yield* eventually(function* () { + foreground = yield* processFacts(sleeper?.pid ?? -1); + return foreground !== undefined && foreground.tpgid === foreground.pgid; + }, 5_000); + check.expect( + "fg made the job the terminal's foreground process group", + foreground !== undefined && foreground.tpgid === foreground.pgid, + foreground, + ); + yield* workspace.keys(3, "C-z"); + let stoppedShell = ""; + yield* eventually(function* () { + stoppedShell = yield* workspace.capture(3); + return /suspended|stopped/i.test(stoppedShell); + }, 5_000); + yield* workspace.keys(3, "kill %1", "Enter"); + check.expect( + "^Z suspended the foreground job", + /suspended|stopped/i.test(stoppedShell), + stoppedShell.trim().split("\n").slice(-3), + ); + + // ^C reaches the child on pane 1, not its worker. + yield* workspace.keys(1, "C-c"); + const bExit = yield* workspace.waitFor(1, isLaunchEvent("exited", "B")); + check.expect( + "^C interrupted child B", + bExit.exitCode === 130 || bExit.signal === "SIGINT", + bExit, + ); + yield* workspace.display(1, "Child B was interrupted; the pane worker is still here.\n"); + check.expect("worker 1 survived the ^C that ended its child", workspace.links[1].connected()); + + // One child exits while siblings remain interactive; its pane is reused. + yield* workspace.keys(0, "exit 3", "Enter"); + const aExit = yield* workspace.waitFor(0, isLaunchEvent("exited", "A")); + check.expect("child A exited 3 on request", aExit.exitCode === 3, aExit); + check.expect("child C still runs while A exited", isReachable(childPids[2])); + yield* workspace.display( + 0, + `Epilogue: the Implementor exited with status ${aExit.exitCode}. Starting a second child.\n`, + ); + yield* workspace.launch(0, { id: "A2", argv: childCommand(evidenceOf("A2"), "plain", "second") }); + const a2 = yield* workspace.waitFor(0, isLaunchEvent("ready", "A2")); + const paneNow = (yield* grid.tmux.run([ + "list-panes", + "-t", + "grid:0", + "-F", + "#{pane_id} #{pane_pid}", + ])).split("\n")[0]; + check.expect( + "second child in pane 0 on the same pane and worker", + a2.type === "ready" && paneNow === `${workspace.pane(0).id} ${workspace.pane(0).pid}`, + { a2, paneNow }, + ); + yield* workspace.keys(0, "second round", "Enter"); + check.expect( + "second child received input", + yield* childEvidenceHas(evidenceOf("A2"), (file) => file.stdin.includes("second round")), + ); + + // Reader close. + let closeDetected = false; + if (client) { + if (context.manualClose) { + yield* workspace.display( + 1, + "\nScripted interactions are done. Detach (prefix, d) to close the grid.\n", + ); + yield* client.process.exited; + } + const closeAt = Date.now(); + if (!context.manualClose) { + yield* grid.detach(client); + } + const { seen, next } = yield* controlUntil( + grid, + cursor, + (event) => event.kind === "client-detached", + ); + cursor = next; + closeDetected = seen.some((event) => event.kind === "client-detached"); + check.fact("closeDetectMs", Date.now() - closeAt); + const exit = yield* client.process.exited; + check.expect("reader close observed as %client-detached", closeDetected, seen); + check.expect("attach client exited 0 after detach", exit.exitCode === 0, exit); + } + check.expect( + "after reader close, children still run until cancelled", + isReachable(childPids[2]) && isReachable(a2.pid), + ); + + // Ordered teardown. + const proofs = yield* all([ + workspace.cancel(0, "A2"), + workspace.cancel(2, "C"), + workspace.cancel(3, "S"), + ]); + check.fact( + "quiescence", + proofs.map((proof) => proof.proof), + ); + check.expect( + "every cancelled child is gone", + proofs.every((proof) => proof.proof.childGone && proof.proof.survivors.length === 0), + proofs.map((proof) => proof.proof), + ); + const cFile = yield* readChildEvidence(evidenceOf("C")); + const cDescendant = cFile?.descendants[0]?.pid; + check.expect( + "C ignored SIGINT and was killed, with its in-group descendant", + proofs[1].proof.method === "killed" && + cDescendant !== undefined && + proofs[1].proof.descendants.some((entry) => entry.pid === cDescendant && entry.gone), + { + method: proofs[1].proof.method, + cDescendant, + descendants: proofs[1].proof.descendants, + signals: cFile?.signals, + }, + ); + const byes = yield* all(workspace.links.map((_, ordinal) => workspace.shutdown(ordinal))); + check.expect( + "every worker acknowledged shutdown with nothing left on its terminal", + byes.length === 4 && byes.every((bye) => bye.ttyHolders.length === 0), + byes.map((bye) => bye.ttyHolders), + ); + const workerPids = workspace.links.map((link) => link.hello.pid); + check.expect("workers gone", yield* allGone(workerPids)); + const stopped = yield* grid.stop(); + check.expect("tmux server gone", stopped.serverGone && stopped.unreachable, stopped); + check.expect("all child pids gone", yield* allGone([...childPids, a2.pid])); + const holders: Record = {}; + for (const pane of grid.panes) { + holders[pane.tty] = yield* holdersOf(pane.tty); + } + check.expect( + "nothing holds a pane terminal open", + Object.values(holders).every((list) => list.length === 0), + holders, + ); + check.expect( + "control client never received pane output", + !grid.controlLog.some((line) => line.startsWith("%output")), + grid.controlLog.length, + ); + check.fact("controlLog", grid.controlLog); + const sttyAfter = yield* sttyState(); + check.expect("terminal settings restored", sttyBefore === sttyAfter, { sttyBefore, sttyAfter }); +} + +export function* checkStartupFailureAtomic(check: Check, context: CheckContext): Operation { + const evidence = (name: string) => join(context.evidenceDirectory, `atomic-${name}.json`); + let serverPid = -1; + let workerPids: number[] = []; + let childPids: number[] = []; + let attachAttempted = false; + let failure: string | undefined; + try { + yield* scoped(function* () { + const workspace = yield* useWorkspace({ + columns: 2, + panes: 4, + evidenceDirectory: context.evidenceDirectory, + onPhase: (_, facts) => { + serverPid = facts.serverPid ?? serverPid; + }, + }); + workerPids = workspace.links.map((link) => link.hello.pid); + yield* workspace.launch(0, { id: "a", argv: childCommand(evidence("a"), "plain") }); + yield* workspace.launch(1, { id: "b", argv: childCommand(evidence("b"), "plain") }); + yield* workspace.launch(2, { id: "c", argv: ["/definitely/missing", "x"] }); + yield* workspace.launch(3, { id: "s", argv: [workspace.env.SHELL ?? "/bin/sh"] }); + const outcomes = yield* all( + [0, 1, 2, 3].map((ordinal) => + workspace.waitFor( + ordinal, + (event): event is PaneEvent & { type: "ready" | "startup-failed" } => + event.type === "ready" || event.type === "startup-failed", + ), + ), + ); + childPids = outcomes.flatMap((event) => (event.type === "ready" ? [event.pid] : [])); + check.fact("outcomes", outcomes); + check.expect( + "pane 2 reported startup-failed", + outcomes[2].type === "startup-failed", + outcomes[2], + ); + check.expect("three siblings had already started", childPids.length === 3); + if (outcomes.some((event) => event.type === "startup-failed")) { + // The grid must not be presented; teardown is the scope ending. + throw new Error("grid startup failed: pane 2"); + } + attachAttempted = true; + yield* workspace.grid.attach(); + }); + } catch (error) { + failure = error instanceof Error ? error.message : String(error); + } + check.expect( + "the grid failed instead of attaching", + failure !== undefined && !attachAttempted, + failure, + ); + check.expect("started siblings torn down", yield* allGone(childPids), childPids); + check.expect("workers torn down", yield* allGone(workerPids), workerPids); + check.expect("server torn down", serverPid > 0 && (yield* allGone([serverPid])), serverPid); +} + +export function* checkSignalsDistinct(check: Check, context: CheckContext): Operation { + if (!context.attachable) { + check.note("no terminal: skipped"); + return; + } + const evidence = (name: string) => join(context.evidenceDirectory, `signals-${name}.json`); + const workspace = yield* useWorkspace({ + columns: 2, + panes: 2, + evidenceDirectory: context.evidenceDirectory, + }); + const { grid } = workspace; + yield* workspace.launch(0, { id: "a", argv: childCommand(evidence("a"), "plain") }); + yield* workspace.launch(1, { id: "b", argv: childCommand(evidence("b"), "plain") }); + const [a, b] = yield* all([ + workspace.waitFor(0, isLaunchEvent("ready", "a")), + workspace.waitFor(1, isLaunchEvent("ready", "b")), + ]); + const children = [a.pid, b.pid]; + + // 1. The reader detaches. + const first = yield* grid.attach(); + let cursor = (yield* controlUntil(grid, 0, (event) => event.kind === "client-attached")).next; + yield* grid.detach(first); + const detached = yield* controlUntil(grid, cursor, (event) => event.kind === "client-detached"); + cursor = detached.next; + yield* first.process.exited; + check.expect( + "detach: %client-detached names the visible client", + detached.seen.some((event) => event.kind === "client-detached" && event.client === first.name), + detached.seen, + ); + check.expect("detach: children keep running", children.every(isReachable)); + + // 2. The control connection is lost while the server and panes live on. + const controlName = (yield* grid.tmux.run([ + "list-clients", + "-F", + "#{client_control_mode} #{client_name}", + ])) + .split("\n") + .map((line) => line.split(" ")) + .find((parts) => parts[0] === "1")?.[1]; + check.fact("controlClient", controlName); + yield* grid.tmux.run(["detach-client", "-t", controlName ?? ""]); + const lost = (yield* controlUntil(grid, cursor, (event) => event.kind === "closed")).seen; + check.expect( + "control loss: the stream ends with %exit, not %client-detached for the reader", + lost.some((event) => event.kind === "exit") && + !lost.some((event) => event.kind === "client-detached" && event.client === first.name), + lost, + ); + check.expect( + "control loss: server still answers", + (yield* grid.tmux.tryRun(["has-session", "-t", grid.session])) !== undefined, + ); + check.expect("control loss: children keep running", children.every(isReachable)); + check.expect( + "control loss: workers still connected", + workspace.links.every((link) => link.connected()), + ); + + // 3. The server stops underneath everything. + yield* grid.tmux.run(["kill-server"]); + const closed = yield* all( + workspace.links.map((_, ordinal) => workspace.waitFor(ordinal, isType("closed"))), + ); + check.expect("server stop: every worker link closed", closed.length === 2); + const childrenGone = yield* allGone(children, 3_000); + check.expect( + "server stop: children ended with their terminal (SIGHUP)", + childrenGone, + children.map(isReachable), + ); + check.expect( + "server stop: workers ended with their terminal", + yield* allGone( + workspace.links.map((link) => link.hello.pid), + 3_000, + ), + ); + check.note( + "the three signals were classified from different sources: attach exit + %client-detached, control EOF/%exit, has-session failure + link EOF", + ); +} + +export function* checkNegativeChildren(check: Check, context: CheckContext): Operation { + const evidence = (name: string) => join(context.evidenceDirectory, `negative-${name}.json`); + const workspace = yield* useWorkspace({ + columns: 3, + panes: 5, + evidenceDirectory: context.evidenceDirectory, + }); + const modes = ["ignore-sigint-fork", "escape", "escape-closed"] as const; + for (const [ordinal, mode] of modes.entries()) { + yield* workspace.launch(ordinal, { id: mode, argv: childCommand(evidence(mode), mode) }); + } + const readies = yield* all( + modes.map((mode, ordinal) => workspace.waitFor(ordinal, isLaunchEvent("ready", mode))), + ); + const files: Record = {}; + for (const mode of modes) { + yield* childEvidenceHas(evidence(mode), (file) => file.descendants.length === 1); + files[mode] = yield* readChildEvidence(evidence(mode)); + } + + yield* workspace.keys(0, "C-c"); + const ignored = yield* childEvidenceHas(evidence("ignore-sigint-fork"), (file) => + file.signals.includes("SIGINT"), + ); + files["ignore-sigint-fork"] = yield* readChildEvidence(evidence("ignore-sigint-fork")); + check.fact("children", files); + check.expect( + "negative child and its in-group descendant survived the first interrupt", + ignored && + isReachable(readies[0].pid) && + isReachable(files["ignore-sigint-fork"]?.descendants[0]?.pid ?? -1), + ); + + const escapedRow = yield* processFacts(files.escape?.descendants[0]?.pid ?? -1); + check.expect( + "escaped descendant left the session and process group", + escapedRow !== undefined && escapedRow.pgid === escapedRow.pid && escapedRow.tty === "??", + escapedRow, + ); + + // The orphans: escaped descendants whose parent has already exited on its + // own, so no ancestry leads to them when the pane is swept. One still holds + // the pane's terminal; the other closed it. + const orphans = [ + { ordinal: 3, mode: "escape" }, + { ordinal: 4, mode: "escape-closed" }, + ] as const; + const orphanPids: number[] = []; + const orphanExits: (PaneEvent & { type: "exited" })[] = []; + for (const orphan of orphans) { + const id = `orphan-${orphan.mode}`; + yield* workspace.launch(orphan.ordinal, { id, argv: childCommand(evidence(id), orphan.mode) }); + yield* workspace.waitFor(orphan.ordinal, isLaunchEvent("ready", id)); + yield* childEvidenceHas(evidence(id), (file) => file.descendants.length === 1); + const file = yield* readChildEvidence(evidence(id)); + const pid = file?.descendants[0]?.pid ?? -1; + orphanPids.push(pid); + const before = yield* processFacts(pid); + check.expect( + `${id}: the descendant left the session and process group while its parent lived`, + before !== undefined && before.pgid === before.pid && before.tty === "??", + before, + ); + yield* workspace.keys(orphan.ordinal, "exit 0", "Enter"); + const exited = yield* workspace.waitFor(orphan.ordinal, isLaunchEvent("exited", id)); + orphanExits.push(exited); + const row = yield* processFacts(pid); + check.fact(`${id}`, { pid, before, afterParentExit: row, settlement: exited.proof }); + check.expect( + `${id}: outside the settlement's ancestry once the parent exited`, + !exited.proof.descendants.some((entry) => entry.pid === pid), + exited.proof.descendants, + ); + } + + const proofs = yield* all(modes.map((mode, ordinal) => workspace.cancel(ordinal, mode))); + for (const [index, mode] of modes.entries()) { + const proof = proofs[index].proof; + const descendant = files[mode]?.descendants[0]?.pid; + const covered = proof.descendants.find((entry) => entry.pid === descendant); + check.fact(`${mode}.proof`, proof); + check.expect( + `${mode}: child stopped (${proof.method})`, + proof.childGone && !isReachable(readies[index].pid), + ); + check.expect( + `${mode}: descendant ${descendant} was found in the pre-kill snapshot and stopped`, + covered !== undefined && covered.gone && descendant !== undefined && !isReachable(descendant), + covered, + ); + } + const byes = yield* all([0, 1, 2, 3, 4].map((ordinal) => workspace.shutdown(ordinal))); + check.expect( + "orphans: outside the pane sweep's ancestry once their parent exited", + orphanPids.every( + (pid) => !byes.some((bye) => bye.proof.descendants.some((entry) => entry.pid === pid)), + ), + byes.map((bye) => bye.proof), + ); + const stopped = yield* workspace.grid.stop(); + check.expect("server stopped", stopped.serverGone && stopped.unreachable); + check.fact( + "ttyHolders", + byes.map((bye) => bye.ttyHolders), + ); + const [holdingOrphan, closedOrphan] = orphanPids; + const foundHolding = orphanExits[0].proof.terminalHolders.find( + (entry) => entry.pid === holdingOrphan, + ); + check.expect( + "orphan holding the terminal: named by its parent's settlement sweep and stopped before `exited`", + foundHolding !== undefined && foundHolding.gone && !isReachable(holdingOrphan), + { holdingOrphan, foundHolding }, + ); + const closedRow = yield* processFacts(closedOrphan); + check.expect( + "orphan that closed the terminal: outlived its parent, reparented, still running", + closedRow !== undefined && closedRow.ppid === 1 && closedRow.tty === "??", + closedRow, + ); + const closedFound = + orphanExits[1].proof.terminalHolders.some((entry) => entry.pid === closedOrphan) || + byes.some((bye) => bye.ttyHolders.some((entry) => entry.pid === closedOrphan)); + const closedAlive = isReachable(closedOrphan); + check.fact("orphanClosed", { + pid: closedOrphan, + foundByAnySweep: closedFound, + stillRunning: closedAlive, + }); + check.expect( + "orphan that closed the terminal: recorded as unprovable by this topology", + !closedFound && closedAlive, + { closedFound, closedAlive }, + ); + if (closedAlive) { + deliver(closedOrphan, "SIGKILL"); + check.note( + `orphan ${closedOrphan} (escaped the group, lost its parent, closed the terminal) is invisible to ancestry, process-group and terminal-holder sweeps; the check killed it afterwards using the child's own record of its pid`, + ); + } + const holders: Record = {}; + for (const pane of workspace.grid.panes) { + holders[pane.tty] = yield* holdersOf(pane.tty); + } + check.expect( + "after the server stopped, `lsof` names no holder of any pane terminal", + Object.values(holders).every((list) => list.length === 0), + holders, + ); + check.note( + "once the worker exits, tmux closes the pane's pty master and macOS revokes the slave, so a holder can only be named by the worker before it leaves", + ); +} + +/** + * Regression: a first child forks a descendant that `setsid()`s, keeps the + * pane's terminal, and outlives its parent. The pane must not admit a second + * child until that descendant is stopped and nothing from the first child's + * lifetime still holds the terminal. + */ +export function* checkSequentialHandoff(check: Check, context: CheckContext): Operation { + const evidence = (name: string) => join(context.evidenceDirectory, `handoff-${name}.json`); + const workspace = yield* useWorkspace({ + columns: 1, + panes: 1, + evidenceDirectory: context.evidenceDirectory, + titles: ["handoff"], + }); + const pane = workspace.pane(0); + const worker = workspace.links[0].hello.pid; + + yield* workspace.launch(0, { id: "first", argv: childCommand(evidence("first"), "escape") }); + const first = yield* workspace.waitFor(0, isLaunchEvent("ready", "first")); + yield* childEvidenceHas(evidence("first"), (file) => file.descendants.length === 1); + const descendant = (yield* readChildEvidence(evidence("first")))?.descendants[0]?.pid ?? -1; + const escaped = yield* processFacts(descendant); + const holdersBefore = yield* holdersOf(pane.tty); + check.fact("first", { child: first.pid, descendant, escaped, holdersBefore }); + check.expect( + "the descendant left the session and process group and still holds the pane terminal", + escaped !== undefined && + escaped.pgid === escaped.pid && + escaped.tty === "??" && + holdersBefore.includes(descendant), + { escaped, holdersBefore }, + ); + + // The parent exits on its own; a second launch is sent before `exited` + // can possibly have arrived. + const tExit = Date.now(); + yield* workspace.keys(0, "exit 0", "Enter"); + yield* workspace.launch(0, { id: "early", argv: childCommand(evidence("early"), "plain") }); + const early = yield* workspace.waitFor( + 0, + (event): event is PaneEvent & { type: "refused" | "ready" } => + (event.type === "refused" || event.type === "ready") && event.id === "early", + ); + const exited = yield* workspace.waitFor(0, isLaunchEvent("exited", "first")); + const handoffMs = Date.now() - tExit; + const order = workspace.events(0).map((event) => event.type); + check.fact("exited", { exitCode: exited.exitCode, proof: exited.proof, handoffMs, order }); + check.expect( + "a launch sent while the first child was settling was refused, before `exited`", + early.type === "refused" && order.indexOf("refused") < order.indexOf("exited"), + { early, order }, + ); + const swept = exited.proof.terminalHolders.find((entry) => entry.pid === descendant); + check.expect( + "the orphaned descendant was outside ancestry but named by the settlement's terminal sweep", + !exited.proof.descendants.some((entry) => entry.pid === descendant) && swept !== undefined, + { descendants: exited.proof.descendants, terminalHolders: exited.proof.terminalHolders }, + ); + check.expect( + "the descendant was stopped before `exited` was reported", + swept?.gone === true && !isReachable(descendant), + { swept, reachable: isReachable(descendant) }, + ); + + const tRelaunch = Date.now(); + yield* workspace.launch(0, { id: "second", argv: childCommand(evidence("second"), "plain") }); + const second = yield* workspace.waitFor(0, isLaunchEvent("ready", "second")); + const relaunchMs = Date.now() - tRelaunch; + yield* childEvidenceHas(evidence("second"), (file) => file.pid === second.pid); + const holdersAfter = yield* holdersOf(pane.tty); + const strangers = holdersAfter.filter((pid) => pid !== worker && pid !== second.pid); + check.fact("second", { child: second.pid, holdersAfter, relaunchMs }); + check.expect( + "after admission, only the worker and the second child hold the pane terminal", + strangers.length === 0 && holdersAfter.includes(second.pid), + { holdersAfter, worker, second: second.pid }, + ); + check.expect( + "the second child runs on the same pane and worker", + (yield* workspace.grid.tmux.run([ + "list-panes", + "-t", + "grid:0", + "-F", + "#{pane_id} #{pane_pid}", + ])) === `${pane.id} ${pane.pid}`, + ); + + yield* workspace.keys(0, "exit 0", "Enter"); + yield* workspace.waitFor(0, isLaunchEvent("exited", "second")); + const bye = yield* workspace.shutdown(0); + check.expect( + "nothing held the terminal at shutdown", + bye.ttyHolders.length === 0, + bye.ttyHolders, + ); + const stopped = yield* workspace.grid.stop(); + check.expect("server stopped", stopped.serverGone && stopped.unreachable); + check.expect( + "first child, descendant, second child gone", + yield* allGone([first.pid, descendant, second.pid]), + ); + check.note( + `handoff (exit requested → exited) ${handoffMs} ms; relaunch (launch → ready) ${relaunchMs} ms`, + ); +} + +export function* checkCancellationPoints(check: Check, context: CheckContext): Operation { + const phases = ["prepared", "workers", "ready", "attached", "active"] as const; + for (const phase of phases) { + if ((phase === "attached" || phase === "active") && !context.attachable) { + check.note(`${phase}: no terminal, skipped`); + continue; + } + let serverPid = -1; + let directory = ""; + const workerPids: number[] = []; + const childPids: number[] = []; + let reached = false; + let taskError: string | undefined; + const task: Task = yield* spawn(function* () { + // A failure inside the task must not escape: it is recorded, and the + // task holds its resources until the check halts it. + try { + yield* steps(); + } catch (error) { + taskError = error instanceof Error ? error.message : String(error); + yield* suspend(); + } + }); + function* steps(): Operation { + const workspace = yield* useWorkspace({ + columns: 2, + panes: 2, + evidenceDirectory: context.evidenceDirectory, + onPhase: (current, facts) => { + serverPid = facts.serverPid ?? serverPid; + directory = facts.directory; + if (current === phase) { + reached = true; + } + }, + }); + directory = workspace.directory; + workerPids.push(...workspace.links.map((link) => link.hello.pid)); + const evidence = (name: string) => + join(context.evidenceDirectory, `cancel-${phase}-${name}.json`); + yield* workspace.launch(0, { id: "a", argv: childCommand(evidence("a"), "plain") }); + yield* workspace.launch(1, { + id: "b", + argv: childCommand(evidence("b"), "ignore-sigint-fork"), + }); + const readies = yield* all([ + workspace.waitFor(0, isLaunchEvent("ready", "a")), + workspace.waitFor(1, isLaunchEvent("ready", "b")), + ]); + childPids.push(...readies.map((event) => event.pid)); + if (phase === "ready") { + reached = true; + } + const client = yield* workspace.grid.attach(); + yield* controlUntil(workspace.grid, 0, (event) => event.kind === "client-attached"); + if (phase === "attached") { + reached = true; + } + yield* workspace.keys(0, "typing", "Enter"); + yield* childEvidenceHas(evidence("a"), (file) => file.stdin.includes("typing")); + void client; + reached = true; + yield* suspend(); + } + // Halt from outside the task, once it reports the phase. + yield* eventually(function* () { + return reached; + }, 30_000); + const haltedAt = Date.now(); + yield* task.halt(); + const teardownMs = Date.now() - haltedAt; + check.fact(`${phase}`, { serverPid, workerPids, childPids, teardownMs }); + check.expect(`${phase}: phase reached`, reached, taskError); + check.expect(`${phase}: server gone`, serverPid > 0 && (yield* allGone([serverPid]))); + check.expect(`${phase}: workers gone`, yield* allGone(workerPids)); + check.expect(`${phase}: children gone`, yield* allGone(childPids)); + check.expect( + `${phase}: private directory removed`, + directory !== "" && !(yield* exists(directory)), + ); + } +} + +export interface MeasuredRun { + panes: number; + layoutMs: number; + workersMs: number; + readyMs: number; + attachMs: number; + closeDetectMs: number; + /** Exit requested on pane 0 → `exited`, including the settlement sweep. */ + handoffMs: number; + /** `exited` → the next child on the same pane ready. */ + relaunchMs: number; + teardownMs: number; +} + +export function* measureOnce(panes: number, context: CheckContext): Operation { + const t0 = Date.now(); + let layoutMs = 0; + let workersMs = 0; + const workspace = yield* useWorkspace({ + columns: 2, + panes, + evidenceDirectory: context.evidenceDirectory, + onPhase: (phase) => { + if (phase === "prepared") { + layoutMs = Date.now() - t0; + } + if (phase === "workers") { + workersMs = Date.now() - t0; + } + }, + }); + for (let ordinal = 0; ordinal < panes; ordinal++) { + yield* workspace.launch(ordinal, { + id: `m${ordinal}`, + argv: childCommand( + join(context.evidenceDirectory, `measure-${panes}-${ordinal}.json`), + "plain", + ), + }); + } + const readies = yield* all( + Array.from({ length: panes }, (_, ordinal) => + workspace.waitFor(ordinal, isLaunchEvent("ready", `m${ordinal}`)), + ), + ); + const readyMs = Date.now() - t0; + const tAttach = Date.now(); + const client = yield* workspace.grid.attach(); + const cursor = (yield* controlUntil( + workspace.grid, + 0, + (event) => event.kind === "client-attached", + )).next; + const attachMs = Date.now() - tAttach; + const tClose = Date.now(); + yield* workspace.grid.detach(client); + yield* controlUntil(workspace.grid, cursor, (event) => event.kind === "client-detached"); + yield* client.process.exited; + const closeDetectMs = Date.now() - tClose; + // Sequential handoff on pane 0: exit requested → `exited` (which follows the + // settlement sweep) → a second child ready on the same pane. + const tHandoff = Date.now(); + yield* workspace.keys(0, "exit 0", "Enter"); + yield* workspace.waitFor(0, isLaunchEvent("exited", "m0")); + const handoffMs = Date.now() - tHandoff; + const tRelaunch = Date.now(); + yield* workspace.launch(0, { + id: "m0b", + argv: childCommand(join(context.evidenceDirectory, `measure-${panes}-0b.json`), "plain"), + }); + const second = yield* workspace.waitFor(0, isLaunchEvent("ready", "m0b")); + const relaunchMs = Date.now() - tRelaunch; + const tTeardown = Date.now(); + yield* all( + readies.map((_, ordinal) => workspace.cancel(ordinal, ordinal === 0 ? "m0b" : `m${ordinal}`)), + ); + yield* all(readies.map((_, ordinal) => workspace.shutdown(ordinal))); + yield* workspace.grid.stop(); + const gone = yield* allGone([ + ...readies.map((event) => event.pid), + second.pid, + ...workspace.links.map((link) => link.hello.pid), + ]); + if (!gone) { + throw new Error(`measurement with ${panes} panes: a process survived teardown`); + } + const teardownMs = Date.now() - tTeardown; + return { + panes, + layoutMs, + workersMs, + readyMs, + attachMs, + closeDetectMs, + handoffMs, + relaunchMs, + teardownMs, + }; +} + +export function* checkMeasurements( + check: Check, + context: CheckContext, + runs: number, +): Operation { + if (!context.attachable) { + check.note("no terminal: skipped"); + return; + } + const results: MeasuredRun[] = []; + for (const panes of [2, 4, 8]) { + for (let run = 0; run < runs; run++) { + results.push(yield* measureOnce(panes, context)); + } + yield* context.log(`measured ${panes} panes × ${runs}`); + } + check.fact("runs", results); + const summary: Record> = {}; + for (const panes of [2, 4, 8]) { + const mine = results.filter((run) => run.panes === panes); + summary[String(panes)] = {}; + for (const key of [ + "layoutMs", + "workersMs", + "readyMs", + "attachMs", + "closeDetectMs", + "handoffMs", + "relaunchMs", + "teardownMs", + ] as const) { + const values = mine.map((run) => run[key]).toSorted((a, b) => a - b); + summary[String(panes)][key] = { + median: values[Math.floor(values.length / 2)], + min: values[0], + max: values[values.length - 1], + }; + } + } + check.fact("summary", summary); + check.expect( + `${results.length} runs completed with complete teardown`, + results.length === runs * 3, + ); +} diff --git a/scripts/proofs/tmux-pane-workers/child.ts b/scripts/proofs/tmux-pane-workers/child.ts new file mode 100644 index 00000000..c278a950 --- /dev/null +++ b/scripts/proofs/tmux-pane-workers/child.ts @@ -0,0 +1,153 @@ +/** + * The deterministic interactive child that stands in for a native Agent UI. + * + * It records what it can see — its argv bytes, its process relationships, and + * whether each standard stream is a terminal — in an evidence file the parent + * reads, prints the same to the pane, then echoes every line typed at it until + * told `exit N`. Negative modes make it misbehave in the ways the topology has + * to survive: + * + * - `exit1`: start, then exit 1 at once (ready and settled together); + * - `ignore-sigint-fork`: swallow SIGINT and fork a descendant that stays in + * the inherited process group; + * - `escape`: fork a descendant that leaves the process group and session + * with `setsid()` while still holding the pane's terminal open; + * - `escape-closed`: the same, with the terminal closed, so nothing but the + * process table remembers where it came from. + * + * Usage: child.ts --evidence --mode -- + * + * Started with `run()`, not `main()`: `main()` would turn every SIGINT into + * its own exit 130, and the negative mode has to be able to ignore one. + */ + +import { spawn as spawnChild } from "node:child_process"; +import { writeFile } from "node:fs/promises"; +import process from "node:process"; +import { writeTextFile } from "@effectionx/fs"; +import { fromReadable } from "@effectionx/node"; +import { lines } from "@effectionx/stream-helpers"; +import { each, run, withResolvers } from "effection"; +import type { Operation } from "effection"; +import { processFacts } from "./processes.ts"; + +export interface ChildEvidence { + mode: string; + argv: string[]; + pid: number; + ppid: number; + pgid: number; + tty: string; + tpgid: number; + isatty: [boolean, boolean, boolean]; + stdin: string[]; + signals: string[]; + descendants: { pid: number; kind: string }[]; +} + +function say(text: string): Operation { + const written = withResolvers(); + process.stdout.write(text, () => written.resolve()); + return written.operation; +} + +function parseArgs(argv: string[]): { evidence: string; mode: string; rest: string[] } { + let evidence = ""; + let mode = "plain"; + let index = 0; + while (index < argv.length) { + const current = argv[index]; + if (current === "--") { + return { evidence, mode, rest: argv.slice(index + 1) }; + } + if (current === "--evidence") { + evidence = argv[index + 1] ?? ""; + index += 2; + continue; + } + if (current === "--mode") { + mode = argv[index + 1] ?? "plain"; + index += 2; + continue; + } + index += 1; + } + return { evidence, mode, rest: [] }; +} + +const status = await run(function* (): Operation { + const { evidence: evidencePath, mode, rest } = parseArgs(process.argv.slice(2)); + const facts = yield* processFacts(process.pid); + const evidence: ChildEvidence = { + mode, + argv: rest, + pid: process.pid, + ppid: process.ppid, + pgid: facts?.pgid ?? -1, + tty: facts?.tty ?? "??", + tpgid: facts?.tpgid ?? -1, + isatty: [ + process.stdin.isTTY === true, + process.stdout.isTTY === true, + process.stderr.isTTY === true, + ], + stdin: [], + signals: [], + descendants: [], + }; + function* record(): Operation { + if (evidencePath.length > 0) { + yield* writeTextFile(evidencePath, JSON.stringify(evidence, null, 2)); + } + } + + if (mode === "ignore-sigint-fork") { + process.on("SIGINT", () => { + evidence.signals.push("SIGINT"); + process.stdout.write("child: ignoring SIGINT\n"); + // From a callback, and SIGKILL may follow within two seconds, so the + // write cannot wait for the next stdin line. + writeFile(evidencePath, JSON.stringify(evidence, null, 2)).catch(() => undefined); + }); + // The descendant ignores SIGINT too: it shares the pane's process group, + // so a `^C` typed at the pane would otherwise end it before teardown + // gets to prove anything. + const descendant = spawnChild("sh", ["-c", "trap '' INT; exec sleep 600"], { stdio: "ignore" }); + if (descendant.pid !== undefined) { + evidence.descendants.push({ pid: descendant.pid, kind: "in-group" }); + } + } + if (mode === "escape" || mode === "escape-closed") { + const descendant = spawnChild("sleep", ["600"], { + detached: true, + stdio: mode === "escape" ? "inherit" : "ignore", + }); + descendant.unref(); + if (descendant.pid !== undefined) { + evidence.descendants.push({ pid: descendant.pid, kind: mode }); + } + } + + yield* record(); + yield* say( + `child[${mode}] pid=${evidence.pid} pgid=${evidence.pgid} tty=${evidence.tty} ` + + `isatty=${evidence.isatty.join(",")} argv=${JSON.stringify(rest)}\n`, + ); + if (mode === "exit1") { + return 1; + } + + for (const line of yield* each(lines()(fromReadable(process.stdin)))) { + evidence.stdin.push(line); + yield* record(); + const exitRequest = /^exit (\d+)$/.exec(line.trim()); + if (exitRequest) { + yield* say(`child: exiting ${exitRequest[1]}\n`); + return Number(exitRequest[1]); + } + yield* say(`> ${line}\n`); + yield* each.next(); + } + return 0; +}); +process.exit(status); diff --git a/scripts/proofs/tmux-pane-workers/evidence.ts b/scripts/proofs/tmux-pane-workers/evidence.ts new file mode 100644 index 00000000..9d8a617e --- /dev/null +++ b/scripts/proofs/tmux-pane-workers/evidence.ts @@ -0,0 +1,120 @@ +/** + * What the proof establishes, as it establishes it. + * + * A check records claims — each a named boolean with the observation behind + * it — rather than throwing on the first miss, so one run reports everything + * it saw. The summary is written for the report; the JSON is the evidence. + */ + +import { writeTextFile } from "@effectionx/fs"; +import { appendFile } from "node:fs/promises"; +import { join } from "node:path"; +import process from "node:process"; +import { until } from "effection"; +import type { Operation } from "effection"; + +export interface Claim { + claim: string; + ok: boolean; + observed?: unknown; +} + +export interface CheckRecord { + name: string; + ok: boolean; + claims: Claim[]; + facts: Record; + notes: string[]; + error?: string; + durationMs: number; +} + +export class Check { + readonly claims: Claim[] = []; + readonly facts: Record = {}; + readonly notes: string[] = []; + constructor(readonly name: string) {} + + expect(claim: string, ok: boolean, observed?: unknown): boolean { + this.claims.push(observed === undefined ? { claim, ok } : { claim, ok, observed }); + return ok; + } + + fact(name: string, value: unknown): void { + this.facts[name] = value; + } + + note(text: string): void { + this.notes.push(text); + } +} + +export interface Logger { + (line: string): Operation; +} + +/** Progress goes to stderr and to a file the outer wrapper tails. */ +export function logger(directory: string): Logger { + const path = join(directory, "progress.log"); + return function* (line) { + const stamped = `${new Date().toISOString().slice(11, 23)} ${line}\n`; + process.stderr.write(stamped); + yield* until(appendFile(path, stamped)); + }; +} + +export class Evidence { + readonly checks: CheckRecord[] = []; + readonly environment: Record = {}; + + *run(name: string, body: (check: Check) => Operation, log: Logger): Operation { + const check = new Check(name); + const started = Date.now(); + let error: string | undefined; + yield* log(`▶ ${name}`); + try { + yield* body(check); + } catch (caught) { + error = caught instanceof Error ? `${caught.name}: ${caught.message}` : String(caught); + } + const record: CheckRecord = { + name, + ok: error === undefined && check.claims.every((claim) => claim.ok), + claims: check.claims, + facts: check.facts, + notes: check.notes, + durationMs: Date.now() - started, + }; + if (error !== undefined) { + record.error = error; + } + this.checks.push(record); + const failed = check.claims.filter((claim) => !claim.ok); + yield* log( + `${record.ok ? "✔" : "✘"} ${name} (${record.durationMs} ms)` + + (error ? ` — ${error}` : "") + + (failed.length > 0 ? ` — ${failed.map((claim) => claim.claim).join("; ")}` : ""), + ); + return record; + } + + *write(directory: string): Operation { + yield* writeTextFile( + join(directory, "evidence.json"), + JSON.stringify({ environment: this.environment, checks: this.checks }, null, 2) + "\n", + ); + yield* writeTextFile(join(directory, "summary.md"), this.summary()); + } + + summary(): string { + const lines: string[] = ["| check | result | claims | notes |", "|---|---|---|---|"]; + for (const check of this.checks) { + const failed = check.claims.filter((claim) => !claim.ok).map((claim) => claim.claim); + lines.push( + `| ${check.name} | ${check.ok ? "PASS" : "FAIL"} | ${check.claims.length - failed.length}/${check.claims.length}` + + ` | ${[...(check.error ? [check.error] : []), ...failed, ...check.notes].join("; ")} |`, + ); + } + return lines.join("\n") + "\n"; + } +} diff --git a/scripts/proofs/tmux-pane-workers/interactive-process.ts b/scripts/proofs/tmux-pane-workers/interactive-process.ts new file mode 100644 index 00000000..996316e0 --- /dev/null +++ b/scripts/proofs/tmux-pane-workers/interactive-process.ts @@ -0,0 +1,241 @@ +/** + * One interactive child that inherits this process's terminal. + * + * Derived from the native launcher in `packages/runtime/launcher.ts`, with the + * two facts the pane-worker topology needs separated out: + * + * - readiness is the child-process `spawn` event and nothing earlier. A pid + * from `forkpty` is not it, and neither is a pane that shows output; the + * `error` event for a missing executable arrives instead of `spawn`, never + * after it; + * - settlement is the `exit` event, reported as an exact code or signal, and + * is independent of readiness — a child that starts and exits 1 at once is + * both ready and settled. + * + * Teardown is owned by the scope the resource was created in. `stop()` runs + * the same escalation on demand and returns what it established, because a + * worker has to send that proof over IPC before its own scope closes; the + * `ensure` runs it again on cancellation and finds nothing left to do. + * + * The child shares this process's process group, so a `^C` on the pane reaches + * both — the worker handles that by ignoring the signal itself. Sharing is + * deliberate: `detached: true` would `setsid()` the child away from the pane's + * controlling terminal, and job control is the point of the pane. + */ + +import { spawn as spawnChild } from "node:child_process"; +import type { ChildProcess } from "node:child_process"; +import process from "node:process"; +import { ensure, Err, Ok, resource, sleep, withResolvers } from "effection"; +import type { Operation, Result } from "effection"; +import { deliver, descendantsOf, groupMembers, isReachable, processTable } from "./processes.ts"; +import type { Delivery, ProcessRow } from "./processes.ts"; + +export interface InteractiveRequest { + command: string[]; + cwd: string; + env: Record; +} + +export interface ProcessOutcome { + exitCode?: number; + signal?: string; +} + +export class StartupFailure extends Error { + override name = "StartupFailure"; + constructor(readonly code: string) { + super(`the interactive child could not be started (${code})`); + } +} + +export interface DescendantOutcome { + pid: number; + command: string; + /** Whether it shared the child's process group. */ + inGroup: boolean; + delivery: Delivery; + gone: boolean; +} + +/** What escalation established, in the order it was established. */ +export interface QuiescenceProof { + method: "exited" | "interrupted" | "killed"; + childPid: number | undefined; + childGone: boolean; + descendants: DescendantOutcome[]; + /** Pids that could still be reached when the proof was written. */ + survivors: number[]; +} + +export interface InteractiveProcess { + /** `Ok(pid)` once the kernel has the child; `Err` if it never will. */ + ready: Operation>; + /** Settles only after `ready` succeeded. */ + exited: Operation; + /** Idempotent: a second call after the first returns the same proof. */ + stop(): Operation; +} + +const INTERRUPT_GRACE_MS = 2_000; +const KILL_SETTLE_MS = 500; +const POLL_MS = 25; + +export function useInteractiveProcess(request: InteractiveRequest): Operation { + return resource(function* (provide) { + const [command, ...args] = request.command; + if (command === undefined) { + throw new Error("interactive process: command must not be empty"); + } + const ready = withResolvers>(); + const exited = withResolvers(); + let child: ChildProcess | undefined; + let outcome: ProcessOutcome | undefined; + let stopping: ReturnType> | undefined; + + // One escalation, however many callers: a worker's cancel and its own + // exit-watching task can both ask while the first is still in flight. + function* stop(): Operation { + if (stopping) { + return yield* stopping.operation; + } + stopping = withResolvers(); + try { + const proof = + child === undefined || child.pid === undefined + ? { + method: "exited" as const, + childPid: undefined, + childGone: true, + descendants: [], + survivors: [], + } + : yield* escalate(child, child.pid, process.pid, () => outcome !== undefined); + stopping.resolve(proof); + return proof; + } catch (error) { + stopping.reject(error instanceof Error ? error : new Error(String(error))); + throw error; + } + } + + // Registered before the spawn: a halt between acquiring a process and + // registering its cleanup would leak the process. + yield* ensure(function* () { + yield* stop(); + }); + + child = spawnChild(command, args, { + cwd: request.cwd, + env: request.env, + stdio: "inherit", + }); + child.once("spawn", () => { + if (child?.pid !== undefined) { + ready.resolve(Ok(child.pid)); + } + }); + child.once("error", (error: Error & { code?: string }) => { + ready.resolve(Err(new StartupFailure(error.code ?? error.message))); + }); + child.once("exit", (code: number | null, signal: string | null) => { + const settled: ProcessOutcome = {}; + if (code !== null) { + settled.exitCode = code; + } + if (signal !== null) { + settled.signal = signal; + } + outcome = settled; + exited.resolve(settled); + }); + + yield* provide({ ready: ready.operation, exited: exited.operation, stop }); + }); +} + +/** + * Interrupt, then insist, then reach the descendants the interrupt left. + * + * The descendant snapshot is taken before the first signal: a child that is + * killed stops being anyone's parent, and its children reparent to init, where + * an ancestry walk no longer finds them. A descendant that leaves the process + * group with `setsid()` is still in that snapshot while its parent lives; one + * created after the snapshot is not, and this proof says so rather than + * claiming otherwise. + */ +function* escalate( + child: ChildProcess, + pid: number, + self: number | undefined, + hasExited: () => boolean, +): Operation { + const before = yield* processTable(); + // The child shares this process's group, so the group is looked up rather + // than assumed to be the child's own pid. + const group = before.find((row) => row.pid === pid)?.pgid ?? pid; + const related = new Map(); + for (const row of descendantsOf(before, pid)) { + related.set(row.pid, row); + } + for (const row of groupMembers(before, group)) { + if (row.pid !== pid && row.pid !== self) { + related.set(row.pid, row); + } + } + + let method: QuiescenceProof["method"] = "exited"; + if (!hasExited() && isReachable(pid)) { + method = "interrupted"; + deliver(pid, "SIGINT"); + const left = yield* waitUntil(() => hasExited() || !isReachable(pid), INTERRUPT_GRACE_MS); + if (!left) { + method = "killed"; + const fatal = deliver(pid, "SIGKILL"); + const gone = yield* waitUntil(() => hasExited() || !isReachable(pid), KILL_SETTLE_MS); + if (!gone && fatal !== "delivered" && fatal !== "absent") { + throw new Error(`could not establish that process ${pid} stopped: SIGKILL was ${fatal}`); + } + } + } + // Deno's `node:child_process` holds the runtime open on a handle it will + // never settle once a signal the child ignored has been delivered. + try { + child.unref(); + } catch { + // Already released. + } + + const descendants: DescendantOutcome[] = []; + for (const row of related.values()) { + const delivery = deliver(row.pid, "SIGKILL"); + descendants.push({ + pid: row.pid, + command: row.command, + inGroup: row.pgid === group, + delivery, + gone: false, + }); + } + yield* waitUntil(() => descendants.every((entry) => !isReachable(entry.pid)), KILL_SETTLE_MS); + for (const entry of descendants) { + entry.gone = !isReachable(entry.pid); + } + const survivors = descendants.filter((entry) => !entry.gone).map((entry) => entry.pid); + const childGone = hasExited() || !isReachable(pid); + if (!childGone) { + survivors.unshift(pid); + } + return { method, childPid: pid, childGone, descendants, survivors }; +} + +function* waitUntil(condition: () => boolean, limitMs: number): Operation { + const deadline = Date.now() + limitMs; + while (!condition()) { + if (Date.now() >= deadline) { + return false; + } + yield* sleep(POLL_MS); + } + return true; +} diff --git a/scripts/proofs/tmux-pane-workers/ipc.ts b/scripts/proofs/tmux-pane-workers/ipc.ts new file mode 100644 index 00000000..1fe25026 --- /dev/null +++ b/scripts/proofs/tmux-pane-workers/ipc.ts @@ -0,0 +1,285 @@ +/** + * The invocation-private channel between the parent and one pane worker. + * + * One Unix socket per pane, inside a mode-0700 directory that exists for one + * invocation. The worker proves which pane it is with a token the parent wrote + * to a mode-0600 file only that worker reads and removes; a connection that + * does not open with the right `hello` is closed, and a second connection to a + * pane already admitted is closed too. Nothing here reaches argv or the + * environment of any process: the pane command names the directory and the + * ordinal, and tmux's command parser sees only those. + * + * Messages are newline-delimited JSON and parsed with zod on both ends, so a + * value is what its schema says or the frame is a protocol error. + * + * The socket directory is short by necessity, not taste: a Unix socket path is + * limited to 104 bytes on macOS, which a temporary directory named after a + * repository path exceeds. + */ + +import { randomBytes } from "node:crypto"; +import { writeFile } from "node:fs/promises"; +import net from "node:net"; +import type { Server, Socket } from "node:net"; +import { join } from "node:path"; +import { + createQueue, + createSignal, + ensure, + race, + resource, + sleep, + spawn, + until, + withResolvers, +} from "effection"; +import type { Operation, Queue } from "effection"; +import { z } from "zod"; + +export const HelloSchema = z.object({ + type: z.literal("hello"), + ordinal: z.number().int().nonnegative(), + token: z.string(), + pid: z.number().int(), + ppid: z.number().int(), + pgid: z.number().int(), + tty: z.string(), + isatty: z.tuple([z.boolean(), z.boolean(), z.boolean()]), +}); + +const DescendantOutcomeSchema = z.object({ + pid: z.number().int(), + command: z.string(), + inGroup: z.boolean(), + delivery: z.enum(["delivered", "absent", "refused"]), + gone: z.boolean(), +}); + +const TerminalHolderSchema = z.object({ pid: z.number().int(), gone: z.boolean() }); + +export const QuiescenceProofSchema = z.object({ + method: z.enum(["exited", "interrupted", "killed"]), + childPid: z.number().int().optional(), + childGone: z.boolean(), + descendants: z.array(DescendantOutcomeSchema), + survivors: z.array(z.number().int()), + /** Whatever still held the pane's terminal after the escalation, and whether it is gone. */ + terminalHolders: z.array(TerminalHolderSchema), +}); + +export const FromWorkerSchema = z.discriminatedUnion("type", [ + HelloSchema, + z.object({ type: z.literal("displayed"), seq: z.number().int() }), + z.object({ type: z.literal("ready"), id: z.string(), pid: z.number().int() }), + z.object({ type: z.literal("startup-failed"), id: z.string(), reason: z.string() }), + z.object({ type: z.literal("refused"), id: z.string(), reason: z.string() }), + z.object({ + type: z.literal("exited"), + id: z.string(), + exitCode: z.number().int().optional(), + signal: z.string().optional(), + /** The settlement that preceded this report; the pane is free once it arrives. */ + proof: QuiescenceProofSchema, + }), + z.object({ + type: z.literal("quiescent"), + id: z.string().optional(), + proof: QuiescenceProofSchema, + }), + z.object({ + type: z.literal("bye"), + /** Processes that still held the pane's terminal at shutdown, and whether they are gone. */ + ttyHolders: z.array(TerminalHolderSchema), + }), +]); + +export const ToWorkerSchema = z.discriminatedUnion("type", [ + z.object({ type: z.literal("welcome") }), + z.object({ type: z.literal("display"), seq: z.number().int(), text: z.string() }), + z.object({ + type: z.literal("launch"), + id: z.string(), + argv: z.array(z.string()).min(1), + cwd: z.string(), + env: z.record(z.string(), z.string()), + }), + z.object({ type: z.literal("cancel"), id: z.string() }), + z.object({ type: z.literal("shutdown") }), +]); + +export type Hello = z.infer; +export type FromWorker = z.infer; +export type ToWorker = z.infer; +export type QuiescenceProof = z.infer; + +export function socketPath(directory: string, ordinal: number): string { + return join(directory, `p${ordinal}.sock`); +} + +export function tokenPath(directory: string, ordinal: number): string { + return join(directory, `p${ordinal}.token`); +} + +/** Feed socket bytes into a queue of parsed frames; close the queue on EOF. */ +export function frames(socket: Socket, parse: (value: unknown) => T): Queue { + const queue = createQueue(); + let remainder = ""; + socket.setEncoding("utf8"); + socket.on("data", (chunk: string) => { + const lines = (remainder + chunk).split("\n"); + remainder = lines.pop() ?? ""; + for (const line of lines) { + if (line.length === 0) { + continue; + } + try { + queue.add(parse(JSON.parse(line))); + } catch { + // A frame that is not the protocol ends the conversation. + socket.destroy(); + } + } + }); + socket.on("close", () => queue.close()); + socket.on("error", () => socket.destroy()); + return queue; +} + +export function send(socket: Socket, message: unknown): Operation { + const written = withResolvers(); + if (socket.destroyed) { + written.resolve(); + return written.operation; + } + socket.write(JSON.stringify(message) + "\n", () => written.resolve()); + return written.operation; +} + +/** The parent's end of one admitted worker. */ +export interface PaneLink { + ordinal: number; + hello: Hello; + send(message: ToWorker): Operation; + /** The next frame, or `undefined` once the worker's connection closed. */ + next(): Operation; + connected(): boolean; +} + +export interface PaneSockets { + directory: string; + /** The admitted worker for `ordinal`; waits for its `hello`. */ + link(ordinal: number): Operation; + /** Connections that were closed without admission, for the evidence. */ + refusals(): string[]; +} + +interface Slot { + resolvers: ReturnType>; + settled: boolean; +} + +const HELLO_TIMEOUT_MS = 10_000; + +function* helloTimeout(): Operation> { + yield* sleep(HELLO_TIMEOUT_MS); + return { done: true, value: undefined }; +} + +/** + * Listen for `count` workers. Sockets and tokens exist before any pane is + * created, so a worker that starts finds its socket already there, and are + * removed with the directory whatever way the scope ends. + */ +export function usePaneSockets(directory: string, count: number): Operation { + return resource(function* (provide) { + const tokens = new Map(); + const slots = new Map(); + const servers: Server[] = []; + const sockets = new Set(); + const refusals: string[] = []; + const connections = createSignal<{ ordinal: number; socket: Socket }, never>(); + + yield* ensure(() => { + for (const socket of sockets) { + socket.destroy(); + } + for (const server of servers) { + server.close(); + } + }); + + // Subscribed before any server listens, so no connection is dropped. + const incoming = yield* connections; + + for (let ordinal = 0; ordinal < count; ordinal++) { + const token = randomBytes(16).toString("hex"); + tokens.set(ordinal, token); + slots.set(ordinal, { resolvers: withResolvers(), settled: false }); + yield* until(writeFile(tokenPath(directory, ordinal), token, { mode: 0o600 })); + const server = net.createServer((socket) => { + sockets.add(socket); + socket.once("close", () => sockets.delete(socket)); + connections.send({ ordinal, socket }); + }); + servers.push(server); + const listening = withResolvers(); + server.once("error", (error: Error) => listening.reject(error)); + server.listen(socketPath(directory, ordinal), () => listening.resolve()); + yield* listening.operation; + } + + function* admit(ordinal: number, socket: Socket): Operation { + const slot = slots.get(ordinal); + const token = tokens.get(ordinal); + const queue = frames(socket, (value) => FromWorkerSchema.parse(value)); + const first = yield* race([queue.next(), helloTimeout()]); + if (slot === undefined || token === undefined || first.done || first.value.type !== "hello") { + refusals.push(`pane ${ordinal}: connection without hello`); + socket.destroy(); + return; + } + const hello = first.value; + if (hello.ordinal !== ordinal || hello.token !== token || slot.settled) { + refusals.push( + `pane ${ordinal}: refused ordinal ${hello.ordinal} ${slot.settled ? "(already admitted)" : "(bad token)"}`, + ); + socket.destroy(); + return; + } + slot.settled = true; + slot.resolvers.resolve({ + ordinal, + hello, + send: (message) => send(socket, message), + *next() { + const next = yield* queue.next(); + return next.done ? undefined : next.value; + }, + connected: () => !socket.destroyed, + }); + } + + yield* spawn(function* () { + while (true) { + const next = yield* incoming.next(); + if (next.done) { + return; + } + const { ordinal, socket } = next.value; + yield* spawn(() => admit(ordinal, socket)); + } + }); + + yield* provide({ + directory, + *link(ordinal) { + const slot = slots.get(ordinal); + if (slot === undefined) { + throw new Error(`no pane ${ordinal}`); + } + return yield* slot.resolvers.operation; + }, + refusals: () => [...refusals], + }); + }); +} diff --git a/scripts/proofs/tmux-pane-workers/layout.ts b/scripts/proofs/tmux-pane-workers/layout.ts new file mode 100644 index 00000000..cae6e1d9 --- /dev/null +++ b/scripts/proofs/tmux-pane-workers/layout.ts @@ -0,0 +1,122 @@ +/** + * The authored grid as explicit tmux geometry. + * + * `select-layout tiled` chooses its own column count from the window's + * dimensions, so it cannot implement an authored `columns`. A layout string + * can: tmux accepts the same description it prints in `#{window_layout}` — + * a checksum, then a tree of cells where `{…}` lays children left to right and + * `[…]` top to bottom, each leaf naming its pane id. Every cell is sized here, + * row-major from the pane count and `columns`, and tmux is told rather than + * asked. A final row with fewer panes than columns spans the row: tmux has no + * empty cells, and the ordinal placement is what the author wrote. + */ + +export interface Cell { + ordinal: number; + left: number; + top: number; + width: number; + height: number; +} + +/** Split `total` into `count` parts with a one-cell separator between them. */ +function partition(total: number, count: number): number[] { + const available = total - (count - 1); + const base = Math.floor(available / count); + const extra = available - base * count; + return Array.from({ length: count }, (_, index) => base + (index < extra ? 1 : 0)); +} + +export function rowMajorCells( + width: number, + height: number, + columns: number, + count: number, +): Cell[] { + const rows = Math.ceil(count / columns); + const heights = partition(height, rows); + const cells: Cell[] = []; + let top = 0; + for (let row = 0; row < rows; row++) { + const inRow = Math.min(columns, count - row * columns); + const widths = partition(width, inRow); + let left = 0; + for (let column = 0; column < inRow; column++) { + cells.push({ + ordinal: row * columns + column, + left, + top, + width: widths[column], + height: heights[row], + }); + left += widths[column] + 1; + } + top += heights[row] + 1; + } + return cells; +} + +/** tmux's `layout_checksum`, so the string is accepted as its own. */ +function checksum(layout: string): string { + let sum = 0; + for (let index = 0; index < layout.length; index++) { + sum = ((sum >> 1) + ((sum & 1) << 15)) & 0xffff; + sum = (sum + layout.charCodeAt(index)) & 0xffff; + } + return sum.toString(16).padStart(4, "0"); +} + +/** + * The layout string placing `paneIds[i]` at ordinal `i`. Pane ids are the + * numeric part of tmux's `%N`. + */ +export function layoutString( + width: number, + height: number, + columns: number, + paneIds: number[], +): string { + const cells = rowMajorCells(width, height, columns, paneIds.length); + const rows = Math.ceil(paneIds.length / columns); + const rowStrings: string[] = []; + for (let row = 0; row < rows; row++) { + const inRow = cells.filter((cell) => Math.floor(cell.ordinal / columns) === row); + const leaves = inRow.map( + (cell) => `${cell.width}x${cell.height},${cell.left},${cell.top},${paneIds[cell.ordinal]}`, + ); + if (leaves.length === 1) { + rowStrings.push(leaves[0]); + } else { + const first = inRow[0]; + rowStrings.push(`${width}x${first.height},0,${first.top}{${leaves.join(",")}}`); + } + } + const body = + rowStrings.length === 1 ? rowStrings[0] : `${width}x${height},0,0[${rowStrings.join(",")}]`; + return `${checksum(body)},${body}`; +} + +/** Whether observed pane geometry is the row-major placement for `columns`. */ +export function placementMatches(observed: Cell[], columns: number): string[] { + const problems: string[] = []; + const byOrdinal = observed.toSorted((a, b) => a.ordinal - b.ordinal); + for (const cell of byOrdinal) { + const row = Math.floor(cell.ordinal / columns); + const column = cell.ordinal % columns; + const above = byOrdinal.find((other) => other.ordinal === cell.ordinal - columns); + const leftOf = + column > 0 ? byOrdinal.find((other) => other.ordinal === cell.ordinal - 1) : undefined; + if (above && !(cell.top > above.top && cell.top === above.top + above.height + 1)) { + problems.push( + `pane ${cell.ordinal} is not directly below pane ${above.ordinal} (row ${row})`, + ); + } + if (leftOf && !(cell.left === leftOf.left + leftOf.width + 1 && cell.top === leftOf.top)) { + problems.push(`pane ${cell.ordinal} is not directly right of pane ${leftOf.ordinal}`); + } + if (column === 0 && cell.left !== 0) { + problems.push(`pane ${cell.ordinal} should start a row at the left edge`); + } + } + return problems; +} diff --git a/scripts/proofs/tmux-pane-workers/processes.ts b/scripts/proofs/tmux-pane-workers/processes.ts new file mode 100644 index 00000000..34918f85 --- /dev/null +++ b/scripts/proofs/tmux-pane-workers/processes.ts @@ -0,0 +1,129 @@ +/** + * What the kernel says about processes: the table, reachability, and signal + * delivery. Shared by the parent and the pane worker. + * + * `ps` rather than `/proc`, because this proof runs on macOS. `tpgid` is the + * terminal's foreground process group, which is how a shell's job control is + * observed from outside rather than inferred from what it printed. + */ + +import { execFile } from "node:child_process"; +import process from "node:process"; +import { until } from "effection"; +import type { Operation } from "effection"; + +export interface ProcessRow { + pid: number; + ppid: number; + pgid: number; + /** `ttys002`, or `??` for a process with no controlling terminal. */ + tty: string; + /** The controlling terminal's foreground process group, or -1. */ + tpgid: number; + command: string; +} + +function run(command: string, args: string[]): Promise { + return new Promise((resolve, reject) => { + execFile(command, args, { maxBuffer: 16 * 1024 * 1024 }, (error, stdout) => { + if (error && !("code" in error && typeof error.code === "number")) { + reject(error); + return; + } + resolve(stdout); + }); + }); +} + +function parseRow(line: string): ProcessRow | undefined { + const match = /^\s*(\d+)\s+(\d+)\s+(-?\d+)\s+(\S+)\s+(-?\d+)\s+(.*)$/.exec(line); + if (!match) { + return undefined; + } + const [, pid, ppid, pgid, tty, tpgid, command] = match; + return { + pid: Number(pid), + ppid: Number(ppid), + pgid: Number(pgid), + tty, + tpgid: Number(tpgid), + command, + }; +} + +export function* processTable(): Operation { + const output = yield* until(run("ps", ["-axo", "pid=,ppid=,pgid=,tty=,tpgid=,command="])); + return output + .split("\n") + .map(parseRow) + .filter((row): row is ProcessRow => row !== undefined); +} + +export function* processFacts(pid: number): Operation { + const rows = yield* processTable(); + return rows.find((row) => row.pid === pid); +} + +/** Every process below `pid` by parent links, in the given table. */ +export function descendantsOf(rows: ProcessRow[], pid: number): ProcessRow[] { + const found: ProcessRow[] = []; + const frontier = [pid]; + while (frontier.length > 0) { + const parent = frontier.pop(); + for (const row of rows) { + if (row.ppid === parent) { + found.push(row); + frontier.push(row.pid); + } + } + } + return found; +} + +export function groupMembers(rows: ProcessRow[], pgid: number): ProcessRow[] { + return rows.filter((row) => row.pgid === pgid); +} + +/** Processes still holding the terminal device open, by `lsof`. */ +export function* holdersOf(ttyDevice: string): Operation { + const output = yield* until(run("lsof", ["-t", ttyDevice])); + return output + .split("\n") + .map((line) => line.trim()) + .filter((line) => line.length > 0) + .map(Number); +} + +export type Delivery = "delivered" | "absent" | "refused"; + +/** + * Send one signal by pid and report what that established. The same rule as + * `packages/runtime/launcher.ts`: gone already is the outcome escalation was + * asking for; anything but ESRCH is a delivery that did not happen. + */ +export function deliver(pid: number, name: "SIGINT" | "SIGTERM" | "SIGKILL"): Delivery { + try { + process.kill(pid, name); + return "delivered"; + } catch (error) { + return isNoSuchProcess(error) ? "absent" : "refused"; + } +} + +export function isReachable(pid: number): boolean { + try { + process.kill(pid, 0); + return true; + } catch { + return false; + } +} + +function isNoSuchProcess(error: unknown): boolean { + return ( + typeof error === "object" && + error !== null && + "code" in error && + Reflect.get(error, "code") === "ESRCH" + ); +} diff --git a/scripts/proofs/tmux-pane-workers/proof.ts b/scripts/proofs/tmux-pane-workers/proof.ts new file mode 100644 index 00000000..b7d32602 --- /dev/null +++ b/scripts/proofs/tmux-pane-workers/proof.ts @@ -0,0 +1,256 @@ +/** + * Executable proof for #726: persistent tmux pane workers for ``. + * + * Usage (from a prepared checkout): + * + * deno task proof:tmux-pane-workers # everything, unattended + * deno task proof:tmux-pane-workers -- --attach # the journey on your terminal + * + * Unattended runs need a terminal for the visible attachment, so the proof + * starts a throwaway outer tmux session of its own and runs itself inside it + * (`--inner`); progress is relayed to stderr and the evidence — `evidence.json`, + * `summary.md`, the children's evidence files — is written to `--out ` + * (default: a fresh directory under the system temporary directory, printed + * at the end). `--runs N` sets the measurement runs per pane count (default + * 20); `--skip-measure` leaves them out; `--only ` runs one check. + * + * `--attach` runs the journey alone on the caller's terminal: the grid + * appears, the scripted interactions run, and the proof waits for you to + * detach (prefix, `d`) before tearing down. + */ + +import { mkdtempSync } from "node:fs"; +import { mkdir, readFile } from "node:fs/promises"; +import { tmpdir } from "node:os"; +import { join } from "node:path"; +import process from "node:process"; +import { exec, Stdio } from "@effectionx/process"; +import { exists, readTextFile } from "@effectionx/fs"; +import { exit, main, sleep, until } from "effection"; +import type { Operation } from "effection"; +import { + checkCancellationPoints, + checkJourney, + checkLayoutGeometry, + checkMeasurements, + checkNegativeChildren, + checkReadinessBoundary, + checkSequentialHandoff, + checkSignalsDistinct, + checkStartupFailureAtomic, +} from "./checks.ts"; +import type { CheckContext } from "./checks.ts"; +import { Evidence, logger } from "./evidence.ts"; +import type { Check } from "./evidence.ts"; +import { tmuxAt } from "./provider.ts"; +import { filteredEnvironment, usePrivateDirectory } from "./workspace.ts"; + +interface Options { + inner: boolean; + attach: boolean; + out: string | undefined; + runs: number; + skipMeasure: boolean; + only: string | undefined; +} + +function parseOptions(argv: string[]): Options { + const options: Options = { + inner: false, + attach: false, + out: undefined, + runs: 20, + skipMeasure: false, + only: undefined, + }; + for (let index = 0; index < argv.length; index++) { + switch (argv[index]) { + case "--inner": + options.inner = true; + break; + case "--attach": + options.attach = true; + break; + case "--out": + options.out = argv[++index]; + break; + case "--runs": + options.runs = Number(argv[++index]); + break; + case "--skip-measure": + options.skipMeasure = true; + break; + case "--only": + options.only = argv[++index]; + break; + default: + throw new Error(`unknown option ${argv[index]}`); + } + } + return options; +} + +const REPO_ROOT = join(import.meta.dirname ?? ".", "..", "..", ".."); + +function* command(cmd: string, args: string[]): Operation { + const result = yield* exec(cmd, { arguments: args }).join(); + return result.stdout.trim(); +} + +function* environmentFacts(): Operation> { + return { + commit: yield* command("git", ["-C", REPO_ROOT, "rev-parse", "HEAD"]), + os: `${process.platform} ${yield* command("uname", ["-r"])}`, + arch: process.arch, + tmux: yield* command("tmux", ["-V"]), + deno: (yield* command("deno", ["--version"])).split("\n")[0], + date: new Date().toISOString(), + }; +} + +function* runChecks(options: Options, outDirectory: string): Operation { + const log = logger(outDirectory); + const evidence = new Evidence(); + Object.assign(evidence.environment, yield* environmentFacts()); + evidence.environment.command = [ + "deno", + "task", + "proof:tmux-pane-workers", + ...process.argv.slice(2), + ].join(" "); + const context: CheckContext = { + evidenceDirectory: join(outDirectory, "children"), + log, + attachable: process.stdout.isTTY === true, + manualClose: options.attach, + }; + yield* log(`evidence → ${outDirectory}; terminal: ${context.attachable ? "yes" : "no"}`); + + const checks: [string, (check: Check) => Operation][] = options.attach + ? [["journey", (check) => checkJourney(check, context)]] + : [ + ["layout-geometry", (check) => checkLayoutGeometry(check, context)], + ["readiness-boundary", (check) => checkReadinessBoundary(check, context)], + ["journey", (check) => checkJourney(check, context)], + ["startup-failure-atomic", (check) => checkStartupFailureAtomic(check, context)], + ["signals-distinct", (check) => checkSignalsDistinct(check, context)], + ["negative-children", (check) => checkNegativeChildren(check, context)], + ["sequential-handoff", (check) => checkSequentialHandoff(check, context)], + ["cancellation-points", (check) => checkCancellationPoints(check, context)], + ["measurements", (check) => checkMeasurements(check, context, options.runs)], + ]; + for (const [name, body] of checks) { + if (options.only !== undefined && name !== options.only) { + continue; + } + if (name === "measurements" && options.skipMeasure) { + continue; + } + yield* evidence.run(name, body, log); + } + yield* evidence.write(outDirectory); + const failed = evidence.checks.filter((check) => !check.ok).length; + yield* log(`done: ${evidence.checks.length - failed}/${evidence.checks.length} checks passed`); + return failed === 0 ? 0 : 1; +} + +/** Run this same program inside a private outer tmux so it has a terminal. */ +function* runWrapped(options: Options, outDirectory: string): Operation { + const directory = yield* usePrivateDirectory(); + const tmux = tmuxAt(join(directory, "o"), filteredEnvironment()); + const passthrough = ["--inner", "--out", outDirectory, "--runs", String(options.runs)]; + if (options.skipMeasure) { + passthrough.push("--skip-measure"); + } + if (options.only !== undefined) { + passthrough.push("--only", options.only); + } + yield* tmux.run([ + "new-session", + "-d", + "-s", + "outer", + "-x", + "200", + "-y", + "56", + "-c", + REPO_ROOT, + "deno", + "run", + "--allow-all", + join(import.meta.dirname ?? ".", "proof.ts"), + ...passthrough, + ]); + yield* tmux.run(["set", "-g", "remain-on-exit", "on"]); + process.stderr.write("running inside a private outer tmux session; progress follows\n"); + + const progress = join(outDirectory, "progress.log"); + let relayed = 0; + while (true) { + if (yield* exists(progress)) { + const bytes = yield* until(readFile(progress)); + if (bytes.length > relayed) { + process.stderr.write(bytes.subarray(relayed)); + relayed = bytes.length; + } + } + const dead = yield* tmux.tryRun([ + "display", + "-p", + "-t", + "outer:0", + "#{pane_dead} #{pane_dead_status}", + ]); + if (dead === undefined) { + process.stderr.write("the outer tmux session ended unexpectedly\n"); + return 1; + } + const [isDead, status] = dead.split(" "); + if (isDead === "1") { + const code = Number(status); + if (code !== 0) { + const screen = yield* tmux.tryRun(["capture-pane", "-p", "-S", "-", "-t", "outer:0"]); + process.stderr.write(`inner proof exited ${code}; its last screen:\n${screen ?? ""}\n`); + } + yield* tmux.tryRun(["kill-server"]); + const summary = join(outDirectory, "summary.md"); + if (yield* exists(summary)) { + process.stdout.write(yield* readTextFile(summary)); + } + process.stdout.write(`\nevidence: ${outDirectory}\n`); + return code; + } + yield* sleep(200); + } +} + +// Losing the terminal is a cancellation, not a crash: `main()` shuts down on +// SIGTERM, and SIGHUP is turned into one so the hidden servers of a run whose +// terminal vanished are torn down rather than orphaned. +process.on("SIGHUP", () => process.kill(process.pid, "SIGTERM")); + +await main(function* () { + const options = parseOptions(process.argv.slice(2)); + // tmux and ps output is collected, never echoed. + yield* Stdio.around({ + *stdout() { + // Collected by the caller, never echoed. + }, + *stderr() { + // Collected by the caller, never echoed. + }, + }); + // oxlint-disable-next-line local/no-sync-filesystem + const outDirectory = options.out ?? mkdtempSync(join(tmpdir(), "xmd-pane-proof-")); + yield* until(mkdir(outDirectory, { recursive: true })); + if (options.inner || options.attach) { + const status = yield* runChecks(options, outDirectory); + if (options.attach) { + process.stdout.write(yield* readTextFile(join(outDirectory, "summary.md"))); + process.stdout.write(`\nevidence: ${outDirectory}\n`); + } + yield* exit(status); + } + yield* exit(yield* runWrapped(options, outDirectory)); +}); diff --git a/scripts/proofs/tmux-pane-workers/provider.ts b/scripts/proofs/tmux-pane-workers/provider.ts new file mode 100644 index 00000000..eb6d7307 --- /dev/null +++ b/scripts/proofs/tmux-pane-workers/provider.ts @@ -0,0 +1,441 @@ +/** + * The tmux side of the topology: one hidden invocation-private server, an + * explicit grid of panes each started on its worker, a control-mode client + * that reports what the server sees, the one visible attachment, and a + * teardown that proves the server is gone. + * + * Every tmux identifier here — socket path, session name, window, pane ids, + * client names, the server pid — stays inside this module's values. The proof + * writes them to its evidence and nowhere else. + * + * The control client attaches with `-f no-output`, so pane bytes never travel + * through the parent: what it receives is `%client-detached`, + * `%client-session-changed`, `%sessions-changed`, `%layout-change` and + * `%exit`, which is exactly the set the proof classifies. An attach client's + * exit code cannot do that classification: on this tmux it is 0 after + * `detach-client`, 0 after `kill-session`, and 1 after `kill-server`. + */ + +import { join } from "node:path"; +import { exec } from "@effectionx/process"; +import { lines } from "@effectionx/stream-helpers"; +import { ensure, resource, sleep, spawn } from "effection"; +import type { Operation } from "effection"; +import { exists } from "@effectionx/fs"; +import { useInteractiveProcess } from "./interactive-process.ts"; +import type { InteractiveProcess } from "./interactive-process.ts"; +import { layoutString, rowMajorCells } from "./layout.ts"; +import type { Cell } from "./layout.ts"; +import { isReachable } from "./processes.ts"; + +export interface Tmux { + socket: string; + /** Run one tmux command against the private server; stdout, trimmed. */ + run(args: string[]): Operation; + /** The same, returning `undefined` instead of throwing on failure. */ + tryRun(args: string[]): Operation; +} + +export class TmuxCommandFailed extends Error { + override name = "TmuxCommandFailed"; + constructor(args: string[], stderr: string, code: number | undefined) { + super(`tmux ${args.join(" ")} failed (${code ?? "signal"}): ${stderr.trim()}`); + } +} + +export function tmuxAt(socket: string, env: Record): Tmux { + const base = ["-S", socket, "-f", "/dev/null"]; + function* run(args: string[]): Operation { + const result = yield* exec("tmux", { arguments: [...base, ...args], env }).join(); + if (result.code !== 0) { + throw new TmuxCommandFailed(args, result.stderr, result.code); + } + return result.stdout.trim(); + } + return { + socket, + run, + *tryRun(args) { + const result = yield* exec("tmux", { arguments: [...base, ...args], env }).join(); + return result.code === 0 ? result.stdout.trim() : undefined; + }, + }; +} + +export interface PaneInfo { + ordinal: number; + id: string; + /** `/dev/ttys002` */ + tty: string; + pid: number; + cell: Cell; +} + +export type ControlEvent = + | { kind: "client-attached"; client: string } + | { kind: "client-detached"; client: string } + | { kind: "sessions-changed" } + | { kind: "layout-change" } + | { kind: "output"; pane: string } + | { kind: "exit" } + | { kind: "closed" } + | { kind: "other"; line: string }; + +export interface GridRequest { + session: string; + columns: number; + panes: number; + width: number; + height: number; + titles: string[]; + workerCommand(ordinal: number): string[]; + cwd: string; + env: Record; +} + +export interface VisibleClient { + process: InteractiveProcess; + /** tmux's name for this client once it is attached: its tty. */ + name: string; +} + +export interface TmuxGrid { + tmux: Tmux; + session: string; + serverPid: number; + panes: PaneInfo[]; + /** Everything the control client reported, in order. */ + controlLog: string[]; + /** The same, classified; `closed` is appended when the client ends. */ + events: ControlEvent[]; + /** Current pane geometry, for verifying placement after a resize. */ + geometry(): Operation; + /** Attach on this process's terminal; resolves once tmux lists the client. */ + attach(): Operation; + detach(client: VisibleClient): Operation; + /** `kill-server`, then wait until the server pid and socket are gone. */ + stop(): Operation; +} + +export interface StopProof { + serverGone: boolean; + unreachable: boolean; + socketFileRemains: boolean; +} + +export function serverSocketPath(directory: string): string { + return join(directory, "s"); +} + +const CLIENT_POLL_MS = 20; +const STOP_LIMIT_MS = 5_000; + +/** + * Prepare the whole hidden composite: server, panes on their workers, explicit + * layout, titles, control client. Nothing is visible until `attach()`. + */ +export function useTmuxGrid(directory: string, request: GridRequest): Operation { + return resource(function* (provide) { + const tmux = tmuxAt(serverSocketPath(directory), request.env); + const target = `${request.session}:0`; + let serverPid = -1; + + // Registered first: a halt anywhere below must still take the server down. + yield* ensure(function* () { + yield* stop(); + }); + + yield* tmux.run([ + "new-session", + "-d", + "-s", + request.session, + "-x", + String(request.width), + "-y", + String(request.height), + "-c", + request.cwd, + ...request.workerCommand(0), + ]); + serverPid = Number(yield* tmux.run(["display", "-p", "#{pid}"])); + yield* tmux.run(["set", "-g", "remain-on-exit", "on"]); + yield* tmux.run(["set", "-g", "status", "off"]); + yield* tmux.run(["set", "-g", "pane-border-status", "top"]); + yield* tmux.run(["set", "-g", "pane-border-format", " #{pane_title} "]); + + // Panes are created by splitting whichever pane has the most room, so a + // small window still fits every pane; the explicit layout below decides + // where each one ends up. + const paneIds: string[] = [yield* tmux.run(["display", "-p", "-t", target, "#{pane_id}"])]; + for (let ordinal = 1; ordinal < request.panes; ordinal++) { + const roomiest = yield* largestPane(tmux, target); + const direction = roomiest.width >= roomiest.height * 2 ? "-h" : "-v"; + const id = yield* tmux.run([ + "split-window", + "-d", + direction, + "-t", + roomiest.id, + "-c", + request.cwd, + "-P", + "-F", + "#{pane_id}", + ...request.workerCommand(ordinal), + ]); + paneIds.push(id); + } + const [width, height] = (yield* tmux.run([ + "display", + "-p", + "-t", + target, + "#{window_width} #{window_height}", + ])) + .split(" ") + .map(Number); + const layout = layoutString( + width, + height, + request.columns, + paneIds.map((id) => Number(id.slice(1))), + ); + yield* tmux.run(["select-layout", "-t", target, layout]); + // tmux assigns panes to the layout's leaves in window-list order and + // ignores the ids written in the string, so the authored order is imposed + // afterwards: a pane found at the wrong visual position is swapped with + // the one that belongs there. Swapping preserves the cells. + for (let pass = 0; pass < paneIds.length; pass++) { + const visual = (yield* paneFacts(tmux, target, paneIds)).toSorted( + (a, b) => a.cell.top - b.cell.top || a.cell.left - b.cell.left, + ); + const misplaced = visual.findIndex((pane, index) => pane.id !== paneIds[index]); + if (misplaced < 0) { + break; + } + yield* tmux.run(["swap-pane", "-d", "-s", paneIds[misplaced], "-t", visual[misplaced].id]); + } + for (const [ordinal, id] of paneIds.entries()) { + yield* tmux.run([ + "select-pane", + "-t", + id, + "-T", + request.titles[ordinal] ?? `pane ${ordinal}`, + ]); + } + const panes = yield* paneFacts(tmux, target, paneIds); + + const controlLog: string[] = []; + const events: ControlEvent[] = []; + yield* spawn(function* () { + const client = yield* exec("tmux", { + arguments: [ + "-S", + tmux.socket, + "-f", + "/dev/null", + "-C", + "attach-session", + "-f", + "no-output", + "-t", + request.session, + ], + env: request.env, + }); + const subscription = yield* lines()(client.stdout); + let next = yield* subscription.next(); + while (!next.done) { + controlLog.push(next.value); + events.push(classify(next.value)); + next = yield* subscription.next(); + } + events.push({ kind: "closed" }); + }); + + // The socket file outlives the server on this tmux, so "gone" is the + // server pid being unreachable and nothing answering on the socket. + function* stop(): Operation { + yield* tmux.tryRun(["kill-server"]); + const deadline = Date.now() + STOP_LIMIT_MS; + let proof: StopProof; + do { + proof = { + serverGone: serverPid < 0 || !isReachable(serverPid), + unreachable: (yield* tmux.tryRun(["has-session", "-t", request.session])) === undefined, + socketFileRemains: yield* exists(tmux.socket), + }; + if (proof.serverGone && proof.unreachable) { + return proof; + } + yield* sleep(CLIENT_POLL_MS); + } while (Date.now() < deadline); + return proof; + } + + yield* provide({ + tmux, + session: request.session, + serverPid, + panes, + controlLog, + events, + *geometry() { + return (yield* paneFacts(tmux, target, paneIds)).map((pane) => pane.cell); + }, + *attach() { + const before = new Set(yield* clientNames(tmux)); + const process = yield* useInteractiveProcess({ + command: [ + "tmux", + "-S", + tmux.socket, + "-f", + "/dev/null", + "attach-session", + "-t", + request.session, + ], + cwd: request.cwd, + env: request.env, + }); + const ready = yield* process.ready; + if (!ready.ok) { + throw ready.error; + } + let name: string | undefined; + // Registered after the process, so it runs first on teardown: a client + // asked to detach restores the terminal itself, and a client that is + // signalled instead may not. The process's own escalation remains + // behind it for a client that does not leave. + yield* ensure(function* () { + if (name === undefined) { + return; + } + yield* tmux.tryRun(["detach-client", "-t", name]); + const deadline = Date.now() + 1_000; + while (Date.now() < deadline && (yield* clientNames(tmux)).includes(name)) { + yield* sleep(CLIENT_POLL_MS); + } + }); + while (true) { + const now = yield* clientNames(tmux); + const added = now.find((candidate) => !before.has(candidate)); + if (added !== undefined) { + name = added; + return { process, name: added }; + } + yield* sleep(CLIENT_POLL_MS); + } + }, + *detach(client) { + yield* tmux.run(["detach-client", "-t", client.name]); + }, + stop, + }); + }); +} + +function classify(line: string): ControlEvent { + const [tag, ...rest] = line.split(" "); + switch (tag) { + case "%client-session-changed": + return { kind: "client-attached", client: rest[0] ?? "" }; + case "%client-detached": + return { kind: "client-detached", client: rest[0] ?? "" }; + case "%sessions-changed": + return { kind: "sessions-changed" }; + case "%layout-change": + return { kind: "layout-change" }; + case "%output": + return { kind: "output", pane: rest[0] ?? "" }; + case "%exit": + return { kind: "exit" }; + default: + return { kind: "other", line }; + } +} + +/** Non-control clients only: the visible attachments. */ +function* clientNames(tmux: Tmux): Operation { + const listed = yield* tmux.tryRun([ + "list-clients", + "-F", + "#{client_control_mode} #{client_name}", + ]); + if (listed === undefined) { + return []; + } + return listed + .split("\n") + .map((line) => line.trim().split(" ")) + .filter((parts) => parts[0] === "0" && parts[1] !== undefined) + .map((parts) => parts[1]); +} + +function* largestPane( + tmux: Tmux, + target: string, +): Operation<{ id: string; width: number; height: number }> { + const listed = yield* tmux.run([ + "list-panes", + "-t", + target, + "-F", + "#{pane_id} #{pane_width} #{pane_height}", + ]); + let best: { id: string; width: number; height: number } | undefined; + for (const line of listed.split("\n")) { + const [id, width, height] = line.split(" "); + const candidate = { id, width: Number(width), height: Number(height) }; + if (best === undefined || candidate.width * candidate.height > best.width * best.height) { + best = candidate; + } + } + if (best === undefined) { + throw new Error("no panes listed"); + } + return best; +} + +function* paneFacts(tmux: Tmux, target: string, paneIds: string[]): Operation { + const listed = yield* tmux.run([ + "list-panes", + "-t", + target, + "-F", + "#{pane_id} #{pane_tty} #{pane_pid} #{pane_left} #{pane_top} #{pane_width} #{pane_height}", + ]); + const byId = new Map(); + for (const line of listed.split("\n")) { + const [id, tty, pid, left, top, width, height] = line.split(" "); + const ordinal = paneIds.indexOf(id); + if (ordinal < 0) { + continue; + } + byId.set(id, { + ordinal, + id, + tty, + pid: Number(pid), + cell: { + ordinal, + left: Number(left), + top: Number(top), + width: Number(width), + height: Number(height), + }, + }); + } + return paneIds.map((id) => { + const info = byId.get(id); + if (info === undefined) { + throw new Error(`pane ${id} disappeared`); + } + return info; + }); +} + +export { rowMajorCells }; diff --git a/scripts/proofs/tmux-pane-workers/worker.ts b/scripts/proofs/tmux-pane-workers/worker.ts new file mode 100644 index 00000000..fb6e8b21 --- /dev/null +++ b/scripts/proofs/tmux-pane-workers/worker.ts @@ -0,0 +1,229 @@ +/** + * The persistent pane worker: tmux's initial process in one pane. + * + * It owns the pane's terminal for the pane's whole life. Everything it does is + * asked over the private socket: display text on the pane, start one + * interactive child that inherits the terminal, cancel it, shut down. It never + * reads the terminal itself, so keystrokes reach the child and only the child. + * + * The worker is the pane's session leader and shares its process group with + * the child, so `^C` on the pane is delivered to both. The worker handles + * SIGINT, SIGQUIT and SIGTSTP by doing nothing — the child inherits default + * dispositions across `exec`, so it is the one interrupted. SIGHUP keeps its + * default: when the pane's terminal goes away, so does the worker. + * + * The program is started with `run()` rather than Effection's `main()`, which + * would bind SIGINT to its own shutdown and exit 130 on the first `^C` typed + * into the pane — the exact keystroke the child is supposed to receive. + * + * Usage (only ever as a tmux pane command): + * deno run --allow-all worker.ts + */ + +import net from "node:net"; +import process from "node:process"; +import { readTextFile, rm } from "@effectionx/fs"; +import { run, sleep, spawn, withResolvers } from "effection"; +import type { Operation } from "effection"; +import { useInteractiveProcess } from "./interactive-process.ts"; +import type { InteractiveProcess, QuiescenceProof } from "./interactive-process.ts"; +import { frames, send, socketPath, tokenPath, ToWorkerSchema } from "./ipc.ts"; +import type { FromWorker } from "./ipc.ts"; +import { deliver, holdersOf, isReachable, processFacts } from "./processes.ts"; + +interface ActiveChild { + id: string; + process: InteractiveProcess | undefined; + /** The one settlement of this child: escalation, then the terminal sweep. */ + settled: ReturnType> | undefined; +} + +/** The proof as it crosses the socket: the escalation plus the pane's sweep. */ +type WireProof = QuiescenceProof & { terminalHolders: { pid: number; gone: boolean }[] }; + +function ignoreTerminalSignals(): void { + for (const name of ["SIGINT", "SIGQUIT", "SIGTSTP"] as const) { + process.on(name, () => { + // Delivered to the whole foreground group; the child is the one it is for. + }); + } +} + +/** + * Kill whatever still holds the pane's terminal other than this worker. Runs + * after every child settles — a descendant that left the process group and + * lost its parent is outside the escalation's snapshot, and the pane is not + * free for the next child while it can still read the terminal. + */ +function* sweepTerminalHolders( + tty: string | undefined, +): Operation<{ pid: number; gone: boolean }[]> { + if (tty === undefined || tty === "??") { + return []; + } + const holders = (yield* holdersOf(`/dev/${tty}`)).filter((pid) => pid !== process.pid); + for (const pid of holders) { + deliver(pid, "SIGKILL"); + } + const deadline = Date.now() + 500; + while (Date.now() < deadline && holders.some(isReachable)) { + yield* sleep(25); + } + return holders.map((pid) => ({ pid, gone: !isReachable(pid) })); +} + +function writeOut(text: string): Operation { + const written = withResolvers(); + process.stdout.write(text, () => written.resolve()); + return written.operation; +} + +const [ordinalArg, directory] = process.argv.slice(2); +const ordinal = Number(ordinalArg); +if (!Number.isInteger(ordinal) || directory === undefined) { + process.stderr.write("usage: worker.ts \n"); + process.exit(2); +} +ignoreTerminalSignals(); + +await run(function* () { + const token = (yield* readTextFile(tokenPath(directory, ordinal))).trim(); + yield* rm(tokenPath(directory, ordinal)); + + const socket = net.createConnection(socketPath(directory, ordinal)); + const connected = withResolvers(); + socket.once("connect", () => connected.resolve()); + socket.once("error", (error: Error) => connected.reject(error)); + yield* connected.operation; + const inbound = frames(socket, (value) => ToWorkerSchema.parse(value)); + const say = (message: FromWorker) => send(socket, message); + + const facts = yield* processFacts(process.pid); + yield* say({ + type: "hello", + ordinal, + token, + pid: process.pid, + ppid: process.ppid, + pgid: facts?.pgid ?? -1, + tty: facts?.tty ?? "??", + isatty: [ + process.stdin.isTTY === true, + process.stdout.isTTY === true, + process.stderr.isTTY === true, + ], + }); + + let active: ActiveChild | undefined; + + // Escalate, then sweep the terminal, once per child however many ask: the + // launch task on exit and the main loop on cancel or shutdown both wait on + // the same settlement, and `active` clears only after it. + function* settle(entry: ActiveChild): Operation { + if (entry.settled) { + return yield* entry.settled.operation; + } + entry.settled = withResolvers(); + try { + const escalation: QuiescenceProof = entry.process + ? yield* entry.process.stop() + : { + method: "exited", + childPid: undefined, + childGone: true, + descendants: [], + survivors: [], + }; + const terminalHolders = yield* sweepTerminalHolders(facts?.tty); + const proof = { ...escalation, terminalHolders }; + if (active === entry) { + active = undefined; + } + entry.settled.resolve(proof); + return proof; + } catch (error) { + entry.settled.reject(error instanceof Error ? error : new Error(String(error))); + throw error; + } + } + + function* quiesce(): Operation { + if (active === undefined) { + return { + method: "exited", + childPid: undefined, + childGone: true, + descendants: [], + survivors: [], + terminalHolders: [], + }; + } + return yield* settle(active); + } + + while (true) { + const next = yield* inbound.next(); + if (next.done) { + break; + } + const message = next.value; + switch (message.type) { + case "welcome": + break; + case "display": + yield* writeOut(message.text); + yield* say({ type: "displayed", seq: message.seq }); + break; + case "launch": { + if (active !== undefined) { + yield* say({ type: "refused", id: message.id, reason: "busy" }); + break; + } + const entry: ActiveChild = { id: message.id, process: undefined, settled: undefined }; + active = entry; + yield* spawn(function* () { + const child = yield* useInteractiveProcess({ + command: message.argv, + cwd: message.cwd, + env: message.env, + }); + entry.process = child; + const ready = yield* child.ready; + if (!ready.ok) { + yield* say({ type: "startup-failed", id: message.id, reason: ready.error.message }); + active = undefined; + return; + } + yield* say({ type: "ready", id: message.id, pid: ready.value }); + const outcome = yield* child.exited; + // `exited` is what makes the pane free for the next child, so it + // follows the whole settlement: a child that exited on its own may + // have left descendants in the group, or an escaped orphan on the + // terminal, and a sweep running beside a new child would reach + // that child too. + const proof = yield* settle(entry); + yield* say({ type: "exited", id: message.id, ...outcome, proof }); + }); + break; + } + case "cancel": { + const proof = yield* quiesce(); + yield* say({ type: "quiescent", id: message.id, proof }); + break; + } + case "shutdown": { + const proof = yield* quiesce(); + yield* say({ type: "quiescent", proof }); + // The pane's last sweep, by the only process that can still make it: + // once this worker exits, tmux closes the pane's pty master and macOS + // revokes the slave, after which nothing can name a process that kept + // the terminal open. Every child's settlement already swept, so a + // holder here arrived between that sweep and now. + const ttyHolders = yield* sweepTerminalHolders(facts?.tty); + yield* say({ type: "bye", ttyHolders }); + socket.end(); + return; + } + } + } +}); diff --git a/scripts/proofs/tmux-pane-workers/workspace.ts b/scripts/proofs/tmux-pane-workers/workspace.ts new file mode 100644 index 00000000..3490a35d --- /dev/null +++ b/scripts/proofs/tmux-pane-workers/workspace.ts @@ -0,0 +1,298 @@ +/** + * One grid of pane workers, from the parent's point of view: the private + * directory, the sockets, the tmux composite, and an admitted link per pane, + * with every frame a worker sent kept in order so a check can wait for the + * one it means by identity rather than by position. + * + * Ownership, innermost last: + * + * workspace scope + * ├─ private directory (mode 0700; removed with the scope) + * ├─ pane sockets (servers + admitted connections; closed with the scope) + * ├─ tmux grid (server, panes, control client; `kill-server` with the scope) + * └─ one reader task per pane (halted with the scope) + * + * A worker is started by tmux, not by this process, so its lifetime is the + * pane's: `shutdown` asks it to leave, and `kill-server` takes the pane's + * terminal away from whatever is left. + */ + +import { mkdtempSync } from "node:fs"; +import { tmpdir } from "node:os"; +import { join } from "node:path"; +import process from "node:process"; +import { chmod, mkdir, rm } from "node:fs/promises"; +import { createSignal, ensure, race, resource, sleep, spawn, until } from "effection"; +import type { Operation } from "effection"; +import { usePaneSockets } from "./ipc.ts"; +import type { FromWorker, PaneLink, PaneSockets, QuiescenceProof } from "./ipc.ts"; +import { useTmuxGrid } from "./provider.ts"; +import type { PaneInfo, TmuxGrid } from "./provider.ts"; + +export type PaneEvent = FromWorker | { type: "closed" }; + +export interface WorkspaceOptions { + columns: number; + panes: number; + width?: number; + height?: number; + titles?: string[]; + /** Called as the composite comes up; a cancellation check halts here. */ + onPhase?: (phase: WorkspacePhase, facts: { directory: string; serverPid?: number }) => void; + /** Where child evidence files go; a longer path is fine here. */ + evidenceDirectory: string; +} + +export type WorkspacePhase = "sockets" | "prepared" | "workers"; + +export interface LaunchSpec { + id: string; + argv: string[]; + cwd?: string; + env?: Record; +} + +export interface Workspace { + directory: string; + sockets: PaneSockets; + grid: TmuxGrid; + links: PaneLink[]; + env: Record; + pane(ordinal: number): PaneInfo; + events(ordinal: number): PaneEvent[]; + /** Wait for the first event on `ordinal` satisfying `test`. */ + waitFor( + ordinal: number, + test: (event: PaneEvent) => event is T, + limitMs?: number, + ): Operation; + display(ordinal: number, text: string): Operation; + launch(ordinal: number, spec: LaunchSpec): Operation; + cancel(ordinal: number, id: string): Operation; + shutdown( + ordinal: number, + ): Operation<{ proof: QuiescenceProof; ttyHolders: { pid: number; gone: boolean }[] }>; + /** Everything typed into `ordinal` goes to whatever reads its terminal. */ + keys(ordinal: number, ...keys: string[]): Operation; + capture(ordinal: number): Operation; +} + +const REPO_ROOT = join(import.meta.dirname ?? ".", "..", "..", ".."); +const PROOF_DIR = import.meta.dirname ?? "."; +const DEFAULT_LIMIT_MS = 15_000; + +export class WaitTimeout extends Error { + override name = "WaitTimeout"; + constructor(ordinal: number, what: string, seen: PaneEvent[]) { + super( + `pane ${ordinal}: no ${what} within the limit; seen ${JSON.stringify(seen.map((event) => event.type))}`, + ); + } +} + +/** The environment every process in the topology receives. */ +export function filteredEnvironment(): Record { + const env: Record = {}; + for (const name of ["PATH", "HOME", "SHELL", "LANG", "TMPDIR", "USER", "LOGNAME"]) { + const value = process.env[name]; + if (value !== undefined) { + env[name] = value; + } + } + env.TERM = "xterm-256color"; + return env; +} + +export function workerCommand(directory: string): (ordinal: number) => string[] { + return (ordinal) => [ + "deno", + "run", + "--allow-all", + join(PROOF_DIR, "worker.ts"), + String(ordinal), + directory, + ]; +} + +export function childCommand(evidenceFile: string, mode: string, ...args: string[]): string[] { + return [ + "deno", + "run", + "--allow-all", + join(PROOF_DIR, "child.ts"), + "--evidence", + evidenceFile, + "--mode", + mode, + "--", + ...args, + ]; +} + +/** + * A short private directory. `tmpdir()` on macOS is already 49 characters; a + * socket path inside it must stay under 104. + */ +export function usePrivateDirectory(): Operation { + return resource(function* (provide) { + // Synchronous so nothing suspends between creating and owning it. + // oxlint-disable-next-line local/no-sync-filesystem + const directory = mkdtempSync(join(tmpdir(), "xtg-")); + yield* ensure(() => + until(rm(directory, { recursive: true, force: true }).catch(() => undefined)), + ); + yield* until(chmod(directory, 0o700)); + yield* provide(directory); + }); +} + +export function useWorkspace(options: WorkspaceOptions): Operation { + return resource(function* (provide) { + const env = filteredEnvironment(); + const directory = yield* usePrivateDirectory(); + yield* until(mkdir(options.evidenceDirectory, { recursive: true })); + const sockets = yield* usePaneSockets(directory, options.panes); + options.onPhase?.("sockets", { directory }); + const grid = yield* useTmuxGrid(directory, { + session: "grid", + columns: options.columns, + panes: options.panes, + width: options.width ?? 160, + height: options.height ?? 48, + titles: options.titles ?? Array.from({ length: options.panes }, (_, i) => `pane ${i}`), + workerCommand: workerCommand(directory), + cwd: REPO_ROOT, + env, + }); + options.onPhase?.("prepared", { directory, serverPid: grid.serverPid }); + + const links: PaneLink[] = []; + for (let ordinal = 0; ordinal < options.panes; ordinal++) { + links.push(yield* sockets.link(ordinal)); + } + options.onPhase?.("workers", { directory, serverPid: grid.serverPid }); + + const logs: PaneEvent[][] = links.map(() => []); + const signals = links.map(() => createSignal()); + for (const [ordinal, link] of links.entries()) { + yield* spawn(function* () { + while (true) { + const event = yield* link.next(); + const value: PaneEvent = event ?? { type: "closed" }; + logs[ordinal].push(value); + signals[ordinal].send(value); + if (event === undefined) { + return; + } + } + }); + } + + let seq = 0; + + function* waitFor( + ordinal: number, + test: (event: PaneEvent) => event is T, + limitMs: number = DEFAULT_LIMIT_MS, + ): Operation { + // Subscribe before scanning, so an event between the scan and the wait + // is not lost. + const subscription = yield* signals[ordinal]; + const already = logs[ordinal].find(test); + if (already) { + return already; + } + const found = yield* race([ + (function* (): Operation { + while (true) { + const next = yield* subscription.next(); + if (next.done) { + return undefined; + } + if (test(next.value)) { + return next.value; + } + } + })(), + (function* (): Operation { + yield* sleep(limitMs); + return undefined; + })(), + ]); + if (found === undefined) { + throw new WaitTimeout(ordinal, test.name || "event", logs[ordinal]); + } + return found; + } + + yield* provide({ + directory, + sockets, + grid, + links, + env, + pane: (ordinal) => grid.panes[ordinal], + events: (ordinal) => [...logs[ordinal]], + waitFor, + *display(ordinal, text) { + const mine = ++seq; + yield* links[ordinal].send({ type: "display", seq: mine, text }); + yield* waitFor( + ordinal, + (event): event is PaneEvent & { type: "displayed" } => + event.type === "displayed" && event.seq === mine, + ); + }, + *launch(ordinal, spec) { + yield* links[ordinal].send({ + type: "launch", + id: spec.id, + argv: spec.argv, + cwd: spec.cwd ?? REPO_ROOT, + env: spec.env ?? env, + }); + }, + *cancel(ordinal, id) { + yield* links[ordinal].send({ type: "cancel", id }); + return yield* waitFor( + ordinal, + (event): event is PaneEvent & { type: "quiescent" } => + isQuiescent(event) && event.id === id, + ); + }, + *shutdown(ordinal) { + yield* links[ordinal].send({ type: "shutdown" }); + const quiescent = yield* waitFor( + ordinal, + (event): event is PaneEvent & { type: "quiescent" } => + isQuiescent(event) && event.id === undefined, + ); + const bye = yield* waitFor(ordinal, isType("bye")); + yield* waitFor(ordinal, isType("closed")); + return { proof: quiescent.proof, ttyHolders: bye.ttyHolders }; + }, + *keys(ordinal, ...keys) { + yield* grid.tmux.run(["send-keys", "-t", grid.panes[ordinal].id, ...keys]); + }, + *capture(ordinal) { + return yield* grid.tmux.run(["capture-pane", "-p", "-J", "-t", grid.panes[ordinal].id]); + }, + }); + }); +} + +function isQuiescent(event: PaneEvent): event is PaneEvent & { type: "quiescent" } { + return event.type === "quiescent"; +} + +export function isType(type: K) { + return (event: PaneEvent): event is Extract => event.type === type; +} + +export function isLaunchEvent( + type: K, + id: string, +) { + return (event: PaneEvent): event is Extract => + event.type === type && "id" in event && event.id === id; +}