Skip to content

feat(overleaf): add the shared checkout barrier (step 3a) - #626

Merged
yaacovcorcos merged 7 commits into
mainfrom
claude/overleaf-checkout-barrier-20261022
Oct 23, 2026
Merged

yaacovcorcos merged 7 commits into
mainfrom
claude/overleaf-checkout-barrier-20261022

Conversation

@yaacovcorcos

@yaacovcorcos yaacovcorcos commented Oct 22, 2026 •

Copy link
Copy Markdown
Contributor

What this adds

Step 3a of the Overleaf plan (#535, coordinator contract section 9). It adds a shared checkout barrier, so an Overleaf apply never runs at the same time as a bulk change of the same project. Bulk changes include a checkpoint restore, a pull, switching branch and removing a worktree.

No apply uses the barrier yet; the step 3b coordinator will. Until then, bulk changes register with it at the cost of a few file-status lookups (about 0.4 ms) and an epoch count. Nothing changes for users.

Rules

  • What counts as one checkout.
    • A checkout is its Git top folder, by physical identity. A subfolder, a symlink or a path not created yet all count as the same checkout.
    • A checkout inside another (a submodule or nested repository) belongs to both. A bulk change of the outer one also waits for, and suspends, applies inside the inner one.
  • Applies and bulk changes.
    • A bulk change closes new apply admission at once, waits for running applies to finish, then runs.
    • An apply asking to start during a bulk change is refused, not queued (CheckoutSuspendedError).
  • Bulk changes of one checkout.
    • They run one at a time.
    • One made by the fiber that holds the section, while it holds it, runs inside it. That covers a provider checkout calling the Git driver. Any other fiber, a forked child included, waits its turn.
    • A queued change looks its path up again when its turn comes. It refuses if the path now names another checkout. If the path vanished and it was asked to skip missing paths, it runs without settlers.
  • Epochs. Each bulk change advances the checkout's epoch as it starts and as it ends, even when it fails. An inner checkout's epoch includes its outer ones, and a plan made against an older epoch is stale.
  • Settlers. They run inside the section before a bulk change. A settler finishes unfinished local work (owner decision 3, recover inline) or refuses the change (CheckoutRecoveryRequiredError). Step 3b registers the Overleaf settler.
  • Lookup failures. A folder that can't be examined fails with CheckoutLookupError. Hooks surface it as a GitCommandError, a restore error, or a kept storage-cleanup entry.

Where it hooks in

Each hook is one wrapper marked SCIENT-FORK:START overleaf-checkout-barrier, and they're listed in UPSTREAM.md.

Hook Covers
Git driver method table (GitVcsDriverCore.ts) Pull, switch, create-and-switch, pull-request worktree refresh, and worktree removal (relative paths resolved against the repository). Because it sits in the driver, it also covers callers that skip GitWorkflowService: startup and broadcaster auto-pull, GitManager's own calls, and provider switchRef.
CheckpointServiceV2.restore A checkpoint restore's git restore / git clean / git reset.
GitManager local pull-request checkout Provider command-line tools (for example glab mr checkout) that never reach the driver.
Storage cleanup's worktree removal Its raw worktree move / worktree remove. A refusal keeps the worktree.

The barrier is a Context.Reference whose default is one instance per server process. Every layer build shares it.

Not covered

  • By design (contract §2.8): arbitrary shell writers, agents' own Git commands, and other server profiles. Checkpoint capture only reads.
  • Accepted limit: a section that awaits another fiber's change of the same checkout waits for itself. No production caller does this.

Tests

CheckoutBarrier.test.ts has 20 tests:

  • the rules above;
  • a real git switch, and a relative-path git worktree remove, each waiting for an application;
  • a refused settlement stopping Git before it runs;
  • a checkpoint restore waiting for an application.

Mutation checks: every rule and fix was removed in turn, and its tests failed each time.

The related suites pass, apart from 14 orphan-report tests in storageCleanup.test.ts, which fail identically on main's file on macOS (/var vs /private/var). Typecheck, lint, knip and scient-seam-check pass.

Review

Five Codex rounds (gpt-6.1-sol, high reasoning), recorded in the comments.

  • Rounds 1–4 found 13 problems, all fixed with tests. The cross-fiber joining that kept producing edge cases was replaced by the same-fiber rule.
  • Round 5: merge-ready, no findings.

Next: step 3b, the coordinator's apply, recover and adopt, plus kept-copy compare and restore.

🤖 Generated with Claude Code

An Overleaf apply and a bulk change of the same checkout now exclude each
other (coordinator contract, section 9). A checkout is its Git top folder by
physical identity. A bulk change closes new apply admission at once, waits for
running applies, runs registered settlers inside its section, then mutates.
It advances the checkout's epoch as it starts and as it ends. Applies asking
to start meanwhile are refused, not queued. Bulk changes do not exclude one
another.

Hooks, each marked SCIENT-FORK overleaf-checkout-barrier:
- Git driver method table: pull, switch, create-and-switch, pull-request
  worktree refresh, worktree removal (covers callers that bypass
  GitWorkflowService, such as startup auto-pull)
- CheckpointServiceV2.restore
- GitManager's local pull-request checkout (provider CLIs)
- storage cleanup's worktree removal

The barrier is a Context.Reference with one default instance per process.
Nothing takes an application section yet; step 3b's coordinator will.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@github-actions github-actions Bot added vouch:trusted PR author is trusted by repo permissions or the VOUCHED list. size:L labels Oct 22, 2026
@github-actions

github-actions Bot commented Oct 22, 2026 •

Copy link
Copy Markdown
Contributor

Thread transfer impact

✅ Thread transfer remains within every enforced ceiling.

Provider Metric Main baseline This PR Impact PR ceiling
Codex Total thread wire 5.6 KiB 5.6 KiB 0 B (0.0%) 6.8 KiB ✅
Codex Thread snapshot wire 4.3 KiB 4.3 KiB 0 B (0.0%) 4.9 KiB ✅
Codex Live turn WebSocket wire 1.3 KiB 1.3 KiB 0 B (0.0%) 2.0 KiB ✅
Codex Live turn WebSocket decoded 26.2 KiB 26.2 KiB 0 B (0.0%) 29.3 KiB ✅
Codex Live turn messages 2 2 0 (0.0%) 8 ✅
Claude Total thread wire 5.6 KiB 5.6 KiB 0 B (0.0%) 6.8 KiB ✅
Claude Thread snapshot wire 4.3 KiB 4.3 KiB 0 B (0.0%) 4.9 KiB ✅
Claude Live turn WebSocket wire 1.3 KiB 1.3 KiB 0 B (0.0%) 2.0 KiB ✅
Claude Live turn WebSocket decoded 26.6 KiB 26.6 KiB 0 B (0.0%) 29.3 KiB ✅
Claude Live turn messages 2 2 0 (0.0%) 8 ✅

Baseline: 9d312f3 · PR result: 9745ae5 · Source CI: success

Scenario and decoded snapshot size

10 historical turns, 5 command tools per turn, 878.9 KiB retained MCP result per historical turn, and a 1.05 MiB retained result in the measured turn.
Full compact HTTP snapshot with live cursor.

  • Codex decoded thread snapshot: 133.1 KiB
  • Claude decoded thread snapshot: 133.4 KiB

Updated in place by a trusted workflow. PR artifacts are strictly validated and never executed.

…heckouts

Codex round 1 on #626:
- Bulk changes of one checkout now run one at a time, so a settler's inline
  recovery never overlaps another restore or pull. A bulk change made inside
  another of the same checkout joins it (fiber-scoped held set).
- removeWorktree resolves a relative path against the repository, as Git does.
- A checkout inside another (submodule, nested repository) belongs to both:
  an outer bulk change waits for and suspends inner applications, and inner
  epochs include the enclosing ones.
- Lookup failures are a typed CheckoutLookupError, mapped by every hook.
- The cancellation test waits for real admission before interrupting.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@yaacovcorcos

Copy link
Copy Markdown
Contributor Author

Codex review, round 1 (gpt-6.1-sol, high reasoning)

Verdict on 11d0f021f4: no, four P2s and one P3. All were reproduced, and all are fixed in HEAD.

Finding Fix
P2: inline recovery could overlap another bulk change. A settler's application ran while a different restore or pull of the same checkout was mid-way. Bulk changes of one checkout now run one at a time. One made inside another of the same checkout (for example, a provider checkout calling the driver) joins it rather than deadlocking. Test: runs bulk changes of one checkout one at a time, joining nested ones.
P2: removing a worktree by relative path skipped the barrier. The path was looked up from the server's folder; Git resolves it from the repository. The path is resolved against input.cwd. Test: a worktree removal by relative path waits for an application inside it (real git worktree remove).
P2: submodules escaped. A recursive branch switch rewrote a submodule while an apply held it. A checkout inside another belongs to both. A bulk change of the outer one waits for, and suspends, applications inside the inner one, and inner epochs include the outer one's. Test: makes a bulk change of an enclosing checkout wait for and suspend inner ones.
P2: file-system errors during the lookup became defects. For example, EACCES or ELOOP. They're now a typed CheckoutLookupError, which every hook maps (GitCommandError, restore error, or a kept storage-cleanup entry). Test: reports a folder it cannot examine as a typed failure.
P3: the cancellation test passed before admission. It now waits until the bulk change has closed admission, then asserts the epoch moved twice.

Each fix fails its test without it (mutation-checked, one failure each).

What held:

  • Shared drain waiters, interruption, stale handles and epoch finalizers.
  • One default instance across contexts.
  • All pull, switch, pull-request and removal paths reach the hooks.
  • No new lock cycle.

Now: 14 barrier tests pass. The related suites pass, apart from the 14 orphan-report tests that fail on main's file on macOS too. Typecheck and lint are clean. Round 2 is reviewing the new head.

🤖 Generated with Claude Code

@github-actions github-actions Bot added size:XL and removed size:L labels Oct 22, 2026
Codex round 2 on #626:
- A nested bulk change joins only while the inherited section is still held,
  so a detached task started inside one cannot bypass the barrier later.
- A queued bulk change looks its path up again once its turn comes and refuses
  if the path now names another checkout.
- Settlers get the inner checkout's full chain and summed epoch.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@yaacovcorcos

Copy link
Copy Markdown
Contributor Author

Codex review, round 2 (gpt-6.1-sol, high reasoning)

Verdict on 8d03f40cb2: no, two P2s and one P3. Round 1's fixes held. All three new findings were reproduced, two of them with the real Git driver, and all are fixed in HEAD.

Finding Fix
P2: an inherited "already inside" marker outlived its section. A detached task started inside a bulk change later bypassed the barrier entirely. A nested change joins only while the inherited section is still held. Test: does not let a detached task join a bulk section that has ended.
P2: a queued bulk change kept a stale identity. It changed a replacement checkout at the same path under the old identity. Once its turn comes, it looks the path up again, and refuses (CheckoutLookupError) if it now names another checkout. Test: refuses a queued bulk change whose path now names another checkout.
P3: settlers got only the innermost key and its own epoch. They now get the full chain and the summed epoch, like current and applications. Test: hands settlers an inner checkout's whole chain and summed epoch.

Each fix fails its test without it (mutation-checked, one failure each).

Known limit: a nested bulk change of the same checkout made from a fresh fiber (runFork, which has no inherited context) and awaited by its enclosing change would wait for itself. Codex found no production caller that does this.

Now: 17 barrier tests pass. The related suites pass, apart from the 14 macOS orphan-report tests that fail on main too. Lint is clean. Round 3 is reviewing the new head.

🤖 Generated with Claude Code

…hed paths

Codex round 3 on #626:
- Work that joins a live bulk section is counted, and the section is not
  released until it finishes, so joined work never runs after admission
  reopens.
- A queued change whose path vanished meanwhile, with `missing: "skip"`, runs
  without settlers, which cannot settle a checkout that is gone.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@yaacovcorcos

Copy link
Copy Markdown
Contributor Author

Codex review, round 3 (gpt-6.1-sol, high reasoning)

Verdict on 97c98a2bca: no, two P2s. Both were reproduced, and both are fixed in HEAD.

Finding Fix
Joined work could outlive its section. A nested change that joined a live section was not waited for, so it could still be changing files after admission reopened. Joined work is counted, and the section is released only once it finishes. Test: keeps a bulk section until work that joined it has finished.
A queued change of a vanished path still ran settlers. With missing: "skip", the settlers ran against the vanished checkout and could refuse an idempotent removal. When the path is gone by its turn, the change runs without settlers. Test: runs a queued change of a vanished path without settlers when told to skip.

Each fix fails its test without it (mutation-checked).

What held: round 1 and 2 fixes, refusal of stale handles, identity refusal before settlers, and epoch accounting on refusal. No new bypass or lock cycle was found.

Known limits:

  • A same-checkout bulk change from a fresh runFork, awaited by its enclosing change, waits for itself.
  • Joined work that waits for its enclosing change to return would do the same.

No production caller does either.

Now: 19 barrier tests pass. The related suites pass, apart from the 14 known macOS orphan-report tests. Lint is clean. Round 4 is reviewing the new head.

🤖 Generated with Claude Code

Codex round 4 on #626 found two more edges in cross-fiber joining (a
non-atomic liveness check, and an interrupted owner waiting on a joined child).
Production only nests bulk changes synchronously in the same fiber (a
provider checkout calling the Git driver), so joining is now limited to the
fiber that owns the section, while it holds it. Any other fiber, a forked
child included, waits its turn. The join accounting is gone with both bugs.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@yaacovcorcos

