Created
March 17, 2025 23:39
-
-
Save lemmy/155632207d7fc59105e782460d0b082f to your computer and use it in GitHub Desktop.
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
| ----- MODULE MergeQueueProcess ----- | |
| EXTENDS Naturals | |
| CONSTANT PRs | |
| VARIABLE pullRequests, time | |
| Init == | |
| /\ pullRequests = [pr \in PRs |-> [state |-> "pending", t |-> 0]] | |
| /\ time = 0 | |
| Queuer(pr) == | |
| /\ time' = time + 1 | |
| /\ pullRequests[pr].state = "pending" | |
| /\ pullRequests' = [pullRequests EXCEPT ![pr].state = "queued-waiting-validation", ![pr].t = time'] | |
| CI(pr) == | |
| /\ time' = time + 1 | |
| /\ pullRequests[pr].state = "queued-waiting-validation" | |
| /\ pullRequests' \in {[pullRequests EXCEPT ![pr].state = "queued-validated"], | |
| [pullRequests EXCEPT ![pr].state = "queued-failed"]} | |
| Worker(pr) == | |
| /\ time' = time + 1 | |
| /\ \/ /\ pullRequests[pr].state = "queued-validated" | |
| /\ \A p \in (PRs \ {pr}) : | |
| pullRequests[p].t < pullRequests[pr].t => pullRequests[p].state = "merged" | |
| /\ pullRequests' = [pullRequests EXCEPT ![pr].state = "merged"] | |
| \/ /\ pullRequests[pr].state = "queued-failed" | |
| /\ pullRequests' = [pullRequests EXCEPT ![pr].state = "blocked"] | |
| Next == | |
| \/ \E prn \in PRs: | |
| \/ Queuer(prn) | |
| \/ CI(prn) | |
| \/ Worker(prn) | |
| -------------------------------- | |
| Spec == | |
| Init /\ [][Next]_<<pullRequests, time>> /\ WF_<<pullRequests, time>>(Next) | |
| Done == | |
| <>[](\A prn \in {p \in PRs: pullRequests[p].state # "blocked" }: pullRequests[prn].state = "merged") | |
| ===== |
Author
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Click here to Interactively explore the spec.
Problem Description
The process described below is about modeling a merge queue system that manages the lifecycle of pull requests (PRs) as they progress through various states before being merged or blocked. The system consists of multiple actors:
State Transitions in the Merge Queue System
The state of a PR changes through the following transitions:
Processes Driving State Transitions
There are three processes in the system that work in parallel:
Queuer Process (Queuer):
CI Worker Process (CI):
If a PR is in queued-waiting-validation, it determines whether the PR passes or fails CI:
If passed → queued-validated
If failed → queued-failed
Merge Queue Worker Process (Worker):
If a PR is in queued-validated and all previously queued PRs have been merged, it transitions to merged. If a PR is in queued-failed, it transitions to blocked.
Handling Queue Order
To enforce merge order: Each PR is assigned a timestamp when queued. A PR can only be merged if all earlier queued PRs have already been merged. Eventually, ever non-blocked PR is merged.
Sequence Diagram
sequenceDiagram participant Developer participant Queuer participant CI_Worker as CI Worker participant Merge_Queue_Worker as Merge Queue Worker Developer ->> Queuer: Submit PR (pending) Queuer ->> Queuer: Move PR to queued-waiting-validation Queuer ->> CI_Worker: PR ready for validation CI_Worker ->> CI_Worker: Validate PR alt If validation passes CI_Worker ->> Merge_Queue_Worker: PR status: queued-validated else If validation fails CI_Worker ->> Merge_Queue_Worker: PR status: queued-failed end Merge_Queue_Worker ->> Merge_Queue_Worker: Check PR state alt If PR is queued-validated and prior PRs are merged Merge_Queue_Worker ->> Merge_Queue_Worker: Transition PR to merged else If PR is queued-failed Merge_Queue_Worker ->> Merge_Queue_Worker: Transition PR to blocked endCredit
The specification is heavily inspired by https://www.aviator.co/blog/merge-queue-tla/