a_run_exceeding_its_budget_kills_a_real_grandchild fails under parallel load, passes in isolation

[kreneskyp]

Found while running the pre-merge gates for #127. Pre-existing and unrelated to that PR — the diff there touches only tests/shared_assurance.rs, a separate test binary, and src/, Cargo.toml and Cargo.lock are byte-identical to origin/main, so the lib test binary is the same one.

Measured

src/kani_execution.rs:1177 a_run_exceeding_its_budget_kills_a_real_grandchild_not_only_the_direct_child.

invocation	result
cargo test --locked (full suite)	FAILED, 40 passed / 1 failed — reproduced twice
cargo test --locked --lib (lib binary, full parallelism)	FAILED, 40 passed / 1 failed
cargo test --locked --lib a_run_exceeding_its_budget (alone)	ok, 3 runs out of 3

Panic at src/kani_execution.rs:1197:

the timed-out run's grandchild (pid 195920) must be killed, not merely its direct
child, and not left running past the deadline its ancestor exceeded

It also passed 41/41 under make ci's msrv target (cargo +1.98.1 test --locked) in the same session, which is more evidence of load sensitivity than of a toolchain difference.

Why it is the repo's inverse defect class

The test gives the launcher a 200 ms budget and then asserts /proc/<grandchild_pid> does not exist, immediately, with no wait and no retry:

let outcome = run_launcher_with_timeout(command, Duration::from_millis(200)).unwrap();
...
assert!(!Path::new(&format!("/proc/{grandchild_pid}")).exists(), ...)

Signal delivery and reaping are not instantaneous, and a killed-but-unreaped process still has a /proc entry. Under parallel load the window closes before the tree walk finishes, so the assertion goes red with no defect present.

That is not "a criterion too weak to fail" but its inverse — a criterion that fails for the wrong reason. It is the same shape as #124: a gate going red for a reason unrelated to the tree under test teaches the next person to distrust or route around the gate.

The test's own doc comment is careful and correct about what it proves — it explicitly records that a weaker version stayed green when kill_process_tree was disabled. The defect is only in how the post-condition is observed, not in what it asserts.

Asked for

1. Observe the post-condition with a bounded wait rather than a single instantaneous sample — poll until the pid is gone or a deadline passes, so the assertion distinguishes "not killed" from "not yet reaped".
2. Distinguish a zombie from a live process. A killed-but-unreaped grandchild still has a /proc/<pid> directory; /proc/<pid>/stat state Z is the difference, and treating it as alive is what makes this red under load.
3. Keep the existing negative control intact: whatever replaces the check must still go red when kill_process_tree is disabled outright, which is the measurement the doc comment records.

Not claimed here

Not reproduced on a quiet machine, and no claim that it fails in CI — CI is workflow_dispatch-only in this repository. The measurement above is from one host under concurrent cargo builds.