self-proof: a live owner pid without its instance marker is undetermined, never proved (#1187) - #1191
Merged
fujibee merged 1 commit intoSep 13, 2026
Conversation
…ned, never proved (#1187) The proof judged the owner alive with agmsg_instance_alive, which reads an absent instance marker as alive: the conservative side for the lock it serves, where nothing contradicts a live pid. Here the same default sat on the dangerous side. A pid reused by a stranger after the session ended, with the marker gone, walked as the owner and, with a complete ancestry, proved into whatever pane the stranger sat in. Measured on 2026-09-13 with the suite's own fixture: alive, unmarked, complete ancestry returned proved. The two CI reds behind #1187 were the same mechanism seen from the other side: a reaped pid handed to a new process on a loaded macOS runner made the verdict's reason change, and the exact-match assertion went red; that it landed on undetermined there was an accident of a fixture whose ancestry did not reach the root, not a property of the classifier. The proof now asks for the marker itself after liveness and does not share the lock's default: absent -> undetermined owner_marker_absent; unreadable -> undetermined owner_liveness_unknown. The fixture's live owner gets its marker in setup, the flaky test skips by name when its reaped pid is found reused before the read, and a control pins alive+unmarked+complete -> undetermined (red before this change).
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Fixes #1187.
What was measured
The flaky test pins that an owner whose process is gone comes back
undetermined. Run against the suite's own fixture:sleep)undetermined invocation_ancestry_truncatedprovedprovedSo the classifier judged liveness once (
kill -0plus the marker) before the walk, never re-checked it, and read an absent marker as alive: with a complete ancestry it then proved a pid that nothing tied to the session. The two CI reds were the same mechanism seen from the red side — a reaped pid handed to a new process on a loaded macOS runner made the reason change fromowner_not_alive, and the exact-match assertion failed. That those runs landed onundeterminedwas an accident of a fixture whose fake ancestry stopped short of the root, not a property of the classifier.Why it matters before release
The self-write path (#1157) writes a seat's identity cells on the strength of
proved. A pid reused after a session ended, with the session's marker cleaned up, is rare — and it is exactly the shape that fails silently: aprovedthat was never established, handed to a caller that writes into someone else's pane.The change
After liveness says alive, the proof asks for the instance marker itself: absent →
undetermined owner_marker_absent; unreadable →undetermined owner_liveness_unknown. The lock's default (an absent marker is alive) stays as it is — it is the conservative side there, where nothing contradicts a live pid and reclaiming would be the harm. The two contexts do not share the default, and the comment at the call site says why, for the next person who wants to unify them.Tests
undetermined owner_marker_absent. Red before this change (it returnedproved); removing the marker requirement reddens it alone (and the whole-suite shell-state harness, which reruns the file).setup, as a live session has.Suite 45/45 including the nested shell-state reruns; the static checkers at their baselines; shellcheck unchanged on the file.