Repository navigation
Conversation
…hold the store lock acquireLock replaced a stale lock with unlink-then-create. Two processes that both read the same dead holder could interleave: the second unlink removed the first process's fresh lock and both proceeded as holders. The takeover now goes through a second wx file (.orch.lock.takeover); only its creator unlinks the stale lock, the other process retries a plain create after a short delay and reports the winner's pid. Tests: a competing mid-takeover marker leaves the stale lock untouched and reports held-by (fails on main); two concurrent takers in one process yield exactly one holder. Fixes cursor#730.
mstephenholl
added a commit
to mstephenholl/pstack-claude-codex
that referenced
this pull request
Oct 20, 2026
## Why `orch` uses `<store>/.orch.lock` to keep two processes from writing the plan store (`units.tsv`, `ledger.tsv`, `gates.md`, `frontier.json`, the inbox) at once. Creating the lock is atomic, but taking over a stale one is not. Upstream reports a race there (cursor#730) and has a fix open (cursor#733), but its test admits it can't reproduce the cross-process case. A model checker can explore every interleaving. ## What changes A project-local skill, `verify-orch-store-lock`, in `.agents/skills/`, symlinked from `.claude/skills/` so that Codex and Claude Code both find it: - **`StoreLock.tla`** models `acquireLock`, `takeOver`, `holderIsDead`, and the release closure in `poteto-mode/scripts/orch/store.ts`. Each action is one filesystem call or `process.kill`, and `writeFile` goes to the inode the process opened, not to whatever is at the path now. - **`MutualExclusion`** is the property: at most one live process is between `acquireLock` returning and `close()`. - **`StoreLockNoCrash.cfg`** runs three processes that never die. **`StoreLock.cfg`** runs three processes, one of which may die at any step. - **`check.sh`** runs both with TLC from TLA+ v1.7.4, which it downloads once to `~/.cache/tla2tools/` and checks by SHA-256. It runs one worker, so a counterexample is the shortest one and the same on every run. Both configurations take about 8 seconds together. - **`SKILL.md`** records the covered code and the sync commit, how the model maps to the code, the expected results, how to tell a bug from a modeling error, how to update the model when the code changes, and what the model leaves out. - **`merge-upstream.py` keeps project skills.** It deletes every tracked path outside `KEEP`, so the next upstream sync would have removed this skill. `KEEP_DIRS` now includes `.agents/skills/` and `.claude/skills/`, and the port README lists them. Upstream tracks nothing under either. ## Findings - **Stale-lock takeover lets two processes hold the lock.** `StoreLock.cfg` fails in 16 states. p1 takes the lock and dies. p2 and p3 both read `p1` from the lock file. p2 takes over and starts work. p3 then confirms that `p1` is dead, unlinks the file at the path, which is now p2's live lock, and also starts work. This is cursor#730. The fork's `store.ts` is identical to upstream's, so the fix should arrive through the sync. The skill says how to update the model when it does. - **A crash between `open` and `writeFile` blocks the store.** It leaves an empty lock that every later process reads as `"unknown"`, which `holderIsDead` never treats as dead. Every `orch` run then refuses until someone passes `--force`. TLC confirmed it with an extra invariant. The skill lists this under what it doesn't cover, because it's a liveness question, not `MutualExclusion`. ## Proof - On the current code, `StoreLockNoCrash.cfg` passes (739 states). `StoreLock.cfg` fails only with the trace above, the same on repeated runs. - **The check catches a break in the real code.** I followed the skill on a scratch change to `create()` in `store.ts`, `open(path, "wx")` changed to `open(path, "w")`. The skill's `git diff` against the sync commit flagged the hunk. I updated the model to match, and `StoreLockNoCrash.cfg` failed in 5 states with two processes working at once. I then dropped the change in both places, and the results were back to the ones above. - **The crash configuration can pass.** In a scratch copy, a compare-and-swap takeover, which unlinks only if the file still holds the dead pid that was read, passes `StoreLock.cfg` (1954 states). So the failure comes from the unconditional `unlink`, not from the crash model. - All 252 unit tests pass, including `test_the_next_sync_deletes_nothing_this_repository_tracks`, which caught the `KEEP` gap. `check.py` reports 0 problems, and `bash -n check.sh` passes. CI runs `shellcheck` on it.
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
1 participant
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.
Summary
Fixes #730.
acquireLockcreates the lock with an atomicopen(path, "wx"), but replacing a stale lock (holderIsDead) wasunlinkthencreate. Two processes that both read the same dead holder could interleave as @BowmanStephen's table shows: the secondunlinkremoves the first process's fresh lock and both proceed as holders.The takeover now goes through a second
wxfile,.orch.lock.takeover. Only the process that creates it unlinks the stale lock and installs its own; a process that finds the takeover file already present waits briefly, retries a plaincreate(), and onEEXISTreportsstore lock held by pid <winner>. The takeover file is removed infinally, so a crash mid-takeover leaves at most a stale marker that the next taker treats as "someone else is mid-takeover" once and then falls through to the normal path.forcetakeover uses the same path.The generated
harness/pstack/claude-codecopy is regenerated from the source.Verification
held by pid. Fails onmain(the old code unlinks regardless), passes here.held by pidrejection, with no takeover file left behind. (In-process the second taker sees a live pid either way, so this one guards the fallback path rather than reproducing the cross-process race.)bun testinpstack/skills/poteto-mode/scripts: 70 pass;bun run typecheckclean;generate-pstack-harness-trees.mjs --checkup to date.