|
| 1 | +# Model Checking with TLA+ |
| 2 | + |
| 3 | +Before changing how stages, queues, or services hand work to each other, we write the protocol down in TLA+ and let the TLC model checker try every ordering of its steps. This RFC proposes when that is required, where the specs live, how CI runs them, and how they stay tied to the Go code. It also explains why more e2e and integration testing cannot do this job. |
| 4 | + |
| 5 | +## Problem |
| 6 | + |
| 7 | +SubmitQueue's worst bugs are not mistakes inside one controller. They are mistakes in the protocol between controllers: a message redelivered after a lost ack, a compare-and-swap lost to another writer, a dead letter reconciled while another stage is still working, a service answering a question the other side has stopped asking. Each controller is correct on its own, and the system is wrong. |
| 8 | + |
| 9 | +The record so far: |
| 10 | + |
| 11 | +| Issue | What went wrong | Found by | Within reach of a spec | |
| 12 | +|---|---|---|---| |
| 13 | +| [#352](https://github.com/uber/submitqueue/issues/352) | Re-trigger publishes reused message IDs and were silently deduped; the pipeline stalled | e2e test hung | Yes: a queue model with dedup | |
| 14 | +| [#821](https://github.com/uber/submitqueue/issues/821) | One batch that could not be scored stopped every batch in the queue | Demo run | Partly: the zero-value batch is a code bug; "one batch's error halts the queue" is a rule a spec states | |
| 15 | +| [#818](https://github.com/uber/submitqueue/issues/818) | DLQ reported `error` for a change that had landed | Demo run, after the push to a real repo | Yes | |
| 16 | +| [#822](https://github.com/uber/submitqueue/issues/822) | A batch stranded in `speculating` with nothing to wake it | Demo run | Yes | |
| 17 | +| [#823](https://github.com/uber/submitqueue/issues/823) | A batch merged on an assumption that had not come true, putting an unbuilt combination on the trunk | Reading the predicates by hand | Yes | |
| 18 | +| [#824](https://github.com/uber/submitqueue/issues/824) | An acked message was redelivered at a fifth of its visibility timeout | Demo run under load | No as a design check: the code strayed from the queue's design. Checking runs against the spec would flag it | |
| 19 | +| [#817](https://github.com/uber/submitqueue/issues/817) | A batch orphaned in `created` wedged its queue for 50+ minutes | Demo run, 65 of 100 PRs in | Yes | |
| 20 | +| [#825](https://github.com/uber/submitqueue/issues/825) | A cancel during batch promotion let a cancelled request reach speculation | Code review | Yes | |
| 21 | +| [#826](https://github.com/uber/submitqueue/issues/826) | The batch DLQ failed requests that another live batch owned | Code review | Yes | |
| 22 | +| [#819](https://github.com/uber/submitqueue/issues/819) | Land and landsignal DLQs fail a `landing` batch that Runway merges | TLC | Found by one | |
| 23 | +| [#820](https://github.com/uber/submitqueue/issues/820) | Runway's DLQ answers `FAILED` for a push that landed | TLC | Found by one | |
| 24 | + |
| 25 | +Nine of the eleven are protocol bugs, and every one of those nine came from a demo run, a hung test, or a careful reviewer. None came from a test written to find it. #819 and #820 were found in an afternoon with a 250-line spec, before anyone saw them happen. #825 and #826 were spotted in review and are still open: the code paths they describe are unchanged on `main`, because nothing short of building the exact ordering would show the bug. |
| 26 | + |
| 27 | +## Why e2e and integration tests cannot close the gap |
| 28 | + |
| 29 | +They are necessary, and they find the code bugs in that table (#821, #824). They cannot find protocol bugs reliably, for reasons that more tests do not fix: |
| 30 | + |
| 31 | +- **They try one ordering per run.** A protocol bug needs a particular fault at a particular step. #819 needs a lost ack after the Runway publish, followed by storage errors on every retry. No run produces that by chance. |
| 32 | +- **Each ordering they pin is built by hand.** `TestCancel_CaughtPreBatch_NeverLands` is deterministic only because it closes a [consumer gate](consumer-gate.md) on Runway's conflict check, to catch the cancel before batching. That pins one ordering. #825's ordering, a cancel between the claim and the promote, needs a different gate at a different stage, and nobody thought to build it until review found the bug. A test checks the orderings its author imagined, while TLC checks every ordering the model allows. |
| 33 | +- **They need scale that CI does not have.** #817 appeared 65 PRs into a 100-PR run, and #824 on a 20-PR run but not on smaller ones. |
| 34 | +- **They show the symptom, not the cause.** #824 could not be root-caused because the row that would have explained it had already been garbage-collected. TLC returns the shortest sequence of steps that breaks the rule, each one named for a controller. |
| 35 | +- **They need the code to exist.** A spec compares designs before any are built. #825 and #826 were caught by reviewers working out orderings in their heads during review of a fix. That works, but it doesn't scale, and it misses some. |
| 36 | +- **Unit tests see one controller.** Every protocol bug above sits between two controllers or two services. #825's acceptance criteria ask for a hand-written test of the two writers interleaving, which can only be written after the ordering is already known. |
| 37 | + |
| 38 | +## Decision |
| 39 | + |
| 40 | +### When a spec is required |
| 41 | + |
| 42 | +A change needs a spec, or an update to an existing one, when it alters any of these: |
| 43 | + |
| 44 | +- the hand-off between pipeline stages, |
| 45 | +- DLQ reconciliation, |
| 46 | +- the order in which two writers compare-and-swap the same record, |
| 47 | +- message IDs or dedup, |
| 48 | +- a contract with another service, |
| 49 | +- the queue's delivery semantics. |
| 50 | + |
| 51 | +Everything else, including most controller logic, extensions, and APIs, does not. |
| 52 | + |
| 53 | +### What a spec contains |
| 54 | + |
| 55 | +A spec models one protocol and states what it leaves out. Each step is named for the controller it stands for and points at its file. The rules it checks are the repository's own rules: a terminal batch keeps its outcome, a reported result matches the target branch, persist before publish, every stuck entity eventually reaches a terminal state. One configuration checks today's behavior. Design alternatives are constants that are checked side by side, so choosing between them becomes a table rather than a debate. |
| 56 | + |
| 57 | +### Where specs live and how they run |
| 58 | + |
| 59 | +Specs live under `spec/{domain}/{protocol}/`, mirroring the domain folders. A spec that crosses services lives with the domain whose rule it checks. A shared model of the message queue lives under `spec/platform/`, and pipeline specs build on it. Specs do not live next to RFCs, because they need to share the queue model. |
| 60 | + |
| 61 | +`tool/tlc` runs TLC under Bazel: the TLA+ tools JAR is pinned in `MODULE.bazel` and runs on a downloaded JDK, so nobody installs Java or fetches a JAR by hand, locally or in CI. Each spec has a matrix file listing its design constants and the expected verdict for every combination; `tlc_matrix_test` turns it into a test that `make test` runs, failing when any verdict changes. `bazel run //tool/tlc -- <matrix.json>` prints the table. A matrix stays small enough to check in under a minute; larger explorations are tagged `manual`. |
| 62 | + |
| 63 | +### How specs stay tied to the code |
| 64 | + |
| 65 | +A spec is a second description of the system, and it drifts unless something connects the two. That connection is built in steps, and each step stands on its own: |
| 66 | + |
| 67 | +1. **Review.** A PR that changes a protocol from the list above updates the spec in the same PR. A protocol bug report includes the TLC trace, and its fix shows the trace gone. |
| 68 | +2. **Check runs against the spec.** Map the request log and controller logs from e2e runs onto spec steps, and have TLC confirm that each recorded run is one the spec allows. This is the step that would have flagged #824. |
| 69 | +3. **Replay specs against the code.** Have TLC list orderings, and play each one against real controllers wired to in-memory stores and queues. Controllers already take their dependencies as injected interfaces, which makes this unusually practical here. |
| 70 | + |
| 71 | +## Evidence: the land outcome spec |
| 72 | + |
| 73 | +[`spec/submitqueue/landoutcome`](../../spec/submitqueue/landoutcome/LandOutcome.tla) models one batch going from `landing` to a terminal state, across `land`, Runway's merge controller and its DLQ, `landsignal`, and the orchestrator's DLQs. It checks three rules: a failed batch is not on the branch, a succeeded batch is, and a landing batch eventually settles. Four constants hold the design choices, and its [matrix](../../spec/submitqueue/landoutcome/matrix.json) checks all 24 combinations in about six seconds. |
| 74 | + |
| 75 | +| Orchestrator DLQ on a landing batch | Runway DLQ answers | Runway remembers verdicts | Answers dedup on request ID | Result | |
| 76 | +|---|---|---|---|---| |
| 77 | +| fail it (today) | any | any | any | Failed while merged ([#819](https://github.com/uber/submitqueue/issues/819)) | |
| 78 | +| any | FAILED (today) | any | any | Failed while merged ([#820](https://github.com/uber/submitqueue/issues/820)) | |
| 79 | +| leave it | checks the branch | any | any | Stuck in `landing` forever | |
| 80 | +| re-send to Runway | checks the branch | no (today) | any | A stale FAILED wins | |
| 81 | +| re-send to Runway | checks the branch | yes | yes (today) | Replay swallowed by dedup | |
| 82 | +| re-send to Runway | checks the branch | yes | no | All three rules hold | |
| 83 | + |
| 84 | +TLC found two live bugs. It also showed that the two obvious fixes are wrong, each in a way that does not show up in a quick run: one trades a wrong answer for a batch that never finishes, and the other trips over the dedup behavior from #352. It also turned four assumptions about Runway that no document states into explicit choices. |
| 85 | + |
| 86 | +## What we do not get |
| 87 | + |
| 88 | +- **Proof for every size.** TLC checks small instances, such as three batches and two faults. Protocol bugs nearly always show up at that size, and every bug above did, but a pass is strong evidence, not proof. |
| 89 | +- **Code bugs.** #821's zero-value batch is invisible to a spec. Step 2 of tying specs to code catches the code straying from the spec, which is a different thing. |
| 90 | +- **Correctness for free.** A spec that leaves out the wrong detail passes and means nothing. The first version of the matrix runner reported TLC parse errors as passes, and concurrent TLC runs sharing a temp directory failed intermittently. Specs and their harnesses need review like any other code. |
| 91 | +- **Performance answers.** TLC says nothing about latency, throughput, or build budget sizing. |
| 92 | + |
| 93 | +## Rollout |
| 94 | + |
| 95 | +| Phase | Work | Done when | |
| 96 | +|---|---|---| |
| 97 | +| 1 | Choose the land outcome contract for #819 and #820 from the matrix | The fix for both issues ships with its matrix row passing | |
| 98 | +| 2 | Queue model (redelivery, dedup, hold); batch creation and cancel; speculation outcomes | Each spec reproduces its historical bugs (#352, #822, #823, #817, #825, #826) and passes once the fix is in the model | |
| 99 | +| 3 | Check e2e runs against the specs | A deliberately introduced deviation is flagged | |
| 100 | +| 4 | Replay spec orderings against real controllers | Decided after phase 3 | |
| 101 | + |
| 102 | +Phase 2 is the real test of this proposal. If a spec cannot reproduce the bug it was written for, or takes much more than a week to write, we stop at phase 1 and keep specs only for cross-service contracts. |
| 103 | + |
| 104 | +## Alternatives considered |
| 105 | + |
| 106 | +- **More e2e tests with fault injection.** Still one ordering per run, and still a new lever for every step that needs a fault. This complements specs but cannot replace them. |
| 107 | +- **Deterministic simulation of the real code.** This means running the services under one scheduler with every store, queue, clock, and external call faked, then exploring orderings and faults. It is the strongest option because it tests the code itself, but it needs all of that infrastructure first. Phase 4 is the cheap first step toward it, and it is not ruled out. |
| 108 | +- **Property-based tests of controllers.** These generate inputs for one controller at a time. Every bug above lives between controllers. |
| 109 | +- **Other specification languages.** Quint has the same logic as TLA+ with a syntax closer to Go, and runs on the same checkers, so it remains an option for spec authors. P targets message-passing systems and can generate tests, but its tooling is thinner. Alloy is strong for data shapes and weaker for orderings over time. TLA+ has the most mature checker and the largest body of industrial use. |
| 110 | + |
| 111 | +## Open questions |
| 112 | + |
| 113 | +- Should spec review require a second reader who knows TLA+? Without one, an abstraction mistake gets no review. |
| 114 | +- Do specs get written in PlusCal, which reads closer to Go, or in plain TLA+? |
| 115 | +- Should Runway gain the per-request state that the one fully passing land design requires, or is there a cheaper design that also passes? Phase 1 answers this. |
0 commit comments