docs(process): framing revision 3 — close review round 2
Three blocking and three major findings, all accepted, all verified in the code before acceptance. - The PTY errno proposal is withdrawn. `nix::unistd::tcgetpgrp` needs `F: AsFd`; `MasterPty` exposes only `Option<RawFd>`; every route from a raw fd to `AsFd` is unsafe and the crate forbids unsafe. The claim is reduced to distinguishing the fallback without the errno. - Revision 2 called `getpgid` ungated. It is not: the gate is a block-level `feature!` opened 168 lines above the function, and rev 2 read the four lines immediately above it. Both calls are available because nix's own `signal` feature depends on `process`, verified with `cargo tree` and by compiling them. The lane now declares `process` explicitly rather than inheriting it. - Bet 4's `setsid` fixture was impossible: a `spec.group` child is already a process-group leader and a group leader's `setsid` fails with EPERM. Replaced with a `setpgid`-into-an-existing-group fixture with a readiness handshake and explicit cleanup. - "Recoverable" is withdrawn. `tick_reap_ledger` drops its entry on any probe error — including the EPERM this occurrence proves reachable — and discards the SIGKILL result while marking the entry killed. The claim is now that escalation remains scheduled, and that still-silent path is parked as its own lane. - Revision 2 falsified the wrong sentence. Stage A's disjointness claim was about the PTY path and remains true; what the occurrence falsifies is the ledger's own EPERM comment. - Failed SIGUSR1 and SIGTERM are disposition-identical, because every failed kill returns before the fatal-signal branch. Acceptance 3 now separates the failure-format comparison from a successful-call disposition control. - Bet 5 proposed a test that already exists at src/process.rs:2501. It is cited as ground truth and retained, not invented. No code changes. Framing only, awaiting review round 3.
This commit is contained in:
parent
76cb13bda8
commit
872e4aacad
|
|
@ -1,107 +1,120 @@
|
||||||
# Framing — make the signal diagnostic discriminating (evidence collection)
|
# Framing — make the signal diagnostic discriminating (evidence collection)
|
||||||
|
|
||||||
**Revision 2.** Status: awaiting review round 2. Lane:
|
**Revision 3.** Status: awaiting review round 3. Lane:
|
||||||
`process-signal-diagnostic-completeness`, worktree
|
`process-signal-diagnostic-completeness`, worktree
|
||||||
`../pmacs-signal-identity`, based on `githubsucks/main` @ `391d38a`.
|
`../pmacs-signal-identity`, based on `githubsucks/main` @ `4cd4a7b`
|
||||||
|
(re-measure at branch time; this is a reading, not a constant).
|
||||||
|
|
||||||
**This is Stage B of the lane whose Stage A merged as PR #176**
|
**This is Stage B of the lane whose Stage A merged as PR #176**
|
||||||
(`docs/process-signal-tolerance-framing.md`, revision 4). Stage A made a
|
(`docs/process-signal-tolerance-framing.md`, revision 4). Stage A made a
|
||||||
failing `kill` self-describing and parked every tolerance rule behind one
|
failing `kill` self-describing and parked every tolerance rule behind
|
||||||
condition: evidence. Evidence has arrived (§1.2). It does not support any
|
evidence. Evidence arrived (§1.2). It supports none of the parked rules,
|
||||||
of the parked rules, and — per review round 1 — it does not support an
|
no identity claim, and — per review round 2 — no claim that today's
|
||||||
identity claim either.
|
escalation path is safe.
|
||||||
|
|
||||||
**Evidence collection only. No tolerance rule, no change to which
|
**Evidence collection only. No tolerance rule, no change to which process
|
||||||
process gets signalled, no disposition change.** Everything behavioural
|
gets signalled, no disposition change.** Everything behavioural is in §5.
|
||||||
is parked in §5.
|
|
||||||
|
|
||||||
## Revision history
|
## Revision history
|
||||||
|
|
||||||
**Revision 1 → 2**, after review round 1 (two blocking, two major). All
|
**Revision 2 → 3**, after review round 2 (three blocking, three major).
|
||||||
four accepted; all four verified against the code before acceptance.
|
All six accepted; all six verified in the code before acceptance.
|
||||||
|
|
||||||
- **Rev 1 proposed measuring the pgid and then *targeting* it.** That is
|
- **The PTY errno proposal had no safe fd bridge.** Withdrawn and reduced
|
||||||
a behavioural change resting on an identity claim a numeric pgid cannot
|
(§1.6). This was rev 2's central new proposal and it does not survive
|
||||||
support (§1.5). Retargeting is parked (§5); this lane only *records*.
|
`#![forbid(unsafe_code)]`.
|
||||||
- **Rev 1 repeated the defect it was written to fix.** Its Bet 1 asserted
|
- **Rev 2 said `getpgid` was "ungated". It is not** (§1.5a). The claim
|
||||||
`getpgid(child) == pid`, which an implementation that ignored `getpgid`
|
came from reading the four lines above the function; the gate is a
|
||||||
and returned `pid` would satisfy — the same non-discrimination the
|
block-level `feature!` opened 168 lines earlier. Same error shape as
|
||||||
review found in the landed acceptance (§1.4). Every measurement in this
|
the truncated-output trap already in the handoff, committed inside a
|
||||||
revision now requires a case where the two values **differ**.
|
document about non-discriminating evidence.
|
||||||
- **Rev 1 scoped the PTY path out.** Review showed the PTY fallback is
|
- **Bet 4's `setsid` fixture was impossible** (§3, Bet 4). A `spec.group`
|
||||||
indistinguishable from a normal pipe child in the report (§1.6), which
|
child is already a process-group leader, and a group leader's `setsid`
|
||||||
is a defect in the diagnostic this lane owns. Scope now includes it,
|
fails with EPERM.
|
||||||
and the rev 1 sentence "this lane does not touch the PTY path" is
|
- **"Recoverable" was unsupported** (§1.8). The ledger drops its entry on
|
||||||
withdrawn.
|
*any* probe error — including the EPERM this occurrence proves can
|
||||||
- **Rev 1 never noticed the report omits the signal** (§1.7).
|
happen — and discards the `SIGKILL` result while marking the entry
|
||||||
|
killed.
|
||||||
|
- **Rev 2 falsified the wrong Stage A sentence** (§1.3). Stage A's
|
||||||
|
disjointness claim was about the **PTY** path and remains true.
|
||||||
|
- **Rev 2's signal-disposition argument was wrong** (§1.7). Failed
|
||||||
|
signals are all disposition-identical.
|
||||||
|
- **Bet 5 proposed a test that already exists** (§1.9). Cited as ground
|
||||||
|
truth now, not invented.
|
||||||
|
|
||||||
**Rev 1 also mis-stated where the lane lived.** It was written to a
|
**Revision 1 → 2**, after review round 1 (two blocking, two major); all
|
||||||
session scratchpad, which is not portable and was not on `githubsucks`,
|
accepted. Rev 1 proposed *retargeting* to a measured pgid — a behavioural
|
||||||
so review round 1 necessarily landed on Stage A's revision 4 instead.
|
change resting on an identity claim a number cannot support; it asserted
|
||||||
That is why round 1's line references point at the merged document. The
|
`getpgid(child) == pid`, which an implementation ignoring `getpgid` would
|
||||||
findings apply regardless — three of the four are defects in code that is
|
satisfy; it scoped the PTY path out; and it never noticed the report
|
||||||
on `main` right now — but the process error is recorded here because
|
omits the signal.
|
||||||
"work is portable only after it is committed and pushed" is a standing
|
|
||||||
project rule and this lane broke it on its first step.
|
**Rev 1 was written to a session scratchpad rather than a branch**, so it
|
||||||
|
was never on `githubsucks` and review round 1 necessarily landed on
|
||||||
|
Stage A's merged document. Recorded because "work is portable only after
|
||||||
|
it is committed and pushed" is a standing rule this lane broke on its
|
||||||
|
first step.
|
||||||
|
|
||||||
|
|
||||||
## 0. Coherence impact (COHERENCE §20)
|
## 0. Coherence impact (COHERENCE §20)
|
||||||
|
|
||||||
- **Journey step 8, "Open a terminal"** (§2), teardown half, plus every
|
- **Journey step 8, "Open a terminal"** (§2), teardown half, plus every
|
||||||
compile/grep run through `spec.group`. **No grade change and no
|
compile/grep run through `spec.group`. **No grade change, no
|
||||||
behavioural change.**
|
behavioural change.**
|
||||||
- **Serves §9 (worker model), failure attribution.** Stage A made the
|
- **Serves §9 (worker model), failure attribution.** Stage A made the
|
||||||
failure describe itself; this lane makes the description
|
failure describe itself; this lane makes the description
|
||||||
*discriminating* — today several distinct failures render identically.
|
*discriminating*, because several distinct failures render identically
|
||||||
|
today.
|
||||||
- **Interaction islands: none. Config registry: not adopted.
|
- **Interaction islands: none. Config registry: not adopted.
|
||||||
Background-work attribution: unchanged.**
|
Background-work attribution: unchanged.**
|
||||||
- **No audited claim in COHERENCE.md changes**, so under §25 no
|
- **No audited claim in COHERENCE.md changes**; under §25 no COHERENCE
|
||||||
COHERENCE edit rides this PR.
|
edit rides this PR.
|
||||||
|
|
||||||
|
|
||||||
## 1. Ground truth (verified at `391d38a`)
|
## 1. Ground truth (verified at `4cd4a7b`)
|
||||||
|
|
||||||
### 1.1 Stage A landed and has now fired
|
### 1.1 Stage A landed and has now fired
|
||||||
|
|
||||||
`signal_failure_report` and `LeaderObservation` merged as **PR #176 on
|
`signal_failure_report` and `LeaderObservation` merged as **PR #176 on
|
||||||
2026-07-26** (`62316a9`). The occurrence below is the first failure
|
2026-07-26** (`62316a9`). §1.2 is the first failure carrying the new
|
||||||
carrying the new format rather than a bare errno. Stage A is the reason
|
format rather than a bare errno. Stage A is why this document can exist.
|
||||||
this document can exist.
|
|
||||||
|
|
||||||
### 1.2 The new occurrence, verbatim
|
### 1.2 The new occurrence, verbatim
|
||||||
|
|
||||||
PR #191, `Test (macos-latest / lua54)`,
|
PR #191, `Test (macos-latest / lua54)`,
|
||||||
[run 30553376486](https://github.com/levineuwirth/pmacs/actions/runs/30553376486/job/90907461258),
|
[run 30553376486](https://github.com/levineuwirth/pmacs/actions/runs/30553376486/job/90907461258),
|
||||||
`process::tests::repeated_terminate_does_not_extend_ledger_deadline`.
|
`process::tests::repeated_terminate_does_not_extend_ledger_deadline`.
|
||||||
1873 passed, 1 failed. **The rerun of the identical head passed 12/12**,
|
1873 passed, 1 failed. **A rerun of the identical head passed 12/12**, so
|
||||||
so the failure is intermittent, not deterministic:
|
the failure is intermittent, not deterministic:
|
||||||
|
|
||||||
```
|
```
|
||||||
re-terminate: "kill: EPERM: Operation not permitted
|
re-terminate: "kill: EPERM: Operation not permitted
|
||||||
(target=-8619 via group, leader_pid=8619, expected_group=-8619, leader=live)"
|
(target=-8619 via group, leader_pid=8619, expected_group=-8619, leader=live)"
|
||||||
```
|
```
|
||||||
|
|
||||||
Established: the target source is `group` (the `spec.group` pipe path,
|
Established: the target source is `group` — the `spec.group` pipe path
|
||||||
`signal_target` `:774-780`; `sh_group_spec` `:3402` sets it), **not** the
|
(`signal_target` `:774-780`; `sh_group_spec` `:3402`) — **not** the PTY
|
||||||
PTY path; and `leader=live`, from a real `try_wait` against the real
|
path; and `leader=live`, from a real `try_wait` against the real child,
|
||||||
child, so the leader had not exited and had not been reaped.
|
so the leader had neither exited nor been reaped.
|
||||||
|
|
||||||
### 1.3 Two written premises are falsified
|
### 1.3 What is actually falsified
|
||||||
|
|
||||||
- **`src/process.rs:1246-1247`** — `tick_reap_ledger` justifies treating
|
- **`src/process.rs:1246-1247` is falsified.** `tick_reap_ledger`
|
||||||
any probe error as "nothing left we can reach" with the comment
|
justifies treating any probe error as "nothing left we can reach" with
|
||||||
"**EPERM cannot happen for our own children**". §1.2 is a
|
the comment "**EPERM cannot happen for our own children**". §1.2 is a
|
||||||
counterexample: our own child, alive, EPERM.
|
counterexample: our own child, alive, EPERM.
|
||||||
- **Stage A §1.3** — "the reap ledger is disjoint from this path", on the
|
- **Stage A §1.3 is *not* falsified.** It said the ledger is disjoint
|
||||||
grounds that the ledger arms only for `proc.spec.group` and PTY mode
|
from **the PTY path**, because the ledger arms only for
|
||||||
cannot set it. §1.2's process **is** a `spec.group` process. Not
|
`proc.spec.group` and PTY mode cannot set it. That remains true. §1.2
|
||||||
disjoint.
|
is the separate `spec.group` path. Rev 2 conflated "this path" with
|
||||||
|
"the signal path generally" and claimed a falsification it had not
|
||||||
|
made.
|
||||||
|
|
||||||
Stage A's §1.2 entity-split analysis concerns the PTY path, where the
|
Stage A's entity-split analysis concerns the PTY path, where the target
|
||||||
target is read from `tcgetpgrp`. **It does not apply to §1.2's
|
is read from `tcgetpgrp`. It does not apply to §1.2, where the target is
|
||||||
occurrence**, where the target is computed as `-leader_pid` with no read.
|
computed as `-leader_pid` with no read at all.
|
||||||
|
|
||||||
### 1.4 The landed acceptance cannot discriminate (round 1, P1)
|
### 1.4 The landed acceptance cannot discriminate
|
||||||
|
|
||||||
`a_group_directed_kill_failure_reports_target_and_leader_separately`
|
`a_group_directed_kill_failure_reports_target_and_leader_separately`
|
||||||
(`:2400`) spawns a PTY child and asserts the exact string
|
(`:2400`) spawns a PTY child and asserts the exact string
|
||||||
|
|
@ -111,50 +124,71 @@ target=-{pid} via tcgetpgrp, leader_pid={pid}, expected_group=-{pid}, leader=liv
|
||||||
```
|
```
|
||||||
|
|
||||||
— the same `pid` three times. **An implementation that ignored
|
— the same `pid` three times. **An implementation that ignored
|
||||||
`tcgetpgrp` entirely and substituted `leader_pid` would pass.** The test's
|
`tcgetpgrp` and substituted `leader_pid` would pass.** The test's own doc
|
||||||
own doc comment concedes it: "here they are asserted to agree only
|
comment concedes it: "here they are asserted to agree only because
|
||||||
because nothing has moved the terminal."
|
nothing has moved the terminal." The premise of the diagnostic is that
|
||||||
|
these entities can diverge, and nothing exercises a case where they do.
|
||||||
|
|
||||||
The premise of the whole diagnostic is that these two entities can
|
### 1.5 A numeric pgid cannot establish identity
|
||||||
diverge, and no test exercises a case where they do. This is the
|
|
||||||
vacuous-assertion family already recorded in the handoff.
|
|
||||||
|
|
||||||
### 1.5 A numeric pgid cannot establish identity (round 1, P1)
|
The value is read before `kill`, the window remains open, and a *number*
|
||||||
|
cannot distinguish the original group from a recycled one.
|
||||||
|
|
||||||
Rev 1 proposed reading the real pgid and targeting it. Review is right
|
**No portable mechanism closes this.** `pidfd_open` + `pidfd_send_signal`
|
||||||
that this does not establish identity: the value is read before `kill`,
|
close pid reuse for a single *process* on Linux; there is no
|
||||||
the read-then-kill window remains, and a *number* cannot distinguish the
|
process-*group* equivalent, and macOS has no pidfd. The failures are
|
||||||
original group from a recycled one.
|
macOS-only, so nothing available makes group signalling identity-safe.
|
||||||
|
|
||||||
**There is no portable mechanism that closes this.** `pidfd_open` +
|
**This lane therefore records and does not retarget.** No acceptance
|
||||||
`pidfd_send_signal` close pid reuse for a single *process* on Linux;
|
claims the telemetry is sufficient.
|
||||||
there is no process-*group* equivalent, and macOS has no pidfd at all.
|
|
||||||
Since the failures are macOS-only so far, no available mechanism makes
|
|
||||||
group signalling identity-safe.
|
|
||||||
|
|
||||||
**Therefore this lane records and does not retarget.** Acceptance
|
One narrowing fact, stated as narrowing and **not** as identity: POSIX
|
||||||
criteria state what was observed, never that the observation is
|
does not free a child's pid until the parent reaps it, and §1.2 observed
|
||||||
sufficient.
|
`leader=live` from a `try_wait` that had not reaped. While that pid is
|
||||||
|
held, no *new* group can be created bearing that pgid value. This makes
|
||||||
|
recycling an unlikely explanation **for that one occurrence**, and says
|
||||||
|
nothing about whether the group still held a signallable member — which
|
||||||
|
is what EPERM actually turns on.
|
||||||
|
|
||||||
One narrowing fact, stated because it constrains the hypothesis space
|
### 1.5a The nix surface is gated, and available for a non-obvious reason
|
||||||
and *not* as an identity claim: POSIX does not free a child's pid until
|
|
||||||
the parent reaps it, and §1.2 observed `leader=live` from a `try_wait`
|
|
||||||
that had not reaped. While that pid is held, no other process can be
|
|
||||||
assigned it, so no *new* group can be created bearing that pgid value
|
|
||||||
during the window. This narrows recycling as a candidate **for that one
|
|
||||||
occurrence**; it says nothing about whether the group still contained a
|
|
||||||
signallable member, which is the question EPERM actually turns on.
|
|
||||||
|
|
||||||
### 1.6 The PTY fallback is invisible in the report (round 1, P2)
|
Both calls this lane would use live inside block-level gates:
|
||||||
|
|
||||||
|
- `getpgid` (`nix-0.29.0/src/unistd.rs:335`) is inside
|
||||||
|
`feature! { #![feature = "process"] }` opened at `:167`.
|
||||||
|
- `tcgetpgrp` (`:368`) is inside
|
||||||
|
`feature! { #![all(feature = "process", feature = "term")] }` at `:360`.
|
||||||
|
|
||||||
|
pmacs declares `nix` with `features = ["signal", "user", "fs", "term",
|
||||||
|
"socket", "poll"]` — **`process` is not listed**. It is enabled anyway
|
||||||
|
because **nix's own `signal` feature depends on `process`**, verified
|
||||||
|
with `cargo tree -e features -i nix:0.29.0`:
|
||||||
|
|
||||||
|
```
|
||||||
|
├── nix feature "process"
|
||||||
|
│ └── nix feature "signal"
|
||||||
|
│ └── pmacs v1.0.0
|
||||||
|
```
|
||||||
|
|
||||||
|
Confirmed by compiling both calls against the real dependency graph.
|
||||||
|
|
||||||
|
**This is stable but implicit.** The lane adds `process` to pmacs' own
|
||||||
|
feature list so the dependency is declared rather than inherited — a
|
||||||
|
one-line change that makes a real requirement visible.
|
||||||
|
|
||||||
|
*Rev 2 asserted `getpgid` was "ungated", from reading the four lines
|
||||||
|
above it. The gate was 168 lines up. Recorded because it is the same
|
||||||
|
defect class this document exists to fix.*
|
||||||
|
|
||||||
|
### 1.6 The PTY fallback is invisible, and the errno cannot be recovered
|
||||||
|
|
||||||
`signal_target` (`:757-785`): when the PTY branch's
|
`signal_target` (`:757-785`): when the PTY branch's
|
||||||
`master.process_group_leader()` returns `None`, control falls through —
|
`master.process_group_leader()` returns `None`, control falls through —
|
||||||
`spec.group` is rejected at spawn for PTY mode — and returns
|
`spec.group` is rejected at spawn for PTY mode — and returns
|
||||||
`TargetSource::LeaderPid`, rendered "leader-pid" (`:738`). **A normal
|
`TargetSource::LeaderPid`, rendered "leader-pid" (`:738`). **A normal
|
||||||
pipe child renders identically.** Two different situations, one string.
|
pipe child renders identically.** Two situations, one string.
|
||||||
|
|
||||||
`portable-pty`'s implementation
|
`portable-pty` (`portable-pty-0.9.0/src/unix.rs:374`) discards the errno:
|
||||||
(`portable-pty-0.9.0/src/unix.rs:374`) is:
|
|
||||||
|
|
||||||
```rust
|
```rust
|
||||||
fn process_group_leader(&self) -> Option<libc::pid_t> {
|
fn process_group_leader(&self) -> Option<libc::pid_t> {
|
||||||
|
|
@ -165,155 +199,193 @@ fn process_group_leader(&self) -> Option<libc::pid_t> {
|
||||||
}
|
}
|
||||||
```
|
```
|
||||||
|
|
||||||
The errno is discarded, so "the tty has no foreground group" and
|
**Rev 2 proposed calling `nix::unistd::tcgetpgrp` ourselves to keep the
|
||||||
"`tcgetpgrp` failed" are already merged before pmacs sees the result.
|
errno. That is withdrawn.** `tcgetpgrp` requires `F: AsFd`, and
|
||||||
|
`MasterPty` exposes only `fn as_raw_fd(&self) -> Option<RawFd>`
|
||||||
|
(`portable-pty-0.9.0/src/lib.rs:114`). Every route from a `RawFd` to
|
||||||
|
something implementing `AsFd` — `BorrowedFd::borrow_raw`,
|
||||||
|
`OwnedFd::from_raw_fd`, `File::from_raw_fd` — is `unsafe`, and the crate
|
||||||
|
is `#![forbid(unsafe_code)]`. There is no safe bridge, and duplicating
|
||||||
|
the fd does not create one because the duplication itself needs the same
|
||||||
|
unsafe conversion.
|
||||||
|
|
||||||
**`nix::unistd::tcgetpgrp` returns `Result<Pid>`** (`nix-0.29.0/src/unistd.rs:368`,
|
**Reduced claim:** the fallback is distinguished **without** the errno.
|
||||||
ungated, and `pub mod unistd` at `lib.rs:183` is unconditional), so pmacs
|
`None` is all pmacs can observe, and the report says exactly that. The
|
||||||
can make this call itself and keep the errno **without `unsafe`** — which
|
errno is recorded here as unavailable-by-construction so a later lane
|
||||||
matters because the crate is `#![forbid(unsafe_code)]`.
|
does not re-propose it.
|
||||||
|
|
||||||
### 1.7 The report omits which signal failed (round 1, P2)
|
### 1.7 The report omits which signal failed
|
||||||
|
|
||||||
`signal_failure_report` (`:830-850`) takes target, leader pid, errno and
|
`signal_failure_report` (`:830-850`) takes target, leader pid, errno and
|
||||||
leader observation. **Not the signal.** `signal` (`:1074`) has it.
|
leader observation — **not the signal**. `signal` (`:1074`) has it, and
|
||||||
|
the public Lua surface accepts INT, USR1, USR2 and QUIT besides the fatal
|
||||||
|
three (`src/lua_bindings/mod.rs:8627-8629`). A failed `SIGUSR1` and a
|
||||||
|
failed `SIGTERM` are today textually indistinguishable.
|
||||||
|
|
||||||
This is not cosmetic: `signal` transitions state and arms the reap ledger
|
**Rev 2 justified this by claiming their dispositions differ. That was
|
||||||
only for `SIGTERM | SIGKILL | SIGHUP` (`:1099-1116`), and the public Lua
|
wrong.** `signal` returns `Err` at `:1092-1098`, *before* the fatal-signal
|
||||||
surface accepts INT, USR1, USR2 and QUIT as well (`src/lua_bindings/mod.rs:8627-8629`).
|
branch at `:1099`, so **every failed kill is disposition-identical**
|
||||||
A failed `SIGUSR1` and a failed `SIGTERM` have different consequences and
|
regardless of signal. The disposition difference is real only for
|
||||||
currently produce indistinguishable text.
|
**successful** calls. The reporting gap stands on its own: you cannot
|
||||||
|
tell which signal failed. Acceptance 3 separates the two.
|
||||||
|
|
||||||
### 1.8 The disposition consequence, worse for the first call
|
### 1.8 The disposition consequence, and why "recoverable" was wrong
|
||||||
|
|
||||||
`signal` returns `Err` **before** the state transition and **before**
|
`signal` returns `Err` **before** the state transition and **before**
|
||||||
arming the ledger:
|
arming the ledger:
|
||||||
|
|
||||||
| Which `terminate` hits EPERM | Consequence |
|
| Which `terminate` hits EPERM | Consequence |
|
||||||
|---|---|
|
|---|---|
|
||||||
| A **later** one (§1.2's case) | Caller sees `Err`; state already `Exiting`, ledger already armed, so SIGKILL escalation still happens. |
|
| A **later** one (§1.2's case) | Caller sees `Err`. State is already `Exiting` and a ledger entry **remains scheduled**. |
|
||||||
| The **first** one | State stays `Running`, ledger never armed. **No escalation is ever scheduled** — the child is abandoned. |
|
| The **first** one | State stays `Running`, ledger never armed. **No escalation is ever scheduled** — the child is abandoned. |
|
||||||
|
|
||||||
Only the recoverable variant has been observed. This lane **pins** the
|
**Rev 2 called the first row "recoverable" and claimed "SIGKILL
|
||||||
first-call variant and changes nothing about it (§5).
|
escalation still happens". Unsupported.** `tick_reap_ledger`
|
||||||
|
(`:1249-1254`):
|
||||||
|
|
||||||
### 1.9 Limits of the evidence
|
```rust
|
||||||
|
if nix::sys::signal::kill(Pid::from_raw(-*pgid), None).is_err() {
|
||||||
|
return false; // drops on ANY error, incl. EPERM
|
||||||
|
}
|
||||||
|
if now >= entry.deadline && !entry.killed {
|
||||||
|
let _ = nix::sys::signal::kill(..., Some(Signal::SIGKILL)); // result discarded
|
||||||
|
entry.killed = true; // marked killed regardless
|
||||||
|
}
|
||||||
|
```
|
||||||
|
|
||||||
- **Not reproduced locally.** Development is Linux; the failures are
|
Since §1.3 falsifies the premise that EPERM cannot occur here, an EPERM
|
||||||
macOS-only. No claim in this lane rests on a local repro of the EPERM.
|
probe **drops the entry and cancels escalation silently**, and a failed
|
||||||
- **Frequency: two occurrences, in different paths** — PR #172 was the
|
`SIGKILL` is recorded as if it succeeded. So the honest statement is that
|
||||||
PTY path (`acc28`, luajit), §1.2 the group path (lua54). This is not
|
escalation remains *scheduled*, not that it happens.
|
||||||
one flaky test.
|
|
||||||
|
**This still-silent path is parked, explicitly** (§5) rather than
|
||||||
|
absorbed: it is a second site with its own disposition questions, and
|
||||||
|
folding it in would repeat Stage A rev 3's error of implementing Stage B
|
||||||
|
inside Stage A.
|
||||||
|
|
||||||
|
### 1.9 The first-call variant is already pinned
|
||||||
|
|
||||||
|
`an_injected_failure_changes_no_state_and_arms_no_ledger` (`:2501`)
|
||||||
|
already spawns a `spec.group` child, injects EPERM on the **first**
|
||||||
|
`terminate`, and asserts `Running` plus an empty ledger. **Rev 2's Bet 5
|
||||||
|
proposed inventing it.** It is ground truth, and its exact-string
|
||||||
|
assertion (`:2517`) is one of the four sites acceptance 5 must update.
|
||||||
|
|
||||||
|
### 1.10 Limits of the evidence
|
||||||
|
|
||||||
|
- **Not reproduced locally.** Development is Linux; failures are
|
||||||
|
macOS-only. No claim rests on a local repro of the EPERM.
|
||||||
|
- **Two occurrences, in different paths** — PR #172 was the PTY path
|
||||||
|
(`acc28`, luajit), §1.2 the group path (lua54). Not one flaky test.
|
||||||
- **The mechanism is not established**, and this lane does not propose
|
- **The mechanism is not established**, and this lane does not propose
|
||||||
one. That is the point of the split.
|
one.
|
||||||
|
|
||||||
|
|
||||||
## 2. Questions
|
## 2. Questions
|
||||||
|
|
||||||
- **Q#DC1** — Can the two entities be made to diverge in a test? *Yes:
|
- **Q#DC1** — Can the two entities be made to diverge in a test? *Yes:
|
||||||
under a PTY with job control enabled, a shell places a background job
|
under a PTY with job control on, a shell places a background job in its
|
||||||
in its own process group and hands it the terminal, so `tcgetpgrp` !=
|
own process group and gives it the terminal, so `tcgetpgrp` != leader
|
||||||
leader pid. §3 Bet 1 builds exactly that.*
|
pid.*
|
||||||
- **Q#DC2** — Should the PTY fallback get its own `TargetSource`?
|
- **Q#DC2** — Should the PTY fallback get its own `TargetSource`?
|
||||||
*Proposed: yes, and pmacs should call `nix::unistd::tcgetpgrp` itself so
|
*Proposed: yes, reporting only that the lookup yielded `None` (§1.6).*
|
||||||
the fallback can report the errno rather than inheriting portable-pty's
|
- **Q#DC3** — Should the report name the signal? *Proposed: yes, on the
|
||||||
discarded `None`.*
|
reporting argument alone (§1.7).*
|
||||||
- **Q#DC3** — Should the report name the signal? *Proposed: yes, with a
|
|
||||||
contrasting non-fatal signal tested.*
|
|
||||||
- **Q#DC4** — Should the measured pgid be reported for `spec.group`
|
- **Q#DC4** — Should the measured pgid be reported for `spec.group`
|
||||||
children? *Proposed: yes, as an observation clearly distinct from the
|
children? *Proposed: yes, as an observation distinct from the assumed
|
||||||
assumed value, and with no claim of sufficiency (§1.5).*
|
value, with no sufficiency claim (§1.5).*
|
||||||
- **Q#DC5** — Should anything be retargeted or tolerated? **No. Parked.**
|
- **Q#DC5** — Retarget or tolerate anything? **No. Parked.**
|
||||||
|
|
||||||
|
|
||||||
## 3. Bets
|
## 3. Bets
|
||||||
|
|
||||||
Each bet names what falsifies it and what falsification teaches.
|
|
||||||
|
|
||||||
- **Bet 1 — the divergence is constructible.** A PTY fixture where the
|
- **Bet 1 — the divergence is constructible.** A PTY fixture where the
|
||||||
foreground group is *not* the leader: job control on, a background job
|
foreground group is not the leader: job control on, a background job
|
||||||
given the terminal. The rewritten acceptance asserts both exact values
|
given the terminal. The rewritten acceptance asserts both exact values
|
||||||
and that they **differ**.
|
**and that they differ**.
|
||||||
- *Falsified if* the fixture cannot be made deterministic in CI (shell
|
- *Falsified if* the fixture cannot be made deterministic in CI. Then
|
||||||
job-control timing). Then the lane says so and falls back to pinning
|
the lane falls back to pinning divergence at the `signal_target` unit
|
||||||
divergence at the `signal_target` unit level with an injected
|
level with an injected foreground group, and labels that as weaker.
|
||||||
foreground group, which is weaker and must be labelled as weaker.
|
- Without this the diagnostic remains unverified in the only case it
|
||||||
- This is the finding that matters most: without it, the entire
|
exists for.
|
||||||
diagnostic remains unverified in the only case it exists for.
|
|
||||||
|
|
||||||
- **Bet 2 — the PTY fallback is reachable and distinguishable.** A test
|
- **Bet 2 — the PTY fallback is reachable and distinguishable.** A test
|
||||||
drives the branch where the foreground-group lookup fails and asserts a
|
drives the branch where the lookup returns `None` and asserts a source
|
||||||
source string distinct from a pipe child's.
|
string distinct from a pipe child's.
|
||||||
- *Falsified if* the branch cannot be reached without faking the
|
- *Falsified if* the branch cannot be reached without faking the
|
||||||
lookup. Then the seam is made injectable exactly as Stage A made the
|
lookup — in which case the seam is made injectable exactly as Stage A
|
||||||
kill injectable (Q#PD4), and that is stated rather than hidden.
|
made the kill injectable (Q#PD4), stated rather than hidden.
|
||||||
|
|
||||||
- **Bet 3 — naming the signal is free.** Thread `signal` into the report.
|
- **Bet 3 — naming the signal is free.** Thread `signal` into the report.
|
||||||
- *Falsified if* any existing exact-string test cannot be updated
|
- *Falsified if* any exact-string test cannot be updated mechanically.
|
||||||
mechanically. Those four sites (`:2408`, `:2435`, `:2485`, `:2517`)
|
|
||||||
are the highest-risk part of the diff: **a wholesale rewrite of
|
|
||||||
expected strings is how a format regression hides**, so each is
|
|
||||||
updated individually and listed in the PR body with before and after.
|
|
||||||
|
|
||||||
- **Bet 4 — the measured pgid can disagree with the assumed one, and the
|
- **Bet 4 — a `spec.group` child's measured pgid can be made to differ
|
||||||
test proves the measurement is real.** A child that calls `setsid`, so
|
from its pid.** **Not via `setsid`:** `spec.group` sets
|
||||||
its pgid is genuinely not its parent-assumed value, is measured and the
|
`process_group(0)` before exec, so the recorded child is already a
|
||||||
two values asserted **different**.
|
process-group leader, and a group leader's `setsid` fails with EPERM.
|
||||||
- *Falsified if* no such case can be built — in which case the
|
Forking a `setsid` helper does not help either — `getpgid(recorded_pid)`
|
||||||
measurement is unfalsifiable and should not ship, exactly per §1.4's
|
still observes the wrapper.
|
||||||
lesson.
|
The fixture instead has the recorded child **`setpgid` into another
|
||||||
|
existing group in the same session**, with a readiness handshake before
|
||||||
- **Bet 5 — §1.8's first-call abandonment is real.** Inject EPERM on the
|
the measurement and explicit cleanup of the anchor group afterwards.
|
||||||
*first* terminate; assert no ledger entry and state still `Running`.
|
- *Falsified if* no such fixture is deterministic — in which case the
|
||||||
- *Falsified if* the ledger is armed anyway, meaning §1.8 misreads
|
measurement is unfalsifiable and **does not ship**, per §1.4's lesson.
|
||||||
`signal`.
|
|
||||||
- **Pins current behaviour; does not fix it.**
|
|
||||||
|
|
||||||
|
|
||||||
## 4. Acceptance
|
## 4. Acceptance
|
||||||
|
|
||||||
1. A PTY job-control fixture in which `tcgetpgrp` != leader pid, with
|
1. A PTY job-control fixture where `tcgetpgrp` != leader pid, both exact
|
||||||
both exact values asserted and asserted to differ. The landed test at
|
values asserted and asserted to differ. The test at `:2400` is
|
||||||
`:2400` is **rewritten**, not supplemented, since it currently pins a
|
**rewritten**, not supplemented — it currently pins a substitution as
|
||||||
substitution as acceptable.
|
acceptable.
|
||||||
2. The PTY foreground-lookup fallback reports a source distinct from a
|
2. The PTY foreground-lookup fallback reports a source distinct from a
|
||||||
pipe child's leader-pid, with a test driving the real branch.
|
pipe child's, with a test driving the real branch. **No errno claim**
|
||||||
3. The report names the signal; at least one non-fatal signal
|
(§1.6).
|
||||||
(`SIGUSR1`) is tested alongside `SIGTERM`, including that its
|
3. The report names the signal, split into two independent checks:
|
||||||
disposition differs.
|
(a) a **failure-format** comparison showing `SIGUSR1` and `SIGTERM`
|
||||||
|
failures differ *in text only*, both leaving state and ledger
|
||||||
|
unchanged; and (b) a **successful-call disposition control** showing
|
||||||
|
a successful `SIGUSR1` does not transition state or arm the ledger
|
||||||
|
while a successful `SIGTERM` does.
|
||||||
4. For `spec.group` children the report carries the measured pgid as a
|
4. For `spec.group` children the report carries the measured pgid as a
|
||||||
field distinct from the assumed one, renderable as unobservable, and
|
field distinct from the assumed one, renderable as unobservable, with
|
||||||
a test asserts a case where they **differ**.
|
a test asserting a case where they **differ** (§3 Bet 4).
|
||||||
5. Every exact-string test updated individually, each listed in the PR
|
5. All four exact-string sites — `:2408`, `:2435`, `:2485`, `:2517` —
|
||||||
body with before and after. No blanket rewrite.
|
updated **individually**, each listed in the PR body with before and
|
||||||
6. §1.8's first-call abandonment pinned, labelled as pinning a known gap.
|
after. No blanket rewrite: that is how a format regression hides.
|
||||||
7. `docs/agent-handoff.md` records that "EPERM cannot happen for our own
|
6. `:2501`'s existing first-call pin is **retained and cited**, updated
|
||||||
|
only for the new format.
|
||||||
|
7. `process` added to pmacs' declared `nix` features (§1.5a).
|
||||||
|
8. `docs/agent-handoff.md` records that "EPERM cannot happen for our own
|
||||||
children" is false, with the run link; the comment at `:1246` is
|
children" is false, with the run link; the comment at `:1246` is
|
||||||
corrected in the same PR.
|
corrected in the same PR.
|
||||||
8. **No acceptance claims the telemetry establishes group identity.**
|
9. **No acceptance claims the telemetry establishes group identity**
|
||||||
§1.5 governs; the PR body repeats it.
|
(§1.5), and none claims escalation is guaranteed (§1.8). The PR body
|
||||||
|
repeats both.
|
||||||
|
|
||||||
|
|
||||||
## 5. Parked
|
## 5. Parked
|
||||||
|
|
||||||
- **Retargeting to the measured pgid.** Behavioural, and unsupported by
|
- **The reap ledger's silent cancellation** (§1.8): an EPERM probe drops
|
||||||
§1.5. Needs this lane's evidence first.
|
the entry and a failed `SIGKILL` is marked as killed. Now known
|
||||||
|
reachable. **Its own lane** — disposition questions, second site.
|
||||||
|
- **Retargeting to the measured pgid.** Behavioural; unsupported by §1.5.
|
||||||
- **Any tolerance rule for EPERM or ESRCH.** Unmotivated across Stage A's
|
- **Any tolerance rule for EPERM or ESRCH.** Unmotivated across Stage A's
|
||||||
three revisions and still unmotivated.
|
three revisions and still unmotivated.
|
||||||
- **§1.8's first-call abandonment.** Its own lane; disposition change.
|
- **§1.8's first-call abandonment.** Pinned at `:2501`, not fixed here.
|
||||||
- **Q#PS6** — `terminate` on an already-reaped process returning `Ok`.
|
- **Q#PS6** — `terminate` on an already-reaped process returning `Ok`.
|
||||||
- **`signal_target`'s read-then-kill of `tcgetpgrp`** — Stage A called it
|
- **`signal_target`'s read-then-kill of `tcgetpgrp`** — Stage A's "most
|
||||||
"the most likely real fix site, still unframed". Still is. This lane
|
likely real fix site, still unframed". This lane makes it *observable*,
|
||||||
makes it *observable*, not fixed.
|
not fixed.
|
||||||
- **`compile_mode_acceptance` reading the developer's real
|
- **`compile_mode_acceptance` reading the developer's real
|
||||||
`~/.config/pmacs/init.lua`** — separate defect (11 local failures,
|
`~/.config/pmacs/init.lua`** — separate defect, 11 local failures,
|
||||||
invisible in CI), unrelated to signals.
|
invisible in CI.
|
||||||
|
|
||||||
|
|
||||||
## 6. Gates
|
## 6. Gates
|
||||||
|
|
||||||
Standard suite, each its own step with a real exit status, nothing after
|
Standard suite, each its own step with a real exit status and nothing
|
||||||
the command that could mask it: `cargo fmt --check`; `cargo clippy
|
after the command that could mask it: `cargo fmt --check`; `cargo clippy
|
||||||
--workspace --all-targets -- -D warnings`; `cargo test --lib`; `cargo
|
--workspace --all-targets -- -D warnings`; `cargo test --lib`; `cargo
|
||||||
test --lib --features crdt`; `compile_mode_acceptance`;
|
test --lib --features crdt`; `compile_mode_acceptance`;
|
||||||
`terminal_copy_mode_acceptance` (both feature configurations);
|
`terminal_copy_mode_acceptance` (both feature configurations);
|
||||||
|
|
@ -322,17 +394,14 @@ test --lib --features crdt`; `compile_mode_acceptance`;
|
||||||
`git diff --check`.
|
`git diff --check`.
|
||||||
|
|
||||||
**All local runs use an isolated `XDG_CONFIG_HOME`** — without it
|
**All local runs use an isolated `XDG_CONFIG_HOME`** — without it
|
||||||
`compile_mode_acceptance` fails 11 tests for reasons unrelated to this
|
`compile_mode_acceptance` fails 11 tests for unrelated reasons.
|
||||||
lane.
|
|
||||||
|
|
||||||
**PTY job-control tests are the load-sensitive kind.** They are run
|
**PTY job-control tests are load-sensitive.** Run repeatedly; the PR body
|
||||||
repeatedly, and the PR body records the repetition count rather than a
|
records the repetition count, not a single green.
|
||||||
single green.
|
|
||||||
|
|
||||||
|
|
||||||
## 7. Branch plan
|
## 7. Branch plan
|
||||||
|
|
||||||
One branch, one PR. Order: Bet 1 first and alone, because it is the
|
One branch, one PR. Bet 1 first and alone: it decides whether the
|
||||||
finding that decides whether the diagnostic is worth extending at all. If
|
diagnostic is worth extending at all. If the divergence fixture cannot be
|
||||||
the divergence fixture cannot be made deterministic, the rest of the lane
|
made deterministic, the lane is re-scoped rather than pushed through.
|
||||||
is re-scoped rather than pushed through.
|
|
||||||
|
|
|
||||||
Loading…
Reference in New Issue