Copy link
Copy Markdown
Contributor Author

Codex review, round 4 (gpt-6.1-sol, high reasoning)

Verdict on a61e84bd1e: no, one P1 and one P2. Both were in joining a section from another fiber.

  • P1: the liveness check and the join count were separate steps, so a stale join could slip in after the section retired.
  • P2: an interrupted owner waited for a joined forkChild, while Effect interrupts children only after finalizers finish. That's a deadlock.

Resolution: a simpler rule, not another patch. Each round from 2 to 4 found a new edge in joining across fibers, while production only nests bulk changes synchronously in the same fiber (a provider checkout calling the Git driver). So:

  • A nested change joins only when made by the fiber that owns the section, while it holds it. It runs inside that fiber's own sequential work and can't outlive it.
  • Any other fiber, a forked child included, waits its turn like everyone else.

The join accounting is gone, and both bugs with it.

Tests:

  • makes another fiber's change of the same checkout wait its turn. It fails if any fiber may join (mutation-checked).
  • reopens admission when an owner is interrupted while its child waits (Codex's P2 scenario).

Known limit, now stated plainly: a section that awaits another fiber's change of the same checkout waits for itself. No production caller does this.

Now: 20 barrier tests pass. The related suites pass, apart from the 14 known macOS orphan-report tests. Lint is clean. Round 5 is reviewing the new head.

🤖 Generated with Claude Code

@yaacovcorcos

Copy link
Copy Markdown
Contributor Author

Codex review, round 5 (gpt-6.1-sol, high reasoning)

Verdict on 4a38d75612: merge-ready. No findings.

  • Round 4's P1 and P2 are resolved. Effect's fiber IDs never recycle, and the owning fiber can't finish its section while suspended. A finalizer resuming later with the owner's captured context fails the live-section check and goes through fresh admission.
  • No production code nests bulk changes across fibers. Codex checked GitManager, every provider's checkout, the broadcaster, rollback, thread launch and storage cleanup. Provider → driver switchRef stays in the owning fiber, and a real-driver probe passes.
  • Earlier guarantees hold:
    • per-checkout serialization;
    • relative removal targets;
    • nested-checkout chains and summed epochs;
    • typed lookup failures;
    • identity rechecked after waiting;
    • vanished paths skip settlers;
    • full settler chains.

Evidence: 20 barrier tests and 8 extra probes passed, plus 845 regression tests (one skipped). Storage cleanup shows the 14 known macOS orphan-report failures.

🤖 Generated with Claude Code

@yaacovcorcos
yaacovcorcos marked this pull request as ready for review October 22, 2026 20:14
yaacovcorcos and others added 2 commits October 23, 2026 01:48
…r changes

The Git driver now imports scient/workspace/CheckoutBarrier.ts, so Droid's
qualification loads it. The managed-provider workflow guards every module its
qualification runs; add the barrier file to Droid's guard list
(managed-provider-runtime-workflow.test.ts).

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@yaacovcorcos

Copy link
Copy Markdown
Contributor Author

CI fix after aligning with main

Bringing this branch up to main pulled in managed-provider-runtime-workflow.test.ts. That test requires the Droid publication workflow to watch every module Droid's qualification loads. The Git driver now imports scient/workspace/CheckoutBarrier.ts, so I've added that one file to Droid's guard list in .github/workflows/managed-provider-runtime-update-provider.yml. The test passes locally (17/17). The code is unchanged since Codex's merge-ready round 5.

🤖 Generated with Claude Code

@yaacovcorcos
yaacovcorcos added this pull request to the merge queue Oct 22, 2026
Merged via the queue into main with commit 6a53599 Oct 23, 2026
65 of 67 checks passed
@yaacovcorcos
yaacovcorcos deleted the claude/overleaf-checkout-barrier-20261022 branch October 23, 2026 00:10
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

size:XL vouch:trusted PR author is trusted by repo permissions or the VOUCHED list.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant