From 968bbf9abfc60211ad7f8b92e608e932070507a3 Mon Sep 17 00:00:00 2001 From: Preetam Dwivedi Date: Thu, 8 Oct 2026 08:09:40 -0700 Subject: [PATCH] docs(rfc): propose model checking protocols with TLA+ MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit ## Summary ### Why? Nine of our last eleven serious bugs were protocol bugs between controllers or services: dead letters, lost acks, CAS races, dedup. Every one was found by a demo run, a hung test, or a reviewer, never by a test written to find it. More e2e coverage cannot fix that, because each run samples one ordering and each pinned ordering needs a hand-built lever. ### What? - `doc/rfc/tla-plus.md`: proposal covering when a change needs a TLA+ spec, the `spec/{domain}/{protocol}/` layout, CI, staged ties to the Go code, a rollout with a stop criterion, and why e2e and integration tests cannot close the gap. - `spec/submitqueue/landoutcome/`: a spec of a batch going from `landing` to terminal across orchestrator and Runway, plus a matrix of 24 DLQ and Runway design combinations with the expected verdict for each. It found #819 and #820, and showed that both obvious fixes are wrong. - `tool/tlc/`: a Python runner and a `tlc_matrix_test` macro. The TLA+ tools JAR is pinned in `MODULE.bazel` and runs on a downloaded JDK (`--java_runtime_version=remotejdk_21`), so nobody installs Java or fetches a JAR, locally or in CI. ## Test Plan ✅ `bazel test //spec/submitqueue/landoutcome:matrix_test`: all 24 verdicts match, in about 6s; `--runs_per_test=10` stable ✅ a deliberately wrong expectation fails the test ✅ `make tidy`, `make gazelle`, and `make fmt` leave the tree unchanged; license linter; `//tool/docsite:site_test` ## Issue Part of #819, #820 --- .bazelrc | 4 + MODULE.bazel | 12 + doc/rfc/index.md | 1 + doc/rfc/tla-plus.md | 115 +++++++++ spec/submitqueue/landoutcome/BUILD.bazel | 7 + spec/submitqueue/landoutcome/LandOutcome.tla | 253 +++++++++++++++++++ spec/submitqueue/landoutcome/matrix.json | 23 ++ tool/README.md | 4 + tool/tlc/BUILD.bazel | 26 ++ tool/tlc/defs.bzl | 25 ++ tool/tlc/tlc.py | 179 +++++++++++++ 11 files changed, 649 insertions(+) create mode 100644 doc/rfc/tla-plus.md create mode 100644 spec/submitqueue/landoutcome/BUILD.bazel create mode 100644 spec/submitqueue/landoutcome/LandOutcome.tla create mode 100644 spec/submitqueue/landoutcome/matrix.json create mode 100644 tool/tlc/BUILD.bazel create mode 100644 tool/tlc/defs.bzl create mode 100644 tool/tlc/tlc.py diff --git a/.bazelrc b/.bazelrc index 0bf6c32e6..c11b225da 100644 --- a/.bazelrc +++ b/.bazelrc @@ -22,3 +22,7 @@ common --sandbox_default_allow_network=false # containers running after a failure for inspection. test --test_env=DOCKER_HOST test --test_env=SKIP_CLEANUP + +# Run Java (TLC under //tool/tlc) on a downloaded JDK rather than whatever is +# installed locally, so model checking needs no host Java and behaves the same in CI. +common --java_runtime_version=remotejdk_21 diff --git a/MODULE.bazel b/MODULE.bazel index e63794f8f..d1e707641 100644 --- a/MODULE.bazel +++ b/MODULE.bazel @@ -6,6 +6,7 @@ bazel_dep(name = "rules_go", version = "0.57.0") bazel_dep(name = "gazelle", version = "0.45.0") bazel_dep(name = "rules_proto", version = "7.1.0") bazel_dep(name = "rules_python", version = "2.2.0") +bazel_dep(name = "rules_java", version = "8.14.0") single_version_override( module_name = "git", @@ -89,3 +90,14 @@ pip.parse( requirements_lock = "//tool/docsite:requirements_lock.txt", ) use_repo(pip, "docsite_pip") + +# TLA+ tools for the TLC model checker (//tool/tlc). TLC runs on the hermetic JDK +# rules_java provides, so neither a local Java install nor a manual download is needed. +http_file = use_repo_rule("@bazel_tools//tools/build_defs/repo:http.bzl", "http_file") + +http_file( + name = "tla2tools", + downloaded_file_path = "tla2tools.jar", + sha256 = "936a262061c914694dfd669a543be24573c45d5aa0ff20a8b96b23d01e050e88", + urls = ["https://github.com/tlaplus/tlaplus/releases/download/v1.7.4/tla2tools.jar"], +) diff --git a/doc/rfc/index.md b/doc/rfc/index.md index f27eaaf0c..99bd64483 100644 --- a/doc/rfc/index.md +++ b/doc/rfc/index.md @@ -13,6 +13,7 @@ Design documents and technical proposals, grouped by scope. Shared/cross-cutting - [Scoped Sequential Resource IDs](scoped-resource-ids.md) - Queue-scoped positive numeric IDs allocated by durable per-domain, per-kind counters, stored without queue/kind prefixes, and rendered directly in resource URL segments - [Hooks Framework](hook-framework.md) - Implemented fire-and-forget side effects: one shared `HookEvent` contract (`api/base/hook/`) on a durable per-domain hook topic, dispatched by `platform/hook` to `platform/extension/hook`. Stovepipe `process` and `record` publish repository events; the SubmitQueue orchestrator registers the stage and does not publish events yet - [Service-Scoped Extensions](service-scoped-extensions.md) - Implemented for SubmitQueue storage: gateway and orchestrator aggregates, schemas, and the core packages that serve one service have moved, while store contracts stay at `submitqueue/extension/storage`. Domain-level `buildrunner`, `conflict`, and `speculation` have not moved, and `changeset` still declares its own store slice +- [Model Checking with TLA+](tla-plus.md) - Proposed: write cross-stage and cross-service protocols as TLA+ specs and check every ordering with TLC; when a spec is required, `spec/` layout, CI, staged ties to the Go code, and why e2e and integration tests cannot find these bugs (#819 and #820 found this way) ## SubmitQueue diff --git a/doc/rfc/tla-plus.md b/doc/rfc/tla-plus.md new file mode 100644 index 000000000..85b3d711c --- /dev/null +++ b/doc/rfc/tla-plus.md @@ -0,0 +1,115 @@ +# Model Checking with TLA+ + +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. + +## Problem + +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. + +The record so far: + +| Issue | What went wrong | Found by | Within reach of a spec | +|---|---|---|---| +| [#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 | +| [#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 | +| [#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 | +| [#822](https://github.com/uber/submitqueue/issues/822) | A batch stranded in `speculating` with nothing to wake it | Demo run | Yes | +| [#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 | +| [#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 | +| [#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 | +| [#825](https://github.com/uber/submitqueue/issues/825) | A cancel during batch promotion let a cancelled request reach speculation | Code review | Yes | +| [#826](https://github.com/uber/submitqueue/issues/826) | The batch DLQ failed requests that another live batch owned | Code review | Yes | +| [#819](https://github.com/uber/submitqueue/issues/819) | Land and landsignal DLQs fail a `landing` batch that Runway merges | TLC | Found by one | +| [#820](https://github.com/uber/submitqueue/issues/820) | Runway's DLQ answers `FAILED` for a push that landed | TLC | Found by one | + +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. + +## Why e2e and integration tests cannot close the gap + +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: + +- **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. +- **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. +- **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. +- **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. +- **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. +- **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. + +## Decision + +### When a spec is required + +A change needs a spec, or an update to an existing one, when it alters any of these: + +- the hand-off between pipeline stages, +- DLQ reconciliation, +- the order in which two writers compare-and-swap the same record, +- message IDs or dedup, +- a contract with another service, +- the queue's delivery semantics. + +Everything else, including most controller logic, extensions, and APIs, does not. + +### What a spec contains + +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. + +### Where specs live and how they run + +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. + +`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 -- ` prints the table. A matrix stays small enough to check in under a minute; larger explorations are tagged `manual`. + +### How specs stay tied to the code + +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: + +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. +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. +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. + +## Evidence: the land outcome spec + +[`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. + +| Orchestrator DLQ on a landing batch | Runway DLQ answers | Runway remembers verdicts | Answers dedup on request ID | Result | +|---|---|---|---|---| +| fail it (today) | any | any | any | Failed while merged ([#819](https://github.com/uber/submitqueue/issues/819)) | +| any | FAILED (today) | any | any | Failed while merged ([#820](https://github.com/uber/submitqueue/issues/820)) | +| leave it | checks the branch | any | any | Stuck in `landing` forever | +| re-send to Runway | checks the branch | no (today) | any | A stale FAILED wins | +| re-send to Runway | checks the branch | yes | yes (today) | Replay swallowed by dedup | +| re-send to Runway | checks the branch | yes | no | All three rules hold | + +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. + +## What we do not get + +- **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. +- **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. +- **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. +- **Performance answers.** TLC says nothing about latency, throughput, or build budget sizing. + +## Rollout + +| Phase | Work | Done when | +|---|---|---| +| 1 | Choose the land outcome contract for #819 and #820 from the matrix | The fix for both issues ships with its matrix row passing | +| 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 | +| 3 | Check e2e runs against the specs | A deliberately introduced deviation is flagged | +| 4 | Replay spec orderings against real controllers | Decided after phase 3 | + +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. + +## Alternatives considered + +- **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. +- **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. +- **Property-based tests of controllers.** These generate inputs for one controller at a time. Every bug above lives between controllers. +- **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. + +## Open questions + +- Should spec review require a second reader who knows TLA+? Without one, an abstraction mistake gets no review. +- Do specs get written in PlusCal, which reads closer to Go, or in plain TLA+? +- 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. diff --git a/spec/submitqueue/landoutcome/BUILD.bazel b/spec/submitqueue/landoutcome/BUILD.bazel new file mode 100644 index 000000000..c8dfc5c94 --- /dev/null +++ b/spec/submitqueue/landoutcome/BUILD.bazel @@ -0,0 +1,7 @@ +load("//tool/tlc:defs.bzl", "tlc_matrix_test") + +tlc_matrix_test( + name = "matrix_test", + matrix = "matrix.json", + spec = "LandOutcome.tla", +) diff --git a/spec/submitqueue/landoutcome/LandOutcome.tla b/spec/submitqueue/landoutcome/LandOutcome.tla new file mode 100644 index 000000000..6f08d3371 --- /dev/null +++ b/spec/submitqueue/landoutcome/LandOutcome.tla @@ -0,0 +1,253 @@ +---------------------------- MODULE LandOutcome ---------------------------- +(***************************************************************************) +(* One batch's trip from `landing` to a terminal state, across the *) +(* orchestrator and Runway. *) +(* *) +(* Modelled: the orchestrator `land` stage, which publishes a MergeRequest *) +(* to Runway as its last step; Runway's merge controller, whose git merger *) +(* is idempotent on redelivery; Runway's DLQ reconciler; `landsignal`, *) +(* which applies a verdict unless the batch is already terminal; and the *) +(* orchestrator DLQ reconcilers for `land` and `landsignal`. Delivery is *) +(* at-least-once. A stage may fail after its side effect already happened *) +(* (a lost ack, an ambiguous publish), and a message that keeps failing is *) +(* dead-lettered. Faults are bounded by MaxFaults so liveness can be *) +(* checked. *) +(* *) +(* Abstracted away: speculation (DecideLand is the whole of it), other *) +(* batches, request fan-out (a request's outcome is its batch's), retry *) +(* counts below the DLQ threshold, and queue GC (dedup is modelled at its *) +(* worst case: a prior answer row is never collected). *) +(* *) +(* The constants are the design choices under test: *) +(* *) +(* DLQPolicy - what the orchestrator's land/landsignal DLQ does *) +(* "FailAlways" : failBatch today: any non-terminal batch -> failed *) +(* "SkipLanding" : leave a landing batch alone, wait for Runway *) +(* "ResendMerge" : re-send the MergeRequest, so Runway re-answers *) +(* *) +(* RunwayDLQ - what Runway's DLQ answers *) +(* "AnswerFailed" : today: always FAILED *) +(* "CheckBranch" : MERGED if the change is on the target, else FAILED *) +(* *) +(* RunwayRemembers - TRUE: Runway records its verdict per request ID and *) +(* replays it instead of acting again. FALSE: stateless, as today. *) +(* *) +(* AnswerDedup - TRUE: an answer's message ID is the request ID alone, *) +(* as today, so a second answer from the primary controller is *) +(* dropped by the queue. FALSE: every answer is delivered. *) +(***************************************************************************) +EXTENDS Naturals + +CONSTANTS DLQPolicy, RunwayDLQ, RunwayRemembers, AnswerDedup, MaxFaults + +ASSUME DLQPolicy \in {"FailAlways", "SkipLanding", "ResendMerge"} +ASSUME RunwayDLQ \in {"AnswerFailed", "CheckBranch"} +ASSUME RunwayRemembers \in BOOLEAN +ASSUME AnswerDedup \in BOOLEAN +ASSUME MaxFaults \in Nat + +VARIABLES + batch, \* orchestrator batch state + landMsg, \* batch ID on submitqueue-land: none | queued | dlq | acked + runwayInbox, \* a MergeRequest is queued for Runway's merge controller + runwayDLQ, \* a MergeRequest is queued for Runway's DLQ reconciler + repo, \* target branch: unmerged | merged | rejected + verdict, \* Runway's recorded verdict, if RunwayRemembers: none | merged | rejected + answers, \* MergeResults queued for landsignal + answersDLQ, \* MergeResults dead-lettered by landsignal + answered, \* answer message IDs the queue has seen (for dedup) + faults \* faults injected so far + +vars == <> + +Terminal == {"succeeded", "failed"} +AnswerIDs == {"primary", "dlq"} +Answers == [id : AnswerIDs, verdict : {"merged", "rejected"}] + +TypeOK == + /\ batch \in {"speculating", "landing"} \cup Terminal + /\ landMsg \in {"none", "queued", "dlq", "acked"} + /\ runwayInbox \in BOOLEAN + /\ runwayDLQ \in BOOLEAN + /\ repo \in {"unmerged", "merged", "rejected"} + /\ verdict \in {"none", "merged", "rejected"} + /\ answers \subseteq Answers + /\ answersDLQ \subseteq Answers + /\ answered \subseteq AnswerIDs + /\ faults \in 0..MaxFaults + +Init == + /\ batch = "speculating" + /\ landMsg = "none" + /\ runwayInbox = FALSE + /\ runwayDLQ = FALSE + /\ repo = "unmerged" + /\ verdict = "none" + /\ answers = {} + /\ answersDLQ = {} + /\ answered = {} + /\ faults = 0 + +--------------------------------------------------------------------------- +(* speculate *) + +DecideLand == + /\ batch = "speculating" + /\ batch' = "landing" + /\ landMsg' = "queued" + /\ UNCHANGED <> + +(* land *) + +LandPublishes == + /\ landMsg = "queued" + /\ runwayInbox' = TRUE + /\ landMsg' = "acked" + /\ UNCHANGED <> + +\* Retries exhausted. The Runway publish is land's last step, so an earlier +\* attempt may already have delivered it. +LandDeadLetters == + /\ landMsg = "queued" + /\ faults < MaxFaults + /\ landMsg' = "dlq" + /\ runwayInbox' \in {runwayInbox, TRUE} + /\ faults' = faults + 1 + /\ UNCHANGED <> + +(* Runway *) + +PublishAnswer(id, v) == + IF AnswerDedup /\ id \in answered + THEN UNCHANGED <> + ELSE /\ answers' = answers \cup {[id |-> id, verdict |-> v]} + /\ answered' = answered \cup {id} + +\* Already-applied changes produce no commits, so a repeat replays the verdict. +MergeOutcome == IF repo = "unmerged" THEN {"merged", "rejected"} ELSE {repo} + +Recorded == RunwayRemembers /\ verdict # "none" + +Record(v) == verdict' = IF RunwayRemembers THEN v ELSE verdict + +RunwayMerges == + /\ runwayInbox + /\ runwayInbox' = FALSE + /\ IF Recorded + THEN /\ PublishAnswer("primary", verdict) + /\ UNCHANGED <> + ELSE \E r \in MergeOutcome : + /\ repo' = r + /\ Record(r) + /\ PublishAnswer("primary", r) + /\ UNCHANGED <> + +\* Retries exhausted, possibly after the push landed but before the verdict +\* was recorded or the answer published. +RunwayDeadLetters == + /\ runwayInbox + /\ ~Recorded + /\ faults < MaxFaults + /\ runwayInbox' = FALSE + /\ runwayDLQ' = TRUE + /\ repo' \in IF repo = "unmerged" THEN {"unmerged", "merged"} ELSE {repo} + /\ faults' = faults + 1 + /\ UNCHANGED <> + +DLQVerdict == + IF Recorded THEN verdict + ELSE IF RunwayDLQ = "CheckBranch" /\ repo = "merged" THEN "merged" + ELSE "rejected" + +RunwayReconcilesDLQ == + /\ runwayDLQ + /\ runwayDLQ' = FALSE + /\ Record(DLQVerdict) + /\ PublishAnswer("dlq", DLQVerdict) + /\ UNCHANGED <> + +(* landsignal *) + +LandsignalApplies(a) == + /\ answers' = answers \ {a} + /\ batch' = IF batch \in Terminal THEN batch + ELSE IF a.verdict = "merged" THEN "succeeded" ELSE "failed" + /\ UNCHANGED <> + +\* e.g. the batch CAS keeps failing on a storage fault. +LandsignalDeadLetters(a) == + /\ faults < MaxFaults + /\ answers' = answers \ {a} + /\ answersDLQ' = answersDLQ \cup {a} + /\ faults' = faults + 1 + /\ UNCHANGED <> + +(* Orchestrator DLQ reconcilers: the step both share. *) + +FailUnlessTerminal == IF batch \in Terminal THEN batch ELSE "failed" + +ReconcileBatch == + CASE DLQPolicy = "FailAlways" -> + /\ batch' = FailUnlessTerminal + /\ UNCHANGED runwayInbox + [] DLQPolicy = "SkipLanding" -> + /\ batch' = IF batch = "landing" THEN batch ELSE FailUnlessTerminal + /\ UNCHANGED runwayInbox + [] DLQPolicy = "ResendMerge" -> + IF batch = "landing" + THEN /\ runwayInbox' = TRUE + /\ UNCHANGED batch + ELSE /\ batch' = FailUnlessTerminal + /\ UNCHANGED runwayInbox + +ReconcileLandDLQ == + /\ landMsg = "dlq" + /\ landMsg' = "acked" + /\ ReconcileBatch + /\ UNCHANGED <> + +ReconcileSignalDLQ(a) == + /\ answersDLQ' = answersDLQ \ {a} + /\ ReconcileBatch + /\ UNCHANGED <> + +--------------------------------------------------------------------------- + +Next == + \/ DecideLand + \/ LandPublishes + \/ LandDeadLetters + \/ RunwayMerges + \/ RunwayDeadLetters + \/ RunwayReconcilesDLQ + \/ \E a \in answers : LandsignalApplies(a) \/ LandsignalDeadLetters(a) + \/ ReconcileLandDLQ + \/ \E a \in answersDLQ : ReconcileSignalDLQ(a) + +\* Faults are never forced; every recovery step eventually runs while it +\* stays possible. +Fairness == + /\ WF_vars(LandPublishes) + /\ WF_vars(RunwayMerges) + /\ WF_vars(RunwayReconcilesDLQ) + /\ WF_vars(\E a \in answers : LandsignalApplies(a)) + /\ WF_vars(ReconcileLandDLQ) + /\ WF_vars(\E a \in answersDLQ : ReconcileSignalDLQ(a)) + +Spec == Init /\ [][Next]_vars /\ Fairness + +--------------------------------------------------------------------------- +(* Properties *) + +\* What SubmitQueue reports never contradicts the branch. +FailedMeansNotMerged == batch = "failed" => repo # "merged" +SucceededMeansMerged == batch = "succeeded" => repo = "merged" + +\* A terminal batch keeps its outcome. +TerminalIsFinal == [][(batch \in Terminal) => (batch' = batch)]_vars + +\* A batch that starts landing eventually reaches a terminal state. +LandingSettles == (batch = "landing") ~> (batch \in Terminal) + +============================================================================= diff --git a/spec/submitqueue/landoutcome/matrix.json b/spec/submitqueue/landoutcome/matrix.json new file mode 100644 index 000000000..91e799efb --- /dev/null +++ b/spec/submitqueue/landoutcome/matrix.json @@ -0,0 +1,23 @@ +{ + "spec": "LandOutcome.tla", + "specification": "Spec", + "fixed": { + "MaxFaults": "2" + }, + "vary": { + "DLQPolicy": ["\"FailAlways\"", "\"SkipLanding\"", "\"ResendMerge\""], + "RunwayDLQ": ["\"AnswerFailed\"", "\"CheckBranch\""], + "RunwayRemembers": ["FALSE", "TRUE"], + "AnswerDedup": ["TRUE", "FALSE"] + }, + "invariants": ["TypeOK", "FailedMeansNotMerged", "SucceededMeansMerged"], + "properties": ["TerminalIsFinal", "LandingSettles"], + "expect": [ + {"when": {"DLQPolicy": "\"FailAlways\""}, "violates": "FailedMeansNotMerged"}, + {"when": {"RunwayDLQ": "\"AnswerFailed\""}, "violates": "FailedMeansNotMerged"}, + {"when": {"DLQPolicy": "\"SkipLanding\""}, "violates": "LandingSettles"}, + {"when": {"RunwayRemembers": "FALSE"}, "violates": "FailedMeansNotMerged"}, + {"when": {"AnswerDedup": "TRUE"}, "violates": "LandingSettles"}, + {"when": {}, "violates": null} + ] +} diff --git a/tool/README.md b/tool/README.md index b4534095c..45c74c4a8 100644 --- a/tool/README.md +++ b/tool/README.md @@ -31,6 +31,10 @@ The Bazel version is controlled by `.bazelversion` at the repository root. Updat `tool/gitsandbox` creates the bare repository that `make local-submitqueue-start PROVIDER=git` merges into. It runs before the stack starts, because Runway clones that repository at boot and fails if the target does not already exist. The result is one seed commit on the target branch. Running it again leaves an existing repository unchanged, so a restart keeps commits that earlier runs landed. The Makefile invokes it; `bazel run //tool/gitsandbox -- -sandbox-dir ` is the direct form. +## TLC model checking + +`tool/tlc` model-checks the TLA+ specs under `spec/` (see `doc/rfc/tla-plus.md`). The TLA+ tools JAR is pinned in `MODULE.bazel` and runs on the JDK Bazel downloads, so no local Java install is needed. Each spec has a `matrix.json` naming its fixed and varied constants, the invariants and temporal properties to check, and the expected verdict for every combination. `tlc_matrix_test` in `tool/tlc/defs.bzl` turns a matrix into a test that `make test` runs and that fails when a verdict changes. `bazel run //tool/tlc -- spec/submitqueue/landoutcome/matrix.json` prints the table. + ## Proto generation `tool/proto` is the Bazel codegen for the committed protobuf Go stubs. `make proto` builds `//tool/proto:generated` and copies each package's output into its `protopb/` directory. The package list and per-source outputs live in `tool/proto/BUILD.bazel`. Change the `.proto` sources and regenerate; do not edit the generated files. `make clean-proto` removes those stubs, and `make proto` writes them again. diff --git a/tool/tlc/BUILD.bazel b/tool/tlc/BUILD.bazel new file mode 100644 index 000000000..7d1749f7a --- /dev/null +++ b/tool/tlc/BUILD.bazel @@ -0,0 +1,26 @@ +load("@rules_java//java:defs.bzl", "java_binary", "java_import") +load("@rules_python//python:defs.bzl", "py_binary") + +exports_files(["tlc.py"]) + +java_import( + name = "tla2tools", + jars = ["@tla2tools//file"], +) + +java_binary( + name = "tlc_java", + jvm_flags = ["-XX:+UseParallelGC"], + main_class = "tlc2.TLC", + visibility = ["//spec:__subpackages__"], + runtime_deps = [":tla2tools"], +) + +py_binary( + name = "tlc", + srcs = ["tlc.py"], + data = [":tlc_java"], + legacy_create_init = 0, + main = "tlc.py", + deps = ["@rules_python//python/runfiles"], +) diff --git a/tool/tlc/defs.bzl b/tool/tlc/defs.bzl new file mode 100644 index 000000000..0675b3908 --- /dev/null +++ b/tool/tlc/defs.bzl @@ -0,0 +1,25 @@ +"""Bazel test that model-checks a TLA+ spec's design matrix with TLC.""" + +load("@rules_python//python:defs.bzl", "py_test") + +def tlc_matrix_test(name, matrix, spec, size = "medium", **kwargs): + """Fails when any combination in `matrix` gets a verdict other than its expectation. + + Args: + name: test name. + matrix: the matrix JSON file. + spec: the .tla file (and any modules it extends) the matrix checks. + size: Bazel test size. + **kwargs: passed through to py_test. + """ + py_test( + name = name, + srcs = ["//tool/tlc:tlc.py"], + main = "//tool/tlc:tlc.py", + args = ["--check", "$(rootpath %s)" % matrix], + data = [matrix, "//tool/tlc:tlc_java"] + (spec if type(spec) == "list" else [spec]), + legacy_create_init = 0, + size = size, + deps = ["@rules_python//python/runfiles"], + **kwargs + ) diff --git a/tool/tlc/tlc.py b/tool/tlc/tlc.py new file mode 100644 index 000000000..a398e5aae --- /dev/null +++ b/tool/tlc/tlc.py @@ -0,0 +1,179 @@ +"""Model-check a TLA+ spec under every combination of its design constants. + +A matrix file (JSON, next to the spec) names the spec, the constants that stay +fixed, the constants that vary with their candidate values, the invariants and +temporal properties to check, and the expected verdict for each combination. +Expectations are an ordered rule list: the first rule whose `when` matches a +combination gives the property TLC must report violated, or null for a pass. + +`bazel run //tool/tlc -- ...` prints one line per combination. +`--check` additionally fails when any verdict differs from its expectation; +`tlc_matrix_test` runs that under `bazel test`. +""" + +import argparse +import concurrent.futures +import dataclasses +import glob +import itertools +import json +import os +import re +import shutil +import subprocess +import sys +import tempfile + +from python.runfiles import runfiles + +TLC_LAUNCHER = "_main/tool/tlc/tlc_java" + +INVARIANT_VIOLATED = re.compile(r"Error: Invariant (\w+) is violated") +TEMPORAL_VIOLATED = "Temporal properties were violated" +PASSED = "No error has been found" +DISTINCT_STATES = re.compile(r"(\d+) distinct states found") + + +@dataclasses.dataclass(frozen=True) +class Verdict: + # Property TLC reported violated; None when every property held. + violated: str | None + # Distinct states explored, as TLC reported them. + states: int + # TLC's output tail when it neither passed nor reported a violation. + error: str | None + + +@dataclasses.dataclass(frozen=True) +class Row: + constants: dict + verdict: Verdict + expected: str | None + + @property + def matches(self) -> bool: + return self.verdict.error is None and self.verdict.violated == self.expected + + +def load_matrix(path: str) -> dict: + with open(path) as f: + matrix = json.load(f) + matrix["dir"] = os.path.dirname(os.path.abspath(path)) + return matrix + + +def combinations(matrix: dict) -> list[dict]: + names = list(matrix["vary"]) + return [dict(zip(names, values)) for values in itertools.product(*(matrix["vary"][n] for n in names))] + + +def expected_violation(matrix: dict, combination: dict) -> str | None: + for rule in matrix["expect"]: + if all(combination[k] == v for k, v in rule["when"].items()): + return rule["violates"] + raise ValueError(f"no expectation matches {combination}") + + +def render_config(matrix: dict, constants: dict, properties: list[str]) -> str: + lines = [f"SPECIFICATION {matrix['specification']}", "CONSTANTS"] + lines += [f" {name} = {value}" for name, value in {**matrix["fixed"], **constants}.items()] + lines += ["INVARIANTS"] + [f" {name}" for name in matrix["invariants"]] + if properties: + lines += ["PROPERTIES"] + [f" {name}" for name in properties] + return "\n".join(lines) + "\n" + + +def run_tlc(launcher: str, env: dict, matrix: dict, constants: dict, properties: list[str]) -> str: + tmp = os.environ.get("TEST_TMPDIR") + with tempfile.TemporaryDirectory(dir=os.path.abspath(tmp) if tmp else None) as work: + # TLC resolves the config, and any module the spec extends, against the spec's + # own directory, so the spec's modules are copied next to a generated config. + for module in glob.glob(os.path.join(matrix["dir"], "*.tla")): + shutil.copy(module, work) + with open(os.path.join(work, "model.cfg"), "w") as f: + f.write(render_config(matrix, constants, properties)) + # A private java.io.tmpdir per run: TLC unpacks its standard modules there, and + # concurrent runs sharing one directory intermittently fail to parse the spec. + # -deadlock: a settled system legitimately has no next step. + result = subprocess.run( + [launcher, f"--jvm_flag=-Djava.io.tmpdir={work}", "--jvm_flag=-Xmx1g", + "-deadlock", "-workers", "1", "-metadir", "states", "-config", "model.cfg", matrix["spec"]], + cwd=work, env=env, capture_output=True, text=True, + ) + return result.stdout + result.stderr + + +def classify(output: str, temporal: str | None) -> Verdict: + states_match = DISTINCT_STATES.search(output) + states = int(states_match.group(1)) if states_match else 0 + if invariant := INVARIANT_VIOLATED.search(output): + return Verdict(invariant.group(1), states, None) + if TEMPORAL_VIOLATED in output: + return Verdict(temporal or "temporal", states, None) + if PASSED in output: + return Verdict(None, states, None) + return Verdict(None, states, "\n".join(output.strip().splitlines()[-8:])) + + +def check_combination(launcher: str, env: dict, matrix: dict, constants: dict) -> Verdict: + properties = matrix.get("properties", []) + verdict = classify(run_tlc(launcher, env, matrix, constants, properties), + properties[0] if len(properties) == 1 else None) + if verdict.violated != "temporal": + return verdict + # TLC does not say which temporal property failed; re-check each alone to name it. + for prop in properties: + single = classify(run_tlc(launcher, env, matrix, constants, [prop]), prop) + if single.violated is not None or single.error is not None: + return single + return verdict + + +def check_matrix(launcher: str, env: dict, matrix: dict) -> list[Row]: + combos = combinations(matrix) + with concurrent.futures.ThreadPoolExecutor(max_workers=os.cpu_count() or 4) as pool: + verdicts = pool.map(lambda c: check_combination(launcher, env, matrix, c), combos) + return [Row(c, v, expected_violation(matrix, c)) for c, v in zip(combos, verdicts)] + + +def format_row(row: Row) -> str: + constants = " ".join(f"{k}={v}" for k, v in row.constants.items()) + if row.verdict.error is not None: + outcome = "TLC error" + else: + outcome = f"violates {row.verdict.violated}" if row.verdict.violated else "ok" + mismatch = "" if row.matches else f" <-- expected {row.expected or 'ok'}" + return f"{constants} => {outcome} ({row.verdict.states} states){mismatch}" + + +def tlc_environment() -> tuple[str, dict]: + r = runfiles.Create() + env = {**os.environ, **r.EnvVars()} + # The java_binary launcher finds its JDK and jars through JAVA_RUNFILES when it + # runs inside another binary's runfiles tree. + env["JAVA_RUNFILES"] = env.get("RUNFILES_DIR") or os.path.dirname(r.Rlocation("_main")) + return r.Rlocation(TLC_LAUNCHER), env + + +def main(argv: list[str]) -> int: + parser = argparse.ArgumentParser(description=__doc__, formatter_class=argparse.RawDescriptionHelpFormatter) + parser.add_argument("matrix", nargs="+", help="matrix JSON files, relative to the workspace or absolute") + parser.add_argument("--check", action="store_true", help="fail when a verdict differs from its expectation") + args = parser.parse_args(argv) + + launcher, env = tlc_environment() + workspace = os.environ.get("BUILD_WORKSPACE_DIRECTORY", "") + failed = False + for path in args.matrix: + matrix = load_matrix(os.path.join(workspace, path)) + print(f"== {path}") + for row in check_matrix(launcher, env, matrix): + print(format_row(row)) + if row.verdict.error is not None: + print(row.verdict.error, file=sys.stderr) + failed |= not row.matches + return 1 if args.check and failed else 0 + + +if __name__ == "__main__": + sys.exit(main(sys.argv[1:]))