Repository navigation
Conversation
Each Modal invocation runs one replay worker, and separate invocations shared no limit, so a third concurrent run would exceed the two the shared account allows. Before app.run(), an invocation now takes one of two slots in the Modal Dict scorecard-replay-simulation-slots: put(skip_if_exists=True) is an atomic create-if-absent on the server. A lease outlasts the function timeout; an expired one is reclaimed by whoever first creates its one-time reclaim token. The slot is released in a finally, interrupts included. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
|
The latest updates on your projects. Learn more about Vercel for GitHub.
|
Review of 14d6dab found three ways the two-slot lease could fail: a reclaimer dying between creating its one-time token and taking the slot lost that slot for good; a holder past its lease could pop a newer claim in release, and a reclaimer's unconditional pop could delete a claim made after it looked, each allowing a third simulation; and the property test asserted something false once 24 ticks passed. Every change of holder, and every renewal, now creates the slot's next generation key with put(skip_if_exists=True), Modal's atomic create-if-absent; nothing is popped, and a holder writes only its own key, only to release or shorten it. A head key names the newest generation as a hint (readers walk forward), and a random chain id separates keys written after Modal expires idle entries. main() renews the lease after the image build, just before the remote call, and the remote function refuses to start unless its 3-hour timeout fits in the lease, so a run ends before its slot can pass on even if the client dies. A renewal after the lease lapsed is refused (exit 75). After ctrl-C, Modal's client asks the server to stop the app's tasks (modal/runner.py _disconnect), and the slot frees 10 minutes later instead of at once. Tests drive the protocol call by call: the review's three scenarios, a holder dying after each possible step, a stale renewal after Modal expired the chain, and a Hypothesis model check interleaving 2-4 holders' Dict calls with clock jumps, crashes, interrupts and 7-day entry expiry (no two runs overlap on a slot; both slots are free again once every lease lapses). 20,000 generated schedules hold; each protection's deterministic test fails when that protection is removed. Assumption, stated in the docstring and RECIPE: no process stalls for days inside one protocol step. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Review of dff81d0: - Modal's runner re-raises a lost connection (modal.exception .ConnectionError) without sending its stop request (modal/runner.py, the ConnectionError branch of _run_app), yet main() freed the slot ten minutes later while the container could run for three hours. The grace now applies only when app.run() itself exits after a caught ctrl-C, where the runner awaited the stop request; any other exception after the run started leaves the claim until the lease lapses, which the remote guard puts after the run's end. A remote error now holds the slot until then too (conservative). - A writer stalled across Modal's 7-day expiry could overwrite head-{slot} with its dead chain and hide a live holder. A protocol step (acquire or renew) that took over a day now gives its claim back and writes no head. - The remote guard keeps a 10-minute margin inside the lease for clock differences and kill latency. - The model check now caps stalls per protocol step, not per tick, and models a lost connection (the run continues to its own end, nothing is written). New tests: a week-stalled acquire cannot replace a live chain; a lost connection keeps the claim at its full lease; a finished run frees the slot at once; the stale-renewal scenario now asserts that the key it would recreate is absent. 20,000 generated schedules hold; the head test fails when the stale-step bail is removed. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Review of 4a5a272: - The step's clock was read after the head response, so a response left unread through a week asleep looked fresh. It is now read before the first call. - A head write landing a week late, after its keys expired, could point readers at a dead chain and hide a live holder. A reader whose head names a claim that is gone now blocks the slot for one lease (any hidden holder's lease began before that write) instead of taking it. - A claim whose head write fails is given back at once, on acquire and on renewal, instead of holding the slot for a lease with no run. - A result that returned is downloaded even if leaving the app then fails. - The docstring and RECIPE now state the guarantee against Modal's 7-day entry expiry, the two detected long-stall cases, and the one case not covered (a head write 7+ days late naming a generation that still exists while later ones expired), instead of an unconditional claim. Tests: a head response read before a week asleep (with and without a claim), a head written a week late, a failed head write on acquire and renewal, a returned result surviving a failed app exit; the model's final phase allows one blocked lease. Each new protection's test fails when the protection is removed; 20,000 generated schedules hold. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Review of bac8974 reproduced three failures by running the code: 1. A head write delayed 6.5 days plus a reader stalled 0.95 days recreated expired generations and overlapped a live run, inside the guarantee as stated. Any pointer can be rolled back by a late write, so the pointer is gone. A slot now has one chain of claims per calendar day (claim-{slot}-{day}-{generation}); a caller creates a chain's next generation, with Modal's atomic create-if-absent, only when its newest one is released or lapsed. A lease that crosses midnight holds a claim in both days' chains, taken in order and given back together. A day's chain matters for at most a day plus a lease, far inside the 7 days after which Modal expires idle entries, so no claim that still matters can have expired and a late write lands in a chain that governs nothing. The guarantee no longer assumes anything about stalls. Head keys, chain ids, the blocker claim, the stale-step bail and renewal are removed. 2. A contender whose clock ran five hours fast took an occupied slot. Leases now run on Modal's clock: main() measures its offset with a small remote function, checks it again after waiting for a slot (drift over 30 s stops the run, exit 75), and a lapsed claim is taken only 2 minutes past its expiry. 3. A Dict failure at release discarded a completed result. A failed release is now reported and the result is still downloaded; the claim lapses. The slot is taken inside app.run(), after the image build, so a build no longer consumes lease time. Tests: the model check now has no stall cap and gives each holder its own clock within the enforced drift, with jumps of any size (including 6.5 and 8 days) at any point, midnight crossings, crashes, interrupts, lost connections and entry expiry; 20,000 generated schedules hold. New deterministic tests cover the clock margin, a lease across midnight, a refused second day, a step that outlasts its lease, the reviewer's late write and five-hour-fast-clock scenarios, the offset measurement, a failed release, and a clock that moved while waiting. Removing the takeover margin, the newest-claim check, the second day's claim or the time-left check each fails a deterministic test. Verified on Modal: a real --preflight-only invocation ran the clock function, took generation 0 in today's and tomorrow's chains (the lease crossed UTC midnight), passed the remote guard and released both claims. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
This branch was successfully deployed
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.
WIP: W6 of the Autumn Budget 2026 CI plan, whose brief caps Modal at two concurrent simulations. Independent of the W6 stack (#160–#165); it branches from main.
Why
pipeline/modal_uk_event.pyruns one replay worker per invocation (max_containers=1,workers=1). Separate invocations shared no limit, so a third concurrent invocation exceeded two simulations. The r4 audit flagged this as "separate Modal invocations currently have no global limit".What
app.run(), an invocation takes one of two slots in the Modal Dictscorecard-replay-simulation-slots(SimulationSlots). Taking a slot usesDict.put(key, value, skip_if_exists=True), an atomic server-side create-if-absent. I read its source in modal 1.3.2:DictUpdateRequest(if_not_exists=...)returnscreated.finally, including on interrupt. Only the holder can release its slot.Invariants and tests (
tests/test_modal_uk_event.py)The 44 Modal-adapter and adoption tests pass.
axiom: n/a: replay infrastructure in scorecard.
🤖 Generated with Claude Code