Add TLA+ model for deployment concurrency leases - #23030
Conversation
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
![devin-ai-integration[bot]](https://avatars.githubusercontent.com/in/811515?s=60&v=4){kind=small}
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: f52502acf8
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: ce88c8653a
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| ClaimReacquire(r, l) == | ||
| LET old == stateLease[r] IN | ||
| /\ runState[r] = "Pending" | ||
| /\ old # NoLease | ||
| /\ leaseState[old] = "Absent" |
There was a problem hiding this comment.
When a PENDING run with an expired lease still has a future scheduled_time, ValidateDeploymentConcurrencyAtRunning acquires a slot and creates a replacement lease, but the later WaitForScheduledTime rule nullifies the transition; ReleaseFlowConcurrencySlots explicitly skips nullified transitions, so the persisted PENDING state retains its old lease ID while the replacement slot and lease are orphaned. ClaimReacquire has no corresponding rollback/nullification action, so the target cannot explore this mapped retry path or its accounting consequences; model it and add a regression, or explicitly exclude it.
AGENTS.md reference: formal/tla/AGENTS.md:L18-L21
Useful? React with 👍 / 👎.
| CreateLease == | ||
| /\ txnKind = "Acquire" | ||
| /\ leaseState[txnLease] = "Unused" | ||
| /\ leaseState' = [leaseState EXCEPT ![txnLease] = "Live"] | ||
| /\ leaseOwner' = [leaseOwner EXCEPT ![txnLease] = txnRun] |
There was a problem hiding this comment.
With a durable external lease store such as the filesystem implementation, terminating the server after create_lease succeeds but before the surrounding orchestration database transaction commits rolls back the slot increment while leaving a live lease; after another run acquires that capacity, reaping the orphan can decrement the replacement run's slot. The split model allows CreateLease only to remain stuck in Acquire or proceed to CommitAcquire, so it implicitly assumes this cross-store crash cannot occur even though the README does not exclude process failure; add an abort action and counterexample or state that availability assumption explicitly.
AGENTS.md reference: formal/tla/AGENTS.md:L11-L13
Useful? React with 👍 / 👎.
1 participant
Adds a bounded TLA+ model of deployment-concurrency release authority and durable repository guidance for keeping future models mapped to production contracts.
xfailregressions.AGENTS.md.The target model does not specify a production schema, migration, or replay protocol, and a green TLC run is not evidence that Prefect's Python implementation conforms.
Related to #22935
Checks and scope
The CI job uses Temurin 21 and checksum-verified TLA+ Tools
v1.7.4. The target explores 55,915 distinct states with no invariant violation. The unsafe configurations fail with their expectedRenewWinsAgainstStaleScanorNoForeignReleaseinvariant.