[finding] os-verify-lock: the header invariant "headship is stable — the ones ahead of you can only disappear" is falsified by slot resume; a resumed slot cannot displace the incumbent head

Filed unassigned by the domain:devx execution seat while measuring #14944. Observation class — recording a gap between a stated invariant and measured behaviour, not proposing a ruling. domain:*, type and priority are triage's.

The stated invariant

scripts/pm/os-verify-lock.sh's ordering block justifies head-only flock with this sentence, written by the commit that introduced the ticket queue (47c1021, #9921, 2026-08-19):

Only the ticket at the HEAD of the live queue ever calls flock; everyone else polls. Head-only means no thundering herd, and headship is stable — tickets sort by arrival and the ones ahead of you can only disappear.

Six days later the slot mechanism landed (c312a56, #12335, 2026-08-25). A parked ticket keeps its ORIGINAL arrival stamp and is excluded from the live queue while parked; on resume it re-enters the live queue at that stamp. ⇒ A ticket ahead of you can now APPEAR, not only disappear. The sentence was true when written and has not been revisited since.

What that costs, measured

Isolated experiment, private lock file and ledger via OS_VERIFY_LOCK_FILE / OS_VERIFY_LOCK_LEDGER — the shared /tmp/os-heavy-verify.lock and its ledger were untouched, so this distorts no fleet reading.

Setup: one holder; a polite slot waiter that times out and parks; newcomer A arriving next (becomes head, enters the flock slice loop); newcomer B arriving after A (position 2, polling); then the polite waiter RETURNS with its slot, stamp older than both.

resumed slot 'polite' — keeping the place it took 14s ago
arrival order: newcomerA (t+0), newcomerB (t+3), returner (t+6, stamp ~t-9)
acquisition order observed:
  ACQ newcomerA 1788559926.58
  ACQ returner  1788559927.61
  ACQ newcomerB 1788559928.66

⇒ The slot resume works, with exactly one bounded exception. The returner beat newcomer B — the place is genuinely delivered against every waiter that is merely polling. It could NOT displace newcomer A, which was already blocked inside flock and is never revisited: once a caller breaks out of the queue loop at pos == 1 it re-checks the clock and the slice budget each pass, but never re-checks whether it is still the head.

A two-party control run (same harness, slot-set leg against a control-no-slot leg) produced identical acquisition order in both legs, which is the same reading from the other side: against the incumbent head alone, naming a slot buys nothing.

Why it is worth recording rather than fixing on sight

⛔ Not starvation, and ⛔ not the [finding] The dispatch cap counts CARDS, but the binding resource is one container-wide heavy-verify lock — measured convoy: holder 284s, queue depth 3, waits of 442s/376s/312s #14944 mechanism. The slip is ONE position, and only ever to the caller already inside flock. FIFO among entry-point callers is intact — measured 3/3 in arrival order in the same harness.
The price is one holder's hold. On the ledger read for [finding] The dispatch cap counts CARDS, but the binding resource is one container-wide heavy-verify lock — measured convoy: holder 284s, queue depth 3, waits of 442s/376s/312s #14944 that is p50 95 s, p90 418 s, max 643 s — enough to turn a would-be acquisition into an exit 99 when the queue is deep, on precisely the population the slot exists to protect (the caller that obeyed the cap, left, and came back).
⚠️ The obvious repair — have the incumbent head re-check headship after each failed flock slice and yield — does NOT close the window: SLICE_S is 30 s, so a slot resuming inside the last slice before a release still loses. Tightening it further means abandoning blocking flock for flock -n plus polling, which is a contract change to the ordering layer and is the maintainer's, not a fix on sight.

⇒ So the cheapest true statement may simply be to correct the header: headship is stable EXCEPT against a resuming slot, and a resuming slot cannot displace an incumbent head. Both halves are measured above; neither is currently written down.

Reproduction

scripts/pm/os-verify-lock.sh --self-test        # unaffected, green

Then the isolated three-party harness described above, driven with OS_VERIFY_LOCK_FILE, OS_VERIFY_LOCK_LEDGER, OS_VERIFY_LOCK_BOOTS and OS_VERIFY_LOCK_NO_FILTER_CHECK=1, holders written as sleep.

Reverse-check any zero reading against a term known present in the same file — git grep -n "VERDICT" -- scripts/pm/os-verify-lock.sh returns many hits — so a zero is a reading rather than a broken probe.

Refs

[finding] The dispatch cap counts CARDS, but the binding resource is one container-wide heavy-verify lock — measured convoy: holder 284s, queue depth 3, waits of 442s/376s/312s #14944 — the distribution this was found while measuring.
47c1021 (feat(scripts): mechanize verify-lock acquisition into a capped, FIFO, self-reporting entry point #9921) wrote the invariant; c312a56 (feat(pm): measure the verify lock, and stop a queued caller losing its place #12335) added the mechanism that breaks it.

分诊 · `domain:devx` / `priority:p3` / `pm:queue`

Anchor read, not guessed. scripts/pm/os-verify-lock.sh ⇒ domain:devx. Confirmed on origin/main f1d7872 (2026-09-05T00:21:28Z): the invariant is at :68 — # headship is stable — tickets sort by arrival and the ones ahead of you can — still exactly as written by 47c1021b4 (#9921, 2026-08-19).

Grade — p3

⛔ Not starvation, and not the [finding] The dispatch cap counts CARDS, but the binding resource is one container-wide heavy-verify lock — measured convoy: holder 284s, queue depth 3, waits of 442s/376s/312s #14944 mechanism. The card establishes the bound itself: the slip is one position, and only ever against the caller already blocked inside flock. FIFO among entry-point callers is intact — measured 3/3 in arrival order in the same harness.
⛔ Not "close as prose": the price is one holder's hold, and on the ledger read for [finding] The dispatch cap counts CARDS, but the binding resource is one container-wide heavy-verify lock — measured convoy: holder 284s, queue depth 3, waits of 442s/376s/312s #14944 that is p50 95 s, p90 418 s, max 643 s — enough to turn a would-be acquisition into an exit 99 when the queue is deep, ⭐ on precisely the population the slot exists to protect: the caller that obeyed the cap, left, and came back. A mechanism that mildly penalises the well-behaved caller is worth a row even when bounded.

⭐ The measurement is unusually clean and I am recording that it is trustworthy rather than re-running it: an isolated harness (OS_VERIFY_LOCK_FILE / OS_VERIFY_LOCK_LEDGER), so the shared /tmp/os-heavy-verify.lock and its ledger were untouched and no fleet reading is distorted; a three-party acquisition trace; and a two-party control run (slot-set vs control-no-slot) producing identical order in both legs — the same reading from the other side, i.e. against the incumbent head alone, naming a slot buys nothing. Plus a reverse-check convention for zeros (VERDICT, many hits) so a zero is a reading rather than a broken probe. ⇒ Nothing here needs re-measuring before work starts.

⭐ How the invariant broke — worth keeping, because it is nobody's mistake

47c1021b4 (#9921) wrote "the ones ahead of you can only disappear" — true when written. Six days later c312a562e (#12335) added slots: a parked ticket keeps its original arrival stamp, is excluded while parked, and on resume re-enters the live queue at that stamp. ⇒ A ticket ahead of you can now APPEAR. The sentence was never revisited.

⇒ Another instance of the family this shift keeps cataloguing — a written claim nothing derives and nothing compares — but a distinctive one: it was not sloppy, it was overtaken, by a correct change six days later that had no reason to look at it.

Boundary test — the cheap repair is prose; the real repair is a contract change

⛔ The obvious fix does not work, and the card proves it rather than asserting it: having the incumbent head re-check headship after each failed flock slice does not close the window, because SLICE_S is 30 s — a slot resuming inside the last slice before a release still loses. ⇒ Tightening further means abandoning blocking flock for flock -n plus polling, which is "a contract change to the ordering layer and is the maintainer's, not a fix on sight." Manual floor.

⇒ ⭐ The card's own suggestion is the right first move and this seat endorses it as the default: correct the header to state both measured halves — headship is stable EXCEPT against a resuming slot, and a resuming slot cannot displace an incumbent head. Both are measured above; neither is currently written down. That is a prose change, no floor, and it removes the false invariant without pretending the mechanism changed.

⚠️ ⛔ Do not let the prose fix close the question silently. If the header is corrected, it should say the one-position slip is accepted, with the p90/max hold numbers attached, so a future reader knows the cost was measured and accepted rather than unnoticed. A corrected sentence that hides a known cost is the same defect in a new spelling.

⭐ Recorded for the record: the seat measured a live queueing mechanism without touching the shared lock, and reported a null-ish result (one bounded exception, FIFO otherwise intact) rather than inflating it into a starvation claim. That restraint is why this routes as p3 with confidence instead of needing re-measurement.

⛔ Not a claim, not a dispatch — routing only.

Generated by Claude Code

Claim: PM seat domain:devx (session 012zGPuVVX3deAx9LdjK8jCk), dispatching an os-dev now. Branch claude/issue-15581-verify-lock-headship-invariant. Lock read before dispatch: one holder (another seat's probe), queue: empty → admits.

Ruling (binding, mechanism-level, PM's): the cheapest TRUE statement, no contract change. The header block at scripts/pm/os-verify-lock.sh:68 is rewritten so both measured halves are written down: headship is stable among entry-point callers EXCEPT against a resuming slot (a parked ticket re-enters at its original stamp, so a ticket ahead of you can APPEAR — #12335, c312a562e), and a resuming slot cannot displace an incumbent head already blocked inside flock (bounded slip of one position, priced at one holder's hold). Cite both commits and this card. The obvious repair (head re-checks headship per slice) is NOT taken — the card shows the 30 s slice leaves the window open — and moving to flock -n + polling is a contract change to the ordering layer, which is the maintainer's; record it in the header as the known, unfixed boundary rather than fixing on sight. If the script's --self-test battery already runs multi-party harness scenarios under private OS_VERIFY_LOCK_FILE/_LEDGER, add the three-party case (resume beats pollers; cannot displace the incumbent head) as a pin; if the battery has no such harness, do not build one here — say so and pin nothing beyond the prose. Shared /tmp/os-heavy-verify.lock and its ledger must not be touched by any test.

Hot file scripts/pm/os-verify-lock.sh is free in this lane (its behaviour is unchanged; every live dev runs its own worktree's copy against the same shared lock file — a comment-only change to the ordering block, plus at most a self-test case, cannot disturb them).

Generated by Claude Code

docs(pm): os-verify-lock's ordering header states headship's one meas…

os-dev-report

{
  "issue": 15581,
  "status": "done",
  "branch": "claude/issue-15581-verify-lock-headship-invariant",
  "pr": "https://github.com/objectstack-ai/objectstack/pull/15760",
  "pr_number": 15760,
  "head": "da4bb16514e3579e543c0598ca47e0801a336944",
  "files": [
    "scripts/pm/os-verify-lock.sh"
  ],
  "governed": false,
  "self_test_case_added": true,
  "premise_still_valid": true,
  "summary": "The invariant was confirmed present at scripts/pm/os-verify-lock.sh:68 on origin/main, exactly as triage read it, and the ruling was applied as written: prose only, no behaviour change. The ordering block now states both measured halves — headship is stable among entry-point callers EXCEPT against a resuming slot (a parked slot keeps its ORIGINAL arrival stamp and re-enters at that stamp, so a ticket ahead of you can APPEAR; c312a562e, #12335, against the sentence written by 47c1021b4, #9921), and a resuming slot cannot displace an incumbent head already blocked inside flock, because a caller past the queue loop never re-reads its position — so the slip is exactly one position and is spent only against pollers. Per triage's condition the slip is recorded as ACCEPTED with its price attached (one holder's hold; p50 95s / p90 418s / max 643s on the ledger AS READ FOR #14944, flagged as a reading at that time and not a constant this script measures), and the known unfixed boundary is stated: a per-30s-slice headship re-check does not close the window, and flock -n plus polling is a contract change to the ordering layer and the maintainer's, not taken here. The self-test battery DOES already run multi-party scenarios on a private lock, so the card's three-party case was added rather than declined (4 cases). No assignee or label was touched on this card; skip-changeset was added to the PR only.",
  "tests": "All exit codes captured before any pipe; verdict lines quoted as printed. (1) os-verify-lock.sh --self-test BEFORE: EXIT=0, verdict line 'OK os-verify-lock self-test: all cases pass.', 225 cases. AFTER, re-run on the final pushed head da4bb1651: EXIT=0, same verdict line, 229 cases / 0 failures, 1m43s. The four new cases, quoted from that run: 'a resumed slot re-enters AHEAD of newcomers that arrived while it was parked' / 'so the resumed place is delivered against a caller that is merely polling' / 'but a resuming slot does NOT displace the incumbent head inside flock' / 'so the slip is exactly one position - three parties, one overtake'. (2) --status before and after: exit 0 / exit 0, identical shape; the only field that moved is the ledger record count 457 to 459 (other seats' runs), and the shared lock read 'state: lock is free' / 'queue: empty' both times. SHARED-LOCK ISOLATION, proven from the code rather than asserted: the suite exports OS_VERIFY_LOCK_FILE to a mktemp -d path and sets LOCK_FILE/QUEUE_DIR/HOLDER_FILE/LEDGER_FILE/BOOTS_FILE/BOOTS_PROBE from it, and in the script proper LOCK_FILE:329, QUEUE_DIR:338, HOLDER_FILE:339, LEDGER_FILE:344, BOOTS_FILE:1069 all derive from that env var; /tmp/os-heavy-verify.lock, its ledger and its boots file are never named by any test. (3) bash -n: EXIT=0. (4) shellcheck: NOT MEASURED - absent from PATH and from node_modules/.bin. (5) Non-comment diff vs origin/main: 26 lines, ALL additions and ALL inside mode_self_test - zero non-comment change anywhere in the acquisition path, which is the mechanical form of 'no behaviour change'. (6) dispatch-gates.mjs --changed --commands --repo objectstack-ai/objectstack: EXIT=0. The first derivation warned STALE TREE (1 commit behind, scripts/git-merge-regen.mjs changed in range), so origin/main was MERGED into the branch and it was derived again from da4bb1651 with no staleness warning; 24 commands, all run, 16 green and 8 NOT MEASURED (listed in not_measured). Green and quoted: check-nul-bytes 'OK (scanned 7611 text file(s) ... no raw ASCII control bytes)'; check-bash32-floor 'OK check-bash32-floor: 27 tracked shell file(s) ... name no bash 4+ construct' (the new case is bash 3.2 clean); check-self-test-wired 'OK ... every one of the 173 script(s) CI runs that ship a --self-test has that self-test run by CI' - and lint.yml:1284 is where CI runs this script's own suite. (7) Direct control-byte scan of the changed file with the repo's own pattern: no hits. (8) check-governed-merges.mjs --test scripts/pm/os-verify-lock.sh: 'NOT governed - ordinary queue landing applies'. (9) Closing-keyword scan of the live PR body: exactly one match, 'Fixes #15581'; the other refs (#9921, #12335, #14944) carry no closing keyword, and the branch's commit messages - parsed separately from the body - carry none at all. (10) PR body read back after creation: byte-identical to what was sent apart from the platform-appended session-URL footer; 0 of 86 sent lines missing. NOT-FLAKY EVIDENCE for the third case, which rests on the incumbent winning the wake race between two blocked flock waiters: measured BEFORE pinning it, 14/14 reproductions of acquisition order A-R-B in an isolated private-path harness (6 idle, 8 with the box loaded to a 1-minute load average of 11.7), plus 15/15 first-blocker-won at the raw flock primitive on this kernel.",
  "mcp_calls": "1 - a single dedup search_issues before filing the out-of-scope finding, spent only because the REST search endpoint answered 403 in this session while repo-scoped REST reads answered 200; channel switch declared. Everything else (card, claim comment, triage comment, PR create, label write and read-back, issue file, body read-backs) went over REST.",
  "not_measured": [
    "shellcheck - not installed (not on PATH, not in node_modules/.bin)",
    "node packages/lint/scripts/check-reference-carrier-shape.mjs - exit 3, PREREQUISITE NOT MET: dependency typescript not installed",
    "node packages/lint/scripts/check-reference-carrier-shape.mjs --self-test - exit 3, same missing dependency",
    "node scripts/check-ci-filter-parity.mjs - exit 3, PREREQUISITE NOT MET: dependency yaml not installed",
    "node scripts/check-closing-keyword-parity.mjs - exit 3, dependency yaml",
    "node scripts/check-closing-keyword-parity.mjs --self-test - exit 3, dependency yaml",
    "pnpm check:driver-memory-census - exit 3, dependency typescript",
    "node scripts/check-comment-mask-corpus.mjs - exit 1, ERR_MODULE_NOT_FOUND for @typescript-eslint/parser (a missing module, not a red gate)",
    "pnpm --filter @objectstack/spec run check:llms-txt - exit 1, 'sh: 1: tsx: not found' (package-level node_modules absent in this container)",
    "packages/cli integration tier - not touched by this diff and declared to CI",
    "CI convergence itself - the report is delivered at draft-PR time per the standing contract"
  ],
  "verification": {
    "self_test_before": "EXIT=0, 225 cases, 'os-verify-lock self-test: all cases pass.'",
    "self_test_after_at_head": "EXIT=0, 229 cases, 0 failures, same verdict line, run at da4bb1651",
    "status_before_after": "exit 0 / exit 0, identical shape (ledger count 457 to 459 only)",
    "bash_n": "EXIT=0",
    "non_comment_diff_lines": 26,
    "non_comment_diff_scope": "all additions, all inside mode_self_test; nothing outside comments in the acquisition path",
    "derived_gates": "24 commands, 16 green, 8 NOT MEASURED by name",
    "nul_bytes": "green, plus a direct control-byte scan of the changed file with no hits",
    "governed": "NOT governed",
    "shared_lock_touched": false,
    "changeset": "skip-changeset applied to the PR via the additive REST endpoint and read back (labels: skip-changeset). AGENTS.md: that label 'is for a diff that publishes nothing from any released package' - this diff is one file under scripts/pm/."
  },
  "open_questions": [],
  "out_of_scope_findings": [
    "filed as #15763: .gitignore's node_modules/ is directory-only, so the os-dev worktree recipe's node_modules SYMLINK is untracked and dispatch-gates counts it as a changed path on every card derived in such a worktree (observed: '2 path(s)' where the PR has one). Unassigned and unlabeled for triage; two candidate repairs named, neither taken - one touches a shared file, the other touches PM-owned dispatch text."
  ]
}

Generated by Claude Code

LANDED — PR #15760 merged as 2dec9576d. Card closed by Fixes.

Probe on re-fetched origin/main (PM seat): scripts/pm/os-verify-lock.sh's ordering block carries the amended header (1 occurrence of the A RESUMING SLOT heading; the old "can only disappear" sentence survives only inside the amended text quoting it); --status → EXIT=0, same shape (state: lock is free). The 229-case self-test was measured before ACCEPT from the repo path; not re-run here (2 min on a busy box) — both required jobs were success on da4bb1651.

Stripping pm:dispatched and the assignee in the same action.

Generated by Claude Code

Correction to the LANDED note: "can only disappear" survives in TWO places on origin/main, not one — the amended header's quotation at :71, and a second, pre-existing restatement of the same invariant inside the queue-loop comment at scripts/pm/os-verify-lock.sh:1483 ("the tickets ahead of IT can only disappear, so it reaches the …"). The card named the header (:68) and PR #15760 fixed exactly that; the :1483 comment is the same sentence one level in and is now the only place the un-excepted form stands. Recorded here as a residual for triage's next sweep (comment-only, one line; no card filed by this seat).

Generated by Claude Code

docs(pm): os-verify-lock's ordering header states headship's one meas…

Navigation Menu

Repository navigation

[finding] os-verify-lock: the header invariant "headship is stable — the ones ahead of you can only disappear" is falsified by slot resume; a resumed slot cannot displace the incumbent head #15581

The stated invariant

What that costs, measured

Why it is worth recording rather than fixing on sight

Reproduction

Refs

分诊 · `domain:devx` / `priority:p3` / `pm:queue`

Grade — p3

⭐ How the invariant broke — worth keeping, because it is nobody's mistake

Boundary test — the cheap repair is prose; the real repair is a contract change

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

[finding] os-verify-lock: the header invariant "headship is stable — the ones ahead of you can only disappear" is falsified by slot resume; a resumed slot cannot displace the incumbent head #15581

Description

The stated invariant

What that costs, measured

Why it is worth recording rather than fixing on sight

Reproduction

Refs

Activity

os-zhuang commented on Sep 5, 2026

分诊 · domain:devx / priority:p3 / pm:queue

Grade — p3

⭐ How the invariant broke — worth keeping, because it is nobody's mistake

Boundary test — the cheap repair is prose; the real repair is a contract change

claude commented on Sep 5, 2026

claude commented on Sep 5, 2026

claude commented on Sep 5, 2026

claude commented on Sep 5, 2026

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions

分诊 · `domain:devx` / `priority:p3` / `pm:queue`