feat(scripts): mechanize verify-lock acquisition into a capped, FIFO, self-reporting entry point

[os-warren]

Fixes#9661

Draft, and it stays draft: .claude/agents/os-dev.md is a governed surface, so this
one is for the maintainer to merge.

What changed

A declared -w cap that nothing enforced was losing to the agents who ignored it. This
moves the cap out of prose and into a call site.

• scripts/pm/os-verify-lock.sh (new) — the one entry point for the container's
  shared heavy-verify lock:
  • scripts/pm/os-verify-lock.sh -c 'pnpm --filter PKG test' (or -- ARGV)
  • --status — holder, how long it has held, and the queue
  • --show-budget, --self-test
• .claude/agents/os-dev.md — rule 1 now points at the entry point instead of
  describing free-hand flock etiquette; rule 7's ladder is unchanged except that
  "name the holder" is now --status rather than fuser -v. Rules 6 and 7 still route
  the queue-timeout path through 干净收尾's declared-narrowing exit, verbatim and
  untouched. Net line change: 0 (358 lines, ceiling 399).
• .github/workflows/lint.yml — runs the entry point's 29-case --self-test.

The three properties the grading comment asked for

(a) the budget cap is enforced at the call site. The entry point accepts no -w at
all — passing one exits 2 with a message saying why. The single knob,
OS_VERIFY_LOCK_WAIT, can only lower the budget; anything above the cap is clamped
and says so:

$ OS_VERIFY_LOCK_WAIT=3000 scripts/pm/os-verify-lock.sh --show-budget
budget: 540s (hard cap 540s, default 540s)
note: OS_VERIFY_LOCK_WAIT=3000 exceeds the declared cap — clamped to 540s (an acquisition wait must fit inside one foreground call)

(b) grants are FIFO. Every call drops a ticket file named by arrival time into
(lockfile).q/; only the ticket at the head of the live queue ever calls flock,
everyone else polls. flock stays the only mutual-exclusion primitive — the ticket
queue is advisory ordering layered on top, which is what makes the coexistence
behaviour below safe.

(c) holder duration is reported. Every run ends with a VERDICT line carrying how
long it held and how long it waited, and a run past 15 minutes prints a loud block
naming itself and its command — so the next long holder (#8716's returned mechanism,
recorded in this card's evidence comment) surfaces itself instead of waiting to be found
by a starved sibling with fuser.

Coexistence during rollout, stated explicitly

A legacy free-hand flock user contends on the same file with the same primitive.
Mutual exclusion is unaffected — a legacy caller cannot corrupt the queue, deadlock
it, or run concurrently with an entry-point holder. What it can do is win a grant ahead
of the queue head, because it never took a ticket. So during rollout the guarantee
degrades to: entry-point callers are FIFO among themselves, legacy callers behave
exactly as they do today, and nobody loses exclusion. Both directions are asserted in
the self-test. --status still names an unregistered legacy holder (via fuser), it
just cannot report its duration.

A waiter that dies, is killed, or times out leaves at most one stale ticket, and a stale
ticket cannot wedge the queue: tickets are pruned by liveness (pid present and its
/proc start time unchanged, so a reused pid cannot resurrect a dead ticket) and by an
absolute age bound. If the queue directory cannot be used at all, acquisition falls back
to a plain capped flock with a warning — the ordering layer is best-effort, the cap
and the exclusion are not.

Measurement — including one prediction this falsified

Real two-process (four-process) demonstrations, all on a private lock under a temp dir,
never the shared one. Direction predicted in writing before each run.

1. The FIFO prediction was WRONG, and that is worth recording. Predicted: three
staggered, continuously-blocked waiters would acquire out of arrival order under
free-hand flock, and in order through the entry point. Observed, 10 runs each:

free-hand runs=10 arrival-order(ABC)=10
entry runs=10 arrival-order(ABC)=10

Linux already grants FIFO among waiters that are continuously blocked. So (b) buys no
change of observed order in that regime. What it does buy is worth keeping anyway: the
order becomes explicit and testable rather than an undocumented kernel property
(flock(2) promises nothing), it becomes observable via --status (the kernel's wait
queue is invisible), and only the head contends, so there is no thundering herd.

2. The card's actual mechanism reproduces exactly — and it is duty cycle, not grant
order. A compliant waiter (short budget, times out, goes off to do lock-free work,
comes back) versus a non-compliant resident waiter, with the compliant one arriving
first. Free-hand, 12 runs:

free-hand flock, 12 runs: resident(-w 60, arrived 2nd) won 12 · compliant(-w 1, arrived 1st) won 0 · neither 0

Twelve out of twelve to the waiter that arrived second, purely for being present at the
handoff. That is the reported inversion, reproduced.

3. Through the entry point, the same scenario reverses completely. The would-be
resident asks for OS_VERIFY_LOCK_WAIT=3000 — the real measured non-compliant value —
and still arrives second:

entry point, 12 runs: would-be resident(WAIT=3000, arrived 2nd) won 0 · compliant(arrived 1st) won 12 · neither 0

Residency cannot be bought, so arrival decides. The enforcement half (a) is the
load-bearing one; (b) is what makes the resulting order explicit rather than
inherited from the kernel.

Honest limitation: FIFO orders waiters that are present. It does not reserve a
place across an agent's off-cycle between two os-verify-lock.sh calls. What removes
the measured 6x skew is that every waiter now has the same maximum residency.

Verification

Gate union re-derived on the final head and run there — 456ec7aa:
node scripts/pm/dispatch-gates.mjs (no paths, off the merge base) derives 17 families
from the three changed paths; 16 of 17 pass, plus check:pm-governed-prose and
scripts/pm/check-dispatch-gates.mjs.

✓ check-skill-line-ratchet: .claude/agents/os-dev.md is 358 lines (ceiling 399; headroom 41).
✓ check-nul-bytes: OK (scanned 6300 text file(s) ... no raw ASCII control bytes).
✓ check:doc-formula-expressions: 22 record-scoped formula example(s) across 402 files / 1413 TS blocks judged clean
✓ os-verify-lock self-test: all cases pass. (29 cases, ~15 s)

One declared narrowing: pnpm check:type-check-debt was not run locally. It refuses
to measure without a built farm closure, and says so itself:

Error: --re-measure cannot run: 55 workspace dependenc(ies) of the ledgered packages
have no built type entry point on disk

This diff contains no TypeScript. Its sibling check:type-check-coverage — the same
script without --re-measure — passes here, and lint.yml builds the closure before this
step, so CI runs it properly.

Ablation legs (both restored, git status --porcelain clean afterwards; this is a
bash script executed from source, so there is no dist/ between edit and run and the
rebuild precondition does not apply):

• removed the budget clamp ⇒ 2 cases red, exactly the two cap assertions.
• removed the {lfd} close-in-child ⇒ the fd-hygiene case red (want: 0 got: 1),
  which is the guard against the orphaned-holder mechanism diagnosed in
  scripts/gen-sdui-manifest.sh.

Dogfooded on the real shared lock while doing this card's own work — pnpm install
(held the lock 9s), the dependency-closure build (held the lock 2m02s) and the gate
union (held the lock 20s), all through the entry point.

Scope note

No changeset: scripts/, .claude/ and .github/workflows/ publish nothing, so this
carries skip-changeset. #8716 remains open to its own triage — this PR does not close
it; it only adds the reporting that makes its mechanism self-announcing.

---

Generated by Claude Code